The arguments of a batched query satisfy the precondition of the query core

Proved

Light.Batch.coreArgs_preA

by xuanji · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

apsp-2995561apsp-exponentfine-grained-complexityword-ram

Let $t\le m$ , the limits satisfy Lim30 lim p t b0 U, the input arrays $A_L$ , $A_R$ be bounded by $U$ (BoundA), and the memory $\mu$ hold the data structure DSReadyA p t aX aY b0 AL AR of Theorem 30 for these arrays. For positions $I,J<N$ whose output-digit string is stored at aWD p b0, the argument list coreArgsA p t hmL b0 AL AR μ I J of the query core satisfies its precondition QueryCorePreP lim μ (the tries of the bands of $I$ and $J$ , their roots, the box and the work areas are where the query core of Theorem 30 expects them).

Preamble

/-
Copyright (c) 2026 Anthropic, PBC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
SPDX-License-Identifier: Apache-2.0
-/
-- Generated by skeleton subtraction from the ThreeSumApsp library at commit 3b45b374640a.

import Definitions.Def_APSP2995561_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false

open Light
open Light.Batch
open ThreeSumApsp ThreeSumApsp.Spec Light.Sec4 Light.Sec4.QueryAt
variable {lim : Limits} {P : Program} {d : ℕ} {p : Sec2.Par} {t : ℕ} {hmL : p.m ≤ p.L}
  {aX aY b0 : ℕ} {AL : ArrL p} {AR : ArrR p} {U : ℤ} {μ : ℕ → ℤ}

Formal statement

theorem Light.Batch.coreArgs_preA (ht : t ≤ p.m) (hlim : Lim30 lim p t b0 U) (hb : BoundA AL AR U)
    (hds : DSReadyA p t aX aY b0 AL AR μ) (I J : Fin p.N)
    (hwd : SegN μ (aWD p b0) (digitsO (outStrOfPos (stdLayout hmL) I J))) :
    QueryCorePreP lim μ (coreArgsA p t hmL b0 AL AR μ I J) := by sorry

Source

Developed for the prove2.me APSP exponent campaign (https://prove2.me/campaigns/apsp-exponent) on top of the Lean formalization anthropics/formal-math, folder 3sum-apsp, commit e1a4e65 (https://github.com/anthropics/formal-math/tree/e1a4e6508154ea59f030480661590a9fe3018011/3sum-apsp; Lean v4.33.1, Mathlib v4.33.1). The statement comes from the file 3sum-apsp/ThreeSumApsp/Batch/QueryA.lean of the campaign's modified copy of that library, which is not published; the new definitions it uses are in the platform definition bundles APSP2995561_Defs1 and APSP2995561_Defs2 (and APSP2996001_Defs1-2, APSP299791_Defs1-5 of the earlier entries). It follows the technical note "Deterministic APSP via thin products" (revised 7 October 2026) refining J. Alman and V. Vassilevska Williams, "Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs", arXiv:2610.06783v1 (https://arxiv.org/abs/2610.06783v1), Theorem 30 for arbitrary input arrays.

View graph