The rounds and final scans of the filtering host at σ = 0.0336175 write the all-edges flags

Proved

Light.Filter2.core_spec

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

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

Let procedure $p_O$ of $P_0$ solve Light.Filter2.oracleTask with time $T_o$ and need $\nu_o$ , let the core body coreBody pRound pFinal, the round body, the procedures of a round (RoundProcs) and of the final answer (FinalProcs) be in place in $P_0\mathbin{+\!\!+}R$ , let Env hold for the all-edges instance $x$ ( $n$ vertices, weight bound $U$ ) with first memory $\mu_0$ and free pointer $f$ , and let $\mu$ satisfy FMem with all candidates active and no pair done. Then the core procedure, called at depth $d\le d_0+1$ with coreArgs x fr, returns within tCore To n U steps with the all-edges flags aeFlags n AB BC AC at x.out (for each pair $(a,b)$ , whether some $c$ has $w(a,b)+w(b,c)+w(a,c)=0$ ), and every other cell below $f$ as in $\mu_0$ (KeptBut).

This is the filtering host of Lemma 3.1 (rounds of prime moduli from a pool in $[R,2R)$ that certify pairs and shrink the active candidates, then the final check), at the block size $s=2^{\lfloor0.0336175k\rfloor}$ of the 2.995561 parameters.

Meets lim P p d args μ T Q means: the call of procedure $p$ of $P$ at depth $d$ with the arguments args on memory $\mu$ returns within $T$ steps, under the limits lim, with a result $r$ and memory $\mu'$ satisfying $Q\,r\,\mu'$ .

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 ThreeSumApsp
open Light
open Light.Filter2
open ThreeSumApsp.Spec Light.Sec3
variable {lim : Limits}
variable {P₀ R : Program} {pO pAggr pStep pFA pCert pArg pCopy : ℕ} {To : List ℕ → ℕ}
  {needo : List ℕ → Need} {d0 : ℕ} {x : AEInst} {fr : ℕ} {μ0 : ℕ → ℤ}
set_option maxHeartbeats 800000

Formal statement

theorem Light.Filter2.core_spec (hsol : SolvesN Light.Filter2.oracleTask P₀ pO To needo) {pCore pRound pFinal pGroup pScan : ℕ}
    (hC : (P₀ ++ R)[pCore]? = some (Light.Filter2.coreBody pRound pFinal))
    (hRd : (P₀ ++ R)[pRound]? = some (Light.Filter2.roundBody pO pAggr pStep pFA))
    (HP : Light.Filter2.RoundProcs (P₀ ++ R) pO pAggr pStep pFA pCert pArg pCopy)
    (HF : Light.Filter2.FinalProcs (P₀ ++ R) pFinal pGroup pScan)
    (E : Light.Filter2.Env lim d0 x fr μ0 needo) {d : ℕ} (hd : d ≤ d0 + 1) {μ : ℕ → ℤ}
    (hmem : Light.Filter2.FMem x fr μ0 μ (fun _ => true) (fun _ => false)) :
    Meets lim (P₀ ++ R) pCore d (Light.Filter2.coreArgs x fr) μ (Light.Filter2.tCore To x.n x.U) fun _ μ' =>
      Seg μ' x.out (aeFlags x.n x.AB x.BC x.AC) ∧ KeptBut μ0 μ' fr x.out (x.n * x.n) := 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/Filter2/HostCore.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 3.1.

View graph