APSP in $O(n^{2.996001})$ : definitions, part 1 of 2

Definition
APSP2996001_Defs1
by xuanji · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)
apsp-2996001apsp-exponentdefinitions
Definitions for the formal proof that all-pairs shortest paths can be solved deterministically in time $O(n^{2.996001})$ on a word RAM, part 1 of 2. It imports the foundation bundles APSPSource_*, TrulySubcubicAPSP_SourceSpecification and the bundles APSP299791_Defs* of the 2.99791 entry.
This part contains the program programF of the pruned thin product at the new parameters (ratParamsF, the regime test $D^{1249}\le N^{71}$ , time and need), the parameters of the filtering reduction (kOf, ellOf, RR, bOf, dOf, roundsOf, sOf, mOf, rOf, hOf, the prime pool pool, QOf, Guard, PmaxOf), the counts cntOf/cntList and the task oracleTask of the counting oracle, the oracle's procedures, data and time (oracleProcs, oCoreBody, oTimeAt), the masses and certificates of Lemma 3.1, and the procedures of the filtering host.
Source modules (in this order): ThreeSumApsp.Lang.Assigns, ThreeSumApsp.Lang.Frames, ThreeSumApsp.Lang.Lib.Logs, ThreeSumApsp.Filter.ThinCosts, ThreeSumApsp.Filter.ThinRegime, ThreeSumApsp.Filter.ThinRegimeTest, ThreeSumApsp.Filter.ThinAll, ThreeSumApsp.Filter.Defs, ThreeSumApsp.Filter.OracleData, ThreeSumApsp.Filter.OracleScatter, ThreeSumApsp.Filter.OracleLoop, ThreeSumApsp.Filter.OracleCore, ThreeSumApsp.Filter.OracleHost, ThreeSumApsp.Filter.OracleNeedPoly, ThreeSumApsp.Filter.Asymp, ThreeSumApsp.Filter.OracleBound, ThreeSumApsp.Filter.Mass, ThreeSumApsp.Filter.HostMath, ThreeSumApsp.Filter.HostProcs.
The bundles belong to the formal proof of the deterministic bound $O(n^{2.996001})$ for APSP (the filtering reduction of the 2.996001 note):
the pruned thin product of the 2.99791 entry at the new parameters $c=212733/10000$ , $\theta=111731/10^6$ , in the regime $D^{1249}\le N^{71}$ , giving #Lop-AE-SparseTri (counting) in time $O(n^2\log^2D/D^{0.0703531}+wD^{0.4296471}\log D+nD+w)$ ;
the modular counting oracle of Lemma 4.1: for a block size $s$ and a modulus $p$ it computes, for every pair $(a,b)$ and every block $C_j$ of $s$ third vertices, the number of $c\in C_j$ with $p\mid w(a,b)+w(b,c)+w(a,c)$ , by #Lop-AE-SparseTri calls at inner dimension $sp$ ;
the deterministic filtering host (Lemma 3.1): rounds of prime moduli from a pool of primes in $[R,2R)$ that certify the pairs with an exact triangle and shrink the set of active candidates, followed by a final check, solving All-Edges Exact Triangle, and the chain to APSP.
Formalization Note Each bundle is generated from the library by deleting the theorems that are not needed ("skeleton subtraction"); it keeps definitions, structures and instances, and the few lemmas that the definitions themselves need, with proofs. Tactic macros of the library are expanded at their uses. Everything else is imported from the bundles APSPSource_*, TrulySubcubicAPSP_SourceSpecification and APSP299791_Defs*.
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 7c34437be804.

import Definitions.Def_APSP299791_Defs1
import Definitions.Def_APSP299791_Defs2
import Definitions.Def_APSP299791_Defs3
import Definitions.Def_APSP299791_Defs4
import Definitions.Def_APSPSource_PaperStatements
import Definitions.Def_APSPSource_RemainingDefinitions
import Definitions.Def_APSPSource_ThreeSumApsp_Lang_Logic
import Definitions.Def_APSPSource_ThreeSumApsp_Lang_Regions
import Definitions.Def_APSPSource_ThreeSumApsp_Lang_Syntax
import Definitions.Def_APSPSource_ThreeSumApsp_Lang_WordSize
import Definitions.Def_APSPSource_ThreeSumApsp_Machine_Realized
import Definitions.Def_APSPSource_ThreeSumApsp_Machine_Solving
import Definitions.Def_APSPSource_ThreeSumApsp_Programs_Sec2_Theorem5_Places
import Definitions.Def_APSPSource_ThreeSumApsp_Sec2_Tiling_Definitions
import Definitions.Def_APSPSource_ThreeSumApsp_Sec4_Boxes
import Definitions.Def_APSPSource_ThreeSumApsp_Sec4_ParameterSteps
import Definitions.Def_APSPSource_ThreeSumApsp_Sec4_Table2_LogBounds
import Definitions.Def_APSPSource_ThreeSumApsp_Sec4_Theorem30
import Definitions.Def_APSPSource_ThreeSumApsp_Spec_Sec2_Theorem5_Alphabets
import Definitions.Def_APSPSource_ThreeSumApsp_Spec_Sec2_Theorem5_Arrays
import Definitions.Def_APSPSource_ThreeSumApsp_Spec_Sec2_Theorem5_Layout
import Definitions.Def_APSPSource_ThreeSumApsp_Spec_Sec2_Theorem5_Subsets
import Definitions.Def_APSPSource_ThreeSumApsp_Spec_Sec3_Theorem17_Chunks
import Definitions.Def_APSPSource_ThreeSumApsp_Spec_Sec3_Theorem17_Hashing
import Definitions.Def_APSPSource_ThreeSumApsp_Spec_Sec3_Theorem17_Instances
import Definitions.Def_APSPSource_ThreeSumApsp_Spec_Sec4_Theorem30_Cubes
import Definitions.Def_APSPSource_ThreeSumApsp_Spec_Sec4_Theorem30_NineStrings
import Definitions.Def_APSPSource_ThreeSumApsp_TimeClaims_Sec3_Definitions
import Definitions.Def_APSPSource_ThreeSumApsp_Util_Asymptotics_Dominated
import Definitions.Def_APSPSource_ThreeSumApsp_Util_Asymptotics_Scale
import Definitions.Def_APSPSource_ThreeSumApsp_Util_Asymptotics_UpperBounds
import Definitions.Def_APSPSource_ThreeSumApsp_Util_Digits
import Definitions.Def_APSPSource_ThreeSumApsp_Util_Flag
import Definitions.Def_APSPSource_ThreeSumApsp_Util_Index
import Definitions.Def_APSPSource_ThreeSumApsp_Util_List
import Definitions.Def_APSPSource_ThreeSumApsp_Util_Log
import Definitions.Def_APSPSource_ThreeSumApsp_Util_PrimesInWindow
import Definitions.Def_TrulySubcubicAPSP_SourceSpecification
import Mathlib.Algebra.BigOperators.Associated
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Field.GeomSum
import Mathlib.Algebra.Group.Action.Defs
import Mathlib.Algebra.Group.Int.Defs
import Mathlib.Algebra.GroupWithZero.Nat
import Mathlib.Algebra.MvPolynomial.Basic
import Mathlib.Algebra.MvPolynomial.CommRing
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Algebra.Order.BigOperators.Group.List
import Mathlib.Algebra.Order.BigOperators.Group.Multiset
import Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Algebra.Order.Field.GeomSum
import Mathlib.Algebra.Order.Floor.Div
import Mathlib.Algebra.Order.Floor.Semifield
import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.Algebra.Order.Group.Abs
import Mathlib.Algebra.Order.Group.Int
import Mathlib.Algebra.Order.Group.Nat
import Mathlib.Algebra.Order.Group.Unbundled.Abs
import Mathlib.Algebra.Order.Ring.Abs
import Mathlib.Algebra.Order.Ring.Int
import Mathlib.Algebra.Order.Ring.Nat
import Mathlib.Algebra.Order.Ring.Rat
import Mathlib.Analysis.Asymptotics.Lemmas
import Mathlib.Analysis.Complex.Exponential
import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Analysis.Convex.SpecificFunctions.Basic
import Mathlib.Analysis.Normed.Field.Basic
import Mathlib.Analysis.SpecialFunctions.BinaryEntropy
import Mathlib.Analysis.SpecialFunctions.Log.Base
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecificLimits.Normed
import Mathlib.Combinatorics.Enumerative.DoubleCounting
import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Data.Bool.Count
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Finset.Sort
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Data.Fintype.Fin
import Mathlib.Data.Int.Cast.Lemmas
import Mathlib.Data.Int.Notation
import Mathlib.Data.Int.SuccPred
import Mathlib.Data.List.GetD
import Mathlib.Data.List.Induction
import Mathlib.Data.List.Iterate
import Mathlib.Data.List.MinMax
import Mathlib.Data.List.OfFn
import Mathlib.Data.List.Range
import Mathlib.Data.List.TakeWhile
import Mathlib.Data.Nat.Bitwise
import Mathlib.Data.Nat.Cast.Order.Ring
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Choose.Bounds
import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Nat.Count
import Mathlib.Data.Nat.Digits.Defs
import Mathlib.Data.Nat.Digits.Lemmas
import Mathlib.Data.Nat.Log
import Mathlib.Data.Nat.Notation
import Mathlib.Data.Nat.Prime.Factorial
import Mathlib.Data.Nat.Size
import Mathlib.Data.Nat.SuccPred
import Mathlib.Data.Real.Basic
import Mathlib.Data.Set.Function
import Mathlib.LinearAlgebra.Finsupp.LinearCombination
import Mathlib.LinearAlgebra.Matrix.Defs
import Mathlib.LinearAlgebra.Matrix.Notation
import Mathlib.Logic.Equiv.Basic
import Mathlib.Logic.Function.Basic
import Mathlib.Logic.Function.Iterate
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.NumberTheory.Bertrand
import Mathlib.NumberTheory.Chebyshev
import Mathlib.NumberTheory.PrimeCounting
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.Order.Filter.AtTopBot.Basic
import Mathlib.Order.Interval.Finset.Fin
import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Probability.Independence.Basic
import Mathlib.RingTheory.AdjoinRoot
import Mathlib.Tactic.Common
import Mathlib.Tactic.DeriveFintype
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NoncommRing
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Mathlib.Tactic.SplitIfs

set_option autoImplicit false
set_option relaxedAutoImplicit false

section
-- Source module: ThreeSumApsp.Lang.Assigns
/-!
# A statement changes only the local variables that it assigns

`s.assigns` lists the local variables that the statement `s` assigns: the targets of its
assignments and the result variables of its calls.  A run of `s` leaves every other local variable
as it was (`Exec.loc_eq_of_notMem_assigns`), so every fact about `s` may be extended by "all other
locals are as before" (`Ends.keeping`).  A lemma about a piece of program text therefore speaks
about the memory and about the locals that the piece assigns, and about no other local.
-/

@[expose] public section

namespace Light

variable {lim : Limits} {P : Program} {d : ℕ}

/-- The local variables that a statement assigns: the targets of its assignments and the result
variables of its calls. -/
@[simp] def Stmt.assigns : Stmt → List ℕ
  | .skip => []
  | .set x _ => [x]
  | .store _ _ => []
  | .seq s t => s.assigns ++ t.assigns
  | .ite _ s t => s.assigns ++ t.assigns
  | .while _ s => s.assigns
  | .call _ _ x => [x]

end Light
end
end

section
-- Source module: ThreeSumApsp.Lang.Frames
/-!
# Local variables as a list

In the proof of a procedure body the state is written out as ⟨frame [a, b, …], μ⟩: the list
holds the local variables 0, 1, …, and all further ones are 0.  An assignment to local x replaces
entry x of the list (setLocal).  The rules of this file treat one statement each.  They are told the
value that is assigned or stored, and they ask for one fact about each expression: that its
evaluation stays within the limits and gives this value (Expr.Gives).  This fact and the comparison
of the costs are proved by default from the hypotheses in the context.  Ends.forFrame and
Ends.forShape are the rules for counting loops in this form.  In the names of the rules, To says
that the state is ⟨frame l, μ⟩.

Locals by name, and locals whose values do not matter:

* `setLocals l [(x, a), (y, b), …]` is the list `l` after the assignments `x := a`, `y := b`, ….
  With the names of the locals for `x`, `y`, … it describes the locals of a procedure by name:
  `setLocals [] [(Size, n), (Bound, U), …]`.
* `updateLocals loc [(x, a), (y, b), …]` is the same for locals that are not given as a list.  A
  lemma about a piece of text that several procedures share is stated for arbitrary locals `loc`.
* `refreshLocals l loc xs` is the list `l` with the entries `xs` read from `loc`.
* `LocalsBut xs l loc` says that `loc` agrees with `frame l` except perhaps at the locals `xs`.  In
  an invariant, `xs` are the scratch variables.  `Ends.asFrame` goes from such locals to a list, and
  `LocalsBut.of_eq` comes back.
* `Ends.pieceTo` and `Ends.pieceToThen` use a lemma about a piece of text that assigns only the
  locals `xs`: afterwards the locals are `refreshLocals l loc' xs`, where `loc'` are the locals of
  which the lemma speaks.  The lemma need not mention the locals that the piece does not assign.
* `Ends.forScratch` is the rule for a counting loop whose body may change the scratch variables
  `xs`: the round says nothing about the locals.
-/

@[expose] public section

namespace Light

variable {lim : Limits} {P : Program} {d : ℕ}

/-! ## The list of the locals -/

/-! ## The value of an expression -/

/-! ## One statement -/

section rules

variable {l : List ℤ} {μ : ℕ → ℤ} {T : ℕ} {Q : State → Prop}

end rules

/-! ## Locals by name, and locals whose values do not matter -/

/-- The list `l` of the locals, with the entries `xs` read from `loc`. -/
@[simp] def refreshLocals (l : List ℤ) (loc : ℕ → ℤ) : List ℕ → List ℤ
  | [] => l
  | x :: xs => refreshLocals (setLocal l x (loc x)) loc xs

/-- The local variables `loc` are those of the list `l`, except perhaps the locals `xs`. -/
def LocalsBut (xs : List ℕ) (l : List ℤ) (loc : ℕ → ℤ) : Prop :=
  ∀ y ∉ xs, loc y = Light.frame l y

section
variable {xs : List ℕ} {l l' : List ℤ} {loc μ : ℕ → ℤ}

/-! ## A piece of program text with a lemma of its own -/

variable {T T₁ : ℕ} {s s₁ s₂ : Stmt} {Q R : State → Prop}

/-! ## Counting loops with scratch variables -/

end

end Light
end
end

section
-- Source module: ThreeSumApsp.Lang.Lib.Logs
/-!
# Logarithms, the cube root and halves, without division

Four routines on local variables only; none of them touches the memory.

* log2(x) returns ⌊log₂ x⌋ (0 for x = 0) by doubling (`log2_meets`).
* clog2(x) returns ⌈log₂ x⌉ (0 for x ≤ 1) by doubling (`clog2_meets`).
* cbrtCeil(n) returns the least s with s³ ≥ n, which is ⌈n^{1/3}⌉, by counting up
  (`cbrtCeil_meets`).
* half(h) returns ⌈h/2⌉ by counting up (`half_meets`).

Each of them is one loop that tries the candidates 0, 1, 2, … in turn.  Local variable 0 holds the
argument and receives the result, local variable 1 holds the candidate (`Arg`, `Cand`), and the two
logarithms keep a power of two in local variable 2 (`Power`).
-/

@[expose] public section

namespace Light

variable {lim : Limits} {P : Program} {d : ℕ}

namespace Logs

@[inherit_doc Light.Logs.Arg] abbrev Power : ℕ := 2

end Logs

open Logs

/-! ## The logarithm, rounded down -/

/-- log2(x): the candidate is L, and the power is 2^(L + 1). -/
def log2Body : Stmt :=
  .set Light.Logs.Cand (Light.k 0) ;;
  .set Light.Logs.Power (Light.k 2) ;;
  .while (Light.v Light.Logs.Power ≤' Light.v Light.Logs.Arg) (
    .set Light.Logs.Power (Light.v Light.Logs.Power +' Light.v Light.Logs.Power) ;;
    .set Light.Logs.Cand (Light.v Light.Logs.Cand +' Light.k 1)) ;;
  .set Light.Logs.Arg (Light.v Light.Logs.Cand)

/-- The time of log2. -/
@[simp] def log2Time (x : ℕ) : ℕ := 14 * Nat.log 2 x + 12

/-! ## The logarithm, rounded up -/

/-! ## The cube root, rounded up -/

/-! ## Halves, rounded up -/

end Light
end
end

section
-- Source module: ThreeSumApsp.Filter.ThinCosts
/-!
# The numbers for `c = 212733/10000`, `θ = 111731/10⁶`

The exponents of the sharper Corollary 31 at the parameters of the filtering reduction:

* `Γ(c, θ) > 0.0703531` (the value is `0.07035314036…`), `GammaOfF_gt`; and `Γ < 0.0704`;
* `A_pruned(c) < 17.5211` (the value is `17.52101369…`), `AprunedF_lt`;
* `q(θ) < 0.4296471` (the value is `0.42964704490…`), `qOfF_lt`;
* the parameters are admissible with `ε = 71/1249` (`admissibleF`): `ε (A + Γ) ≈ 0.99999 < 1`.

The lower bound on `Γ` is tight (about `4·10⁻⁸`), so `Γ ln 4` is written as
`(1-θ) ln(1-θ) + (c-1) ln((c-1+θ)/(c-1)) + θ ln(c-1+θ) - θ ln 9`: the two large terms
`(c-1+θ) ln(c-1+θ) - (c-1) ln(c-1)` are combined, so that the error of the bounds on `ln 2` is
multiplied only by `θ`.
-/

@[expose] public section

namespace ThreeSumApsp

/-- The parameter `c = 212733/10000` of the filtering reduction. -/
noncomputable abbrev cF : ℝ := 212733 / 10000

/-- The parameter `θ = 111731/10⁶` of the filtering reduction. -/
noncomputable abbrev θF : ℝ := 111731 / 1000000

lemma logF_a : Real.log (888269 / 1000000) ∈ Set.Icc (-0.118480654) (-0.118480653) :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 0 5).1, (log_mem_b299791 0 5).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma logF_b : Real.log (20385031 / 20273300) ∈ Set.Icc 0.0054961076 0.0054961077 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 0 3).1, (log_mem_b299791 0 3).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma logF_c : Real.log (20385031 / 1000000) ∈ Set.Icc 3.01480085 3.01480086 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 4 6).1, (log_mem_b299791 4 6).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma logF_9 : Real.log 9 ∈ Set.Icc 2.197224576 2.197224579 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 3 6).1, (log_mem_b299791 3 6).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma logF_4 : Real.log 4 ∈ Set.Icc 1.3862943606 1.3862943616 := by
  rw [Real.log_four]
  exact ⟨by linarith [Real.log_two_gt_d9], by linarith [Real.log_two_lt_d9]⟩

lemma logF_cc : Real.log (212733 / 10000) ∈ Set.Icc 3.0574527 3.0574528 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 4 6).1, (log_mem_b299791 4 6).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma logF_c1 : Real.log (202733 / 10000) ∈ Set.Icc 3.0093047 3.0093048 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 4 6).1, (log_mem_b299791 4 6).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

lemma logF_3 : Real.log 3 ∈ Set.Icc 1.0986122 1.0986123 :=
  ⟨le_trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                   ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                   ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC])) (log_mem_b299791 2 8).1, (log_mem_b299791 2 8).2.trans (by (norm_num [ThreeSumApsp.logApprox, ThreeSumApsp.logErr, ThreeSumApsp.seriesArg,
                                                                                                                                                                           ThreeSumApsp.logTwoLo, ThreeSumApsp.logTwoHi, ThreeSumApsp.logThreeLo, ThreeSumApsp.logThreeHi,
                                                                                                                                                                           ThreeSumApsp.logTenLo, ThreeSumApsp.logTenHi, Finset.sum_range_succ, ThreeSumApsp.rhoC]))⟩

/-- `Γ ln 4` at `c = 212733/10000`, `θ = 111731/10⁶`, with the two large terms combined. -/
lemma GammaOfF_eq :
    GammaOf cF θF * Real.log 4
      = 888269 / 1000000 * Real.log (888269 / 1000000)
        + 202733 / 10000 * Real.log (20385031 / 20273300)
        + 111731 / 1000000 * Real.log (20385031 / 1000000)
        - 111731 / 1000000 * Real.log 9 := by
  rw [GammaOf_mul_log_four (by norm_num) (by norm_num) (by norm_num)]
  unfold cF θF
  have h1 : (1 : ℝ) - 111731 / 1000000 = 888269 / 1000000 := by norm_num
  have h2 : (212733 / 10000 : ℝ) - 1 + 111731 / 1000000 = 20385031 / 1000000 := by norm_num
  have h3 : (212733 / 10000 : ℝ) - 1 = 202733 / 10000 := by norm_num
  rw [h1, h2, h3, show (20385031 / 20273300 : ℝ) = (20385031 / 1000000) / (202733 / 10000) by
    norm_num, Real.log_div (x := 20385031 / 1000000) (y := 202733 / 10000) (by norm_num)
    (by norm_num)]
  ring

/-- `Γ(212733/10000, 111731/10⁶) < 0.0704`. -/
theorem GammaOfF_lt : GammaOf cF θF < 0.0704 := by
  refine lt_of_mul_lt_mul_right ?_ log_four_pos.le
  rw [GammaOfF_eq]
  have h1 := logF_a; have h2 := logF_b; have h3 := logF_c; have h4 := logF_9
  have h5 := logF_4
  simp only [Set.mem_Icc] at *
  linarith

/-- `A_pruned(212733/10000) < 17.5211` (the value is `17.52101369…`). -/
theorem AprunedF_lt : Apruned cF < 17.5211 := by
  refine lt_of_mul_lt_mul_right ?_ log_four_pos.le
  rw [Apruned_mul_log_four (by norm_num)]
  have h1 := logF_cc; have h2 := logF_c1; have h3 := logF_3; have h5 := logF_4
  simp only [Set.mem_Icc] at *
  norm_num
  linarith

/-- The parameters `c = 212733/10000`, `θ = 111731/10⁶`, `ε = 71/1249` are admissible. -/
theorem admissibleF : AdmissibleP cF θF (71 / 1249) where
  c_gt := by norm_num
  θ_pos := by norm_num
  θ_lt := by norm_num
  thin := by
    have h1 := AprunedF_lt
    have h2 := GammaOfF_lt
    nlinarith

end ThreeSumApsp
end
end

section
-- Source module: ThreeSumApsp.Filter.ThinRegime
/-!
# The parameters 212733/10000 and 111731/10⁶, and the regime D^1249 ≤ N^71

The program with rational parameters at `c = 212733/10000`, `θ = 111731/10⁶` and a threshold `m₀`
from `CorollaryP.costs admissibleF` (`ratParamsF`).  On the inputs with `D^1249 ≤ N^71`, i.e.
`D ≤ N^{71/1249}`, the bounds

    Tp = N² (log D + 1)²/D^{0.0703531}     and     Tq = D^{0.4296471} (log D + 1)

dominate the pruned cost of the preprocessing and the cost of a query of Theorem 30 at these
parameters (`regimeF`).  As `RegimeP.lean`, at the new parameters.
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec4

/-! ## The parameters -/

/-- The constant of the sharper corollary at `c = 212733/10000`, `θ = 111731/10⁶`,
`ε = 71/1249`. -/
noncomputable def costsFC : ℝ := Classical.choose (CorollaryP.costs admissibleF)

/-- The threshold of the sharper corollary at these parameters. -/
noncomputable def costsFm : ℕ :=
  Classical.choose (Classical.choose_spec (CorollaryP.costs admissibleF))

/-- The parameters in the program text: `L = ⌈212733 m/10000⌉`, `t = ⌈111731 m/10⁶⌉`, and the
threshold. -/
noncomputable def ratParamsF : RatParams where
  a := 212733
  b := 10000
  p := 111731
  q := 1000000
  m₀ := max costsFm 1
  hb := by norm_num
  hq := by norm_num
  hc := by norm_num
  hp := by norm_num
  hθ := by norm_num
  hm₀ := le_max_right _ _

/-! ## The bounds -/

/-- The bound on the preprocessing, `N² (log D + 1)²/D^{0.0703531}`. -/
noncomputable def preBoundF (N D₀ : ℕ) : ℝ :=
  (N : ℝ) ^ 2 * (Real.log D₀ + 1) ^ 2 / (D₀ : ℝ) ^ (0.0703531 : ℝ)

/-- The bound on a query, `D^{0.4296471} (log D + 1)`. -/
noncomputable def queryBoundF (D₀ : ℕ) : ℝ := (D₀ : ℝ) ^ (0.4296471 : ℝ) * (Real.log D₀ + 1)

section bounds

variable {N D₀ : ℕ}

end bounds

/-! ## The regime -/

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.ThinRegimeTest
/-!
# The test D^1249 ≤ N^71

regimeTestF(N, D) returns 1 if `D^1249 ≤ N^71` and 0 if not, and changes no cell.  It computes
`X = N^71` by a loop of 71 multiplications (each partial power is at most `N^71`, or 0), and then
compares `D^1249` with `X` as `regimeTestP` compares `D^91` with `N^5`: by at most 1249
multiplications, none of which exceeds `X D` (but for the first product, which is `D`), stopping as
soon as a power of `D` exceeds `X`.
-/

@[expose] public section

namespace Light.Filter

open ThreeSumApsp

variable {lim : Limits} {P : Program} {d : ℕ}

/-! ## The text -/

/-- One round of the computation of `N^71` (`N` is local 0, the power local 2, its exponent
local 3). -/
def nPowRoundF : Stmt :=
  .set 2 (Light.v 2 *' Light.v 0) ;; .set 3 (Light.v 3 +' k 1)

/-- The computation of `N^71` into local 2. -/
def nPowF : Stmt :=
  .set 2 (k 1) ;;
  .set 3 (k 0) ;;
  .while (Light.v 3 <' k 71) nPowRoundF

/-- One round of the comparison of `D^1249` with `X` (local 0; `D` is local 1, the power local 7,
its exponent local 8, the flag local 9). -/
def regimePowRoundF : Stmt :=
  .ite (Light.v 0 <' Light.v 7 *' Light.v 1)
    (.set 9 (k 0) ;; .set 8 (k 1249))
    (.set 7 (Light.v 7 *' Light.v 1) ;; .set 8 (Light.v 8 +' k 1))

/-- The test `D^1249 ≤ X`: the flag (local 9) ends as 1 if it holds and as 0 if not. -/
def regimePowF : Stmt :=
  .set 7 (k 1) ;;
  .set 8 (k 0) ;;
  .set 9 (k 1) ;;
  .while (Light.v 8 <' k 1249) regimePowRoundF

/-- regimeTestF(N, D): `X := N^71`, then the test `D^1249 ≤ X`. -/
def regimeTestFBody : Stmt :=
  nPowF ;;
  .set 0 (Light.v 2) ;;
  regimePowF ;;
  .set 0 (Light.v 9)

/-! ## The power of N -/

/-- The states of the loop that computes `N^71`. -/
def NPowInvF (N D : ℕ) (μ : ℕ → ℤ) (σ : State) : Prop :=
  σ.mem = μ ∧ σ.loc 0 = N ∧ σ.loc 1 = D ∧
    ∃ j : ℕ, j ≤ 71 ∧ σ.loc 3 = j ∧ σ.loc 2 = ((N ^ j : ℕ) : ℤ)

/-! ## The comparison -/

/-- The states of the loop: as `PowInv91`, with 1249 in place of 91. -/
def PowInvF (X D : ℕ) (loc μ : ℕ → ℤ) (σ : State) : Prop :=
  σ.mem = μ ∧ (∀ x < 7, σ.loc x = loc x) ∧
    ((∃ j : ℕ, j ≤ 1249 ∧ σ.loc 8 = j ∧ σ.loc 9 = 1 ∧ σ.loc 7 = ((D ^ j : ℕ) : ℤ) ∧
        (j = 0 ∨ D ^ j ≤ X)) ∨
      (σ.loc 8 = 1249 ∧ σ.loc 9 = 0 ∧ X < D ^ 1249))

/-! ## The test -/

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.ThinAll
/-!
# The pruned thin product on all instances, at the parameters of the filtering reduction

allInstancesF(N, D, w, U, x, y, wi, wj, out, fr) tests whether `D^1249 ≤ N^71`, calls the offline
routine offline32 of the programs with rational parameters at `ratParamsF` (`c = 212733/10000`,
`θ = 111731/10⁶`) if so, and the brute force if not.  The program is `programF`:
`program31P ratParamsF` followed by allInstancesF (number 74) and regimeTestF (number 75).  As
`Pruned/AllInstancesP.lean`, at the new parameters.

* It solves the task `thinTask` on all instances (`allInstancesF_solves`), with a polynomial need
  (`allInstancesNeedF_poly`).
* In the regime its time is `O(w D^{0.4296471} (log D + 1) + N² (log D + 1)²/D^{0.0703531})`
  (`allInstancesTimeF_le`).
* `claim_thinProductF`: the thin product in this time for programs of the light language.
-/

@[expose] public section

namespace Light.Filter

open ThreeSumApsp ThreeSumApsp.Spec Light.Sec4

/-! ## The program -/

/-- The numbers of the two new procedures. -/
abbrev Proc.allInstancesF : ℕ := 74
@[inherit_doc Proc.allInstancesF] abbrev Proc.regimeTestF : ℕ := 75

/-- allInstancesF(N, D, w, U, x, y, wi, wj, out, fr). Local 10 is the result of the test. -/
def allInstancesFBody : Stmt :=
  .call Proc.regimeTestF [Light.v 0, Light.v 1] 10 ;;
  .ite (k 0 <' Light.v 10)
    (.call Proc.offline32 [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 6, Light.v 7, Light.v 8, Light.v 9] 0)
    (.call Sec2.pThinBrute [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 6, Light.v 7, Light.v 8, Light.v 9] 0)

/-- The program: the programs with rational parameters at `ratParamsF`, then allInstancesP and
regimeTestP. -/
noncomputable def programF : Program := program31P ratParamsF ++ [allInstancesFBody, regimeTestFBody]

/-! ## Time and need -/

/-- The time of allInstancesF, for the parameters N, D, w, U. -/
noncomputable def allInstancesTimeF (c : ℕ) : List ℕ → ℕ
  | [N, D, w, _] =>
    30000 + (if D ^ 1249 ≤ N ^ 71 then tOffline32P c ratParamsF N D w else 40 * ((w + 1) * (D + 1)))
  | _ => 0

/-- The word part of the need. -/
noncomputable def wordNeedF (N D U : ℕ) : ℕ :=
  1100000 + 1300000 * D + N * D + D * (U * U) + ((N + 1) ^ 5) ^ 3 * (U * U)
    + 7 * ((N + 1) ^ 5 * U) + 10 * (N + 1) ^ 5 + N ^ 71 * D + N ^ 71 + ratParamsF.m₀

/-- What allInstancesF needs, for the parameters N, D, w, U. -/
noncomputable def allInstancesNeedF : List ℕ → Need
  | [N, D, _, U] => ⟨wordNeedF N D U, 4 + N + 8 * (N * D) + 222 * ((N + 1) ^ 5) ^ 4, 88 * D + 12⟩
  | _ => ⟨0, 0, 0⟩

/-! ## The limits -/

section need

variable {lim : Limits} {N D₀ w U fr d : ℕ}

end need

/-! ## The routine -/

/-! ## The time in the regime -/

/-! ## The need is polynomial in the parameters -/

section summands

variable {N D U Q : ℕ}

end summands

/-! ## The claim -/

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.Defs
/-!
# Deterministic filtering: parameters and the counting oracle

The filtering reduction of the 2.996001 note (Lemma 3.1, Lemma 4.1).  A candidate is a triple
`(a, b, j)`: the pair `(a, b)` and the block `C_j = [j s, min((j+1) s, n))` of third vertices.  It
lies at index `i = j n² + a n + b`; its group is the pair, `i % (n n) = a n + b`.  For a modulus
`p ≥ 1` its count is the number of `c ∈ C_j` with `p ∣ w(a,b) + w(b,c) + w(a,c)`.

* The parameters, as functions of `n` and `U` (§3, (3.5)): `kOf`, `ellOf`, `RR`, `bOf`, `dOf`,
  `roundsOf`, `sOf`, `mOf`, `cKOf`, `rOf`, `BOf`, `hOf`, `pool`, `QOf`, `Guard`, `PmaxOf`.
* The counts (`cntList`) and the task of the counting oracle (`oracleTask`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec3

/-! ## Parameters -/

/-- `k`, the bit length of `n`: `n < 2^k`. -/
def kOf (n : ℕ) : ℕ := Nat.size n

/-- `ℓ = ⌊√k⌋ + 1`. -/
def ellOf (n : ℕ) : ℕ := Nat.sqrt (kOf n) + 1

/-- `R = 2^ℓ`; the pool is the primes in `[R, 2R)`. -/
def RR (n : ℕ) : ℕ := 2 ^ ellOf n

/-- `b = ℓ (⌊√ℓ⌋ + 1)`, about `k^{3/4}`. -/
def bOf (n : ℕ) : ℕ := ellOf n * (Nat.sqrt (ellOf n) + 1)

/-- `d = ⌊b/2⌋`: a round with the guard shrinks the active set by `2^d`. -/
def dOf (n : ℕ) : ℕ := bOf n / 2

/-- The number of rounds, `⌊3k/d⌋ + 1`, so that `d · rounds > 3k`. -/
def roundsOf (n : ℕ) : ℕ := 3 * kOf n / dOf n + 1

/-- The block size `s = 2^{⌊σ k⌋}`, `σ = 0.0284225`. -/
def sOf (n : ℕ) : ℕ := 2 ^ (284225 * kOf n / 10 ^ 7)

/-- The number of blocks, `⌈n/s⌉`. -/
def mOf (n : ℕ) : ℕ := (n + sOf n - 1) / sOf n

/-- `c_K`, the bit length of the largest witness count `s`. -/
def cKOf (n : ℕ) : ℕ := Nat.size (sOf n)

/-- The number of prime factors per round, `⌊(c_K + b)/ℓ⌋ + 1`. -/
def rOf (n : ℕ) : ℕ := (cKOf n + bOf n) / ellOf n + 1

/-- `B`, the bit length of `3U`: every triangle sum has absolute value below `2^B`. -/
def BOf (U : ℕ) : ℕ := Nat.size (3 * U)

/-- `h = ⌊(B − 1)/ℓ⌋`: a nonzero integer below `2^B` in absolute value has at most `h` prime
divisors in the pool. -/
def hOf (n U : ℕ) : ℕ := (BOf U - 1) / ellOf n

/-- The pool: the primes in `[R, 2R)`. -/
def pool (n : ℕ) : Finset ℕ := (Finset.range (2 * RR n)).filter fun q => RR n ≤ q ∧ q.Prime

/-- `Q`, the size of the pool. -/
def QOf (n : ℕ) : ℕ := (Light.Filter.pool n).card

/-- The guard (3.6), `K (2h)^r 2^d ≤ Q^r` with `K = s`.  Not tested by the program on the main
path; it holds for all large `n` along polynomially bounded `U`. -/
def Guard (n U : ℕ) : Prop := sOf n * (2 * hOf n U) ^ rOf n * 2 ^ dOf n ≤ QOf n ^ rOf n

instance (n U : ℕ) : Decidable (Guard n U) := by unfold Guard; infer_instance

/-- The largest modulus, `(2R)^r`. -/
def PmaxOf (n : ℕ) : ℕ := (2 * RR n) ^ rOf n

/-! ## The counts -/

/-- The block `j` of third vertices: `c` with `j s ≤ c < (j + 1) s` and `c < n`. -/
def InBlock (n s j c : ℕ) : Prop := j * s ≤ c ∧ c < (j + 1) * s ∧ c < n

instance (n s j c : ℕ) : Decidable (InBlock n s j c) := by unfold InBlock; infer_instance

/-- The triangle sum `w(a,b) + w(b,c) + w(a,c)` of the pair `q = a n + b` and the vertex `c`, as in
`aeFlags`. -/
def triSum (n : ℕ) (AB BC AC : List ℤ) (q c : ℕ) : ℤ :=
  AB.getD q 0 + BC.getD (q % n * n + c) 0 + AC.getD (q / n * n + c) 0

/-- The count of the candidate `i = j n² + q` at the modulus `p`: the `c` in block `j` with
`p ∣ triSum q c`. -/
def cntOf (n s p : ℕ) (AB BC AC : List ℤ) (i : ℕ) : ℕ :=
  ((Finset.range n).filter fun c =>
    InBlock n s (i / (n * n)) c ∧ (p : ℤ) ∣ triSum n AB BC AC (i % (n * n)) c).card

/-- All `m n²` counts at the modulus `p`, candidate `i` in cell `i`. -/
def cntList (n s p : ℕ) (AB BC AC : List ℤ) : List ℤ :=
  (List.range ((n + s - 1) / s * (n * n))).map fun i => (cntOf n s p AB BC AC i : ℤ)

/-! ## The counting oracle as a task -/

/-- An instance of the oracle: an all-edges instance (without the place of the flags), a block size
`s`, a modulus `p`, and the place `cnt` of the `m n²` counts. -/
structure OracleInst : Type extends TriInst where
  s : ℕ
  p : ℕ
  cnt : ℕ

/-- The number of counts, `⌈n/s⌉ n²`. -/
def OracleInst.len (x : OracleInst) : ℕ := (x.n + x.s - 1) / x.s * (x.n * x.n)

/-- The matrices and the place of the counts lie below the free pointer and do not meet;
`1 ≤ s ≤ n`, `1 ≤ p`. -/
structure OracleInst.Pre (x : OracleInst) (μ : ℕ → ℤ) (fr : ℕ) : Prop
    extends TriInst.Pre x.toTriInst μ fr where
  s_pos : 1 ≤ x.s
  s_le : x.s ≤ x.n
  p_pos : 1 ≤ x.p
  belowCnt : x.cnt + x.len ≤ fr
  apartAB : Apart x.ab (x.n * x.n) x.cnt x.len
  apartBC : Apart x.bc (x.n * x.n) x.cnt x.len
  apartAC : Apart x.ac (x.n * x.n) x.cnt x.len

/-- **The counting oracle** (Lemma 4.1): `oracle(n, U, ab, bc, ac, s, p, cnt, fr)` writes the counts
of all candidates at the modulus `p` to `cnt`, and changes no other cell below `fr`. -/
def oracleTask : TaskN where
  Inst := OracleInst
  pars x := [x.n, x.U, x.s, x.p]
  args x := [x.n, x.U, x.ab, x.bc, x.ac, x.s, x.p, x.cnt]
  Pre := OracleInst.Pre
  Post x μ fr _ μ' := Seg μ' x.cnt (cntList x.n x.s x.p x.AB x.BC x.AC) ∧
    KeptBut μ μ' fr x.cnt x.len

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.OracleData
/-!
# The counting oracle (Lemma 4.1): its instances, as pure data

The oracle reuses the instances of the host of Theorem 17 (`HostData`): the block size `s` plays the
part of the piece size `q`, the inner dimension is `D = s p`, and a class `W_ϱ` of the pairs is cut
into chunks of at most `cap = ⌈n²/p⌉` pairs.  The block of instance `t` is `j = t / chunkCount`.
The answer of the counting solver for the query pair number `i` of instance `t` is the count of the
candidate `j n² + place` (`oThinEntry_eq_cntOf`), and every candidate is the query pair of some
instance (`oCover`).  There are at most `⌈n/s⌉ · 2p` instances (`oData_m_le`).
-/

@[expose] public section

namespace Light.Filter

open ThreeSumApsp ThreeSumApsp.Spec Light.Sec3

/-- The largest number of query pairs of a call: `⌈n²/p⌉`. -/
def oCap (n p : ℕ) : ℕ := (n * n) ⌈/⌉ p

/-- The data of the instances of the oracle. -/
def oData (n s p : ℕ) (AB BC AC : List ℤ) : HostData := ⟨n, s * p, p, s, oCap n p, AB, BC, AC⟩

/-! ## The counts -/

section OData

open HostData

variable {X : HostData}

end OData

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.OracleScatter
/-!
# The counting oracle (Lemma 4.1): writing the answers to their candidates

`oScatter(out, qi, qj, w, base, n)` copies the `w` answers at `out` to the cells
`base + WI[i] n + WJ[i]`, where `WI` and `WJ` are the rows and the columns of the query pairs, at
`qi` and `qj`.  The answer of a query pair is a function `f` of its place `a n + b`, so a cell that
is written twice gets the same value twice.
-/

@[expose] public section

namespace Light.Filter

variable {lim : Limits} {P : Program} {d : ℕ}

/-- oScatter(out, qi, qj, w, base, n); local 6 is the counter. -/
def oScatterBody : Stmt :=
  Stmt.for 6 (Light.v 3) (.store (Light.v 4 +' Light.M (Light.v 1 +' Light.v 6) *' Light.v 5 +' Light.M (Light.v 2 +' Light.v 6)) (Light.M (Light.v 0 +' Light.v 6)))

/-- The time of oScatter. -/
def tOScatter (w : ℕ) : ℕ := 26 * w + 10

/-- The place of the query pair number `i`. -/
def oAddr (n : ℕ) (WI WJ : List ℕ) (i : ℕ) : ℕ := WI.getD i 0 * n + WJ.getD i 0

/-- What oScatter assumes. -/
structure ScatterPre (lim : Limits) (μ : ℕ → ℤ) (out qi qj w base n : ℕ) (WI WJ : List ℕ)
    (A : List ℤ) (f : ℕ → ℤ) : Prop where
  hw : (lim.space : ℤ) ≤ lim.word
  segI : SegN μ qi WI
  segJ : SegN μ qj WJ
  segA : Seg μ out A
  lenI : WI.length = w
  lenJ : WJ.length = w
  lenA : A.length = w
  ltI : ∀ x ∈ WI, x < n
  ltJ : ∀ x ∈ WJ, x < n
  val : ∀ i < w, A.getD i 0 = f (oAddr n WI WJ i)
  spaceB : base + n * n ≤ lim.space
  spaceI : qi + w ≤ lim.space
  spaceJ : qj + w ≤ lim.space
  spaceA : out + w ≤ lim.space
  apartI : Apart base (n * n) qi w
  apartJ : Apart base (n * n) qj w
  apartA : Apart base (n * n) out w

/-- The cells that the first `j` rounds have written, and no other cell, have changed. -/
def ScatterInv (μ : ℕ → ℤ) (base n : ℕ) (WI WJ : List ℕ) (f : ℕ → ℤ) (j : ℕ) (μ' : ℕ → ℤ) :
    Prop :=
  (∀ i < j, μ' (base + oAddr n WI WJ i) = f (oAddr n WI WJ i)) ∧
    ∀ a, (∀ i < j, a ≠ base + oAddr n WI WJ i) → μ' a = μ a

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.OracleLoop
/-!
# The counting oracle (Lemma 4.1): the loop over the instances

The loop has the shape of the loop of the host of Theorem 17 (`hostLoopBody`), and it reuses its
parts `hostParams` and `hostNext` with their specifications.  For each instance it writes the two
matrices, calls the counting solver, and writes the answers to the cells of their candidates
(`oScatter`).  The local `Found` of the loop of Theorem 17 holds here the place `cnt + j n²` of the
counts of the block `j` of the instance (`oBaseAt`); it moves on by `n²` when the chunks of a block
are done (`oBase`).

`oLoop_spec`: at the end every one of the `h n²` cells from `cnt` holds the count of its candidate,
and no other cell below `x` (the first matrix) has changed.
-/

@[expose] public section

namespace Light.Filter

open ThreeSumApsp ThreeSumApsp.Spec Light.Sec3 Light.Sec3.HostLocal

variable {lim : Limits} {d : ℕ}

/-! ## The procedure -/

/-- The four calls for one instance: the two matrices, the counting solver, the answers. -/
def oCalls (pS pWriteX pWriteY pScat : ℕ) : Stmt :=
  .call pWriteX [Light.v Light.Sec3.HostLocal.MatX, Light.v Light.Sec3.HostLocal.ResAC, Light.v Light.Sec3.HostLocal.Size, Light.v Light.Sec3.HostLocal.ParD, Light.v Light.Sec3.HostLocal.ThePrime, Light.v Light.Sec3.HostLocal.PieceStart, Light.v Light.Sec3.HostLocal.Len, Light.v Residue]
    Light.Sec3.HostLocal.Unused ;;
  .call pWriteY [Light.v Light.Sec3.HostLocal.MatY, Light.v Light.Sec3.HostLocal.ResBC, Light.v Light.Sec3.HostLocal.Size, Light.v Light.Sec3.HostLocal.ParD, Light.v Light.Sec3.HostLocal.ThePrime, Light.v Light.Sec3.HostLocal.PieceStart, Light.v Light.Sec3.HostLocal.Len] Light.Sec3.HostLocal.Unused ;;
  .call pS [Light.v Light.Sec3.HostLocal.Size, Light.v Light.Sec3.HostLocal.ParD, Light.v NumPairs, Light.k 1, Light.v Light.Sec3.HostLocal.MatX, Light.v Light.Sec3.HostLocal.MatY, Light.v Light.Sec3.HostLocal.Rows +' Light.v Light.Sec3.HostLocal.Start, Light.v Light.Sec3.HostLocal.Cols +' Light.v Light.Sec3.HostLocal.Start,
    Light.v Light.Sec3.HostLocal.AdrOut, Light.v Light.Sec3.HostLocal.SolverFree] Light.Sec3.HostLocal.Unused ;;
  .call pScat [Light.v Light.Sec3.HostLocal.AdrOut, Light.v Light.Sec3.HostLocal.Rows +' Light.v Light.Sec3.HostLocal.Start, Light.v Light.Sec3.HostLocal.Cols +' Light.v Light.Sec3.HostLocal.Start, Light.v NumPairs, Light.v Light.Sec3.HostLocal.Found, Light.v Light.Sec3.HostLocal.Size] Light.Sec3.HostLocal.Unused

/-- The place of the counts of the next block, after the last chunk of a block. -/
def oBase : Stmt :=
  .ite (Light.v Light.Sec3.HostLocal.ChunkNo +' Light.k 1 =' Light.v Light.Sec3.HostLocal.NumChunks) (.set Light.Sec3.HostLocal.Found (Light.v Light.Sec3.HostLocal.Found +' Light.v Light.Sec3.HostLocal.Size *' Light.v Light.Sec3.HostLocal.Size)) .skip

/-- One round of the loop. -/
def oRound (pS pWriteX pWriteY pScat : ℕ) : Stmt :=
  hostParams ;; oCalls pS pWriteX pWriteY pScat ;; oBase ;; hostNext

/-- oLoop(n, D, p, q, chunkCount, m, ab, bc, ac, rac, rbc, qi, qj, cr, cl, cw, x, y, out, fr, 0, 0, 0,
cnt). -/
def oLoopBody (pS pWriteX pWriteY pScat : ℕ) : Stmt :=
  .set Light.Sec3.HostLocal.Inst (Light.k 0) ;; .set Light.Sec3.HostLocal.ChunkNo (Light.k 0) ;; .set Light.Sec3.HostLocal.PieceStart (Light.k 0) ;;
  .while (Light.v Light.Sec3.HostLocal.Inst <' Light.v Light.Sec3.HostLocal.NumInst) (oRound pS pWriteX pWriteY pScat)

/-! ## The data -/

/-- The number of candidates, `h n²`. -/
def oLen (X : HostData) : ℕ := X.h * (X.n * X.n)

/-- The place of the counts of the block of instance t. -/
def oBaseAt (X : HostData) (cnt t : ℕ) : ℕ := cnt + t / X.chunkCount * (X.n * X.n)

/-- The count of the candidate e. -/
def oCnt (X : HostData) (e : ℕ) : ℤ := (cntOf X.n X.q X.p X.AB X.BC X.AC e : ℤ)

/-- The candidate e is a query pair of an instance before t. -/
def ODone (X : HostData) (t e : ℕ) : Prop :=
  ∃ t' < t, ∃ i < X.w t', e = t' / X.chunkCount * (X.n * X.n) + X.place t' i

/-- The largest time of the counting solver on an instance with at most cap query pairs. -/
def oSupTime (Tn : List ℕ → ℕ) (n D cap : ℕ) : ℕ :=
  (Finset.range (cap + 1)).sup fun w => Tn [n, D, w]

/-- The time of a round, in the worst case. -/
def tORound (Tn : List ℕ → ℕ) (X : HostData) : ℕ :=
  tWriteX X.n X.D X.q + tWriteY X.n X.D X.q + oSupTime Tn X.n X.D X.cap + tOScatter X.cap + 104

/-- The time of the loop. -/
def tOLoop (Tn : List ℕ → ℕ) (X : HostData) : ℕ := X.m * (4 + tORound Tn X) + 10

/-- The context of the loop: a solver of #Lop-AE-SparseTri, and the procedures writeX, writeY and
oScatter in the program. -/
structure OCtx (P₀ R : Program) (pS pWriteX pWriteY pScat : ℕ) (Tn : List ℕ → ℕ)
    (need : List ℕ → Light.Need) : Prop where
  sol : SolvesN lopCountTask P₀ pS Tn need
  writeX : (P₀ ++ R)[pWriteX]? = some writeXBody
  writeY : (P₀ ++ R)[pWriteY]? = some writeYBody
  scat : (P₀ ++ R)[pScat]? = some oScatterBody

/-- What the loop assumes: what the loop of Theorem 17 assumes, in the first memory μ₀, and the
place of the `h n²` counts meets none of the arrays that the loop reads. -/
structure OSetting (lim : Limits) (d : ℕ) (X : HostData) (U : ℕ) (A : HostAddr)
    (need : List ℕ → Light.Need) (cnt : ℕ) (μ₀ : ℕ → ℤ) : Prop where
  ok : HostOk X U
  mem : HostMem X A μ₀
  lay : HostLay X A
  fits : HostLim lim d X U A need
  apAB : Apart A.ab (X.n * X.n) cnt (oLen X)
  apBC : Apart A.bc (X.n * X.n) cnt (oLen X)
  apAC : Apart A.ac (X.n * X.n) cnt (oLen X)
  lowRAC : cnt + oLen X ≤ A.rac
  lowRBC : cnt + oLen X ≤ A.rbc
  lowQI : cnt + oLen X ≤ A.qi
  lowQJ : cnt + oLen X ≤ A.qj
  lowCR : cnt + oLen X ≤ A.cr
  lowCL : cnt + oLen X ≤ A.cl
  lowCW : cnt + oLen X ≤ A.cw

/-- The memory before instance t: below `x`, only counts have changed, and the counts of the
candidates of the instances before t are written. -/
def OMem (X : HostData) (A : HostAddr) (cnt : ℕ) (μ₀ μ : ℕ → ℤ) (t : ℕ) : Prop :=
  SameOn (fun a => a < A.x ∧ Outside cnt (oLen X) a) μ₀ μ ∧
    ∀ e < oLen X, ODone X t e → μ (cnt + e) = oCnt X e

/-! ## Facts about the data -/

section facts

variable {X : HostData} {U : ℕ} {A : HostAddr} {need : List ℕ → Need} {cnt : ℕ} {μ₀ : ℕ → ℤ}

end facts

/-! ## The parts of a round -/

variable {P₀ R : Program} {pS pWriteX pWriteY pScat : ℕ} {Tn : List ℕ → ℕ}
  {need : List ℕ → Need} {X : HostData} {U : ℕ} {A : HostAddr} {cnt : ℕ} {μ₀ : ℕ → ℤ} {t : ℕ}

/-- The time of the four calls of instance t. -/
def tOCalls (Tn : List ℕ → ℕ) (X : HostData) (t : ℕ) : ℕ :=
  tWriteX X.n X.D (X.len t) + tWriteY X.n X.D (X.len t) + Tn [X.n, X.D, X.w t] +
    tOScatter (X.w t) + 47

/-! ## The loop -/

/-- The invariant of the loop, before instance t. -/
def OInv (X : HostData) (A : HostAddr) (cnt : ℕ) (μ₀ : ℕ → ℤ) (t : ℕ) (σ : State) : Prop :=
  ∃ (len rho lo w res : ℤ) (μ : ℕ → ℤ),
    σ = hostState X A t (t % X.chunkCount) (X.c0 t) (oBaseAt X cnt t : ℕ) len rho lo w res μ ∧
    OMem X A cnt μ₀ μ t

/-- The arguments of the loop. -/
def oLoopArgs (X : HostData) (A : HostAddr) (cnt : ℕ) : List ℤ :=
  hostLoopArgs X A ++ [0, 0, 0, (cnt : ℤ)]

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.OracleCore
/-!
# The counting oracle (Lemma 4.1): the core procedure

The core procedure of the oracle gets its locals in the layout of the host of Theorem 17 (`Et17`),
with the place `cnt` of the counts in the local `ParG` and the block size `s` in `RootD`, so that the
parts of that host can be reused: the addresses (`et17Addr_spec`), the table of doubles and the
residues (`resid_then`), the classes and the chunks (`classes_then`).  Then it runs the loop over
the instances (`oLoop_spec`).

`oCore_spec`: afterwards the place `cnt` holds the counts of all candidates, and no other cell below
the free pointer has changed.
-/

@[expose] public section

namespace Light.Filter

open ThreeSumApsp ThreeSumApsp.Spec Light.Sec3 Light.Sec3.Et17

variable {lim : Limits} {d : ℕ}

/-- The numbers of the procedures of the oracle. -/
structure ONums : Type where
  pS : ℕ
  pCeil : ℕ
  pBitLen : ℕ
  pDbl : ℕ
  pResid : ℕ
  pResidues : ℕ
  pClasses : ℕ
  pChunks : ℕ
  pWriteX : ℕ
  pWriteY : ℕ
  pScat : ℕ
  pLoop : ℕ
  pCore : ℕ

/-- oCore(n, U, ab, bc, ac, fr, D, cnt, s, p, cap, s, h, bits), in the locals of et17. -/
def oCoreBody (ν : ONums) : Stmt :=
  et17Addr ;;
  .call ν.pDbl [Light.v Light.Sec3.Et17.Free, Light.v ThePrime, Light.v Bits] Light.Sec3.Et17.Small ;;
  .call ν.pResidues [Light.v Light.Sec3.Et17.AdrAB, Light.v ResAB, Light.v SizeSq, Light.v Light.Sec3.Et17.Free, Light.v Bits] Light.Sec3.Et17.Small ;;
  .call ν.pResidues [Light.v Light.Sec3.Et17.AdrBC, Light.v ResBC, Light.v SizeSq, Light.v Light.Sec3.Et17.Free, Light.v Bits] Light.Sec3.Et17.Small ;;
  .call ν.pResidues [Light.v Light.Sec3.Et17.AdrAC, Light.v ResAC, Light.v SizeSq, Light.v Light.Sec3.Et17.Free, Light.v Bits] Light.Sec3.Et17.Small ;;
  .call ν.pClasses [Light.v ResAB, Light.v Light.Sec3.Et17.Size, Light.v ThePrime, Light.v Cls, Light.v Light.Sec3.Et17.Cur, Light.v Light.Sec3.Et17.Rows, Light.v Light.Sec3.Et17.Cols] Light.Sec3.Et17.Small ;;
  .call ν.pChunks [Light.v Cls, Light.v ThePrime, Light.v Cap, Light.v TabR, Light.v TabL, Light.v TabW] NumChunks ;;
  .set NumInst (Light.v NumPieces *' Light.v NumChunks) ;;
  .call ν.pLoop [Light.v Light.Sec3.Et17.Size, Light.v ParD, Light.v ThePrime, Light.v PieceLen, Light.v NumChunks, Light.v NumInst, Light.v Light.Sec3.Et17.AdrAB, Light.v Light.Sec3.Et17.AdrBC,
    Light.v Light.Sec3.Et17.AdrAC, Light.v ResAC, Light.v ResBC, Light.v Light.Sec3.Et17.Rows, Light.v Light.Sec3.Et17.Cols, Light.v TabR, Light.v TabL, Light.v TabW, Light.v Light.Sec3.Et17.MatX, Light.v Light.Sec3.Et17.MatY, Light.v AdrOut,
    Light.v Light.Sec3.Et17.SolverFree, Light.k 0, Light.k 0, Light.k 0, Light.v ParG] 0

/-- The context of the core procedure. -/
structure OCoreCtx (P₀ R : Program) (ν : ONums) (Tn : List ℕ → ℕ) (need : List ℕ → Light.Need) :
    Prop where
  loop : OCtx P₀ R ν.pS ν.pWriteX ν.pWriteY ν.pScat Tn need
  hLoop : (P₀ ++ R)[ν.pLoop]? = some (oLoopBody ν.pS ν.pWriteX ν.pWriteY ν.pScat)
  hDbl : (P₀ ++ R)[ν.pDbl]? = some dblTableBody
  hResid : (P₀ ++ R)[ν.pResid]? = some residBody
  hResidues : (P₀ ++ R)[ν.pResidues]? = some (residuesBody ν.pResid)
  hClasses : (P₀ ++ R)[ν.pClasses]? = some classesBody
  hChunks : (P₀ ++ R)[ν.pChunks]? = some chunksBody

/-- The data of the instances of an instance of the oracle. -/
def oDataOf (x : OracleInst) : HostData := oData x.n x.s x.p x.AB x.BC x.AC

/-- The time of the core procedure in a run. -/
def tCoreRun (Tn : List ℕ → ℕ) (X : HostData) (U : ℕ) : ℕ :=
  tDblTable (bitLen U) + 3 * tResidues (X.n * X.n) (bitLen U) + tClasses X.n X.p
    + tChunks X.p X.chunkCount + tOLoop Tn X + 150

/-- The arguments of the core procedure. -/
def oCoreArgs (x : OracleInst) (fr : ℕ) : List ℤ :=
  [(x.n : ℤ), (x.U : ℤ), (x.ab : ℤ), (x.bc : ℤ), (x.ac : ℤ), (fr : ℤ), ((x.s * x.p : ℕ) : ℤ),
    (x.cnt : ℤ), (x.s : ℤ), (x.p : ℤ), (oCap x.n x.p : ℕ), (x.s : ℤ), ((x.n ⌈/⌉ x.s : ℕ) : ℤ),
    ((bitLen x.U : ℕ) : ℤ)]

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.OracleHost
/-!
# The counting oracle (Lemma 4.1) as a host

The top procedure `oracle(n, U, ab, bc, ac, s, p, cnt, fr)` computes `D = s p`, `cap = ⌈n²/p⌉`,
the number `h = ⌈n/s⌉` of blocks and the number of binary digits of `U`, and calls the core
procedure (`oCore_spec`).  With an arbitrary solver of #Lop-AE-SparseTri it solves `oracleTask`
(`oracle_solves`), within the time `oracleTime` and the need `oracleNeed`.

The time: `⌈n/s⌉ · 2p` calls of the solver, each with `n` rows, inner dimension `s p` and at most
`cap` query pairs, so the solver enters only through `oSupTime Tl n (s p) cap`, its largest time on
such instances; besides, writing the matrices (`O(n s p)` per call), the answers (`O(cap)` per
call), the residues (`O(n² log U)`), the classes and the chunks.
-/

@[expose] public section

namespace Light.Filter

open ThreeSumApsp ThreeSumApsp.Spec Light.Sec3

variable {lim : Limits} {d : ℕ}

/-! ## The procedure -/

/-- oracle(n, U, ab, bc, ac, s, p, cnt, fr): locals 9 to 12 are `D`, `cap`, `h` and the number of
binary digits of `U`. -/
def oracleBody (pCeil pBitLen pCore : ℕ) : Stmt :=
  .set 9 (Light.v 5 *' Light.v 6) ;;
  .call pCeil [Light.v 0 *' Light.v 0, Light.v 6] 10 ;;
  .call pCeil [Light.v 0, Light.v 5] 11 ;;
  .call pBitLen [Light.v 1] 12 ;;
  .call pCore [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 8, Light.v 9, Light.v 7, Light.v 5, Light.v 6, Light.v 10, Light.v 5, Light.v 11, Light.v 12] 0

/-! ## Time and need -/

/-- **The time of the oracle**, over a solver with the time `Tl`, for `n`, `U`, `s`, `p`. -/
def oTimeAt (Tl : List ℕ → ℕ) (n U s p : ℕ) : ℕ :=
  tCeilDiv (n * n) p + tCeilDiv n s + tBitLen U + tDblTable (bitLen U)
    + 3 * tResidues (n * n) (bitLen U) + tClasses n p + tChunks p (2 * p)
    + (n + s - 1) / s * (2 * p) *
      (tWriteX n (s * p) s + tWriteY n (s * p) s + oSupTime Tl n (s * p) (oCap n p)
        + tOScatter (oCap n p) + 108)
    + 300

/-- The time of the oracle as a function of the parameters `[n, U, s, p]`. -/
def oracleTime (Tl : List ℕ → ℕ) (ps : List ℕ) : ℕ :=
  oTimeAt Tl (ps.getD 0 0) (ps.getD 1 0) (ps.getD 2 0) (ps.getD 3 0)

/-- The cells of the arrays of the oracle, from the free pointer on. -/
def oLayout (n U s p : ℕ) : ℕ :=
  (bitLen U + 1) + 3 * (n * n) + (p + 1) + p + 2 * (n * n) + 3 * (n * n + p) + 2 * (n * (s * p))
    + oCap n p

/-- The largest number that the oracle forms, apart from the solver. -/
def oWord (n U s p : ℕ) : ℕ :=
  (n * n + p + 1) + (n + s + 1) + (2 * U + 2) + s * p + p * (4 * (U + 1)) + (3 * U + 1)
    + (n + s - 1) / s * (2 * p) + 1

/-- The largest need of the solver on an instance with at most cap query pairs. -/
def oSupNeed (need : List ℕ → Light.Need) (n D cap : ℕ) : Need :=
  ⟨(Finset.range (cap + 1)).sup fun w => (need [n, D, w]).word,
    (Finset.range (cap + 1)).sup fun w => (need [n, D, w]).cells,
    (Finset.range (cap + 1)).sup fun w => (need [n, D, w]).depth⟩

/-- The need of the oracle, for `n`, `U`, `s`, `p`. -/
def oNeedAt (need : List ℕ → Light.Need) (n U s p : ℕ) : Need :=
  ⟨oWord n U s p + (oSupNeed need n (s * p) (oCap n p)).word,
    oLayout n U s p + (oSupNeed need n (s * p) (oCap n p)).cells + 1,
    4 + (oSupNeed need n (s * p) (oCap n p)).depth⟩

/-- **The need of the oracle** as a function of the parameters `[n, U, s, p]`. -/
def oracleNeed (need : List ℕ → Light.Need) (ps : List ℕ) : Need :=
  oNeedAt need (ps.getD 0 0) (ps.getD 1 0) (ps.getD 2 0) (ps.getD 3 0)

/-! ## The limits -/

section limits

variable {need : List ℕ → Need} {x : OracleInst} {μ : ℕ → ℤ} {fr : ℕ}

end limits

/-! ## The oracle -/

/-- The context of the oracle: the core and the two small procedures. -/
structure OracleCtx (P₀ R : Program) (ν : ONums) (Tn : List ℕ → ℕ) (need : List ℕ → Light.Need) :
    Prop where
  core : OCoreCtx P₀ R ν Tn need
  hCore : (P₀ ++ R)[ν.pCore]? = some (oCoreBody ν)
  hCeil : (P₀ ++ R)[ν.pCeil]? = some ceilDivBody
  hBitLen : (P₀ ++ R)[ν.pBitLen]? = some bitLenBody

/-! ## The program -/

/-- The numbers of the procedures of the oracle, if its list starts at the number `o`; `pS` is the
solver. -/
def oNumsAt (pS o : ℕ) : ONums where
  pS := pS
  pCeil := o
  pBitLen := o + 1
  pDbl := o + 2
  pResid := o + 3
  pResidues := o + 4
  pClasses := o + 5
  pChunks := o + 6
  pWriteX := o + 7
  pWriteY := o + 8
  pScat := o + 9
  pLoop := o + 10
  pCore := o + 11

/-- **The procedures of the oracle**: procedure number `i` of this list gets the number `o + i`;
the oracle itself is number `o + 12`. -/
def oracleProcs (pS o : ℕ) : Program :=
  let ν := oNumsAt pS o
  [ceilDivBody,                                             -- 0
    bitLenBody,                                             -- 1
    dblTableBody,                                           -- 2
    residBody,                                              -- 3
    residuesBody ν.pResid,                                  -- 4
    classesBody,                                            -- 5
    chunksBody,                                             -- 6
    writeXBody,                                             -- 7
    writeYBody,                                             -- 8
    oScatterBody,                                           -- 9
    oLoopBody ν.pS ν.pWriteX ν.pWriteY ν.pScat,             -- 10
    oCoreBody ν,                                            -- 11
    oracleBody ν.pCeil ν.pBitLen ν.pCore]                   -- 12

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.OracleNeedPoly
/-!
# The counting oracle (Lemma 4.1): the need stays polynomial, and the host

If the need of the solver of #Lop-AE-SparseTri is polynomially bounded in its parameters
`[N, D, w]`, then the need of the oracle is polynomially bounded in `[n, U, s, p]`
(`oracleNeed_poly`): every part of it is at most `2^S Q^K` with `Q = (n + 1)(U + 1)(s + 1)(p + 1)`.

`oracle_host` puts the two together: from an arbitrary solver of #Lop-AE-SparseTri, a solver of the
counting oracle with the time `oracleTime` and the need `oracleNeed`.
-/

@[expose] public section

namespace Light.Filter

open ThreeSumApsp ThreeSumApsp.Spec Light.Sec3

/-- The product of the four parameters, each plus one. -/
def oQ (ps : List ℕ) : ℕ :=
  (ps.getD 0 0 + 1) * (ps.getD 1 0 + 1) * (ps.getD 2 0 + 1) * (ps.getD 3 0 + 1)

section bounds

variable {n U s p : ℕ}

/-- `Q` for `[n, U, s, p]`. -/
abbrev Q4 (n U s p : ℕ) : ℕ := (n + 1) * (U + 1) * (s + 1) * (p + 1)

end bounds

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.Asymp
/-!
# Asymptotics of the filtering parameters

With `k = Nat.size n`, `ℓ = ⌊√k⌋ + 1`, `m = ⌊√ℓ⌋` (so `b = ℓ (m + 1)`), every parameter is a power
of two whose exponent is a polynomial in `m`, `ℓ`, `k`, and `m → ∞` with `n`.

* `rpow_le_two_mul_sOf`, `sOf_le_two_mul_rpow`: `n^σ / 2 ≤ s ≤ 2 n^σ`, `σ = 0.0284225`.
* `RR_le_rpow`, `QOf_le_rpow`, `calls_le_rpow`, `PmaxOf_le`: `R, Q, rounds · (r (Q + 1) + 2)` are
  `n^{o(1)}`, and `Pmax ≤ s n^{o(1)}`.
* `regime`: eventually `2 ≤ s p` and `(s p)^1249 ≤ n^71` for all `1 ≤ p ≤ Pmax`.
* `guard_eventually`: eventually `Guard n U` for all `U ≤ c n^κ`.
-/

@[expose] public section

open Filter

namespace Light.Filter

/-! ## Basic facts -/

/-- `m = ⌊√ℓ⌋`. -/
def mmOf (n : ℕ) : ℕ := Nat.sqrt (ellOf n)

/-- The exponent of `s`: `s = 2^{jOf n}`. -/
def jOf (n : ℕ) : ℕ := 284225 * kOf n / 10 ^ 7

/-! ## Polynomial inequalities, eventually -/

/-! ## The parameters are `n^{o(1)}` -/

/-! ## The regime of the thin product -/

/-! ## The block size and the number of blocks -/

/-! ## The guard -/

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.OracleBound
/-!
# An eventual bound on the time of one oracle call

`oracle_bound`: if the solver of #Lop-AE-SparseTri runs in time
`C (n² log² D / D^{0.0703531} + w D^{0.4296471} log D + n D + w + 1)` in the thin regime, then
eventually, for `U ≤ c n^κ` and `1 ≤ p ≤ Pmax`, one call of the oracle at `s = sOf n` takes at most
`n^{2.9960008}`.

The proof passes to logarithms: with `ν = log n`, `x = log s`, `y = log p`, `μ = log ⌈n/s⌉`, every
part of the time is a constant times `exp` of a linear form in these, and the constraints
`μ + x ≤ log 2 + ν`, `y ≤ x + η ν`, `σ ν ≤ log 2 + x ≤ 2 log 2 + σ ν` bound it by
`exp(4 log 2 + 2.996000795 ν)` (`core_bound`).
-/

@[expose] public section

open Filter

namespace Light.Filter

/-- The constant of `core_bound`. -/
noncomputable def Kc (C' A κ' : ℝ) : ℝ :=
  (2 * (300 + 2 * C') + 4 * (26 + C') + 2 * C' * 10 ^ 18 + 4 * C' * 10 ^ 9
    + 1200 * (1 + A / Real.log 2 + κ' * 10 ^ 9 / Real.log 2)) * Real.exp (4 * Real.log 2)
end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.Mass
/-!
# The arithmetic of the filtering (Lemma 3.1)

For an active set `A` (a predicate on candidates `i < L`, `L = m n²`) and a modulus `M`, the mass of
the group `g` is `mass A M g = Σ_{i < L, A i, i % n² = g} cnt_M(i)`.  The count at modulus `0` is the
number of exact witnesses (`(0 : ℤ) ∣ v ↔ v = 0`).

* `sum_pool_cntOf_le` (3.2): summed over the pool, the counts at `M q` are at most `Q` times the
  exact witnesses plus `h` times the count at `M`.
* `exists_witness_of_certified` (3.3): a certified group has an exact witness.
* `contract` : with one prime `q*` minimizing the remaining mass, the remaining mass shrinks by
  `2h/Q`.
* `cntOf_pos_of_zero_pos`: an exact witness is counted at every modulus.
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec

variable {n s U : ℕ} {AB BC AC : List ℤ}

/-- The mass of the group `g` over the active candidates `A` at the modulus `M`. -/
def mass (n s : ℕ) (AB BC AC : List ℤ) (A : ℕ → Bool) (M g : ℕ) : ℕ :=
  ∑ i ∈ (Finset.range ((n + s - 1) / s * (n * n))).filter (fun i => A i = true ∧ i % (n * n) = g),
    cntOf n s M AB BC AC i

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.HostMath
/-!
# The filtering host: the pure arithmetic

* `Arr`: an array of the memory, given by a function.
* `poolL`: the pool as a list (the primes of `[R, 2R)` in ascending order); it is never empty
  (Bertrand's postulate).
* The mass of a group as a sum over the blocks (`mass_eq_sum`); the total mass `tot` and the number
  `cardA` of active candidates.
* The step of a round (`step_contract`), the end of a round (`card_filter_le_tot`), and the count
  of the candidates (`card_lt_two_pow`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec

/-! ## Arrays -/

/-- The `L` cells from `a` hold `f 0, …, f (L - 1)`. -/
def Arr (μ : ℕ → ℤ) (a L : ℕ) (f : ℕ → ℤ) : Prop := ∀ i < L, μ (a + i) = f i

/-- A truth value as a number. -/
def bitB (b : Bool) : ℤ := if b then 1 else 0

@[simp] theorem bitB_true : bitB true = 1 := rfl
@[simp] theorem bitB_false : bitB false = 0 := rfl

/-! ## Parameters -/

/-! ## The pool as a list -/

/-- The pool: the primes of `[R, 2R)` in ascending order. -/
def poolL (n : ℕ) : List ℕ := (Sieve.primesBelow (2 * RR n)).filter fun q => decide (RR n ≤ q)

/-- The pool, read with a default. -/
def poolAt (n t : ℕ) : ℕ := (poolL n).getD t 0

/-! ## Masses as sums over the blocks -/

variable {n s U : ℕ} {AB BC AC : List ℤ}

/-- The total mass of the active candidates. -/
def tot (n s : ℕ) (AB BC AC : List ℤ) (A : ℕ → Bool) (M : ℕ) : ℕ :=
  ∑ g ∈ Finset.range (n * n), mass n s AB BC AC A M g

/-- The number of active candidates. -/
def cardA (n s : ℕ) (A : ℕ → Bool) : ℕ :=
  ∑ g ∈ Finset.range (n * n), ∑ j ∈ Finset.range ((n + s - 1) / s),
    if A (j * (n * n) + g) then 1 else 0

/-- The candidates of the groups that are not done, among those that are marked active. -/
def eff (N : ℕ) (act D : ℕ → Bool) : ℕ → Bool := fun i => act i && !D (i % N)

/-! ## Witnesses -/

/-! ## The step of a round -/

/-- The certificate of the group `g`, from the counts `act` at the moduli `M` and `M q`. -/
def certOf (n s U : ℕ) (AB BC AC : List ℤ) (act : ℕ → Bool) (M g : ℕ) : Prop :=
  ∀ t < QOf n, hOf n U * mass n s AB BC AC act M g < QOf n * mass n s AB BC AC act (M * poolAt n t) g

/-! ## Rounds -/

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.HostProcs
/-!
# The filtering host: small procedures

* `div(a, b) = ⌊a/b⌋` and `pow2(e) = 2^e`, by counting up.
* `aggr(cnt, act, dst, N, m)`: `dst[g] := Σ_{j<m} act[j N + g] · cnt[j N + g]` for `g < N`.
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

variable {lim : Limits} {P : Program} {d : ℕ}

/-! ## Helpers for expressions -/

/-! ## Division and powers of two, by counting up -/

/-- div(a, b).  Locals: 0 a, 1 b, 2 the candidate q, 3 the multiple (q + 1) b. -/
def divBody : Stmt :=
  .set 2 (Light.k 0) ;;
  .set 3 (Light.v 1) ;;
  .while (Light.v 3 ≤' Light.v 0) (
    .set 3 (Light.v 3 +' Light.v 1) ;;
    .set 2 (Light.v 2 +' Light.k 1)) ;;
  .set 0 (Light.v 2)

/-- The time of div. -/
def tDiv (a b : ℕ) : ℕ := 14 * (a / b) + 12

/-- pow2(e).  Locals: 0 e, 1 the counter i, 2 the power 2^i. -/
def pow2Body : Stmt :=
  .set 1 (Light.k 0) ;;
  .set 2 (Light.k 1) ;;
  .while (Light.v 1 <' Light.v 0) (
    .set 2 (Light.v 2 +' Light.v 2) ;;
    .set 1 (Light.v 1 +' Light.k 1)) ;;
  .set 0 (Light.v 2)

/-- The time of pow2. -/
def tPow2 (e : ℕ) : ℕ := 12 * e + 12

/-! ## Aggregation -/

/-- The inner loop of aggr.  Locals: 0 cnt, 1 act, 2 dst, 3 N, 4 m, 5 g, 6 acc, 7 j. -/
def aggrInner : Stmt :=
  Stmt.for 7 (Light.v 4) (.set 6 (Light.v 6 +' M (Light.v 1 +' Light.v 7 *' Light.v 3 +' Light.v 5) *' M (Light.v 0 +' Light.v 7 *' Light.v 3 +' Light.v 5)))

/-- aggr(cnt, act, dst, N, m): `dst[g] := Σ_{j<m} act[j N + g] · cnt[j N + g]` for `g < N`. -/
def aggrBody : Stmt :=
  Stmt.for 5 (Light.v 3) (.set 6 (Light.k 0) ;; aggrInner ;; .store (Light.v 2 +' Light.v 5) (Light.v 6)) ;;
  .set 0 (Light.k 0)

/-- The sum over the first `j` blocks of the counts of the active candidates of the group `g`. -/
def aggrSum (N g : ℕ) (A : ℕ → Bool) (c : ℕ → ℕ) (j : ℕ) : ℕ :=
  ∑ j' ∈ Finset.range j, if A (j' * N + g) then c (j' * N + g) else 0

/-- The time of aggr. -/
def tAggr (N m : ℕ) : ℕ := N * (30 * m + 30) + 10

/-! ## Certification -/

/-- The inner loop of cert: the test of the group `g` against every prime of the pool.
Locals: 0 ua, 1 gt, 2 done, 3 N, 4 Q, 5 h, 6 g, 7 flag, 8 t. -/
def certInner : Stmt :=
  Stmt.for 8 (Light.v 4) (.ite (Light.v 4 *' M (Light.v 1 +' Light.v 8 *' Light.v 3 +' Light.v 6) <' Light.v 5 *' M (Light.v 0 +' Light.v 6) +' Light.k 1)
    (.set 7 (Light.k 0)) .skip)

/-- cert(ua, gt, done, N, Q, h): every group `g < N` that is not done is certified, `done[g] := 1`,
if `h · ua[g] < Q · gt[t N + g]` for every `t < Q`. -/
def certBody : Stmt :=
  Stmt.for 6 (Light.v 3) (.ite (M (Light.v 2 +' Light.v 6) =' Light.k 0)
    (.set 7 (Light.k 1) ;; certInner ;; .store (Light.v 2 +' Light.v 6) (Light.v 7)) .skip) ;;
  .set 0 (Light.k 0)

/-- The time of cert. -/
def tCert (N Q : ℕ) : ℕ := N * (30 * Q + 30) + 10

/-! ## The choice of the prime -/

/-- The inner loop of argmin: the remaining mass of the row `t`.
Locals: 0 gt, 1 done, 2 N, 3 Q, 4 t, 5 S, 6 g, 7 best, 8 arg. -/
def argInner : Stmt :=
  Stmt.for 6 (Light.v 2) (.set 5 (Light.v 5 +' (Light.k 1 -' M (Light.v 1 +' Light.v 6)) *' M (Light.v 0 +' Light.v 4 *' Light.v 2 +' Light.v 6)))

/-- argmin(gt, done, N, Q): the first row `t < Q` of least remaining mass
`Σ_{g < N} (1 - done[g]) gt[t N + g]`. -/
def argminBody : Stmt :=
  Stmt.for 4 (Light.v 3) (.set 5 (Light.k 0) ;; argInner ;;
    .ite (Light.v 4 =' Light.k 0) (.set 7 (Light.v 5) ;; .set 8 (Light.v 4))
      (.ite (Light.v 5 <' Light.v 7) (.set 7 (Light.v 5) ;; .set 8 (Light.v 4)) .skip)) ;;
  .set 0 (Light.v 8)

/-- The time of argmin. -/
def tArgmin (N Q : ℕ) : ℕ := Q * (30 * N + 30) + 10

/-- The remaining mass of the first `g` groups in the row `t`. -/
def remSum (D : ℕ → Bool) (Gv : ℕ → ℕ → ℕ) (t g : ℕ) : ℕ :=
  ∑ g' ∈ Finset.range g, if D g' then 0 else Gv t g'

/-! ## The end of a round -/

/-- filterAct(act, cnt, L): `act[i] := 0` where `cnt[i] = 0`.  Locals: 0 act, 1 cnt, 2 L, 3 i. -/
def filterActBody : Stmt :=
  Stmt.for 3 (Light.v 2) (.ite (M (Light.v 1 +' Light.v 3) =' Light.k 0) (.store (Light.v 0 +' Light.v 3) (Light.k 0)) .skip) ;;
  .set 0 (Light.k 0)

/-- The time of filterAct. -/
def tFilterAct (L : ℕ) : ℕ := 20 * L + 10

/-! ## The pool -/

/-- poolFilter(src, c, R, dst): the entries `≥ R` of the `c` cells from `src` are written, in their
order, to the cells from `dst`; it returns their number.
Locals: 0 src, 1 c, 2 R, 3 dst, 4 i, 5 the number so far. -/
def poolFilterBody : Stmt :=
  Stmt.for 4 (Light.v 1) (.ite (Light.v 2 ≤' M (Light.v 0 +' Light.v 4))
    (.store (Light.v 3 +' Light.v 5) (M (Light.v 0 +' Light.v 4)) ;; .set 5 (Light.v 5 +' Light.k 1)) .skip) ;;
  .set 0 (Light.v 5)

/-- The time of poolFilter. -/
def tPoolFilter (c : ℕ) : ℕ := 30 * c + 10

end Light.Filter
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 definitions for the 2.996001 bound). Mathematics: 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), Lemmas 3.1, 4.1 and 5.1.
View graph
APSP in O(n2.996001)O(n^{2.996001})O(n2.996001): definitions, part 1 of 2

APSP in $O(n^{2.996001})$ : definitions, part 1 of 2
