diff --git a/Complexity.lean b/Complexity.lean
index ec7df05b6..18c01bdbd 100644
--- a/Complexity.lean
+++ b/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
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime.lean
new file mode 100644
index 000000000..9c7890f9e
--- /dev/null
+++ b/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.
+-/
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Accounting.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Accounting.lean
new file mode 100644
index 000000000..579fac87c
--- /dev/null
+++ b/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
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Entry.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Entry.lean
new file mode 100644
index 000000000..e69f7e361
--- /dev/null
+++ b/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
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Flat.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Flat.lean
new file mode 100644
index 000000000..d7ce96683
--- /dev/null
+++ b/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
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Loop.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Loop.lean
new file mode 100644
index 000000000..52db6a815
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Loop.lean
@@ -0,0 +1,273 @@
+/-
+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.Step
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Potential
+
+/-!
+# Complete traversal of the actual prepared catalogue
+
+Every guarded iteration delivers the next occupied ordinal to the concrete record program.
+The invariant counts only the visited prefix: distinct failures share one global budget and
+the actual successful-return flags sum to at most one. Scratch is reused above the producer
+heap; protected readback and the genuine original producer execution are kept separate.
+-/
+
+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
+
+attribute [local instance] Classical.propDecidable
+
+private structure Invariant {m n g p : ℕ} (V : ℕ → ℤ) (a : Data 64)
+    (start : Data 416) (order : ℕ → InstanceIndex p) (hn : 0 < n) (x : Data 416) : Prop where
+  bank : ∀ j : Fin 64, x.regs
+    (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j
+  protected_mem : Set.EqOn x.mem a.mem (Set.Iio (a.regs Instances.heap))
+  frame : ∀ u, u < a.regs Instances.heap ∨
+    a.regs Instances.heap + CallableProduct.windowSize n (n * n) ≤ u → x.mem u = start.mem u
+  index_le : x.regs Reg.index ≤ a.regs Instances.produced
+  one : x.regs Reg.one = 1
+  flag : x.regs Reg.found = 0 ∨ x.regs Reg.found = 1
+  limit : x.regs Reg.limit =
+    (if x.regs Reg.found = 1 then x.regs Reg.index else a.regs Instances.produced)
+  scans_failed : x.regs Reg.scans ≤
+    (∑ j ∈ Finset.range (x.regs Reg.index),
+      recordFailures (m := m) (g := g) hn V a.mem (order j)) + x.regs Reg.found
+  scans_coarse : x.regs Reg.scans ≤ x.regs Reg.index * (n * n + 1)
+  searched : Nat.count (fun j => recordHit (m := m) (n := n) (g := g) V (order j))
+    (x.regs Reg.index) = x.regs Reg.found
+  witness : x.regs Reg.found = 1 →
+    x.regs (recordBank RecordWitness.Reg.witnessA) < n ∧
+    x.regs (recordBank RecordWitness.Reg.witnessB) < n ∧
+    x.regs (recordBank RecordWitness.Reg.witnessC) < n ∧
+    V (x.regs (recordBank RecordWitness.Reg.witnessA) * n +
+        x.regs (recordBank RecordWitness.Reg.witnessB)) +
+      V (n * n + (x.regs (recordBank RecordWitness.Reg.witnessB) * n +
+        x.regs (recordBank RecordWitness.Reg.witnessC))) +
+      V (2 * (n * n) + (x.regs (recordBank RecordWitness.Reg.witnessA) * n +
+        x.regs (recordBank RecordWitness.Reg.witnessC))) = 0
+
+private theorem window_mono {n Q : ℕ} (hQ : Q ≤ n * n) :
+    CallableProduct.windowSize n Q ≤ CallableProduct.windowSize n (n * n) := by
+  unfold CallableProduct.windowSize CallableProduct.sourceWidth
+  exact Nat.pow_le_pow_right (by decide)
+    (Nat.mul_le_mul_left 128 (Nat.clog_mono_right 2 (by omega)))
+
+/-- Run all occupied records, stopping at the first original witness. The original producer
+readback is a caller premise; the initialized theorem constructs it by running the producer
+once. No intermediate layout, answer, scan order or execution contract is an algorithm input. -/
+theorem exec_traverse {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)
+    (a : Data 64) (x : Data 416)
+    (hout : Instances.Output n (D m) g p (fun q => values.getD q 0)
+      (.init (PreparationInput.input n (D m) g p values)) a)
+    (hbank : ∀ j : Fin 64,
+      x.regs (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j)
+    (hmem : Set.EqOn x.mem a.mem (Set.Iio (a.regs Instances.heap)))
+    (hheap : a.regs Instances.heap ≤ PreparationInput.wordBound n (D m) g p A) :
+    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)
+    ∃ y, ExecWithin (w + 2) traverse x y
+        ((∑ 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) + 7) ∧
+      (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 = x.mem u) ∧
+      ∀ j : Fin 64, y.regs
+        (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j := by
+  classical
+  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))
+  have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN
+  have hn : 0 < n := lt_of_lt_of_le (by omega) hDn
+  have hp0 := (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.ne_zero
+  let M := a.regs Instances.produced
+  let I := instanceIndices wAB (D m) g p
+  obtain ⟨f, -, hf, fsurj⟩ := exists_occupied_order V hout hD hDn hg hp0
+  let order : ℕ → InstanceIndex p := fun i =>
+    if hi : i < M then f ⟨i, hi⟩ else (⟨0, Nat.pos_of_ne_zero hp0⟩, 0, 0)
+  have order_at (i : ℕ) (hi : i < M) : order i = f ⟨i, hi⟩ := dite_eq_left hi
+  have order_mem (i : ℕ) (hi : i < M) : order i ∈ I := by
+    rw [order_at i hi]
+    exact (hf _).1
+  have order_ord (i : ℕ) (hi : i < M) :
+      RecordProduct.recordOrdinal n (D m) g p V (order i) = i := by
+    rw [order_at i hi]
+    exact (hf _).2
+  have order_inj : Set.InjOn order (Finset.range M) := by
+    intro i hi j hj hij
+    exact (order_ord i (Finset.mem_range.mp hi)).symm.trans
+      ((congrArg (RecordProduct.recordOrdinal n (D m) g p V) hij).trans
+        (order_ord j (Finset.mem_range.mp hj)))
+  have image_eq : (Finset.range M).image order = I := by
+    ext idx
+    simp only [Finset.mem_image, Finset.mem_range]
+    constructor
+    · rintro ⟨i, hi, rfl⟩
+      exact order_mem i hi
+    · intro hi
+      obtain ⟨i, hi⟩ := fsurj idx hi
+      exact ⟨i.val, i.isLt, (order_at i.val i.isLt).trans hi⟩
+  have sum_eq (charge : InstanceIndex p → ℕ) :
+      (∑ j ∈ Finset.range M, charge (order j)) = ∑ idx ∈ I, charge idx := by
+    rw [← image_eq, Finset.sum_image order_inj]
+  let B := fun i => recordBase (m := m) hn V a.mem (order i)
+  let F := fun i => recordFailures (m := m) (g := g) hn V a.mem (order i)
+  let C := 42 * pieceSize (D m) g + 28
+  have hF : (∑ j ∈ Finset.range M, F j) ≤ falsePositiveCount wAB wBC wAC p := by
+    rw [show (∑ j ∈ Finset.range M, F j) =
+      ∑ idx ∈ I, recordFailures (m := m) (g := g) hn V a.mem idx from
+        sum_eq (recordFailures (m := m) (g := g) hn V a.mem)]
+    exact sum_recordFailures_le hn V hout hD hDn hg hp I (fun _ hi => hi)
+  let Inv := Invariant (m := m) (g := g) V a x order hn
+  let Φ := fun z : Data 416 => remainingCharge B F C M (z.regs Reg.index) (z.regs Reg.found)
+  have body : ∀ z, Inv z → (Cond.lt Reg.index Reg.limit).Holds z →
+      ∃ y T, ExecWithin (w + 2) step z y T ∧ Inv y ∧ T + 2 + Φ y ≤ Φ z := by
+    intro z hz hc
+    have hguard : z.regs Reg.index < z.regs Reg.limit := hc
+    have before : z.regs Reg.found = 0 := by
+      rcases hz.flag with h | h
+      · exact h
+      · have hlim := hz.limit
+        rw [h, ite_eq_left rfl] at hlim
+        omega
+    have lim : z.regs Reg.limit = M := by
+      simpa only [before, zero_ne_one, ite_false] using hz.limit
+    have hi : z.regs Reg.index < M := by omega
+    obtain ⟨y, S, T, he, hT, yi, yl, yo, ys, yf, hS, hcoarse, yhit, yw, ym, ybank⟩ :=
+      exec_step values hlen hD hg hp hN hv hW a z hout hz.bank hz.protected_mem hheap rfl hi lim
+        hz.one hz.scans_coarse (order (z.regs Reg.index)) (order_mem _ hi) (order_ord _ hi)
+    have newflag : y.regs Reg.found ≤ 1 := by rcases yf with h | h <;> omega
+    have yInv : Inv y := by
+      refine ⟨ybank, ?_, ?_, ?_, yo, yf, ?_, ?_, ?_, ?_, yw⟩
+      · intro u hu
+        exact (ym u (Or.inl hu)).trans (hz.protected_mem hu)
+      · intro u hu
+        have houtside : u < a.regs Instances.heap ∨ a.regs Instances.heap +
+            CallableProduct.windowSize n
+              (RecordProduct.recordQueryCount n (D m) p V (order (z.regs Reg.index))) ≤ u := by
+          rcases hu with h | h
+          · exact Or.inl h
+          · exact Or.inr (le_trans (Nat.add_le_add_left
+              (window_mono (recordQueryCount_le n (D m) p V _)) _) h)
+        exact (ym u houtside).trans (hz.frame u hu)
+      · rw [yi]
+        exact Nat.succ_le_of_lt hi
+      · simpa only [yi] using yl
+      · have hs := hz.scans_failed
+        rw [before, Nat.add_zero] at hs
+        rw [ys, yi, Finset.sum_range_succ]
+        change z.regs Reg.scans + S ≤
+          (∑ j ∈ Finset.range (z.regs Reg.index), F j) + F (z.regs Reg.index) + y.regs Reg.found
+        change S ≤ F (z.regs Reg.index) + y.regs Reg.found at hS
+        change z.regs Reg.scans ≤ ∑ j ∈ Finset.range (z.regs Reg.index), F j at hs
+        omega
+      · rw [ys, yi, Nat.add_mul, Nat.one_mul]
+        exact Nat.add_le_add hz.scans_coarse hcoarse
+      · rw [yi, Nat.count_succ]
+        have searched := hz.searched
+        rw [before] at searched
+        rw [searched, Nat.zero_add]
+        rcases yf with h | h
+        · rw [ite_eq_right (by intro hh; have := yhit.mpr hh; omega), h]
+        · rw [ite_eq_left (yhit.mp h), h]
+    refine ⟨y, T, he, yInv, ?_⟩
+    have paid := remainingCharge_step (base := B) (failures := F) (C := C) hi hT hS newflag
+    simpa only [Φ, yi, before] using paid
+  have h1 : Fits (w + 2) 1 := (counter_fits hW).of_le (by unfold counterEnvelope; omega)
+  obtain ⟨s, hs, sm, si, sl, sf, ss, so, sbank⟩ := exec_setup x h1
+  have sInv : Inv s := by
+    refine ⟨fun j => (sbank _ (by change j.val < 400; omega)).trans (hbank j), ?_, ?_, ?_,
+      so, Or.inl sf, ?_, ?_, ?_, ?_, ?_⟩
+    · intro u hu
+      exact (congrFun sm u).trans (hmem hu)
+    · intro u _
+      exact congrFun sm u
+    · rw [si]
+      exact Nat.zero_le _
+    · rw [sf, ite_eq_right (by decide : ¬(0 : ℕ) = 1), sl, hbank]
+    · simp only [si, ss, sf, Finset.range_zero, Finset.sum_empty, Nat.zero_add, le_refl]
+    · simp only [ss, si, Nat.zero_mul, le_refl]
+    · simp only [si, sf, Nat.count_zero]
+    · intro h
+      omega
+  obtain ⟨y, hy, hIy, hcy⟩ := ExecWithin.loop_potential Inv Φ body sInv
+  have hbudget : 5 + (Φ s + 2) ≤
+      (∑ idx ∈ I, recordBase (m := m) hn V a.mem idx) +
+        C * (falsePositiveCount wAB wBC wAC p + 1) + 7 := by
+    dsimp only [Φ, remainingCharge]
+    rw [si, sf]
+    simp only [Finset.range_zero, Finset.sum_empty, Nat.sub_zero]
+    have hmul := Nat.mul_le_mul_left C (Nat.add_le_add_right hF 1)
+    rw [sum_eq (recordBase (m := m) hn V a.mem)]
+    omega
+  have hex : ExecWithin (w + 2) traverse x y
+      ((∑ idx ∈ I, recordBase (m := m) hn V a.mem idx) +
+        C * (falsePositiveCount wAB wBC wAC p + 1) + 7) := (hs.seq hy).mono hbudget
+  refine ⟨y, hex, hIy.flag, ?_, ?_, hIy.witness, hIy.frame, hIy.bank⟩
+  · exact hIy.scans_failed.trans (Nat.add_le_add_right
+      ((sum_prefix_le F hIy.index_le).trans hF) _)
+  · constructor
+    · intro hf
+      obtain ⟨ha, hb, hc, hw⟩ := hIy.witness hf
+      exact ⟨⟨_, ha⟩, ⟨_, hb⟩, ⟨_, hc⟩, hw⟩
+    · intro hzero
+      by_contra hnot
+      have hf : y.regs Reg.found = 0 := by rcases hIy.flag with h | h <;> omega
+      have hlim : y.regs Reg.limit = M := by
+        simpa only [hf, zero_ne_one, ite_false] using hIy.limit
+      have hi : y.regs Reg.index = M := by
+        change ¬ y.regs Reg.index < y.regs Reg.limit at hcy
+        have := hIy.index_le
+        omega
+      obtain ⟨u, v, c, hw⟩ := hzero
+      have hans := RecordProduct.product_answers_correct V wAB wBC wAC hD hg hp
+        (by intro b c; rfl) (by intro u c; rfl)
+      obtain ⟨rho, k, piece, hacc, hc⟩ := exists_mem_acceptedPairs hD hDn hg hp0 hans hw
+      obtain ⟨hidx, hquery, -⟩ := mem_acceptedPairs.mp hacc
+      obtain ⟨j, hj⟩ := fsurj (rho, k, piece) hidx
+      have hh : recordHit (m := m) (n := n) (g := g) V (order j.val) := by
+        rw [order_at j.val j.isLt, hj]
+        exact ⟨(u, v), hquery, c, hc, hw⟩
+      have hpositive := Nat.count_strict_mono (p := fun j =>
+        recordHit (m := m) (n := n) (g := g) V (order j)) hh j.isLt
+      have searched := hIy.searched
+      rw [hf, hi] at searched
+      rw [searched] at hpositive
+      exact Nat.not_lt_zero _ hpositive
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Program.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Program.lean
new file mode 100644
index 000000000..121b77bb9
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Program.lean
@@ -0,0 +1,72 @@
+/-
+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.Controller
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness.Width
+
+/-!
+# Box-backed native traversal of the occupied ExactTriangle catalogue
+
+The producer runs once. The controller visits actual occupied ordinals and invokes the complete
+400-register box-product/witness code. A success closes the loop immediately; no later
+product or original-weight scan is called. Five disjoint controller registers are used,
+and no catalogue/window snapshot or clearing operation is introduced.
+
+The control adapts the fixed-prime part of `Host.Loop` at
+`anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`. The existing native producer
+uses chunk-major order and prepares all matrices first; the source uses piece-major rounds and
+writes each pair of matrices in its round. The code and native charges here are original.
+These stage definitions are implementation interfaces, not a parameter/prime-selection host.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
+
+open Cslib.WordRAM FixedPrime
+
+/-- Actual product computation, descriptor reading and original signed-weight verification. -/
+@[expose] def record : Code .standard 416 := BoxRecordWitness.program.rename recordBank
+
+/-- One actual occupied record, with all argument/return/controller work in native code. -/
+@[expose] def step : Code .standard 416 := .seq select (.seq record receive)
+
+/-- Traverse the computed catalogue from a genuine prepared state. -/
+@[expose] def traverse : Code .standard 416 :=
+  .seq setup (.loop (.lt Reg.index Reg.limit) step)
+
+/-- Complete original-input fixed-prime solver: one preparation and the actual native loop. -/
+@[expose] def program : Code .standard 416 := .seq produce traverse
+
+/-- The complete structured solver never reads the physical word width. This form is used
+by actual memory-window compilation as well as by the flat initialized client. -/
+theorem program_not_readsWidth : ¬program.ReadsWidth := by
+  simp only [program, produce, traverse, setup, step, select, record, receive,
+    RecordWitness.produce, RecordProduct.produce, BoxRecordWitness.program,
+    Code.ReadsWidth, Code.readsWidth_rename, Op.ReadsWidth, Op.bin, reduceCtorEq,
+    false_or, or_false]
+  exact not_or.mpr ⟨Instances.program_fixed.2,
+    not_or.mpr ⟨RecordBoxProduct.program_fixed.2, RecordWitness.consume_fixed.2⟩⟩
+
+/-- The whole fixed-prime controller is one standard-native program, with a fixed register
+bank and at most 133152 flat slots including halt. It never reads the physical word width. -/
+theorem program_fixed : (program.program Reg.found).length ≤ 133152 ∧
+    ¬(program.program Reg.found).ReadsWidth := by
+  constructor
+  · simp only [Code.program, List.length_append, Code.length_assemble,
+      List.length_singleton, program, produce, traverse, setup, step, select, record,
+      receive, RecordWitness.produce, RecordProduct.produce, BoxRecordWitness.program,
+      Code.size, Code.size_rename]
+    have hp := Instances.program_fixed.1
+    have hr := RecordBoxProduct.program_fixed.1
+    have hc := RecordWitness.consume_fixed.1
+    omega
+  · exact Code.not_readsWidth_program program_not_readsWidth _
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Record.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Record.lean
new file mode 100644
index 000000000..a6ef05055
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Record.lean
@@ -0,0 +1,221 @@
+/-
+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.Accounting
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Controller
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Width
+import Complexity.Computability.WordRAM.RegisterFrame
+
+/-!
+# An actual record call after dirty workspace reuse
+
+Protected producer words and registers retain their original meaning even after earlier
+products have used the workspace. The caller reuses the actual full 400-register code and
+derives its finite failure/success semantics from real output words. No producer rerun, clean
+workspace, intermediate solver execution or scan-count certificate is assumed.
+-/
+
+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
+
+private theorem recordBank_injective : Function.Injective recordBank := by
+  intro i j h
+  exact Fin.ext (congrArg (fun k : Fin 416 => k.val) h)
+
+/-- Execute the real product and verifier from protected producer readback. The explicit heap
+bound is supplied by the actual one-time producer's prefix theorem in the initialized client.
+All other record/counter fits follow from original input and the numerical admission. -/
+theorem exec_record {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)
+    (a : Data 64) (x : Data 416)
+    (hout : Instances.Output n (D m) g p (fun q => values.getD q 0)
+      (.init (PreparationInput.input n (D m) g p values)) a)
+    (hbank : ∀ j : Fin 64,
+      x.regs (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j)
+    (hmem : Set.EqOn x.mem a.mem (Set.Iio (a.regs Instances.heap)))
+    (hheap : a.regs Instances.heap ≤ PreparationInput.wordBound n (D m) g p A)
+    (idx : InstanceIndex p)
+    (hidx : idx ∈ instanceIndices
+      (fun u v : Fin n => values.getD (pairIndex (u, v)) 0) (D m) g p)
+    (hi : x.regs (recordBank (RecordWitness.productBank RecordProduct.Reg.ordinal)) =
+      RecordProduct.recordOrdinal n (D m) g p (fun q => values.getD q 0) idx) :
+    let V := fun q => values.getD q 0
+    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)
+    let Q := RecordProduct.recordQueryCount n (D m) p V idx
+    let qs := RecordProduct.decodedQueries hn a.mem (RecordProduct.recordQueries n (D m) p idx) Q
+    ∃ y S, ExecWithin (w + 2) record x y
+        (RecordBoxProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q +
+          (42 * pieceSize (D m) g + 28) * S + 52) ∧
+      y.regs (recordBank RecordWitness.Reg.scans) = S ∧
+      (y.regs (recordBank RecordWitness.Reg.found) = 0 ∨
+        y.regs (recordBank RecordWitness.Reg.found) = 1) ∧
+      S ≤ recordFailures (m := m) (g := g) hn V a.mem idx +
+        y.regs (recordBank RecordWitness.Reg.found) ∧
+      S ≤ n * n + 1 ∧
+      (y.regs (recordBank RecordWitness.Reg.found) = 1 ↔
+        ∃ q ∈ chunkOf (fun u v : Fin n => V (pairIndex (u, v))) (D m) p idx.1 idx.2.1,
+          ∃ c ∈ piece n (D m) g idx.2.2,
+            V (pairIndex (q.1, q.2)) + V (n * n + pairIndex (q.2, c)) +
+              V (2 * (n * n) + pairIndex (q.1, c)) = 0) ∧
+      (y.regs (recordBank RecordWitness.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 Q ≤ u → y.mem u = x.mem u) ∧
+      (∀ j : Fin 64, y.regs
+        (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j) ∧
+      ∀ j : Fin 416, 400 ≤ j.val → y.regs j = x.regs j := by
+  let V := fun q => values.getD q 0
+  let AB := fun u v : ℕ => V (u * n + v)
+  let BC := fun v c : ℕ => V (n * n + (v * n + c))
+  let AC := fun u c : ℕ => V (2 * (n * n) + (u * n + c))
+  let wAB := fun u v : Fin n => V (pairIndex (u, v))
+  let wBC := fun v c : Fin n => V (n * n + pairIndex (v, c))
+  let wAC := fun u c : Fin n => V (2 * (n * n) + pairIndex (u, c))
+  have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN
+  have hn : 0 < n := lt_of_lt_of_le (by omega) hDn
+  have hp0 := (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.ne_zero
+  let z := x.comap recordBank
+  let z₀ := (z.comap RecordWitness.productBank).comap RecordProduct.producerBank
+  have zr : z₀.regs = a.regs := funext hbank
+  have zheap : z.regs (RecordWitness.productBank 42) = a.regs Instances.heap := hbank 42
+  have hcurrent : Instances.Output n (D m) g p V z₀ z₀ :=
+    hout.reframe V zr hmem
+  obtain ⟨hend, -, hspan, -, -, hcoords, hprefix⟩ :=
+    RecordWitness.record_view V _ a hout hD hDn hg hp0 idx hidx
+  have mem_eq (u : ℕ) (hu : u < a.regs Instances.heap) : z.mem u = a.mem u := hmem hu
+  have header (u : ℕ) (hu : u < 5 + 3 * (n * n)) : z₀.mem u =
+      (Data.init (PreparationInput.input n (D m) g p values) : Data 64).mem u :=
+    (mem_eq u (lt_of_lt_of_le hu hend)).trans (hprefix u hu)
+  have original (q : ℕ) (hq : q < 3 * (n * n)) : z.mem (5 + q) = Signed.encode (V q) :=
+    (header (5 + q) (by omega)).trans (PreparationInput.input_word n (D m) g p values q)
+  have hmatrix : ∀ u < n, ∀ v < n,
+      z.mem (5 + (u * n + v)) = Signed.encode (AB u v) ∧
+      z.mem (5 + n * n + (u * n + v)) = Signed.encode (BC u v) ∧
+      z.mem (5 + n * n + n * n + (u * n + v)) = Signed.encode (AC u v) := by
+    intro u hu v hv'
+    have hrow := Nat.mul_le_mul_right n (Nat.succ_le_of_lt hu)
+    rw [Nat.succ_mul] at hrow
+    refine ⟨original _ (by omega), ?_, ?_⟩
+    · simpa only [Nat.add_assoc] using original (n * n + (u * n + v)) (by omega)
+    · have he : 5 + n * n + n * n + (u * n + v) =
+          5 + (2 * (n * n) + (u * n + v)) := by omega
+      rw [he]
+      exact original _ (by omega)
+  have hmag : ∀ u < n, ∀ v < n,
+      (AB u v).natAbs ≤ A ∧ (BC u v).natAbs ≤ A ∧ (AC u v).natAbs ≤ A := by
+    intro u hu v hv'
+    have hrow := Nat.mul_le_mul_right n (Nat.succ_le_of_lt hu)
+    rw [Nat.succ_mul] at hrow
+    exact ⟨RecordWitness.original_magnitude values hlen hv (by omega),
+      RecordWitness.original_magnitude values hlen hv (by omega),
+      RecordWitness.original_magnitude values hlen hv (by omega)⟩
+  let q := RecordProduct.recordQueries n (D m) p idx
+  let Q := RecordProduct.recordQueryCount n (D m) p V idx
+  let qs := RecordProduct.decodedQueries hn a.mem q Q
+  have hQ : Q ≤ n ^ 2 := (recordQueryCount_le n (D m) p V idx).trans_eq (pow_two n).symm
+  have hlenQ : qs.length = Q := RecordProduct.decodedQueries_length hn a.mem q Q
+  have hqs : RecordProduct.decodedQueries hn z.mem q Q = qs :=
+    decodedQueries_eq_of_eqOn hn z.mem a.mem hmem hspan
+  have admitted := record_admitted hW
+  obtain ⟨r, S, he, rs, rf, hS, riff, answers, rwit, rframe, rregs⟩ :=
+    BoxRecordWitness.exec_of_output V AB BC AC z₀ z hcurrent hD hg hp0 hN
+      ((header 1 (by omega)).trans rfl) ((header 2 (by omega)).trans rfl)
+      ((header 3 (by omega)).trans rfl) idx hidx hi hmatrix hmag
+      (RecordWitness.signed_fits admitted) (by
+        rw [zheap]
+        exact BoxRecordWitness.physical_fits hheap hQ hN admitted)
+  dsimp only [q, Q] at hqs
+  rw [hqs] at he answers
+  have hcoordinate (i : Fin qs.length) :
+      z.mem (q + 2 * i.val) = (qs.get i).1.val ∧
+      z.mem (q + 2 * i.val + 1) = (qs.get i).2.val := by
+    have hj : i.val < Q := by simpa only [hlenQ] using i.isLt
+    have hv := RecordProduct.decodedQueries_get_val hn a.mem q Q i
+      (hcoords i.val hj).1 (hcoords i.val hj).2
+    exact ⟨(mem_eq _ (by omega)).trans hv.1.symm,
+      (mem_eq _ (by omega)).trans hv.2.symm⟩
+  have hfail := RecordWitness.native_failed_count_le V AB BC AC wAB wBC wAC hD hg
+    (by intro u v; rfl) (by intro u v; rfl) (by intro u v; rfl) idx qs
+    (⟨0, hn⟩, ⟨0, hn⟩) (fun j => z.mem (q + 2 * j))
+    (fun j => z.mem (q + 2 * j + 1)) hcoordinate r.mem
+    (r.regs (RecordWitness.productBank RecordProduct.Reg.result)) answers
+  rw [hlenQ] at hfail
+  have hsuccess := RecordWitness.actual_success_iff V AB BC AC wAB wBC wAC hD hg hp
+    (by intro u v; rfl) (by intro u v; rfl) (by intro u v; rfl)
+    (by intro v c; rfl) (by intro u c; rfl) idx qs
+    (actual_queries_chunk hn V hout hD hDn hp0 idx hidx).2
+    (fun j => z.mem (q + 2 * j)) (fun j => z.mem (q + 2 * j + 1))
+    hcoordinate r.mem (r.regs (RecordWitness.productBank RecordProduct.Reg.result)) answers
+  rw [hlenQ] at hsuccess
+  let y := r.extend recordBank x
+  have yr (j : Fin 400) : y.regs (recordBank j) = r.regs j :=
+    recordBank_injective.extend_apply _ _ j
+  have hex : ExecWithin (w + 2) record x y
+      (RecordBoxProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q +
+        (42 * pieceSize (D m) g + 28) * S + 52) := by
+    apply (he.rename recordBank_injective).mono
+    have ht := Nat.mul_le_mul_right S (show
+      42 * min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g) + 28 ≤
+        42 * pieceSize (D m) g + 28 by omega)
+    omega
+  refine ⟨y, S, hex, (yr _).trans rs, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · simpa only [yr] using rf
+  · have hh := hS.trans (Nat.add_le_add_right hfail _)
+    simpa only [recordFailures, qs, q, Q, RecordProduct.decodedQueries_length,
+      yr, V, wAB, wBC, wAC] using hh
+  · have hc : Nat.count (fun j =>
+        r.mem (r.regs (RecordWitness.productBank RecordProduct.Reg.result) + j) ≠ 0 ∧
+        ∀ c : Fin (min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g)),
+          AB (z.mem (q + 2 * j)) (z.mem (q + 2 * j + 1)) +
+            BC (z.mem (q + 2 * j + 1)) (idx.2.2 * pieceSize (D m) g + c.val) +
+            AC (z.mem (q + 2 * j)) (idx.2.2 * pieceSize (D m) g + c.val) ≠ 0) Q ≤ Q :=
+      Nat.count_le _
+    have hflag : r.regs RecordWitness.Reg.found ≤ 1 := by rcases rf with h | h <;> omega
+    have hQ' := recordQueryCount_le n (D m) p V idx
+    have hcS : S ≤ Q + r.regs RecordWitness.Reg.found :=
+      hS.trans (Nat.add_le_add_right hc _)
+    omega
+  · simpa only [yr, wAB, wBC, wAC, weightSum] using riff.trans hsuccess
+  · intro hf
+    obtain ⟨ha, hb, hlo, hhi, hz, -⟩ := rwit ((yr _).symm.trans hf)
+    have hlen := min_le_right (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g)
+    exact ⟨by simpa only [yr] using ha, by simpa only [yr] using hb,
+      by simp only [yr]; omega, by simpa only [yr] using hz⟩
+  · intro u hu
+    exact rframe u (by simpa only [zheap] using hu)
+  · intro j
+    exact (yr _).trans ((rregs _ (by change j.val < 65; omega)).trans (hbank j))
+  · intro j hj
+    apply hex.regs_eq
+    apply Code.preserves_rename_of_forall_ne
+    intro i hij
+    have hv := congrArg (fun k : Fin 416 => k.val) hij
+    change i.val = j.val at hv
+    omega
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/SourceBounds.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/SourceBounds.lean
new file mode 100644
index 000000000..6f58ea8db
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/SourceBounds.lean
@@ -0,0 +1,63 @@
+/-
+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.Flat
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.SourceBounds
+
+/-!
+# Original-input box-controller bounds for every fixed-prime native prefix
+
+The admission remains logarithmic for polynomial original weights and bounded scalar headers.
+The actual minimum-width halting run controls all wider prefixes, including dirty loads and
+all reused-workspace calls. The support envelope is independent of the physical width, and
+does not instruct the machine to clear or snapshot that range.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
+
+open FixedPrime
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Every actually reached state at every admitted wider width has the same original-input
+polynomial word/support envelope. The concrete minimum-width run, not an assumed execution
+certificate, supplies the comparison run. -/
+theorem bounded_reachable_original {W m n g p A k : ℕ} (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)
+    {s : State 416} (hr : Runs W (program.program Reg.found)
+      (State.init (PreparationInput.input n (D m) g p values)) s k) :
+    (∀ i, s.data.regs i < wordBound n (D m) g p A) ∧
+      (∀ a, s.data.mem a < wordBound n (D m) g p A) ∧
+      ∀ a, wordBound n (D m) g p A ≤ a → s.data.mem a = 0 := by
+  obtain ⟨hi, a, ha, hout, y, t, ht, hpref, he, -⟩ :=
+    runs_input values hlen hD hg hp hN hv le_rfl
+  have hlow := Runs.prefix_at_smaller_width program_fixed.2 hW hr he
+  have hs := hlow.bounded (Data.Bounded.init hi)
+  refine ⟨hs.1, hs.2, ?_⟩
+  intro a ha
+  rw [hlow.mem_above (Data.Bounded.init hi) ha]
+  cases a with
+  | zero =>
+    change 2 ^ admissionWidth n (D m) g p A ≤ 0 at ha
+    have := Nat.two_pow_pos (admissionWidth n (D m) g p A)
+    omega
+  | succ a =>
+    change (PreparationInput.input n (D m) g p values).getD a 0 = 0
+    apply List.getD_eq_default
+    have hlen := hi.1
+    dsimp only [Fits] at hlen
+    change 2 ^ admissionWidth n (D m) g p A ≤ a + 1 at ha
+    omega
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Step.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Step.lean
new file mode 100644
index 000000000..b5973d093
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/Step.lean
@@ -0,0 +1,145 @@
+/-
+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.Record
+
+/-!
+# Box-backed charged ordinal delivery, concrete call and native return
+
+This internal step theorem composes the actual copy, unchanged full record computation and
+native scan/flag/counter return. The selected finite index is proved from the runtime ordinal;
+it is not an additional input field or a supplied algorithm.
+-/
+
+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
+
+/-- Execute one real occupied ordinal. The instruction bound includes every argument/return
+instruction; its two outer-loop instructions appear in `recordBase`. -/
+theorem exec_step {w m n g p A i : ℕ} (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)
+    (a : Data 64) (x : Data 416)
+    (hout : Instances.Output n (D m) g p (fun q => values.getD q 0)
+      (.init (PreparationInput.input n (D m) g p values)) a)
+    (hbank : ∀ j : Fin 64,
+      x.regs (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j)
+    (hmem : Set.EqOn x.mem a.mem (Set.Iio (a.regs Instances.heap)))
+    (hheap : a.regs Instances.heap ≤ PreparationInput.wordBound n (D m) g p A)
+    (hi : x.regs Reg.index = i) (hiM : i < a.regs Instances.produced)
+    (hl : x.regs Reg.limit = a.regs Instances.produced) (h1 : x.regs Reg.one = 1)
+    (hscans : x.regs Reg.scans ≤ i * (n * n + 1))
+    (idx : InstanceIndex p)
+    (hidx : idx ∈ instanceIndices
+      (fun u v : Fin n => values.getD (pairIndex (u, v)) 0) (D m) g p)
+    (hord : RecordProduct.recordOrdinal n (D m) g p (fun q => values.getD q 0) idx = i) :
+    let V := fun q => values.getD q 0
+    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)
+    let Q := RecordProduct.recordQueryCount n (D m) p V idx
+    ∃ y S T, ExecWithin (w + 2) step x y T ∧
+      T + 2 ≤ recordBase (m := m) hn V a.mem idx +
+        (42 * pieceSize (D m) g + 28) * S ∧
+      y.regs Reg.index = i + 1 ∧
+      y.regs Reg.limit = (if y.regs Reg.found = 1 then i + 1 else a.regs Instances.produced) ∧
+      y.regs Reg.one = 1 ∧
+      y.regs Reg.scans = x.regs Reg.scans + S ∧
+      (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+      S ≤ recordFailures (m := m) (g := g) hn V a.mem idx + y.regs Reg.found ∧
+      S ≤ n * n + 1 ∧
+      (y.regs Reg.found = 1 ↔ recordHit (m := m) (n := n) (g := g) V idx) ∧
+      (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 Q ≤ u → y.mem u = x.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
+  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)
+  let dst := recordBank (RecordWitness.productBank RecordProduct.Reg.ordinal)
+  let z := x.set dst i
+  have hselect : ExecWithin (w + 2) select x z 1 := by
+    simpa only [select, hi, dst, z] using
+      (ExecWithin.copy (B := .standard) (w := w + 2) (x := x) (d := dst) (s := Reg.index))
+  have zbank (j : Fin 64) :
+      z.regs (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) =
+        a.regs j := by
+    change Function.update x.regs dst i
+      (recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = a.regs j
+    rw [Function.update_of_ne (by
+      intro h
+      have hv := congrArg (fun k : Fin 416 => k.val) h
+      change j.val = 64 at hv
+      omega)]
+    exact hbank j
+  have control (j : Fin 416) (hj : 400 ≤ j.val) : z.regs j = x.regs j := by
+    change Function.update x.regs dst i j = x.regs j
+    apply Function.update_of_ne
+    intro h
+    have hv := congrArg (fun k : Fin 416 => k.val) h
+    change j.val = 64 at hv
+    omega
+  obtain ⟨r, S, hr, rs, rf, hS, hcoarse, hit, wit, frame, bank, ctrl⟩ :=
+    exec_record values hlen hD hg hp hN hv hW a z hout zbank hmem hheap idx hidx (by
+      change Function.update x.regs dst i dst = _
+      simpa using hord.symm)
+  have rc (j : Fin 416) (hj : 400 ≤ j.val) : r.regs j = x.regs j :=
+    (ctrl j hj).trans (control j hj)
+  have hfits := return_fits hW
+    (produced_le V hout hD ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN) hg)
+    hiM hscans hcoarse
+  obtain ⟨y, hy, ym, yi, yl, ys, yf, ypres⟩ := exec_receive r
+    ((rc Reg.index (by decide)).trans hi) ((rc Reg.limit (by decide)).trans hl)
+    (rc Reg.scans (by decide)) rs rfl ((rc Reg.one (by decide)).trans h1) hfits.1 hfits.2
+  have yflag : y.regs Reg.found = r.regs (recordBank RecordWitness.Reg.found) := yf
+  have ylow (j : Fin 400) : y.regs (recordBank j) = r.regs (recordBank j) :=
+    ypres _ (Or.inl (by change j.val < 400; exact j.isLt))
+  let T := RecordBoxProduct.timeBound (m := m)
+    (RecordProduct.decodedQueries hn a.mem (RecordProduct.recordQueries n (D m) p idx)
+      (RecordProduct.recordQueryCount n (D m) p V idx)) +
+    5 * Nat.sqrt (D m) + 8 * RecordProduct.recordQueryCount n (D m) p V idx +
+      (42 * pieceSize (D m) g + 28) * S + 59
+  have hex : ExecWithin (w + 2) step x y T := (hselect.seq (hr.seq hy)).mono (by
+    dsimp only [T, V]
+    omega)
+  refine ⟨y, S, T, hex, ?_, yi, ?_, ?_, ys, ?_, ?_, hcoarse, ?_, ?_, ?_, ?_⟩
+  · dsimp only [recordBase, T, V]
+    omega
+  · rw [yflag]
+    exact yl
+  · exact (ypres _ (Or.inr rfl)).trans ((rc Reg.one (by decide)).trans h1)
+  · simpa only [yflag] using rf
+  · simpa only [yflag] using hS
+  · simpa only [yflag, recordHit, weightSum] using hit
+  · intro hf
+    simpa only [ylow] using wit (yflag ▸ hf)
+  · intro u hu
+    exact (congrFun ym u).trans (frame u hu)
+  · intro j
+    exact (ylow _).trans (bank j)
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/TimeBound.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/TimeBound.lean
new file mode 100644
index 000000000..2672e6069
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxFixedPrime/TimeBound.lean
@@ -0,0 +1,125 @@
+/-
+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.Flat
+import Mathlib.Tactic.Positivity
+
+/-!
+# Aggregate box-backed native fixed-prime charges
+
+For `m = 9k`, the actual producer chunk cardinalities derive occurrence sparsity for every
+real product.
+Summing over the existing finite instances gives an aggregate product saving, with the
+one-time preparation and all root/query/controller costs separate. Failed original-weight
+scans use one global `F(p)+1` reserve, not that reserve per instance. The fixed prime is still
+an input: this does not select parameters or establish the final ET/3SUM source exponent.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
+
+open FixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- The existing finite family bounds the sum of actual queried-product charges, including a
+standalone halt for each term as a conservative upper bound. Every occurrence bound is derived
+from the real chunk count; there is no supplied sparse execution or solver premise. -/
+theorem products_time_le {k n g p : ℕ} (hn : 0 < n) (values : ℕ → ℤ) (mem : ℕ → ℕ)
+    (hD : 16 ≤ D (9 * k)) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D (9 * k)))
+    (hN : D (9 * k) ^ 18 ≤ n) :
+    let I := instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) (D (9 * k)) g p
+    let qs := fun idx => RecordProduct.decodedQueries hn mem
+      (RecordProduct.recordQueries n (D (9 * k)) p idx)
+      (RecordProduct.recordQueryCount n (D (9 * k)) p values idx)
+    ((∑ idx ∈ I, (RecordBoxProduct.timeBound (m := 9 * k) (qs idx) + 1) : ℕ) : ℝ) ≤
+      125829120 * ((189 * k + 1 : ℕ) : ℝ) ^ 2 * ((9 * k + 1 : ℕ) : ℝ) *
+        (D (9 * k) : ℝ) ^ (-(8 / 125 : ℝ)) * (n : ℝ) ^ 3 * g := by
+  let I := instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) (D (9 * k)) g p
+  let qs := fun idx => RecordProduct.decodedQueries hn mem
+    (RecordProduct.recordQueries n (D (9 * k)) p idx)
+    (RecordProduct.recordQueryCount n (D (9 * k)) p values idx)
+  let R : ℝ := 31457280 * ((189 * k + 1 : ℕ) : ℝ) ^ 2 * ((9 * k + 1 : ℕ) : ℝ) *
+    (D (9 * k) : ℝ) ^ (-(8 / 125 : ℝ)) * (n : ℝ) ^ 2
+  have hr (idx : InstanceIndex p) :
+      ((RecordBoxProduct.timeBound (m := 9 * k) (qs idx) + 1 : ℕ) : ℝ) ≤ R := by
+    apply RecordBoxProduct.thin_timeBound _ hN
+    rw [RecordProduct.decodedQueries_length]
+    exact (Nat.mul_le_mul_right (2 ^ (9 * k)) (min_le_left _ _)).trans
+      (RecordProduct.queryCap_mul_two_pow_le n (9 * k))
+  have hc : (I.card : ℝ) ≤ 4 * (n : ℝ) * g := by
+    exact card_instanceIndices_le _ hD
+      ((Nat.le_self_pow (by decide : 18 ≠ 0) (D (9 * k))).trans hN) hg hp
+  calc
+    _ = ∑ idx ∈ I, ((RecordBoxProduct.timeBound (m := 9 * k) (qs idx) + 1 : ℕ) : ℝ) := by
+      rw [Nat.cast_sum]
+    _ ≤ ∑ _idx ∈ I, R := Finset.sum_le_sum (fun idx _ => hr idx)
+    _ = I.card * R := by rw [Finset.sum_const, nsmul_eq_mul]
+    _ ≤ (4 * (n : ℝ) * g) * R := mul_le_mul_of_nonneg_right hc (by dsimp only [R]; positivity)
+    _ = _ := by dsimp only [R]; ring
+
+/-- Complete halt-inclusive charged bound, retaining the one-time producer and the single
+global failed-scan reserve. Root, query, ordinal, call, return and loop overheads are explicit.
+In particular this is not a prime-selection or an unconditional aggregate exponent theorem. -/
+theorem timeBound_le {k n g p : ℕ} (hn : 0 < n) (values : List ℤ) (mem : ℕ → ℕ)
+    (hD : 16 ≤ D (9 * k)) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D (9 * k)))
+    (hN : D (9 * k) ^ 18 ≤ n) :
+    let V := fun q => values.getD q 0
+    let F := 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
+    ((timeBound (m := 9 * k) hn g p values mem : ℕ) : ℝ) ≤
+      690 * (n : ℝ) ^ 2 * D (9 * k) * g +
+        125829120 * ((189 * k + 1 : ℕ) : ℝ) ^ 2 * ((9 * k + 1 : ℕ) : ℝ) *
+          (D (9 * k) : ℝ) ^ (-(8 / 125 : ℝ)) * (n : ℝ) ^ 3 * g +
+        (4 * (n : ℝ) * g) * ((5 * Nat.sqrt (D (9 * k)) + 8 * queryCap n (D (9 * k)) + 61 : ℕ) : ℝ) +
+        (((42 * pieceSize (D (9 * k)) g + 28) * (F + 1) + 7 : ℕ) : ℝ) := by
+  let V := fun q => values.getD q 0
+  let I := instanceIndices (fun u v : Fin n => V (pairIndex (u, v))) (D (9 * k)) g p
+  let qs := fun idx => RecordProduct.decodedQueries hn mem
+    (RecordProduct.recordQueries n (D (9 * k)) p idx)
+    (RecordProduct.recordQueryCount n (D (9 * k)) p V idx)
+  let extra := 5 * Nat.sqrt (D (9 * k)) + 8 * queryCap n (D (9 * k)) + 61
+  have hDn : D (9 * k) ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D (9 * k))).trans hN
+  have hprep : (RecordProduct.preparationTime n (D (9 * k)) g p values : ℝ) ≤
+      690 * (n : ℝ) ^ 2 * D (9 * k) * g := by
+    have hnat : RecordProduct.preparationTime n (D (9 * k)) g p values ≤
+        690 * n ^ 2 * D (9 * k) * g := by
+      simpa only [RecordProduct.preparationTime, pow_two] using
+        PreparationBounds.computed_timeBound_le values hD hDn hg hp
+    exact_mod_cast hnat
+  have hterms : (∑ idx ∈ I, recordBase (m := 9 * k) hn V mem idx) ≤
+      (∑ idx ∈ I, (RecordBoxProduct.timeBound (m := 9 * k) (qs idx) + 1)) + I.card * extra := by
+    rw [show I.card * extra = ∑ _idx ∈ I, extra by simp, ← Finset.sum_add_distrib]
+    apply Finset.sum_le_sum
+    intro idx _
+    have hQ : RecordProduct.recordQueryCount n (D (9 * k)) p V idx ≤ queryCap n (D (9 * k)) :=
+      min_le_left _ _
+    dsimp only [recordBase, extra, qs]
+    omega
+  have hc : (I.card : ℝ) ≤ 4 * (n : ℝ) * g := card_instanceIndices_le _ hD hDn hg hp
+  have hextra := mul_le_mul_of_nonneg_right hc (Nat.cast_nonneg extra : (0 : ℝ) ≤ extra)
+  have hprod := products_time_le hn V mem hD hg hp hN
+  have hcast := (Nat.cast_le (α := ℝ)).mpr hterms
+  push_cast at hcast hprod
+  have hbase : ((∑ idx ∈ I, recordBase (m := 9 * k) hn V mem idx : ℕ) : ℝ) ≤
+      125829120 * ((189 * k + 1 : ℕ) : ℝ) ^ 2 * ((9 * k + 1 : ℕ) : ℝ) *
+          (D (9 * k) : ℝ) ^ (-(8 / 125 : ℝ)) * (n : ℝ) ^ 3 * g + (4 * (n : ℝ) * g) * extra := by
+    dsimp only [I, qs] at hcast hprod ⊢
+    push_cast
+    linarith only [hcast, hextra, hprod]
+  dsimp only [timeBound]
+  push_cast
+  dsimp only [I, V, extra] at hbase hprep ⊢
+  push_cast at hbase
+  linarith only [hbase, hprep]
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxRecordWitness/Exec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxRecordWitness/Exec.lean
new file mode 100644
index 000000000..8cd98cf2f
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxRecordWitness/Exec.lean
@@ -0,0 +1,209 @@
+/-
+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.RecordWitness.Consume
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Readback
+public import Complexity.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness.Program
+
+/-!
+# The real box product followed by candidate verification
+
+The general caller selects any occupied record. The actual product is executed on its whole
+renamed 320-register bank; the consumer then reads its real answers and protected query words.
+The original signed arrays and caller catalogue remain untouched. The initialized entry derives
+the numerical premises from original input, rather than supplying an intermediate run contract.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness
+
+open RecordWitness
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+private theorem productBank_injective : Function.Injective productBank := by
+  intro i j h
+  exact Fin.ext (congrArg (fun k : Fin 400 => k.val) h)
+
+/-- Execute the actual product and verifier from one genuine producer output. No product
+execution, accepted-pair list, witness or time certificate is a hypothesis. -/
+theorem exec_of_output {w U m n g p : ℕ} (values : ℕ → ℤ)
+    (AB BC AC : ℕ → ℕ → ℤ) (initial : Data 64) (x : Data 400)
+    (h : Instances.Output n (D m) g p values initial
+      ((x.comap productBank).comap RecordProduct.producerBank))
+    (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ≠ 0) (hN : D m ^ 18 ≤ n)
+    (hheaderD : initial.mem 1 = D m) (hheaderG : initial.mem 2 = g)
+    (hheaderN : initial.mem 3 = n)
+    (idx : InstanceIndex p)
+    (hidx : idx ∈ instanceIndices (fun a b : Fin n => values (pairIndex (a, b))) (D m) g p)
+    (hi : x.regs (productBank RecordProduct.Reg.ordinal) =
+      RecordProduct.recordOrdinal n (D m) g p values idx)
+    (hmem : ∀ a < n, ∀ b < n,
+      x.mem (5 + (a * n + b)) = Signed.encode (AB a b) ∧
+      x.mem (5 + n * n + (a * n + b)) = Signed.encode (BC a b) ∧
+      x.mem (5 + n * n + n * n + (a * n + b)) = Signed.encode (AC a b))
+    (hmag : ∀ a < n, ∀ b < n,
+      (AB a b).natAbs ≤ U ∧ (BC a b).natAbs ≤ U ∧ (AC a b).natAbs ≤ U)
+    (hU : GenericRAM.Signed.Fits w (2 * U : ℕ))
+    (hfit : Fits (w + 2)
+      (4 * x.regs (productBank 42) +
+        4 * CallableProduct.windowSize n (RecordProduct.recordQueryCount n (D m) p values idx) +
+        QueriedProduct.outputBase (21 * m) m n
+          (RecordProduct.recordQueryCount n (D m) p values idx) +
+        4 * RecordProduct.recordQueryCount n (D m) p values idx + 4 * D m +
+        2 * (n * D m) + 9 * (n * n) + 4 * n + g + 4096)) :
+    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)
+    let q := RecordProduct.recordQueries n (D m) p idx
+    let Q := RecordProduct.recordQueryCount n (D m) p values idx
+    let qs := RecordProduct.decodedQueries hn x.mem q Q
+    let first := idx.2.2 * pieceSize (D m) g
+    let length := min (pieceSize (D m) g) (n - first)
+    ∃ y S, ExecWithin (w + 2) program x y
+        (RecordBoxProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q +
+          (42 * length + 28) * S + 52) ∧
+      y.regs Reg.scans = S ∧ (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+      S ≤ Nat.count (fun j => y.mem (y.regs (productBank RecordProduct.Reg.result) + j) ≠ 0 ∧
+        ∀ c : Fin length,
+          AB (x.mem (q + 2 * j)) (x.mem (q + 2 * j + 1)) +
+            BC (x.mem (q + 2 * j + 1)) (first + c.val) +
+            AC (x.mem (q + 2 * j)) (first + c.val) ≠ 0) Q + y.regs Reg.found ∧
+      (y.regs Reg.found = 1 ↔ ∃ j < Q,
+        y.mem (y.regs (productBank RecordProduct.Reg.result) + j) ≠ 0 ∧
+        ∃ c, first ≤ c ∧ c < first + length ∧
+          AB (x.mem (q + 2 * j)) (x.mem (q + 2 * j + 1)) +
+            BC (x.mem (q + 2 * j + 1)) c + AC (x.mem (q + 2 * j)) c = 0) ∧
+      (∀ j : Fin qs.length,
+        y.mem (y.regs (productBank RecordProduct.Reg.result) + j.val) = Signed.encode
+          ((RecordProduct.leftMatrix m n g p values idx *
+            RecordProduct.rightMatrix m n g p values idx) (qs.get j).1 (qs.get j).2)) ∧
+      (y.regs Reg.found = 1 →
+        y.regs Reg.witnessA < n ∧ y.regs Reg.witnessB < n ∧
+        first ≤ y.regs Reg.witnessC ∧ y.regs Reg.witnessC < first + length ∧
+        AB (y.regs Reg.witnessA) (y.regs Reg.witnessB) +
+          BC (y.regs Reg.witnessB) (y.regs Reg.witnessC) +
+          AC (y.regs Reg.witnessA) (y.regs Reg.witnessC) = 0 ∧
+        ∃ j < Q, y.regs Reg.witnessA = x.mem (q + 2 * j) ∧
+          y.regs Reg.witnessB = x.mem (q + 2 * j + 1)) ∧
+      (∀ u, u < x.regs (productBank 42) ∨
+        x.regs (productBank 42) + CallableProduct.windowSize n Q ≤ u → y.mem u = x.mem u) ∧
+      (∀ j : Fin 320, j.val < 65 → y.regs (productBank j) = x.regs (productBank j)) := by
+  let x' := x.comap productBank
+  let produced := x'.comap RecordProduct.producerBank
+  let heap := x.regs (productBank 42)
+  let q := RecordProduct.recordQueries n (D m) p idx
+  let Q := RecordProduct.recordQueryCount n (D m) p values idx
+  let ord := RecordProduct.recordOrdinal n (D m) g p values idx
+  let base := x.regs (productBank (RecordProduct.producerBank Instances.output)) +
+    ord * (6 + 2 * (n * D m))
+  let out := heap + QueriedProduct.outputBase (21 * m) m n Q
+  change Fits (w + 2) (4 * heap + 4 * CallableProduct.windowSize n Q +
+    QueriedProduct.outputBase (21 * m) m n Q + 4 * Q + 4 * D m +
+    2 * (n * D m) + 9 * (n * n) + 4 * n + g + 4096) at hfit
+  have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN
+  have hn : 0 < n := lt_of_lt_of_le (by omega) hDn
+  let qs := RecordProduct.decodedQueries hn x.mem q Q
+  have hlen : qs.length = Q := RecordProduct.decodedQueries_length hn x.mem q Q
+  obtain ⟨hinputEnd, hrec, hq, hfirst, hv, hcoords, hprefix⟩ :=
+    record_view values initial produced h hD hDn hg hp idx hidx
+  change 5 + 3 * (n * n) ≤ heap at hinputEnd
+  change base + 6 ≤ heap at hrec
+  change q + 2 * Q ≤ heap at hq
+  change ∀ j : Fin 6, x.mem (base + j.val) =
+    ![idx.1.val, idx.2.2, q, Q, base + 6, base + 6 + n * D m] j at hv
+  change ∀ j < Q, x.mem (q + 2 * j) < n ∧ x.mem (q + 2 * j + 1) < n at hcoords
+  change ∀ j < 5 + 3 * (n * n), x.mem j = initial.mem j at hprefix
+  obtain ⟨r, hr, rr, rvalues, rmem, rregs, -⟩ := RecordBoxProduct.exec_of_output values
+    initial x' h hD hg hp hN hheaderD hheaderN idx hidx hi (hfit.of_le (by
+      change 2 * heap + 4 * CallableProduct.windowSize n Q + 1024 ≤ _
+      omega))
+  change r.regs RecordProduct.Reg.result =
+    heap + QueriedProduct.outputBase (21 * m) m n qs.length at rr
+  change ∀ j : Fin qs.length,
+    r.mem (heap + (QueriedProduct.outputBase (21 * m) m n qs.length + j.val)) =
+      Signed.encode ((RecordProduct.leftMatrix m n g p values idx *
+        RecordProduct.rightMatrix m n g p values idx) (qs.get j).1 (qs.get j).2) at rvalues
+  simp only [RecordProduct.decodedQueries_length] at rmem
+  change ∀ u, u < heap ∨ heap + CallableProduct.windowSize n Q ≤ u →
+    r.mem u = x.mem u at rmem
+  let s := r.extend productBank x
+  have hs : ExecWithin (w + 2) (RecordBoxProduct.program.rename productBank) x s
+      (RecordBoxProduct.timeBound (m := m) qs) := hr.rename productBank_injective
+  have sr (j : Fin 320) : s.regs (productBank j) = r.regs j :=
+    productBank_injective.extend_apply _ _ j
+  have sm (u : ℕ) (hu : u < heap) : s.mem u = x.mem u := rmem u (Or.inl hu)
+  have snative (j : Fin 320) (hj : j.val < 65) :
+      s.regs (productBank j) = x.regs (productBank j) := (sr j).trans (rregs j hj)
+  have sout : s.regs (productBank RecordProduct.Reg.result) = out := by
+    simpa only [out, hlen] using (sr RecordProduct.Reg.result).trans rr
+  let v : Fin 6 → ℕ := ![idx.1.val, idx.2.2, q, Q, base + 6, base + 6 + n * D m]
+  have hread (j : Fin 6) : s.mem (base + j.val) = v j :=
+    (sm _ (by have := j.isLt; omega)).trans (hv j)
+  have hquery : ∀ j < Q, s.mem (q + 2 * j) = x.mem (q + 2 * j) ∧
+      s.mem (q + 2 * j + 1) = x.mem (q + 2 * j + 1) ∧
+      x.mem (q + 2 * j) < n ∧ x.mem (q + 2 * j + 1) < n := by
+    intro j hj
+    exact ⟨sm _ (by omega), sm _ (by omega), hcoords j hj⟩
+  have smem : ∀ a < n, ∀ b < n,
+      s.mem (5 + (a * n + b)) = Signed.encode (AB a b) ∧
+      s.mem (5 + n * n + (a * n + b)) = Signed.encode (BC a b) ∧
+      s.mem (5 + n * n + n * n + (a * n + b)) = Signed.encode (AC a b) := by
+    intro a ha b hb
+    have hn := Nat.mul_le_mul_right n (Nat.succ_le_of_lt ha)
+    rw [Nat.succ_mul] at hn
+    simpa only [sm _ (by omega : 5 + (a * n + b) < heap),
+      sm _ (by omega : 5 + n * n + (a * n + b) < heap),
+      sm _ (by omega : 5 + n * n + n * n + (a * n + b) < heap)] using hmem a ha b hb
+  obtain ⟨y, S, he, ym, ys, hS, yf, yiff, yw, frame⟩ := exec_consume AB BC AC
+    (fun j => x.mem (q + 2 * j)) (fun j => x.mem (q + 2 * j + 1)) s v
+    ((sm 1 (by omega)).trans ((hprefix 1 (by omega)).trans hheaderD))
+    ((sm 2 (by omega)).trans ((hprefix 2 (by omega)).trans hheaderG))
+    ((sm 3 (by omega)).trans ((hprefix 3 (by omega)).trans hheaderN))
+    ((snative _ (by decide)).trans hi) (snative _ (by decide)) sout hrec hread hfirst
+    hquery smem hmag hU (hfit.of_le (by
+      change heap + out + q + 4 * Q + 4 * D m + 2 * (n * D m) +
+        9 * (n * n) + 4 * n + g + 2048 ≤ _
+      dsimp only [out]
+      omega))
+  change ExecWithin (w + 2) consume s y
+    (5 * Nat.sqrt (D m) + 8 * Q +
+      (42 * min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g) + 28) * S + 52) at he
+  change S ≤ Nat.count (fun j => s.mem (out + j) ≠ 0 ∧
+    ∀ c : Fin (min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g)),
+      AB (x.mem (q + 2 * j)) (x.mem (q + 2 * j + 1)) +
+        BC (x.mem (q + 2 * j + 1)) (idx.2.2 * pieceSize (D m) g + c.val) +
+        AC (x.mem (q + 2 * j)) (idx.2.2 * pieceSize (D m) g + c.val) ≠ 0) Q + y.regs Reg.found at hS
+  simp_rw [show v 1 = idx.2.2 from rfl, show v 3 = Q from rfl] at yiff
+  have hexe : ExecWithin (w + 2) program x y
+      (RecordBoxProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q +
+        (42 * min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g) + 28) * S + 52) :=
+    (hs.seq he).mono (by omega)
+  refine ⟨y, S, hexe, ys, yf, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · simpa only [ym, frame (productBank RecordProduct.Reg.result) (by decide), sout] using hS
+  · simpa only [ym, frame (productBank RecordProduct.Reg.result) (by decide), sout] using yiff
+  · intro j
+    have hv := rvalues j
+    rw [frame _ (by decide), sout, ym]
+    change r.mem (out + j.val) = _
+    simpa only [out, hlen, Nat.add_assoc] using hv
+  · intro hy
+    obtain ⟨j, hj, -, hwa, hwb, hlo, hhi, hz⟩ := yw hy
+    obtain ⟨ha, hb⟩ := hcoords j hj
+    exact ⟨by simpa only [hwa] using ha, by simpa only [hwb] using hb,
+      hlo, hhi, by simpa only [hwa, hwb] using hz, j, hj, hwa, hwb⟩
+  · intro u hu
+    rw [ym]
+    exact rmem u hu
+  · intro j hj
+    exact (frame _ (by change j.val < 320; omega)).trans (snative j hj)
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxRecordWitness/Program.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxRecordWitness/Program.lean
new file mode 100644
index 000000000..bc98984fa
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxRecordWitness/Program.lean
@@ -0,0 +1,31 @@
+/-
+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.RecordWitness.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordBoxProduct
+
+/-!
+# The box product followed by original-weight witness verification
+
+The selected record executes the actual threshold-aware box backend and then the existing
+read-only verifier. Register banks, query decoding and witness semantics are shared with
+`RecordWitness`; the changed output layout is established by execution of the box program.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness
+
+open Cslib.WordRAM RecordWitness
+
+/-- Actual box-product call followed by the unchanged original-weight consumer. -/
+@[expose] def program : Code .standard 400 :=
+  .seq (RecordBoxProduct.program.rename productBank) consume
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/BoxRecordWitness/Width.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxRecordWitness/Width.lean
new file mode 100644
index 000000000..f7723d443
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/BoxRecordWitness/Width.lean
@@ -0,0 +1,76 @@
+/-
+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.BoxRecordWitness.Exec
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Width
+
+/-!
+# Original-input admission for product-selected witness recovery
+
+One positive width threshold covers the original producer/product admission, all real
+descriptor/query/address arithmetic and both signed additions of original weights. It depends
+on the original scalar headers and magnitude envelope, not on the physical width chosen by
+the caller. The reserved product window is an address bound, not a charged clearing operation.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness
+
+open Cslib.WordRAM RecordWitness
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+/-- The existing product's output slice precedes its admitted virtual-window boundary. -/
+theorem outputBase_lt_window {m n Q : ℕ} (hN : D m ^ 18 ≤ n) :
+    QueriedProduct.outputBase (21 * m) m n Q < CallableProduct.windowSize n Q := by
+  have hout : QueriedProduct.outputBase (21 * m) m n Q ≤
+      QueriedProduct.memoryEnd (21 * m) m n Q := by
+    unfold QueriedProduct.memoryEnd QueriedProduct.stampBase QueriedProduct.scratchBase
+    have hten := Nat.zero_le (10 ^ (21 * m))
+    have hframes := Nat.zero_le (2 * (21 * m + 1) * 10 ^ (21 * m))
+    omega
+  have hword : QueriedProduct.memoryEnd (21 * m) m n Q ≤
+      QueriedProduct.wordBudget (21 * m) m n Q := by
+    unfold QueriedProduct.wordBudget
+    omega
+  have hbox : QueriedProduct.wordBudget (21 * m) m n Q ≤
+      BoxProduct.wordBudget (21 * m) m (m / 9) n Q := by
+    unfold BoxProduct.wordBudget
+    omega
+  exact (hout.trans (hword.trans hbox)).trans_lt
+    (CallableBoxProduct.source_admission (Nat.div_le_self m 9) hN).2.2
+
+/-- Every pointer and temporary of the actual per-record caller fits from the original
+producer word bound and the actual chunk count. No intermediate fit certificate is supplied. -/
+theorem physical_fits {w m n g p A heap Q : ℕ}
+    (hheap : heap ≤ PreparationInput.wordBound n (D m) g p A)
+    (hQ : Q ≤ n ^ 2) (hN : D m ^ 18 ≤ n)
+    (hW : admissionWidth n (D m) g p A ≤ w + 2) :
+    Fits (w + 2) (4 * heap + 4 * CallableProduct.windowSize n Q +
+      QueriedProduct.outputBase (21 * m) m n Q + 4 * Q + 4 * D m +
+      2 * (n * D m) + 9 * (n * n) + 4 * n + g + 4096) := by
+  have hwindow : CallableProduct.windowSize n Q ≤ CallableProduct.windowSize n (n ^ 2) := by
+    unfold CallableProduct.windowSize CallableProduct.sourceWidth
+    apply Nat.pow_le_pow_right (by decide)
+    exact Nat.mul_le_mul_left 128 (Nat.clog_mono_right 2 (by omega))
+  have hout := (outputBase_lt_window (Q := Q) hN).le.trans hwindow
+  have he : Fits (w + 2) (envelope n (D m) g p A) := by
+    have hn := Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) (envelope n (D m) g p A)
+    have hw : Nat.clog 2 (envelope n (D m) g p A) < w + 2 := by
+      unfold admissionWidth at hW
+      omega
+    exact hn.trans_lt (Nat.pow_lt_pow_right (by decide : 1 < (2 : ℕ)) hw)
+  apply he.of_le
+  unfold envelope
+  rw [pow_two] at hQ hwindow hout ⊢
+  omega
+
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.BoxRecordWitness
diff --git a/ComplexityTests/WordRAMExactTriangleBoxFixedPrime.lean b/ComplexityTests/WordRAMExactTriangleBoxFixedPrime.lean
new file mode 100644
index 000000000..2da0a15d4
--- /dev/null
+++ b/ComplexityTests/WordRAMExactTriangleBoxFixedPrime.lean
@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+-- upstream: local-only (tests)
+
+import Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime
+import Mathlib.Data.List.GetD
+
+/-!
+# Full box-backed fixed-prime decisions at positive threshold
+
+Both clients retain the actual same-state prefix and halt at valid positive thin geometry.
+The constant-257 negative input has modular false positives at prime 257, but no original zero;
+its unsuccessful records collectively receive no additive successful-scan allowance. These
+kernel proofs do not evaluate the enormous catalogue or encoder through the interpreter.
+-/
+
+namespace ComplexityTests.WordRAMExactTriangleBoxFixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.WordRAM.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+private def side : ℕ := D 9 ^ 18
+private def weights (N : ℕ) (z : ℤ) : List ℤ := List.replicate (3 * (N * N)) z
+private def width (N A : ℕ) : ℕ := FixedPrime.admissionWidth N (D 9) 1 257 A
+
+private theorem prime : 257 ∈ Nat.sqrtPrimeWindow (D 9) :=
+  Nat.mem_sqrtPrimeWindow_iff_sq.mpr
+    ⟨by norm_num, by norm_num [D], by norm_num [D]⟩
+
+/-- The complete finite bound includes preparation, all box calls, all overhead and halt. -/
+private noncomputable def zeroCharge (N : ℕ) : ℝ :=
+  690 * (N : ℝ) ^ 2 * D 9 +
+    125829120 * ((189 * 1 + 1 : ℕ) : ℝ) ^ 2 * ((9 * 1 + 1 : ℕ) : ℝ) *
+      (D 9 : ℝ) ^ (-(8 / 125 : ℝ)) * (N : ℝ) ^ 3 +
+    (4 * (N : ℝ)) * ((5 * Nat.sqrt (D 9) + 8 * queryCap N (D 9) + 61 : ℕ) : ℝ) +
+    (((42 * pieceSize (D 9) 1 + 28) * (0 + 1) + 7 : ℕ) : ℝ)
+
+/-- The complete actual program returns one and an original witness on all-zero input. -/
+private theorem initialized_zero (N : ℕ) (hgeo : D 9 ^ 18 ≤ N) : ∃ y : Data 416, ∃ t : ℕ,
+    Runs (width N 0) (BoxFixedPrime.program.program FixedPrime.Reg.found)
+      (State.init (PreparationInput.input N (D 9) 1 257 (weights N 0)))
+      ⟨BoxFixedPrime.program.size, y⟩ t ∧
+    Executes (width N 0) (BoxFixedPrime.program.program FixedPrime.Reg.found)
+      (State.init (PreparationInput.input N (D 9) 1 257 (weights N 0))) 1 (t + 1) ∧
+    y.regs FixedPrime.Reg.found = 1 ∧ y.regs FixedPrime.Reg.scans ≤ 1 ∧
+    ((t + 1 : ℕ) : ℝ) ≤ zeroCharge N ∧
+    ∃ u v c : Fin N,
+      y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessA) = u.val ∧
+      y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessB) = v.val ∧
+      y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessC) = c.val := by
+  have hmag : ∀ z ∈ weights N 0, z.natAbs ≤ 0 := by
+    intro z hz
+    have he := List.eq_of_mem_replicate hz
+    subst z
+    decide
+  obtain ⟨hi, a, ha, hout, y, t, ht, hr, he, yb, yf, ys, yiff, yw, frame, regs⟩ :=
+    BoxFixedPrime.runs_input (m := 9) (n := N) (g := 1) (p := 257) (A := 0)
+      (W := width N 0) (weights N 0) (by simp only [weights, List.length_replicate])
+      (by decide) (by decide) prime hgeo hmag le_rfl
+  let V := fun q => (weights N 0).getD q 0
+  have hval (q : ℕ) : V q = 0 := List.getElem?_getD_replicate_default_eq _ _ _
+  have hzero : HasZeroTriangle (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))) := by
+    let v : Fin N := ⟨0, lt_of_lt_of_le (by decide : 0 < D 9 ^ 18) hgeo⟩
+    exact ⟨v, v, v, by simp only [hval, zero_add]⟩
+  have hf : y.regs FixedPrime.Reg.found = 1 := yiff.mpr hzero
+  have hF : 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))) 257 = 0 := by
+    simp only [falsePositiveCount, IsFalsePositive, weightSum, hval, zero_add,
+      ne_eq, not_true_eq_false, false_and, Finset.filter_false, Finset.card_empty]
+  obtain ⟨u, v, c, hu, hv, hc, _⟩ := yw hf
+  refine ⟨y, t, hr, ?_, hf, ?_, ?_, u, v, c, hu, hv, hc⟩
+  · simpa only [hf] using he
+  · have hs : y.regs FixedPrime.Reg.scans ≤
+        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))) 257 +
+          y.regs FixedPrime.Reg.found := ys
+    simpa only [hF, hf, zero_add] using hs
+  · have hcharge := BoxFixedPrime.timeBound_le (k := 1) (n := N) (g := 1) (p := 257)
+        (lt_of_lt_of_le (by decide : 0 < D 9 ^ 18) hgeo)
+        (weights N 0) a.mem (by decide) (by decide) prime hgeo
+    have hcast := (Nat.cast_le (α := ℝ)).mpr ht
+    have hbound := hcast.trans hcharge
+    dsimp only [V] at hF
+    simpa only [Nat.mul_one, Nat.cast_one, hF, zero_add, mul_one, zeroCharge] using hbound
+
+/-- Even with nonzero modular candidates, exhaustion of every actual record returns zero
+exactly. The total scan bound is the single global false-positive count, with no extra one. -/
+private theorem initialized_false_positive (N : ℕ) (hgeo : D 9 ^ 18 ≤ N) :
+    let V := fun q => (weights N 257).getD q 0
+    let F := 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))) 257
+    ∃ y : Data 416, ∃ t : ℕ,
+      Runs (width N 257) (BoxFixedPrime.program.program FixedPrime.Reg.found)
+        (State.init (PreparationInput.input N (D 9) 1 257 (weights N 257)))
+        ⟨BoxFixedPrime.program.size, y⟩ t ∧
+      Executes (width N 257) (BoxFixedPrime.program.program FixedPrime.Reg.found)
+        (State.init (PreparationInput.input N (D 9) 1 257 (weights N 257))) 0 (t + 1) ∧
+      y.regs FixedPrime.Reg.found = 0 ∧ y.regs FixedPrime.Reg.scans ≤ F := by
+  have hmag : ∀ z ∈ weights N 257, z.natAbs ≤ 257 := by
+    intro z hz
+    have he := List.eq_of_mem_replicate hz
+    subst z
+    decide
+  obtain ⟨hi, a, ha, hout, y, t, ht, hr, he, yb, yf, ys, yiff, yw, frame, regs⟩ :=
+    BoxFixedPrime.runs_input (m := 9) (n := N) (g := 1) (p := 257) (A := 257)
+      (W := width N 257) (weights N 257) (by simp only [weights, List.length_replicate])
+      (by decide) (by decide) prime hgeo hmag le_rfl
+  let V := fun q => (weights N 257).getD q 0
+  have hval (q : ℕ) (hq : q < 3 * (N * N)) : V q = 257 :=
+    List.getD_replicate (257 : ℤ) hq
+  have pair_bound (u v : Fin N) : pairIndex (u, v) < N * N := by
+    have hu := Nat.mul_le_mul_right N (Nat.succ_le_of_lt u.isLt)
+    rw [Nat.succ_mul] at hu
+    change u.val * N + v.val < N * N
+    have hv := v.isLt
+    omega
+  have hn : ¬ HasZeroTriangle (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))) := by
+    rintro ⟨u, v, c, hz⟩
+    change V (pairIndex (u, v)) + V (N * N + pairIndex (v, c)) +
+      V (2 * (N * N) + pairIndex (u, c)) = 0 at hz
+    rw [hval (pairIndex (u, v)) (by have := pair_bound u v; omega),
+      hval (N * N + pairIndex (v, c)) (by have := pair_bound v c; omega),
+      hval (2 * (N * N) + pairIndex (u, c)) (by have := pair_bound u c; omega)] at hz
+    norm_num at hz
+  have hf : y.regs FixedPrime.Reg.found = 0 := by
+    rcases yf with h | h
+    · exact h
+    · exact False.elim (hn (yiff.mp h))
+  refine ⟨y, t, hr, ?_, hf, ?_⟩
+  · simpa only [hf] using he
+  · simpa only [hf, Nat.add_zero] using ys
+
+
+example : ∃ y : Data 416, ∃ t : ℕ,
+    Runs (width side 0) (BoxFixedPrime.program.program FixedPrime.Reg.found)
+      (State.init (PreparationInput.input side (D 9) 1 257 (weights side 0)))
+      ⟨BoxFixedPrime.program.size, y⟩ t ∧
+    Executes (width side 0) (BoxFixedPrime.program.program FixedPrime.Reg.found)
+      (State.init (PreparationInput.input side (D 9) 1 257 (weights side 0))) 1 (t + 1) ∧
+    y.regs FixedPrime.Reg.found = 1 ∧ y.regs FixedPrime.Reg.scans ≤ 1 ∧
+    ((t + 1 : ℕ) : ℝ) ≤ zeroCharge side ∧
+    ∃ u v c : Fin side,
+      y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessA) = u.val ∧
+      y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessB) = v.val ∧
+      y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessC) = c.val :=
+  initialized_zero side (by decide)
+
+example :
+    let V := fun q => (weights side 257).getD q 0
+    let F := falsePositiveCount (fun u v : Fin side => V (pairIndex (u, v)))
+      (fun b c => V (side * side + pairIndex (b, c)))
+      (fun u c => V (2 * (side * side) + pairIndex (u, c))) 257
+    ∃ y : Data 416, ∃ t : ℕ,
+      Runs (width side 257) (BoxFixedPrime.program.program FixedPrime.Reg.found)
+        (State.init (PreparationInput.input side (D 9) 1 257 (weights side 257)))
+        ⟨BoxFixedPrime.program.size, y⟩ t ∧
+      Executes (width side 257) (BoxFixedPrime.program.program FixedPrime.Reg.found)
+        (State.init (PreparationInput.input side (D 9) 1 257 (weights side 257))) 0 (t + 1) ∧
+      y.regs FixedPrime.Reg.found = 0 ∧ y.regs FixedPrime.Reg.scans ≤ F :=
+  initialized_false_positive side (by decide)
+
+end ComplexityTests.WordRAMExactTriangleBoxFixedPrime
diff --git a/manual/algorithms-and-memory/algorithm-endpoints.md b/manual/algorithms-and-memory/algorithm-endpoints.md
index da43a2391..198ff9ba5 100644
--- a/manual/algorithms-and-memory/algorithm-endpoints.md
+++ b/manual/algorithms-and-memory/algorithm-endpoints.md
@@ -210,6 +210,45 @@ This is polynomially bounded integer Word-RAM time, not bit/Turing time or arbit
 3SUM. Its conservative exponent is `2-1/5184`; the sharper box-backed 1.9992 theorem is the
 separate [PR #2358](https://github.com/cslib-community/complexitylib/pull/2358).
 
+## Box-backed fixed-prime Exact Triangle
+
+To decide whether three signed integer matrices contain a zero-weight triangle, import
+`Complexity.Algorithms.WordRAM.ExactTriangle.BoxFixedPrime` and use
+`BoxFixedPrime.runs_input`. The complete
+[initialized client](https://github.com/cslib-community/complexitylib/blob/ddcdaef6055c7079c97d47fc121e2d5a7af8d44e/ComplexityTests/WordRAMExactTriangleBoxFixedPrime.lean)
+includes imports, admission proofs, successful witness recovery and negative exhaustion.
+Check that client on the endpoint revision before adapting it; this endpoint is introduced
+by [PR #2342](https://github.com/cslib-community/complexitylib/pull/2342).
+
+Provide `3*n²` signed weights in row-major AB, BC, AC order, with every absolute value at most
+`A`. `PreparationInput.input n (D m) g p values` supplies the scalar headers and canonical
+signed encoding; `State.init` stores the input length at address 0, places these raw words at
+successive addresses from 1, and zeroes the remaining memory. The
+geometric premises are `D m = 4^m >= 16`, `(D m)^18 <= n`, `g >= 1` and
+`p` in `Nat.sqrtPrimeWindow (D m)`. The physical width must satisfy
+`FixedPrime.admissionWidth n (D m) g p A <= W`. If application fails, check the list length,
+weight bound, prime-window inequalities and width against the complete client; the theorem
+does not select an admissible prime or geometry for you.
+
+The fixed 416-register program executes the producer once, then reuses dirty workspace for
+actual box-product calls and verifies candidates against the original signed weights. Its
+same-state prefix and charged halt return one exactly for an original zero triangle; on
+success, the returned state contains original vertex coordinates. The stated outer memory
+frame and producer registers are preserved. Raw input placement is an initial-state convention;
+the executed producer, controller and final halt are charged.
+
+For `m=9k`, apply `BoxFixedPrime.timeBound_le` to the actual producer memory returned by
+`runs_input`. Its complete finite bound retains preparation, aggregate box charges,
+root/query/controller overhead and **one global** `F(p)+1` original-weight scan reserve.
+The product term is `125829120(189k+1)^2(9k+1)D^(-8/125)n³g`; that saving alone is not an
+unconditional total exponent. The zero-weight and constant-257 negative clients are checked
+symbolic execution witnesses at admitted positive-threshold geometry, not interpreter runs
+or benchmarks.
+
+Global parameter/prime selection still uses the previous backend. Connecting this controller,
+absorbing polynomial factors and proving ordinary 3SUM exponent 1.9992 remain open under
+[#1394](https://github.com/cslib-community/complexitylib/issues/1394).
+
 ## Tree Evaluation
 
 The [Cook–Mertz endpoint](catalytic-and-tree-evaluation.md) computes the root of an explicitly table-encoded perfect binary tree in native independent workspace `O(log n · log log n)` for positive value length and height. The output is not charged to workspace, and the theorem leaves time existential. The same page distinguishes borrowed-register restoration and fan-in/packed procedure variants.