One round of the deterministic filtering host keeps its invariants and shrinks the weighted active set

Proved

Light.Filter.round_spec

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

apsp-2996001apsp-exponentfine-grained-complexityword-ram

Let the oracle procedure $p_O$ of $P_0$ solve oracleTask with time $T_o$ and need $\nu_o$ , and let the procedures of a round (roundBody, aggregation, step, final marks, certificates, arg-min, copy) be in place in $P_0\mathbin{+\!\!+}R$ (RoundProcs). 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 the memory $\mu$ between two rounds satisfy FMem with active marks $act$ and done flags $D$ , the invariant Inv1 (a done pair has a witness $c$ with $w(a,b)+w(b,c)+w(a,c)=0$ ) and Inv2 (an active candidate of a pair that is not done, whose block contains a witness, is marked).

Then the round, called at depth $d\le d_0+2$ with the step arguments, ends within tRound To n U steps, and the new memory satisfies FMem, Inv1, Inv2 for some new $act'$ , $D'$ with

Q^{r}\cdot|A'|\le (2h)^{r}\cdot s\cdot|A|,

where $|A|$ is the number of active candidates of pairs that are not done (cardA of eff), $Q$ the size of the prime pool in $[R,2R)$ , $r$ the number of steps per round, $h$ the bound on the number of pool primes dividing a nonzero triangle sum, and $s$ the block size (Lemma 3.1).

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 7c34437be804.

import Definitions.Def_APSP2996001_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false

open ThreeSumApsp
open Light
open Light.Filter
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.Filter.round_spec (hsol : SolvesN oracleTask P₀ pO To needo) {pRound : ℕ}
    (hRd : (P₀ ++ R)[pRound]? = some (roundBody pO pAggr pStep pFA))
    (HP : RoundProcs (P₀ ++ R) pO pAggr pStep pFA pCert pArg pCopy)
    (E : Light.Filter.Env lim d0 x fr μ0 needo) {d : ℕ} (hd : d ≤ d0 + 2) {act D : ℕ → Bool} {μ : ℕ → ℤ}
    (hmem : FMem x fr μ0 μ act D) (hI1 : Inv1 x D) (hI2 : Inv2 x act D) :
    Meets lim (P₀ ++ R) pRound d (stepArgs x fr (rOf x.n)) μ (Light.Filter.tRound To x.n x.U) fun _ μ' =>
      ∃ act' D' : ℕ → Bool, FMem x fr μ0 μ' act' D' ∧ Inv1 x D' ∧ Inv2 x act' D' ∧
        QOf x.n ^ rOf x.n * cardA x.n (sOf x.n) (eff (x.n * x.n) act' D') ≤
          (2 * hOf x.n x.U) ^ rOf x.n * (sOf x.n * cardA x.n (sOf x.n) (eff (x.n * x.n) act D)) := 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/Filter/HostRound.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 APSP2996001_Defs1 and APSP2996001_Defs2 (and APSP299791_Defs1 to APSP299791_Defs5 of the 2.99791 entry). It follows the technical note "Deterministic APSP via thin products" (6 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