APSP in $O(n^{2.99791})$ : definitions, part 5 of 5

Definition

APSP299791_Defs5

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

apsp-299791apsp-exponentdefinitions

Definitions for the formal proof that all-pairs shortest paths can be solved deterministically in time $O(n^{2.99791})$ on a word RAM, part 5 of 5. It imports APSP299791_Defs4.

This part contains the claims and costs: Theorem 17 at the middle dimension, the uniform all-edges bound and Theorem 19 at the middle dimension, the pruned cost accounting (Costs, CostsP, Within8p) and the regime $D^{91}\le N^5$ with $c=22$ , $\theta=29/250$ , the program allInstancesP, and the passes and per-pair specification used to go from all-edges Exact Triangle to pairs.

Source modules (in this order): ThreeSumApsp.AllEdges.Pairs.

Across the six parts, the development changes the construction of Alman and Vassilevska Williams in three ways:

pruned encodings in the data structure of Theorem 30: only the leaves whose $L$ decimal digits contain at most $m$ nines are computed and stored, since a query reads no other leaf, and the shared stage costs $\sum_{j\le m}\binom Lj9^{L-j}$ per band instead of $10^L$ ;
the thin regime $D^{91}\le N^5$ with the parameters $c=22$ , $\theta=29/250$ ;
an all-edges Exact Triangle host for Theorem 17 that calls its oracle at the middle dimension $\lceil s/g\rceil s$ , $s=\lfloor\sqrt D\rfloor$ , followed by the chain all-edges Exact Triangle → pairs → (min,+)-product → APSP.

Formalization Note The bundle is generated from the library by deleting the theorems that are not needed ("skeleton subtraction"); it keeps definitions, structures, instances, notations and tactic macros, and the few lemmas that the definitions themselves need, with proofs. Section 4 declarations whose meaning changed with pruning carry the suffix P (for example Specs40P, base58P, QueryAtSpecP), so that they do not clash with the declarations of the foundation bundles.

Definition code

/-
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 27a2fa4bab32.

import Definitions.Def_APSP299791_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false

section
-- Source module: ThreeSumApsp.AllEdges.Pairs
/-!
# All pairs from all-edges Exact Triangle, as a host

pa(n, U, x, y, v, out, fr) finds, for all pairs `(i, j)` at once, whether some `k` has
`X[i,k] + Y[k,j] < V[i,j]`.  It is the host nt of Negative Triangle with all-edges Exact Triangle in
the place of Exact Triangle: the weights are `−V`, `Yᵀ` and `X`, a triangle on the edge `(i, j)` is
negative exactly if the pair `(i, j)` has the property, and at each of the `2L` questions the flags
of the answer are or-ed into out (`isHost_pa`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Sec3

open ThreeSumApsp.Spec

/-! ## The text -/

namespace PaHost

abbrev Verts : ℕ := 0
abbrev Bound : ℕ := 1
abbrev MatX : ℕ := 2
abbrev MatY : ℕ := 3
abbrev MatV : ℕ := 4
abbrev Out : ℕ := 5
abbrev PreAB : ℕ := 6
abbrev Cells : ℕ := 7
abbrev Power : ℕ := 8
abbrev Levels : ℕ := 9
abbrev Round : ℕ := 10
abbrev Res : ℕ := 11
abbrev Bound6 : ℕ := 12
abbrev PreBC : ℕ := 13
abbrev PreAC : ℕ := 14
abbrev RestAB : ℕ := 15
abbrev RestBC : ℕ := 16
abbrev RestAC : ℕ := 17
abbrev Third : ℕ := 18
abbrev Flags : ℕ := 19
abbrev SolverFree : ℕ := 20
abbrev Cells3 : ℕ := 21

end PaHost

open PaHost

/-- The beginning of pa: sizes and addresses. -/
def paInit : Stmt :=
  .set Light.Sec3.PaHost.Cells (v Light.Sec3.PaHost.Verts *' v Light.Sec3.PaHost.Verts) ;;
  .set Bound6 (Light.k 6 *' v Light.Sec3.PaHost.Bound) ;;
  .set PreBC (v PreAB +' v Light.Sec3.PaHost.Cells) ;;
  .set PreAC (v PreBC +' v Light.Sec3.PaHost.Cells) ;;
  .set RestAB (v PreAC +' v Light.Sec3.PaHost.Cells) ;;
  .set RestBC (v RestAB +' v Light.Sec3.PaHost.Cells) ;;
  .set RestAC (v RestBC +' v Light.Sec3.PaHost.Cells) ;;
  .set Third (v RestAC +' v Light.Sec3.PaHost.Cells) ;;
  .set Light.Sec3.PaHost.Flags (v Third +' v Light.Sec3.PaHost.Cells) ;;
  .set Light.Sec3.PaHost.SolverFree (v Light.Sec3.PaHost.Flags +' v Light.Sec3.PaHost.Cells) ;;
  .set Cells3 (Light.k 3 *' v Light.Sec3.PaHost.Cells) ;;
  .set Light.Sec3.PaHost.Power (Light.k 1) ;;
  .set Light.Sec3.PaHost.Levels (Light.k 0)

/-- The number of levels L and the power 2^L, by doubling. -/
def paPow : Stmt :=
  .while (v Light.Sec3.PaHost.Power ≤' v Bound6) (
    .set Light.Sec3.PaHost.Power (Light.k 2 *' v Light.Sec3.PaHost.Power) ;;
    .set Light.Sec3.PaHost.Levels (v Light.Sec3.PaHost.Levels +' Light.k 1))

/-- The arrays r and q at the top level, and zeros in out. -/
def paFill (pAff pTr pFill : ℕ) : Stmt :=
  .call pAff [v Light.Sec3.PaHost.Cells, v MatV, Light.k 0 -' Light.k 2, Light.k 2 *' v Light.Sec3.PaHost.Bound, v RestAB] Light.Sec3.PaHost.Res ;;
  .call pTr [v Light.Sec3.PaHost.Verts, v Light.Sec3.PaHost.MatY, v Third] Light.Sec3.PaHost.Res ;;
  .call pAff [v Light.Sec3.PaHost.Cells, v Third, Light.k 2, Light.k 2 *' v Light.Sec3.PaHost.Bound, v RestBC] Light.Sec3.PaHost.Res ;;
  .call pAff [v Light.Sec3.PaHost.Cells, v Light.Sec3.PaHost.MatX, Light.k 0 -' Light.k 2, Light.k 4 *' v Light.Sec3.PaHost.Bound, v RestAC] Light.Sec3.PaHost.Res ;;
  .call pAff [v Cells3, v RestAB, Light.k 0, Light.k 0, v PreAB] Light.Sec3.PaHost.Res ;;
  .call pFill [v Light.Sec3.PaHost.Out, v Light.Sec3.PaHost.Cells, Light.k 0] Light.Sec3.PaHost.Res

/-- One question to the solver of all-edges Exact Triangle, and the or of its flags into out. -/
def paProbe (pAE pAff pOr e : ℕ) : Stmt :=
  .call pAff [v Light.Sec3.PaHost.Cells, v PreAC, Light.k 0 -' Light.k 1, Light.k e, v Third] Light.Sec3.PaHost.Res ;;
  .call pAE [v Light.Sec3.PaHost.Verts, v Bound6, v PreAB, v PreBC, v Third, v Light.Sec3.PaHost.Flags, v Light.Sec3.PaHost.SolverFree] Light.Sec3.PaHost.Res ;;
  .call pOr [v Light.Sec3.PaHost.Cells, v Light.Sec3.PaHost.Out, v Light.Sec3.PaHost.Flags] Light.Sec3.PaHost.Res

/-- One round: the next level, and its two questions. -/
def paRound (pAE pAff pDown pOr : ℕ) : Stmt :=
  .call pDown [v Cells3, v PreAB, v RestAB, v Light.Sec3.PaHost.Power] Light.Sec3.PaHost.Res ;;
  paProbe pAE pAff pOr 2 ;;
  paProbe pAE pAff pOr 3

/-- pa(n, U, x, y, v, out, fr). -/
def paBody (pAE pAff pDown pTr pFill pOr : ℕ) : Stmt :=
  paInit ;; paPow ;; paFill pAff pTr pFill ;;
    .for Round (v Light.Sec3.PaHost.Levels) (paRound pAE pAff pDown pOr) ;; .set 0 (Light.k 0)

/-- The time of pa, if the solver of all-edges Exact Triangle takes T n U steps. -/
def paTime (T : ℕ → ℕ → ℕ) (n U : ℕ) : ℕ :=
  250 * (n * n) + 400 + ntLevels U * (250 * (n * n) + 200 + 2 * T n (6 * U))

/-- The need of pa, if the solver needs r n U. -/
def paNeed (r : ℕ → ℕ → Light.Need) (n U : ℕ) : Light.Need where
  word := 24 * U + 8 + (r n (6 * U)).word
  cells := 8 * (n * n) + (r n (6 * U)).cells
  depth := (r n (6 * U)).depth + 2

/-! ## The local variables and the hypotheses -/

namespace PaHost

/-- The locals of pa after its beginning. -/
abbrev locals (q : PairsInst) (fr : ℕ) (pw lv rd res : ℤ) : List ℤ :=
  [q.n, q.U, q.x, q.y, q.v, q.out, fr, (q.n * q.n : ℕ), pw, lv, rd, res, (6 * q.U : ℕ),
    (fr + q.n * q.n : ℕ), (fr + 2 * (q.n * q.n) : ℕ), (fr + 3 * (q.n * q.n) : ℕ),
    (fr + 4 * (q.n * q.n) : ℕ), (fr + 5 * (q.n * q.n) : ℕ), (fr + 6 * (q.n * q.n) : ℕ),
    (fr + 7 * (q.n * q.n) : ℕ), (fr + 8 * (q.n * q.n) : ℕ), (3 * (q.n * q.n) : ℕ)]

/-- The program has the solver and the loops over arrays, the instance is as the task prescribes,
and the limits allow for the need of pa. -/
structure Ctx (P₀ R' : Program) (p pAff pDown pTr pRow pFill pOr : ℕ) (T : ℕ → ℕ → ℕ)
    (r : ℕ → ℕ → Light.Need) (lim : Limits) (d : ℕ) (q : PairsInst) (μ : ℕ → ℤ) (fr : ℕ) : Prop where
  solver : Solves aeTask P₀ p T r
  aff : (P₀ ++ R')[pAff]? = some affineBody
  down : (P₀ ++ R')[pDown]? = some prefDownBody
  tr : (P₀ ++ R')[pTr]? = some (transBody pRow)
  row : (P₀ ++ R')[pRow]? = some rowBody
  fill : (P₀ ++ R')[pFill]? = some fillBody
  or : (P₀ ++ R')[pOr]? = some orBody
  pre : q.Pre μ fr
  ok : (paNeed r q.n q.U).Ok lim fr d

variable {P₀ R' : Program} {p pAff pDown pTr pRow pFill pOr : ℕ} {T : ℕ → ℕ → ℕ}
  {r : ℕ → ℕ → Need} {lim : Limits} {d : ℕ} {q : PairsInst} {μ : ℕ → ℤ} {fr : ℕ}

/-! ## The lists -/

/-- The shifted and doubled weights `2(−V + U)`, `2(Yᵀ + U)`, `2(2U − X)`. -/
noncomputable abbrev zs (q : PairsInst) : List ℤ := negStart q.U (negL q.V) (transL q.n q.Y) q.X

/-- The flags of the pairs found at the levels from ℓ₀ on. -/
def PYes (q : PairsInst) (ℓ : ℕ) (e : ℤ) (i : ℕ) : Prop :=
  ∃ c < q.n, (pairsQAB q.U ℓ q.V).getD i 0 + (pairsQBC q.n q.U ℓ q.Y).getD (i % q.n * q.n + c) 0 +
    (negThird q.U ℓ e q.X).getD (i / q.n * q.n + c) 0 = 0

/-- A question at one of the levels from ℓ₀ on has found the pair `i`. -/
def PFound (q : PairsInst) (L ℓ₀ : ℕ) (i : ℕ) : Prop :=
  ∃ ℓ, ℓ₀ ≤ ℓ ∧ ℓ < L ∧ ∃ e : ℤ, (e = 2 ∨ e = 3) ∧ PYes q ℓ e i

/-- The memory of pa at the level ℓ: the prefixes and the rests, the flags found so far in out, and
nothing else below the free pointer has changed. -/
def PaMem (q : PairsInst) (μ : ℕ → ℤ) (fr ℓ : ℕ) (A : ℕ → Prop) (μ' : ℕ → ℤ) : Prop :=
  Seg μ' fr ((Light.Sec3.PaHost.zs q).map (prefQ ℓ)) ∧
    Seg μ' (fr + 3 * (q.n * q.n)) ((Light.Sec3.PaHost.zs q).map (prefR (ntLevels q.U) ℓ)) ∧
    Seg μ' q.out (flagsOf (q.n * q.n) A) ∧ KeptBut μ μ' fr q.out (q.n * q.n)

/-! ## The beginning -/

/-- The state of the loop that doubles after i rounds. -/
def PowInv (q : PairsInst) (μ : ℕ → ℤ) (fr i : ℕ) (σ : State) : Prop :=
  σ = ⟨Light.frame (Light.Sec3.PaHost.locals q fr (2 ^ i : ℕ) i 0 0), μ⟩

/-! ## The arrays at the top level -/

/-! ## One question -/

/-- The instance of all-edges Exact Triangle for the level ℓ and the exact value e, as it lies in
the arrays of pa. -/
def aeQ (q : PairsInst) (fr ℓ : ℕ) (e : ℤ) : AEInst :=
  ⟨⟨q.n, 6 * q.U, fr, fr + q.n * q.n, fr + 6 * (q.n * q.n), pairsQAB q.U ℓ q.V,
    pairsQBC q.n q.U ℓ q.Y, negThird q.U ℓ e q.X⟩, fr + 7 * (q.n * q.n)⟩

/-- The state of pa between two steps of a round. -/
def St (q : PairsInst) (μ : ℕ → ℤ) (fr : ℕ) (rd : ℤ) (ℓ : ℕ) (A : ℕ → Prop) (σ : State) : Prop :=
  ∃ (res : ℤ) (μ' : ℕ → ℤ),
    σ = ⟨Light.frame (Light.Sec3.PaHost.locals q fr (2 ^ ntLevels q.U : ℕ) (ntLevels q.U) rd res), μ'⟩ ∧
      PaMem q μ fr ℓ A μ'

/-! ## The rounds -/

end PaHost

end Light.Sec3
end
end

Source

Lean formalization anthropics/formal-math, folder 3sum-apsp, commit e1a4e65 (https://github.com/anthropics/formal-math/tree/e1a4e6508154ea59f030480661590a9fe3018011/3sum-apsp), as modified for the prove2.me APSP exponent campaign (the modified copy is not published; these bundles are its new and modified definitions). Paper: 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), Sections 2-4 (Theorem 17 p. 33, Theorem 30 pp. 46-47).

View graph

APSP in O(n2.99791)O(n^{2.99791})O(n2.99791): definitions, part 5 of 5

APSP in $O(n^{2.99791})$ : definitions, part 5 of 5