Prove2Me

The query core of Theorem 30 for arbitrary input arrays returns the value of the query

Proved
Light.Batch.queryAtCore_specA

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

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

If the query core procedure meets its specification (QueryCoreSpecP lim P), t≤mt\le m, Lim30 lim p t b0 U holds, AL,ARA_L,A_R are bounded by UU, the memory holds DSReadyA p t aX aY b0 AL AR, and the depth leaves room for two calls, then for I,J<NI,J<N the statement queryAtCore, run in the frame of the locals of queryAt with a result cell rr, ends within tQueryCore p.L p.m t + 60 steps with the value queryValue p.m t (encRowA AL (I / (K0 N0))) (encColA AR (J / (K0 N0))) (outStrOfPos (stdLayout hmL) I J) in the first local (the query of Lemma 28 for the encodings of the bands of II and JJ), changing only the scratch areas (SameOutside2).

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.queryAtCore_specA (hCore : QueryCoreSpecP lim P) (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) (hd : d + 2 ≤ lim.depth) (r : ℤ)
    (hwd : SegN μ (aWD p b0) (digitsO (outStrOfPos (stdLayout hmL) I J))) :
    Ends lim P d queryAtCore ⟨Light.frame (queryAtLocals p t b0 I J ++ [r]), μ⟩
      (tQueryCore p.L p.m t + 60) fun σ' =>
        σ'.loc 0 = queryValue p.m t (encRowA AL ((I : ℕ) / (p.K0 * p.N0)))
          (encColA AR ((J : ℕ) / (p.K0 * p.N0))) (outStrOfPos (stdLayout hmL) I J) ∧
        SameOutside2 μ σ'.mem (aSS p b0) p.m (aBOX p b0) p.L := 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 and Lemma 28.

View graph