The filtering host computes its parameters and sets up its frame

Proved

Light.Filter2.params_spec

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

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

In a program $P$ that holds the procedures for $\log_2$ , integer square root, powers of two and division (ParamProcs), for an all-edges instance $x$ with $n,U\ge1$ , a free pointer $f$ and limits whose space, word size and depth allow the host (aTOP x.n fr ≤ lim.space, filterWord n U ≤ lim.word, $d<$ depth), the statement paramsStmt, run in the frame $[n,U,ab,bc,ac,out,f]$ , ends within tParams n U steps with the memory unchanged and the frame topFrame x fr holding the parameters of the filtering host.

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}
set_option maxHeartbeats 1600000

Formal statement

theorem Light.Filter2.params_spec {P : Program} {d : ℕ} {pLog pSqrt pPow pDiv : ℕ}
    (HP : Light.Filter2.ParamProcs P pLog pSqrt pPow pDiv) {x : AEInst} {fr : ℕ} {μ : ℕ → ℤ}
    (hn : 1 ≤ x.n) (hU : 1 ≤ x.U) (hw : (lim.space : ℤ) ≤ lim.word)
    (hsp : Light.Filter2.aTOP x.n fr ≤ lim.space) (hword : (Light.Filter2.filterWord x.n x.U : ℤ) ≤ lim.word)
    (hdep : d < lim.depth) :
    Ends lim P d (Light.Filter2.paramsStmt pLog pSqrt pPow pDiv)
      ⟨Light.frame [x.n, x.U, x.ab, x.bc, x.ac, x.out, fr], μ⟩ (Light.Filter2.tParams x.n x.U)
      fun σ' => σ' = ⟨Light.frame (Light.Filter2.topFrame x fr), μ⟩ := 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/HostTop.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 (parameters).

View graph