The four calls of one batch of the batched counting oracle write the counts of the batch

Proved

Light.Batch.oBatchTail_ends

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

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

Let $x$ be an instance of the counting oracle (Light.Filter2.OracleInst: an Exact Triangle instance with $n$ vertices per part and weight bound $U$ , a block size $s$ , a modulus $p$ , a place cnt) with precondition at free pointer $f$ , the need oNeedAt n U s p allowed by the limits, and the tables of the oracle in memory (BTabs). For a batch $bt$ with $1\le kb\le$ oKK s p products and $bt\cdot$ oKK $+kb\le$ oProd n s, the statement oBatchTail (two calls of writeSrc for the digit-lifted sources, preCore, and the queries), run in oProg ++ R in the frame of the oracle's locals, ends within tOBTail n s p steps; afterwards the tables are kept, the $kb\,n^2$ counts of the batch stand at cnt + bt·oKK·n² — the entry $e$ equals cntOf n s p AB BC AC (bt·oKK·n² + e), the number of $c$ in the middle block with $p\mid w(a,b)+w(b,c)+w(a,c)$ — and every other cell below $f$ is unchanged.

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.Batch Light.Sec4 Light.Filter2 OS
set_option maxHeartbeats 1000000

Formal statement

theorem Light.Batch.oBatchTail_ends (R : Program) {lim : Limits} {d : ℕ} {x : Light.Filter2.OracleInst} {μ₀ μ : ℕ → ℤ}
    {fr : ℕ} (hpre : x.Pre μ₀ fr) (hok : (Light.Batch.oNeedAt x.n x.U x.s x.p).Ok lim fr d) {bt kb : ℕ}
    (hkb1 : 1 ≤ kb) (hkbK : kb ≤ oKK x.s x.p) (hkbT : bt * oKK x.s x.p + kb ≤ oProd x.n x.s)
    (tmp : ℤ) (hT : BTabs x fr μ) :
    Ends lim (oProg ++ R) d oBatchTail
      ⟨frame (oLocA x fr tmp bt (bt * oKK x.s x.p : ℕ) kb), μ⟩ (tOBTail x.n x.s x.p)
      fun σ' => ∃ tmp' : ℤ, σ'.loc = frame (oLocA x fr tmp' bt (bt * oKK x.s x.p : ℕ) kb) ∧
        BTabs x fr σ'.mem ∧
        (∀ e < kb * (x.n * x.n), σ'.mem (x.cnt + bt * oKK x.s x.p * (x.n * x.n) + e)
          = (Light.Filter2.cntOf x.n x.s x.p x.AB x.BC x.AC (bt * oKK x.s x.p * (x.n * x.n) + e) : ℤ)) ∧
        (∀ b < fr, (b < x.cnt + bt * oKK x.s x.p * (x.n * x.n) ∨
          x.cnt + bt * oKK x.s x.p * (x.n * x.n) + kb * (x.n * x.n) ≤ b) → σ'.mem b = μ b) := 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/ORunBatch.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), Lemma 4.1 (digit lifting) and Proposition 2.1.

View graph