feat(ExactTriangle): run the box-backed fixed-prime controller

Complexity.lean

@@ -124,6 +124,19 @@ public import Complexity.Algorithms.WordRAM.Dijkstra.LogLinear
 public import Complexity.Algorithms.WordRAM.Dijkstra.Statement
 public import Complexity.Algorithms.WordRAM.ElementDistinctness
 public import Complexity.Algorithms.WordRAM.ElementDistinctnessRAM
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Accounting
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Entry
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Flat
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Loop
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Record
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.SourceBounds
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Step
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.TimeBound
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness.Exec
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness.Width
 public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime
 public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Adapt
 public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Admission

Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.SourceBounds
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.TimeBound
+
+/-!
+# Complete box-backed native Exact Triangle decision at a fixed prime
+
+`BoxFixedPrime.runs_input` executes the actual producer once and traverses its occupied
+records with `RecordBoxProduct`, followed by the existing original-weight verifier. The
+same-state prefix and halt return one exactly for `HasZeroTriangle`, and retain original
+witness coordinates. Calls reuse dirty workspace and preserve the producer catalogue.
+
+For `m = 9k`, `BoxFixedPrime.timeBound_le` bounds aggregate product charges by
+`125829120 (189k+1)^2 (9k+1) D^(-8/125) n^3 g`, with the actual producer, roots, queries,
+controller and one global `F(p)+1` original-weight scan reserve stated separately. Correctness
+also holds for general `m`, using the executable threshold `m/9`.
+
+The concrete program uses 416 registers, at most 133152 flat slots including halt, and never
+reads physical width. It shares `FixedPrime.admissionWidth` and `FixedPrime.wordBound`:
+logarithmic admission and polynomial prefix words/support follow from original scalar bounds
+and polynomial original weight magnitude. No solver, intermediate execution, clean workspace
+or sparse occurrence certificate is supplied as an input hypothesis.
+
+Parameters and the prime are still explicit admitted inputs (`D >= 16`, `n >= D^18`, `g >= 1`
+and the stated prime window). Connecting this program to global parameter/prime selection,
+absorbing polynomial factors and proving ordinary 3SUM exponent 1.9992 remain open.
+-/

Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Accounting.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Anthropic, PBC, Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anthropic, PBC, Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Accounting
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Program
+
+/-!
+# Box-backed charges for actual catalogue records
+
+Each block is decoded from the real protected producer memory, in its original rank order.
+The mathematical products are those computed by the concrete native product; their answer
+correctness is proved, not assumed. Failed occurrences in distinct records therefore share
+one global false-positive budget. These value lemmas supply the native loop invariant.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
+
+open FixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Real per-record product, root, query and controller charges, excluding interval scans.
+The constant includes the outer loop's two control instructions. -/
+@[expose] noncomputable def recordBase {m n p : ℕ} (hn : 0 < n)
+    (values : ℕ → ℤ) (mem : ℕ → ℕ) (idx : InstanceIndex p) : ℕ :=
+  let Q := RecordProduct.recordQueryCount n (D m) p values idx
+  let qs := RecordProduct.decodedQueries hn mem (RecordProduct.recordQueries n (D m) p idx) Q
+  RecordBoxProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q + 61
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime

Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Entry.lean

@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Loop
+
+/-!
+# Initialized box-backed fixed-prime ExactTriangle computation
+
+The original input alone supplies scalar headers and canonical signed weights. The producer
+runs once, its actual heap and occupied records feed the complete native traversal, and the
+returned flag decides original ExactTriangle across every record. All fits follow from the
+original numerical admission; no intermediate producer, layout or solver result is an input.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
+
+open FixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+/-- One real preparation followed by the entire actual fixed-prime traversal. Its structured
+bound excludes the final halt, and retains the preparation charge separately from record work.
+The physical width may be any larger admitted width. -/
+theorem exec_input {w m n g p A : ℕ} (values : List ℤ)
+    (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m)
+    (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n)
+    (hv : ∀ z ∈ values, z.natAbs ≤ A)
+    (hW : admissionWidth n (D m) g p A ≤ w + 2) :
+    let V := fun q => values.getD q 0
+    let wAB := fun u v : Fin n => V (pairIndex (u, v))
+    let wBC := fun b c : Fin n => V (n * n + pairIndex (b, c))
+    let wAC := fun u c : Fin n => V (2 * (n * n) + pairIndex (u, c))
+    let hn : 0 < n := lt_of_lt_of_le (by omega : 0 < D m)
+      ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN)
+    InputFits (w + 2) (PreparationInput.input n (D m) g p values) ∧
+    ∃ a : Data 64,
+      ExecWithin (w + 2) Instances.program
+        (.init (PreparationInput.input n (D m) g p values)) a
+        (RecordProduct.preparationTime n (D m) g p values - 1) ∧
+      Instances.Output n (D m) g p V
+        (.init (PreparationInput.input n (D m) g p values)) a ∧
+      ∃ y, ExecWithin (w + 2) program
+          (.init (PreparationInput.input n (D m) g p values)) y
+          (RecordProduct.preparationTime n (D m) g p values +
+            (∑ idx ∈ instanceIndices wAB (D m) g p, recordBase (m := m) hn V a.mem idx) +
+            (42 * pieceSize (D m) g + 28) * (falsePositiveCount wAB wBC wAC p + 1) + 6) ∧
+        y.Bounded (w + 2) ∧
+        (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+        y.regs Reg.scans ≤ falsePositiveCount wAB wBC wAC p + y.regs Reg.found ∧
+        (y.regs Reg.found = 1 ↔ HasZeroTriangle wAB wBC wAC) ∧
+        (y.regs Reg.found = 1 →
+          y.regs (recordBank RecordWitness.Reg.witnessA) < n ∧
+          y.regs (recordBank RecordWitness.Reg.witnessB) < n ∧
+          y.regs (recordBank RecordWitness.Reg.witnessC) < n ∧
+          V (y.regs (recordBank RecordWitness.Reg.witnessA) * n +
+              y.regs (recordBank RecordWitness.Reg.witnessB)) +
+            V (n * n + (y.regs (recordBank RecordWitness.Reg.witnessB) * n +
+              y.regs (recordBank RecordWitness.Reg.witnessC))) +
+            V (2 * (n * n) + (y.regs (recordBank RecordWitness.Reg.witnessA) * n +
+              y.regs (recordBank RecordWitness.Reg.witnessC))) = 0) ∧
+        (∀ u, u < a.regs Instances.heap ∨
+          a.regs Instances.heap + CallableProduct.windowSize n (n * n) ≤ u → y.mem u = a.mem u) ∧
+        ∀ j : Fin 64, y.regs
+          (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j := by
+  let V := fun q => values.getD q 0
+  have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN
+  have hp0 := (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.pos
+  have hw : PreparationInput.width n (D m) g p A ≤ w + 2 := by
+    have hr := record_admitted hW
+    unfold RecordWitness.admissionWidth RecordProduct.admissionWidth at hr
+    omega
+  obtain ⟨a, ha, hout, hinput, -⟩ := PreparationInput.exec_input values hlen
+    (by omega) hDn hg hp0 hv hw
+  have ha' : ExecWithin (w + 2) Instances.program
+      (.init (PreparationInput.input n (D m) g p values)) a
+      (RecordProduct.preparationTime n (D m) g p values - 1) := ha
+  have hf : Function.Injective RecordProduct.producerBank := by
+    intro i j h
+    exact Fin.ext (congrArg (fun k : Fin 320 => k.val) h)
+  have hf' : Function.Injective RecordWitness.productBank := by
+    intro i j h
+    exact Fin.ext (congrArg (fun k : Fin 400 => k.val) h)
+  have hf'' : Function.Injective recordBank := by
+    intro i j h
+    exact Fin.ext (congrArg (fun k : Fin 416 => k.val) h)
+  let x₀ : Data 320 := .init (PreparationInput.input n (D m) g p values)
+  let b := a.extend RecordProduct.producerBank x₀
+  have hb : ExecWithin (w + 2) RecordProduct.produce x₀ b
+      (RecordProduct.preparationTime n (D m) g p values - 1) := ha'.rename hf
+  let b₀ : Data 400 := .init (PreparationInput.input n (D m) g p values)
+  let c := b.extend RecordWitness.productBank b₀
+  have hc : ExecWithin (w + 2) RecordWitness.produce b₀ c
+      (RecordProduct.preparationTime n (D m) g p values - 1) := hb.rename hf'
+  let c₀ : Data 416 := .init (PreparationInput.input n (D m) g p values)
+  let x := c.extend recordBank c₀
+  have hx : ExecWithin (w + 2) produce c₀ x
+      (RecordProduct.preparationTime n (D m) g p values - 1) := hc.rename hf''
+  have bank (j : Fin 64) : x.regs
+      (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j :=
+    (hf''.extend_apply _ _ _).trans ((hf'.extend_apply _ _ _).trans (hf.extend_apply _ _ _))
+  have mem : x.mem = a.mem := rfl
+  have heap : a.regs Instances.heap ≤ PreparationInput.wordBound n (D m) g p A := by
+    obtain ⟨t, ht, he⟩ := ha'
+    have hr : Runs (w + 2) PreparationInput.flatProgram
+        (State.init (PreparationInput.input n (D m) g p values)) ⟨Instances.program.size, a⟩ t := by
+      simpa only [Nat.zero_add, State.init] using he.runs (pc := 0)
+        (p := PreparationInput.flatProgram) (Program.Contains.self _).append_left
+    exact ((PreparationInput.bounded_reachable values hlen (by omega) hDn hg hp0 hv hw
+      ⟨Instances.program.size, a⟩ t hr).1 Instances.heap).le
+  obtain ⟨y, hy, yf, ys, yiff, yw, frame, regs⟩ :=
+    exec_traverse values hlen hD hg hp hN hv hW a x hout bank (fun _ _ => rfl) heap
+  have hpos : 1 ≤ RecordProduct.preparationTime n (D m) g p values := by
+    dsimp only [RecordProduct.preparationTime, Instances.timeBound]
+    omega
+  have hex : ExecWithin (w + 2) program
+      (.init (PreparationInput.input n (D m) g p values)) y
+      (RecordProduct.preparationTime n (D m) g p values +
+        (∑ idx ∈ instanceIndices (fun u v : Fin n => V (pairIndex (u, v))) (D m) g p,
+          recordBase (m := m) (lt_of_lt_of_le (by omega : 0 < D m) hDn) V a.mem idx) +
+        (42 * pieceSize (D m) g + 28) *
+          (falsePositiveCount (fun u v : Fin n => V (pairIndex (u, v)))
+            (fun b c => V (n * n + pairIndex (b, c)))
+            (fun u c => V (2 * (n * n) + pairIndex (u, c))) p + 1) + 6) :=
+    (hx.seq hy).mono (by dsimp only [V]; omega)
+  refine ⟨hinput, a, ha', hout, y, hex, hex.bounded (Data.Bounded.init hinput),
+    yf, ys, yiff, yw, ?_, regs⟩
+  simpa only [mem] using frame
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime

Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Flat.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime.Entry
+
+/-!
+# Initialized box-backed halting fixed-prime ExactTriangle decision
+
+The actual fixed 416-register standard-native program decides the original signed input at
+every admitted physical width. Its prefix witness and halt share the same state, which retains
+the original-coordinate witness on success and a single global failure-scan bound. Global
+parameter/prime selection and the final source exponent are not supplied by this component.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
+
+open FixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+/-- Actual one-time preparation, all occupied record charges, one global failed-scan budget,
+and all controller/loop/halt work. No whole-window initialization is charged or performed. -/
+@[expose] noncomputable def timeBound {m n : ℕ} (hn : 0 < n) (g p : ℕ)
+    (values : List ℤ) (mem : ℕ → ℕ) : ℕ :=
+  let V := fun q => values.getD q 0
+  let wAB := fun u v : Fin n => V (pairIndex (u, v))
+  let wBC := fun b c : Fin n => V (n * n + pairIndex (b, c))
+  let wAC := fun u c : Fin n => V (2 * (n * n) + pairIndex (u, c))
+  RecordProduct.preparationTime n (D m) g p values +
+    (∑ idx ∈ instanceIndices wAB (D m) g p, recordBase (m := m) hn V mem idx) +
+    (42 * pieceSize (D m) g + 28) * (falsePositiveCount wAB wBC wAC p + 1) + 7
+
+/-- Same-state prefix and charged halt, with exact original positive and negative ET decisions.
+All geometric, prime, original-input and every-wide-width premises are explicit. -/
+theorem runs_input {W m n g p A : ℕ} (values : List ℤ)
+    (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m)
+    (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n)
+    (hv : ∀ z ∈ values, z.natAbs ≤ A) (hW : admissionWidth n (D m) g p A ≤ W) :
+    let V := fun q => values.getD q 0
+    let wAB := fun u v : Fin n => V (pairIndex (u, v))
+    let wBC := fun b c : Fin n => V (n * n + pairIndex (b, c))
+    let wAC := fun u c : Fin n => V (2 * (n * n) + pairIndex (u, c))
+    let hn : 0 < n := lt_of_lt_of_le (by omega : 0 < D m)
+      ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN)
+    InputFits W (PreparationInput.input n (D m) g p values) ∧
+    ∃ a : Data 64,
+      ExecWithin W Instances.program (.init (PreparationInput.input n (D m) g p values)) a
+        (RecordProduct.preparationTime n (D m) g p values - 1) ∧
+      Instances.Output n (D m) g p V (.init (PreparationInput.input n (D m) g p values)) a ∧
+      ∃ y t, t + 1 ≤ timeBound (m := m) hn g p values a.mem ∧
+        Runs W (program.program Reg.found)
+          (State.init (PreparationInput.input n (D m) g p values)) ⟨program.size, y⟩ t ∧
+        Executes W (program.program Reg.found)
+          (State.init (PreparationInput.input n (D m) g p values)) (y.regs Reg.found) (t + 1) ∧
+        y.Bounded W ∧ (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+        y.regs Reg.scans ≤ falsePositiveCount wAB wBC wAC p + y.regs Reg.found ∧
+        (y.regs Reg.found = 1 ↔ HasZeroTriangle wAB wBC wAC) ∧
+        (y.regs Reg.found = 1 → ∃ u v c : Fin n,
+          y.regs (recordBank RecordWitness.Reg.witnessA) = u.val ∧
+          y.regs (recordBank RecordWitness.Reg.witnessB) = v.val ∧
+          y.regs (recordBank RecordWitness.Reg.witnessC) = c.val ∧
+          weightSum wAB wBC wAC u v c = 0) ∧
+        (∀ u, u < a.regs Instances.heap ∨
+          a.regs Instances.heap + CallableProduct.windowSize n (n * n) ≤ u → y.mem u = a.mem u) ∧
+        ∀ j : Fin 64, y.regs
+          (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j := by
+  have htwo : 2 ≤ W := by
+    have hr := record_admitted hW
+    unfold RecordWitness.admissionWidth at hr
+    omega
+  have heq : W - 2 + 2 = W := Nat.sub_add_cancel htwo
+  have h := exec_input (w := W - 2) values hlen hD hg hp hN hv
+    (by simpa only [heq] using hW)
+  rw [heq] at h
+  obtain ⟨hi, a, ha, hout, y, he, yb, yf, ys, yiff, yw, frame, regs⟩ := h
+  obtain ⟨t, ht, hex⟩ := he
+  refine ⟨hi, a, ha, hout, y, t, ?_, ?_, ?_, yb, yf, ys, yiff, ?_, frame, regs⟩
+  · simpa only [timeBound, Nat.add_assoc] using Nat.add_le_add_right ht 1
+  · simpa only [Nat.zero_add, State.init] using hex.runs (pc := 0)
+      (p := program.program Reg.found) (Program.Contains.self _).append_left
+  · simpa only [State.init] using hex.executes Reg.found
+  · intro hf
+    obtain ⟨ha, hb, hc, hz⟩ := yw hf
+    exact ⟨⟨_, ha⟩, ⟨_, hb⟩, ⟨_, hc⟩, rfl, rfl, rfl, hz⟩
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime