diff --git a/Complexity.lean b/Complexity.lean
index 7fc984d68..93d033d82 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1,6 +1,7 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
 public import Complexity.Algorithms.ExactTriangle.Defs
+public import Complexity.Algorithms.ExactTriangle.FailureAccounting
 public import Complexity.Algorithms.ExactTriangle.Hashing
 public import Complexity.Algorithms.ExactTriangle.Lopsided
 public import Complexity.Algorithms.ExactTriangle.PieceBounds
@@ -94,6 +95,20 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.Catalogue
 public import Complexity.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue
 public import Complexity.Algorithms.WordRAM.ExactTriangle.Chunks
 public import Complexity.Algorithms.WordRAM.ExactTriangle.Classes
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Accounting
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Controller
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Entry
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Flat
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Indexing
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Loop
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Potential
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Record
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.SourceBounds
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Step
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.TimeBound
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Width
 public import Complexity.Algorithms.WordRAM.ExactTriangle.InstancePair
 public import Complexity.Algorithms.WordRAM.ExactTriangle.Instances
 public import Complexity.Algorithms.WordRAM.ExactTriangle.MatrixSpec
@@ -101,6 +116,7 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.Parameters
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationAdjacency
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationBounds
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationInput
+public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationLocality
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationSpec
 public import Complexity.Algorithms.WordRAM.ExactTriangle.QueryScan
 public import Complexity.Algorithms.WordRAM.ExactTriangle.QuerySpec
@@ -127,6 +143,7 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Consume
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Entry
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Exec
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.FailureCount
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Failures
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Flat
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Header
diff --git a/Complexity/Algorithms/ExactTriangle/FailureAccounting.lean b/Complexity/Algorithms/ExactTriangle/FailureAccounting.lean
new file mode 100644
index 000000000..1ef3e3c28
--- /dev/null
+++ b/Complexity/Algorithms/ExactTriangle/FailureAccounting.lean
@@ -0,0 +1,86 @@
+/-
+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.ExactTriangle.Witnesses
+public import Mathlib.Data.Nat.Count
+import Mathlib.Data.List.GetD
+
+/-!
+# One false-positive budget for distinct record/query occurrences
+
+Lists within distinct existing instances inject into the existing global `failedScans` set.
+Consequently their failed accepted occurrences share one `falsePositiveCount` bound. This
+finite bridge does not multiply that bound by the number of records. A native caller must
+derive list membership, nonrepetition and answers from its actual execution/readback.
+
+The counting argument adapts `Host.FailedScans.sum_fails_le` from
+`anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`, using the existing local
+finite instances and failed-scan API rather than a second host-data model.
+-/
+
+public section
+
+namespace Cslib.Algorithms.ExactTriangle
+
+/-- Failed accepted occurrences across distinct records inject into the single global
+failed-scan set. Lists may be partial chunks, but each occurrence list must be repetition-free. -/
+theorem sum_failed_occurrences_le {n D g p : ℕ}
+    (wAB wBC wAC : Fin n → Fin n → ℤ) (hp : p ≠ 0)
+    (ans : InstanceIndex p → Fin n × Fin n → Bool)
+    (hans : AnswersCorrect wAB wBC wAC D g p ans)
+    (I : Finset (InstanceIndex p)) (hI : I ⊆ instanceIndices wAB D g p)
+    (queries : InstanceIndex p → List (Fin n × Fin n)) (default : Fin n × Fin n)
+    (hnodup : ∀ idx ∈ I, (queries idx).Nodup)
+    (hquery : ∀ idx ∈ I, ∀ q ∈ queries idx, q ∈ (lopInstance wAB wBC wAC D g p idx).W) :
+    (∑ idx ∈ I, Nat.count (fun j => ans idx ((queries idx).getD j default) = true ∧
+      scanPiece wAB wBC wAC D g idx.2.2
+        ((queries idx).getD j default).1 ((queries idx).getD j default).2 = none)
+      (queries idx).length) ≤ falsePositiveCount wAB wBC wAC p := by
+  classical
+  let P := fun idx j => ans idx ((queries idx).getD j default) = true ∧
+    scanPiece wAB wBC wAC D g idx.2.2
+      ((queries idx).getD j default).1 ((queries idx).getD j default).2 = none
+  let occurrences : Finset (Σ _ : InstanceIndex p, ℕ) :=
+    I.sigma fun idx => (Finset.range (queries idx).length).filter (P idx)
+  let failures := failedScans wAB wBC wAC D g p ans
+  have mem_occurrence (z : Σ _ : InstanceIndex p, ℕ) (hz : z ∈ occurrences) :
+      z.1 ∈ I ∧ z.2 < (queries z.1).length ∧ P z.1 z.2 := by
+    simpa only [occurrences, Finset.mem_sigma, Finset.mem_filter, Finset.mem_range,
+      and_assoc] using hz
+  have get_eq (idx : InstanceIndex p) (j : ℕ) (hj : j < (queries idx).length) :
+      (queries idx).getD j default = (queries idx).get ⟨j, hj⟩ := by
+    rw [List.getD_eq_getElem _ _ hj, List.get_eq_getElem]
+  let f : {z // z ∈ occurrences} → {s // s ∈ failures} := fun z =>
+    ⟨(z.val.1, (queries z.val.1).getD z.val.2 default), by
+      obtain ⟨hidx, hj, hacc, hnone⟩ := mem_occurrence z.val z.prop
+      apply Finset.mem_filter.mpr
+      refine ⟨mem_acceptedPairs.mpr ⟨hI hidx, ?_, hacc⟩, hnone⟩
+      exact hquery _ hidx _ (get_eq _ _ hj ▸ List.get_mem _ _)⟩
+  have hf : Function.Injective f := by
+    rintro ⟨⟨idx, j⟩, hx⟩ ⟨⟨idx', j'⟩, hy⟩ hxy
+    have he : idx = idx' := congrArg (fun s => s.val.1) hxy
+    subst idx'
+    obtain ⟨hidx, hj, -⟩ := mem_occurrence ⟨idx, j⟩ hx
+    obtain ⟨-, hj', -⟩ := mem_occurrence ⟨idx, j'⟩ hy
+    have hpair := congrArg (fun s => s.val.2) hxy
+    change (queries idx).getD j default = (queries idx).getD j' default at hpair
+    rw [get_eq idx j hj, get_eq idx j' hj'] at hpair
+    have hpos := List.nodup_iff_injective_get.mp (hnodup idx hidx) hpair
+    exact Subtype.ext (Sigma.ext rfl (heq_of_eq (congrArg Fin.val hpos)))
+  have hcard : (∑ idx ∈ I, Nat.count (P idx) (queries idx).length) = occurrences.card := by
+    simp only [occurrences, Finset.card_sigma, Nat.count_eq_card_filter_range]
+  change (∑ idx ∈ I, Nat.count (P idx) (queries idx).length) ≤ _
+  rw [hcard]
+  calc
+    _ = Fintype.card {z // z ∈ occurrences} := (Fintype.card_coe _).symm
+    _ ≤ Fintype.card {s // s ∈ failures} := Fintype.card_le_of_injective f hf
+    _ = failures.card := Fintype.card_coe _
+    _ ≤ falsePositiveCount wAB wBC wAC p := card_failedScans_le hp hans
+
+end Cslib.Algorithms.ExactTriangle
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime.lean
new file mode 100644
index 000000000..40bff2d99
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime.lean
@@ -0,0 +1,38 @@
+/-
+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.FixedPrime.SourceBounds
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.TimeBound
+
+/-!
+# Complete native ExactTriangle decision at a fixed admitted prime
+
+`FixedPrime.runs_input` executes one concrete 416-register standard-native program from the
+original signed input, with actual preparation once, all computed catalogue records and
+original-weight witness verification. Its same-state prefix/halt verdict is equivalent to
+original `HasZeroTriangle`; a successful state retains the original coordinates.
+
+`FixedPrime.timeBound_le` derives all-instance queried-product charges and one global
+false-positive scan budget. Preparation costs at most `690n²Dg`, product charges at most
+`138412032(19m+1)n³g/D^(1/18)`, with explicit additional root/query/controller and original
+scan terms. The total actual scans satisfy `S ≤ F(p)+returnedFlag`: empty/failed records do
+not each receive a successful-scan allowance. The runtime order is the producer's actual
+chunk-major order, without a precomputed record list or a clean-workspace premise.
+
+All initialized results require `D=4^m≥16`, `n≥D^18`, `g≥1`, the stated prime window and the
+original signed magnitude bound. The original-input threshold is positive, logarithmic for
+polynomial weights and bounded scalar headers, and works at every wider physical width.
+`FixedPrime.bounded_reachable_original` derives polynomial words and zero support above an
+original-input envelope independent of that larger width. The code never reads word width,
+has at most 133152 flat slots including halt, and performs no whole-window clear or snapshot.
+
+Global parameter/prime selection, unrestricted small geometry and the complete aggregate
+source exponent remain separate. This component does not complete ordinary 3SUM 1.9992.
+The stage execution lemmas in the submodules are internal implementation interfaces.
+-/
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Accounting.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Accounting.lean
new file mode 100644
index 000000000..43ca14ea9
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Accounting.lean
@@ -0,0 +1,115 @@
+/-
+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.ExactTriangle.FailureAccounting
+public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Indexing
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Failures
+
+/-!
+# Global accounting for actual catalogue query blocks
+
+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.FixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Existing original-weight witness condition restricted to one existing chunk and piece. -/
+@[expose] def recordHit {m n g p : ℕ} (values : ℕ → ℤ) (idx : InstanceIndex p) : Prop :=
+  ∃ q ∈ chunkOf (fun u v : Fin n => values (pairIndex (u, v))) (D m) p idx.1 idx.2.1,
+    ∃ c ∈ piece n (D m) g idx.2.2,
+      weightSum (fun u v : Fin n => values (pairIndex (u, v)))
+        (fun b c => values (n * n + pairIndex (b, c)))
+        (fun u c => values (2 * (n * n) + pairIndex (u, c))) q.1 q.2 c = 0
+
+/-- 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
+  RecordProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q + 61
+
+/-- Number of accepted queries without an original witness in one actual producer block.
+This is a value specification for charged native scans, not an executable scan oracle. -/
+@[expose] noncomputable def recordFailures {m n g p : ℕ} (hn : 0 < n)
+    (values : ℕ → ℤ) (mem : ℕ → ℕ) (idx : InstanceIndex p) : ℕ :=
+  let qs := RecordProduct.decodedQueries hn mem (RecordProduct.recordQueries n (D m) p idx)
+    (RecordProduct.recordQueryCount n (D m) p values idx)
+  let default : Fin n × Fin n := (⟨0, hn⟩, ⟨0, hn⟩)
+  Nat.count (fun i =>
+    (RecordProduct.leftMatrix m n g p values idx * RecordProduct.rightMatrix m n g p values idx)
+        (qs.getD i default).1 (qs.getD i default).2 ≠ 0 ∧
+      scanPiece (fun a b => values (pairIndex (a, b)))
+        (fun b c => values (n * n + pairIndex (b, c)))
+        (fun a c => values (2 * (n * n) + pairIndex (a, c))) (D m) g idx.2.2
+        (qs.getD i default).1 (qs.getD i default).2 = none) qs.length
+
+/-- Every original query occurs at most once in each actual chunk. -/
+theorem actual_queries_chunk {m n g p : ℕ} (hn : 0 < n) (values : ℕ → ℤ)
+    {initial a : Data 64} (h : Instances.Output n (D m) g p values initial a)
+    (hD : 16 ≤ D m) (hDn : D m ≤ n) (hp : p ≠ 0) (idx : InstanceIndex p)
+    (hidx : idx ∈ instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) (D m) g p) :
+    let qs := RecordProduct.decodedQueries hn a.mem (RecordProduct.recordQueries n (D m) p idx)
+      (RecordProduct.recordQueryCount n (D m) p values idx)
+    qs.Nodup ∧ qs.toFinset = chunkOf
+      (fun u v : Fin n => values (pairIndex (u, v))) (D m) p idx.1 idx.2.1 := by
+  let wAB := fun u v : Fin n => values (pairIndex (u, v))
+  have hc := QuerySpec.card_residueClass wAB hp
+    (fun q => (values q % (p : ℤ)).toNat) (by intro pair; rfl) idx.1
+  obtain ⟨-, hnodup, hset⟩ := RecordProduct.decodedQueries_chunkOf values wAB hn hp
+    (by intro u v; rfl) (by omega) hDn h idx.1 idx.2.1
+    ((mem_instanceIndices wAB idx).mp hidx).1
+  rw [hc] at hnodup hset
+  exact ⟨hnodup, hset⟩
+
+/-- Add distinct actual records before applying the global bound; no per-record false-positive
+allowance is duplicated. The real product's detection theorem supplies answer correctness. -/
+theorem sum_recordFailures_le {m n g p : ℕ} (hn : 0 < n) (values : ℕ → ℤ)
+    {initial a : Data 64} (h : Instances.Output n (D m) g p values initial a)
+    (hD : 16 ≤ D m) (hDn : D m ≤ n) (hg : 1 ≤ g)
+    (hp : p ∈ Nat.sqrtPrimeWindow (D m))
+    (I : Finset (InstanceIndex p))
+    (hI : I ⊆ instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) (D m) g p) :
+    (∑ idx ∈ I, recordFailures (m := m) (g := g) hn values a.mem idx) ≤
+      falsePositiveCount (fun u v : Fin n => values (pairIndex (u, v)))
+        (fun b c => values (n * n + pairIndex (b, c)))
+        (fun u c => values (2 * (n * n) + pairIndex (u, c))) p := by
+  classical
+  let wAB := fun u v : Fin n => values (pairIndex (u, v))
+  let wBC := fun b c : Fin n => values (n * n + pairIndex (b, c))
+  let wAC := fun u c : Fin n => values (2 * (n * n) + pairIndex (u, c))
+  let queries := fun idx => RecordProduct.decodedQueries hn a.mem
+    (RecordProduct.recordQueries n (D m) p idx)
+    (RecordProduct.recordQueryCount n (D m) p values idx)
+  let ans := fun (idx : InstanceIndex p) (q : Fin n × Fin n) => decide
+    ((RecordProduct.leftMatrix m n g p values idx *
+      RecordProduct.rightMatrix m n g p values idx) q.1 q.2 ≠ 0)
+  have hp0 := (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.ne_zero
+  have hans : AnswersCorrect wAB wBC wAC (D m) g p ans :=
+    RecordProduct.product_answers_correct values wAB wBC wAC hD hg hp
+      (by intro b c; rfl) (by intro u c; rfl)
+  have hquery (idx) (hi : idx ∈ I) :=
+    actual_queries_chunk hn values h hD hDn hp0 idx (hI hi)
+  have hbound := sum_failed_occurrences_le wAB wBC wAC hp0 ans hans I hI queries
+    (⟨0, hn⟩, ⟨0, hn⟩) (fun idx hi => (hquery idx hi).1) (by
+      intro idx hi q hq
+      change q ∈ chunkOf wAB (D m) p idx.1 idx.2.1
+      rw [← (hquery idx hi).2, List.mem_toFinset]
+      exact hq)
+  simpa only [recordFailures, queries, ans, decide_eq_true_eq] using hbound
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Controller.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Controller.lean
new file mode 100644
index 000000000..29bca5009
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Controller.lean
@@ -0,0 +1,87 @@
+/-
+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.FixedPrime.Program
+
+/-!
+# Charged catalogue-controller setup and return
+
+The occupied count is read from the real producer bank. The return code adds the actual
+callee scan count, retains its actual unsigned flag, advances the visited prefix and closes
+the loop only after success. These internal rules use concrete data instructions; neither
+the scan count nor the verdict is supplied as an execution oracle.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
+
+open Cslib.WordRAM
+
+-- These closed checks cover only the short controller and its finite register bank.
+set_option maxRecDepth 4096 in
+private theorem setup_preserves : ∀ i : Fin 416, i.val < 400 → setup.Preserves i := by
+  decide
+
+-- The return branch writes four controller registers and no part of the callee bank.
+set_option maxRecDepth 4096 in
+private theorem receive_preserves : ∀ i : Fin 416,
+    i.val < 400 ∨ i = Reg.one → receive.Preserves i := by decide
+
+/-- Read the actual occupied count, with all five initialization instructions charged. -/
+theorem exec_setup {w : ℕ} (x : Data 416) (h1 : Fits w 1) :
+    ∃ y, ExecWithin w setup x y 5 ∧ y.mem = x.mem ∧
+      y.regs Reg.index = 0 ∧
+      y.regs Reg.limit = x.regs (recordBank
+        (RecordWitness.productBank (RecordProduct.producerBank Instances.produced))) ∧
+      y.regs Reg.found = 0 ∧ y.regs Reg.scans = 0 ∧
+      y.regs Reg.one = 1 ∧
+      ∀ j : Fin 416, j.val < 400 → y.regs j = x.regs j := by
+  let M := x.regs (recordBank
+    (RecordWitness.productBank (RecordProduct.producerBank Instances.produced)))
+  let y := x.set Reg.index 0 |>.set Reg.limit M |>.set Reg.found 0 |>.set Reg.scans 0
+    |>.set Reg.one 1
+  have he : ExecWithin w setup x y 5 := by
+    ram_eval [setup, y, M, h1, Reg.index, Reg.limit, Reg.found, Reg.scans, Reg.one,
+      recordBank, RecordWitness.productBank, RecordProduct.producerBank,
+      Instances.produced, Fin.castLE]
+  refine ⟨y, he, rfl, ?_, ?_, ?_, ?_, ?_, fun j hj =>
+    he.regs_eq (setup_preserves j hj)⟩
+  all_goals simp +decide [y, M, Reg.index, Reg.limit, Reg.found, Reg.scans, Reg.one]
+
+/-- The native return needs at most six instructions, including control. Its limit
+is shortened exactly when the actual callee flag equals one. The complete callee bank survives. -/
+theorem exec_receive {w i limit S performed flag : ℕ} (x : Data 416)
+    (hi : x.regs Reg.index = i) (hl : x.regs Reg.limit = limit)
+    (hs : x.regs Reg.scans = S)
+    (hp : x.regs (recordBank RecordWitness.Reg.scans) = performed)
+    (hf : x.regs (recordBank RecordWitness.Reg.found) = flag)
+    (h1 : x.regs Reg.one = 1) (hS : Fits w (S + performed)) (hI : Fits w (i + 1)) :
+    ∃ y, ExecWithin w receive x y 6 ∧ y.mem = x.mem ∧
+      y.regs Reg.index = i + 1 ∧ y.regs Reg.limit = (if flag = 1 then i + 1 else limit) ∧
+      y.regs Reg.scans = S + performed ∧ y.regs Reg.found = flag ∧
+      ∀ j : Fin 416, j.val < 400 ∨ j = Reg.one →
+        y.regs j = x.regs j := by
+  dsimp only [Reg.index, Reg.limit, Reg.scans, Reg.one, recordBank,
+    RecordWitness.Reg.found, RecordWitness.Reg.scans, Fin.castLE] at hi hl hs hp hf h1
+  let y := x.set Reg.scans (S + performed) |>.set Reg.found flag |>.set Reg.index (i + 1)
+    |>.set Reg.limit (if flag = 1 then i + 1 else limit)
+  have he : ExecWithin w receive x y 6 := by
+    by_cases hflag : flag = 1
+    · ram_eval [receive, y, hi, hl, hs, hp, hf, h1, hS, hI, hflag,
+        Reg.index, Reg.limit, Reg.found, Reg.scans, Reg.one, recordBank,
+        RecordWitness.Reg.found, RecordWitness.Reg.scans, Fin.castLE]
+    · ram_eval [receive, y, hi, hl, hs, hp, hf, h1, hS, hI, hflag,
+        Reg.index, Reg.limit, Reg.found, Reg.scans, Reg.one, recordBank,
+        RecordWitness.Reg.found, RecordWitness.Reg.scans, Fin.castLE]
+  refine ⟨y, he, rfl, ?_, ?_, ?_, ?_, fun j hj =>
+    he.regs_eq (receive_preserves j hj)⟩
+  all_goals simp +decide [y, Reg.index, Reg.limit, Reg.found, Reg.scans]
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Entry.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Entry.lean
new file mode 100644
index 000000000..0f0379d01
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Entry.lean
@@ -0,0 +1,137 @@
+/-
+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.FixedPrime.Loop
+
+/-!
+# Initialized 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.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.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Flat.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Flat.lean
new file mode 100644
index 000000000..f75a94fec
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Flat.lean
@@ -0,0 +1,94 @@
+/-
+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.FixedPrime.Entry
+
+/-!
+# Initialized 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.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.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Indexing.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Indexing.lean
new file mode 100644
index 000000000..fd74b2c48
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Indexing.lean
@@ -0,0 +1,91 @@
+/-
+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.Readback
+public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationLocality
+
+/-!
+# The actual occupied ordinals name the existing finite instances
+
+The producer's real counter supplies the range, and its existing dependent-sum readback
+supplies the unique residue/chunk/piece for each ordinal. These are consequences of output,
+not a second enumeration or a list supplied to the native controller.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+
+/-- Every occupied runtime ordinal has exactly one existing finite meaning. -/
+theorem occupied_index_unique {n D g p i : ℕ} (values : ℕ → ℤ)
+    {initial a : Data 64} (h : Instances.Output n D g p values initial a)
+    (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ≠ 0)
+    (hi : i < a.regs Instances.produced) :
+    ∃! idx : InstanceIndex p,
+      idx ∈ instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) D g p ∧
+        RecordProduct.recordOrdinal n D g p values idx = i := by
+  have hc := h.2.2.2.2.1
+  rw [hc] at hi
+  obtain ⟨idx, hidx, huniq⟩ := PreparationSpec.index_unique values
+    (fun u v : Fin n => values (pairIndex (u, v))) hp (by intro u v; rfl)
+    hD hDn hg i hi
+  refine ⟨idx, ⟨hidx.1, hidx.2.symm⟩, fun other hother => ?_⟩
+  exact huniq other ⟨hother.1, hother.2.symm⟩
+
+/-- The actual occupied range enumerates every existing instance exactly once. This is a
+proof-side interpretation of the native ordinal, not a table consumed by the program. -/
+theorem exists_occupied_order {n D g p : ℕ} (values : ℕ → ℤ)
+    {initial a : Data 64} (h : Instances.Output n D g p values initial a)
+    (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ≠ 0) :
+    ∃ f : Fin (a.regs Instances.produced) → InstanceIndex p,
+      Function.Injective f ∧
+      (∀ i, f i ∈ instanceIndices
+        (fun u v : Fin n => values (pairIndex (u, v))) D g p ∧
+        RecordProduct.recordOrdinal n D g p values (f i) = i.val) ∧
+      ∀ idx ∈ instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) D g p,
+        ∃ i, f i = idx := by
+  classical
+  let I := instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) D g p
+  have he (i : Fin (a.regs Instances.produced)) : ∃ idx, idx ∈ I ∧
+      RecordProduct.recordOrdinal n D g p values idx = i.val :=
+    (occupied_index_unique values h hD hDn hg hp i.isLt).exists
+  choose f hf using he
+  have hinj : Function.Injective f := by
+    intro i j hij
+    apply Fin.ext
+    exact (hf i).2.symm.trans ((congrArg
+      (RecordProduct.recordOrdinal n D g p values) hij).trans (hf j).2)
+  let f' : Fin (a.regs Instances.produced) → I := fun i => ⟨f i, (hf i).1⟩
+  have hinj' : Function.Injective f' := fun _ _ hij =>
+    hinj (congrArg Subtype.val hij)
+  have hcard : Fintype.card (Fin (a.regs Instances.produced)) = Fintype.card I := by
+    simpa only [Fintype.card_fin, Fintype.card_coe, I] using
+      PreparationSpec.count_eq_card values _ hp (by intro u v; rfl) h
+  have hsurj := ((Fintype.bijective_iff_injective_and_card f').mpr ⟨hinj', hcard⟩).2
+  refine ⟨f, hinj, hf, ?_⟩
+  intro idx hidx
+  obtain ⟨i, hi⟩ := hsurj ⟨idx, hidx⟩
+  exact ⟨i, congrArg Subtype.val hi⟩
+
+/-- Original interleaved query readback survives changes outside its protected span. -/
+theorem decodedQueries_eq_of_eqOn {n q Q heap : ℕ} (hn : 0 < n)
+    (x y : ℕ → ℕ) (h : Set.EqOn x y (Set.Iio heap)) (hspan : q + 2 * Q ≤ heap) :
+    RecordProduct.decodedQueries hn x q Q = RecordProduct.decodedQueries hn y q Q := by
+  unfold RecordProduct.decodedQueries
+  apply congrArg List.ofFn
+  funext i
+  apply Prod.ext <;> apply Fin.ext
+  · change x (q + 2 * i.val) % n = y (q + 2 * i.val) % n
+    rw [h (by have := i.isLt; change q + 2 * i.val < heap; omega)]
+  · change x (q + 2 * i.val + 1) % n = y (q + 2 * i.val + 1) % n
+    rw [h (by have := i.isLt; change q + 2 * i.val + 1 < heap; omega)]
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Loop.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Loop.lean
new file mode 100644
index 000000000..8283536cb
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Loop.lean
@@ -0,0 +1,271 @@
+/-
+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.FixedPrime.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.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.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Potential.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Potential.lean
new file mode 100644
index 000000000..450568fe2
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Potential.lean
@@ -0,0 +1,75 @@
+/-
+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.Init
+public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Tactic.Ring
+
+/-!
+# Paying for the native catalogue traversal
+
+The remaining potential reserves one successful scan in total. A failed call consumes only
+its own distinct failed occurrences; a successful call consumes that reserve and terminates
+the traversal. These internal arithmetic lemmas do not provide an execution or cost oracle.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
+
+/-- One actual return consumes its failed occurrences and, only on success, the single reserve.
+The base charge includes this iteration's real call/controller/loop overhead. -/
+theorem pay_return {T base C scans failures flag restBase restFailures : ℕ}
+    (hT : T + 2 ≤ base + C * scans) (hscans : scans ≤ failures + flag)
+    (hflag : flag ≤ 1) :
+    T + 2 + (restBase + C * (restFailures + 1 - flag)) ≤
+      base + restBase + C * (failures + restFailures + 1) := by
+  have he : failures + flag + (restFailures + 1 - flag) =
+      failures + restFailures + 1 := by omega
+  have hpaid := Nat.mul_le_mul_left C hscans
+  calc
+    _ ≤ base + C * (failures + flag) +
+        (restBase + C * (restFailures + 1 - flag)) := by omega
+    _ = base + restBase + C * (failures + flag + (restFailures + 1 - flag)) := by ring
+    _ = _ := by rw [he]
+
+/-- Nonnegative charges in a visited prefix are bounded by those in the complete range. -/
+theorem sum_prefix_le (charge : ℕ → ℕ) {i M : ℕ} (hi : i ≤ M) :
+    ∑ j ∈ Finset.range i, charge j ≤ ∑ j ∈ Finset.range M, charge j :=
+  Finset.sum_le_sum_of_subset (Finset.range_mono hi)
+
+/-- Reserve potential for a concrete finite sequence of base and failed-occurrence charges. -/
+@[expose] def remainingCharge (base failures : ℕ → ℕ) (C M i flag : ℕ) : ℕ :=
+  ((∑ j ∈ Finset.range M, base j) - (∑ j ∈ Finset.range i, base j)) +
+    C * (((∑ j ∈ Finset.range M, failures j) -
+      (∑ j ∈ Finset.range i, failures j)) + 1 - flag)
+
+/-- The actual per-call bound decreases the potential by the charged body and loop work.
+The loop invariant establishes zero prior success whenever its guard still holds. -/
+theorem remainingCharge_step {base failures : ℕ → ℕ} {C M i T scans flag : ℕ}
+    (hi : i < M) (hT : T + 2 ≤ base i + C * scans)
+    (hscans : scans ≤ failures i + flag) (hflag : flag ≤ 1) :
+    T + 2 + remainingCharge base failures C M (i + 1) flag ≤
+      remainingCharge base failures C M i 0 := by
+  have hB := sum_prefix_le base (Nat.succ_le_of_lt hi)
+  have hF := sum_prefix_le failures (Nat.succ_le_of_lt hi)
+  rw [Finset.sum_range_succ] at hB hF
+  have eqB : (∑ j ∈ Finset.range M, base j) - (∑ j ∈ Finset.range i, base j) =
+      base i + ((∑ j ∈ Finset.range M, base j) -
+        ((∑ j ∈ Finset.range i, base j) + base i)) := by omega
+  have eqF : (∑ j ∈ Finset.range M, failures j) - (∑ j ∈ Finset.range i, failures j) =
+      failures i + ((∑ j ∈ Finset.range M, failures j) -
+        ((∑ j ∈ Finset.range i, failures j) + failures i)) := by omega
+  unfold remainingCharge
+  rw [Finset.sum_range_succ, Finset.sum_range_succ, eqB, eqF]
+  simpa only [Nat.sub_zero, Nat.add_assoc] using pay_return hT hscans hflag
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Program.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Program.lean
new file mode 100644
index 000000000..062e51944
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Program.lean
@@ -0,0 +1,107 @@
+/-
+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
+
+/-!
+# Native traversal of the occupied ExactTriangle catalogue
+
+The producer runs once. The controller visits actual occupied ordinals and invokes the complete
+400-register record-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.FixedPrime
+
+open Cslib.WordRAM
+
+/-- The complete record-product/witness bank moves together, including both internal banks. -/
+@[expose] def recordBank : Fin 400 → Fin 416 := Fin.castLE (by decide)
+
+namespace Reg
+
+/-- Number of actual occupied records visited. -/
+abbrev index : Fin 416 := 400
+/-- Original occupied count, shortened to the visited prefix only after success. -/
+abbrev limit : Fin 416 := 401
+/-- Raw unsigned original-witness verdict. -/
+abbrev found : Fin 416 := 402
+/-- Total actual original-weight scans across all visited records. -/
+abbrev scans : Fin 416 := 403
+/-- Constant one outside the callee bank. -/
+abbrev one : Fin 416 := 404
+end Reg
+
+/-- Execute the actual producer once, without changing its finite instruction graph. -/
+@[expose] def produce : Code .standard 416 := RecordWitness.produce.rename recordBank
+
+open Reg in
+/-- Read the actual producer count and initialize the native controller. -/
+@[expose] def setup : Code .standard 416 :=
+  let count := recordBank
+    (RecordWitness.productBank (RecordProduct.producerBank Instances.produced))
+  ram[ index ← #0; limit ← count; found ← #0; scans ← #0; one ← #1 ]
+
+open Reg in
+/-- Deliver the actual ordinal to the concrete callee. -/
+@[expose] def select : Code .standard 416 :=
+  .op (.copy (recordBank (RecordWitness.productBank RecordProduct.Reg.ordinal)) index)
+
+/-- Actual product computation, descriptor reading and original signed-weight verification. -/
+@[expose] def record : Code .standard 416 := RecordWitness.program.rename recordBank
+
+open Reg in
+/-- Accumulate the actual scan counter and close the loop exactly on a successful return. -/
+@[expose] def receive : Code .standard 416 :=
+  let returned := recordBank RecordWitness.Reg.found
+  let performed := recordBank RecordWitness.Reg.scans
+  ram[ scans ← scans + performed; found ← returned; index ← index + one;
+    if found = one then [ limit ← index ] else [ limit ← limit ] ]
+
+/-- 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 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, RecordWitness.program,
+      Code.size, Code.size_rename]
+    have hp := Instances.program_fixed.1
+    have hr := RecordProduct.program_fixed.1
+    have hc := RecordWitness.consume_fixed.1
+    omega
+  · apply Code.not_readsWidth_program
+    simp only [program, produce, traverse, setup, step, select, record, receive,
+      RecordWitness.produce, RecordProduct.produce, RecordWitness.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 ⟨RecordProduct.program_fixed.2, RecordWitness.consume_fixed.2⟩⟩
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Record.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Record.lean
new file mode 100644
index 000000000..ec4b0c690
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Record.lean
@@ -0,0 +1,219 @@
+/-
+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.FixedPrime.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.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
+        (RecordProduct.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⟩ :=
+    RecordWitness.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 RecordWitness.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
+      (RecordProduct.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.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/SourceBounds.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/SourceBounds.lean
new file mode 100644
index 000000000..bbe40d1b9
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/SourceBounds.lean
@@ -0,0 +1,83 @@
+/-
+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.FixedPrime.Flat
+import Complexity.Foundations.Data.Nat.Log
+
+/-!
+# Original-input 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.FixedPrime
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- A fixed original-input bound for all prefix words and memory support. -/
+@[expose] def wordBound (n D g p A : ℕ) : ℕ := 2 ^ admissionWidth n D g p A
+
+/-- The all-record controller retains an explicit polynomial envelope for each weight exponent. -/
+theorem wordBound_le_pow {n D g p A κ : ℕ} (hn : 1 ≤ n)
+    (hD : D ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) :
+    wordBound n D g p A ≤ (n + 2) ^ (514 * κ + 11818) := by
+  let b := n + 2
+  have hb : 2 ≤ b := by dsimp only [b]; omega
+  have hbase : 2 ^ Nat.clog 2 b ≤ b ^ 2 :=
+    (Nat.pow_clog_le_mul (by decide : 1 < (2 : ℕ)) (by omega : b ≠ 0)).trans
+      (by nlinarith only [hb])
+  have hw := admissionWidth_le_log hn hD hg hp hA
+  change 2 ^ admissionWidth n D g p A ≤ _
+  calc
+    _ ≤ 2 ^ ((257 * κ + 5909) * Nat.clog 2 b) := Nat.pow_le_pow_right (by decide) hw
+    _ = (2 ^ Nat.clog 2 b) ^ (257 * κ + 5909) := by rw [← Nat.pow_mul, Nat.mul_comm]
+    _ ≤ (b ^ 2) ^ (257 * κ + 5909) := Nat.pow_le_pow_left hbase _
+    _ = b ^ (514 * κ + 11818) := by
+      rw [← Nat.pow_mul]
+      exact congrArg (fun j : ℕ => b ^ j) (by omega : 2 * (257 * κ + 5909) = 514 * κ + 11818)
+
+/-- 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.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Step.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Step.lean
new file mode 100644
index 000000000..afc37d1d5
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Step.lean
@@ -0,0 +1,143 @@
+/-
+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.FixedPrime.Record
+
+/-!
+# 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.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 := RecordProduct.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.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/TimeBound.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/TimeBound.lean
new file mode 100644
index 000000000..725b4bb1e
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/TimeBound.lean
@@ -0,0 +1,119 @@
+/-
+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.FixedPrime.Flat
+import Mathlib.Tactic.Positivity
+
+/-!
+# Aggregate native fixed-prime charges
+
+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.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 {m n g p : ℕ} (hn : 0 < n) (values : ℕ → ℤ) (mem : ℕ → ℕ)
+    (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n) :
+    let I := instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) (D m) g p
+    let qs := fun idx => RecordProduct.decodedQueries hn mem
+      (RecordProduct.recordQueries n (D m) p idx)
+      (RecordProduct.recordQueryCount n (D m) p values idx)
+    ((∑ idx ∈ I, (RecordProduct.timeBound (m := m) (qs idx) + 1) : ℕ) : ℝ) ≤
+      138412032 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 3 * g /
+        (D m : ℝ) ^ (1 / 18 : ℝ) := by
+  let I := instanceIndices (fun u v : Fin n => values (pairIndex (u, v))) (D m) g p
+  let qs := fun idx => RecordProduct.decodedQueries hn mem
+    (RecordProduct.recordQueries n (D m) p idx)
+    (RecordProduct.recordQueryCount n (D m) p values idx)
+  let R : ℝ := 34603008 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 2 /
+    (D m : ℝ) ^ (1 / 18 : ℝ)
+  have hr (idx : InstanceIndex p) :
+      ((RecordProduct.timeBound (m := m) (qs idx) + 1 : ℕ) : ℝ) ≤ R := by
+    apply RecordProduct.thin_timeBound_sparse _ hN
+    rw [RecordProduct.decodedQueries_length]
+    exact (Nat.mul_le_mul_right (2 ^ m) (min_le_left _ _)).trans
+      (RecordProduct.queryCap_mul_two_pow_le n m)
+  have hc : (I.card : ℝ) ≤ 4 * (n : ℝ) * g := by
+    exact card_instanceIndices_le _ hD
+      ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN) hg hp
+  calc
+    _ = ∑ idx ∈ I, ((RecordProduct.timeBound (m := m) (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 {m n g p : ℕ} (hn : 0 < n) (values : List ℤ) (mem : ℕ → ℕ)
+    (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 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 := m) hn g p values mem : ℕ) : ℝ) ≤
+      690 * (n : ℝ) ^ 2 * D m * g +
+        138412032 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 3 * g /
+          (D m : ℝ) ^ (1 / 18 : ℝ) +
+        (4 * (n : ℝ) * g) * ((5 * Nat.sqrt (D m) + 8 * queryCap n (D m) + 61 : ℕ) : ℝ) +
+        (((42 * pieceSize (D m) 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 m) g p
+  let qs := fun idx => RecordProduct.decodedQueries hn mem
+    (RecordProduct.recordQueries n (D m) p idx)
+    (RecordProduct.recordQueryCount n (D m) p V idx)
+  let extra := 5 * Nat.sqrt (D m) + 8 * queryCap n (D m) + 61
+  have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN
+  have hprep : (RecordProduct.preparationTime n (D m) g p values : ℝ) ≤
+      690 * (n : ℝ) ^ 2 * D m * g := by
+    have hnat : RecordProduct.preparationTime n (D m) g p values ≤ 690 * n ^ 2 * D m * 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 := m) hn V mem idx) ≤
+      (∑ idx ∈ I, (RecordProduct.timeBound (m := m) (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 m) p V idx ≤ queryCap n (D m) :=
+      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 := m) hn V mem idx : ℕ) : ℝ) ≤
+      138412032 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 3 * g /
+          (D m : ℝ) ^ (1 / 18 : ℝ) + (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.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Width.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Width.lean
new file mode 100644
index 000000000..f95a3685f
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Width.lean
@@ -0,0 +1,141 @@
+/-
+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.FixedPrime.Indexing
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.SourceBounds
+
+/-!
+# Original-input bounds for the catalogue controller
+
+The controller's counters fit from original scalar dimensions. A coarse polynomial counter
+bound is used only for physical admission; charged scan accounting uses the single global
+false-positive count instead. No intermediate counter fit is supplied by the caller.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+
+/-- A polynomial envelope for ordinal and accumulated scan-counter arithmetic. -/
+@[expose] def counterEnvelope (n p : ℕ) : ℕ :=
+  (p * n * n * n + 1) * (n * n + 1) + n + 64
+
+/-- Original-input threshold for the unchanged record code and its new controller. -/
+@[expose] def admissionWidth (n D g p A : ℕ) : ℕ :=
+  max (RecordWitness.admissionWidth n D g p A) (Nat.clog 2 (counterEnvelope n p) + 1)
+
+/-- The original-input physical threshold is positive even before imposing source geometry. -/
+theorem admissionWidth_pos (n D g p A : ℕ) : 0 < admissionWidth n D g p A := by
+  unfold admissionWidth
+  omega
+
+/-- The real occupied count has a polynomial bound without inspecting a workspace. -/
+theorem produced_le {n D g p : ℕ} (values : ℕ → ℤ)
+    {initial a : Data 64} (h : Instances.Output n D g p values initial a)
+    (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) :
+    a.regs Instances.produced ≤ p * n * n * n := by
+  let C := fun rho => Nat.count (fun q => (values q % (p : ℤ)).toNat = rho) (n * n)
+  have hK : ChunkCatalogue.before C (queryCap n D) p ≤ p * (n * n) :=
+    ChunkCatalogue.before_le (one_le_queryCap (by omega) hDn)
+      (fun _ _ => Nat.count_le _) (le_refl p)
+  have hH : numPieces n D g ≤ n :=
+    (Nat.ceilDiv_le_iff (pieceSize_pos hD hg)).mpr
+      (Nat.le_mul_of_pos_right n (pieceSize_pos hD hg))
+  have hc := h.2.2.2.2.1
+  change a.regs Instances.produced = ChunkCatalogue.before C (queryCap n D) p *
+    numPieces n D g at hc
+  rw [hc]
+  exact (Nat.mul_le_mul hK hH).trans_eq (by ring)
+
+/-- All record query-occurrence counts are at most the number of original pairs. -/
+theorem recordQueryCount_le (n D p : ℕ) (values : ℕ → ℤ) (idx : InstanceIndex p) :
+    RecordProduct.recordQueryCount n D p values idx ≤ n * n := by
+  unfold RecordProduct.recordQueryCount
+  exact (min_le_right _ _).trans ((Nat.sub_le _ _).trans (Nat.count_le _))
+
+/-- Every larger admitted physical width contains the complete accumulated-counter bound. -/
+theorem counter_fits {W n D g p A : ℕ} (hW : admissionWidth n D g p A ≤ W) :
+    Fits W (counterEnvelope n p) := by
+  have hc : Nat.clog 2 (counterEnvelope n p) < W := by
+    unfold admissionWidth at hW
+    omega
+  exact (Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) _).trans_lt
+    (Nat.pow_lt_pow_right (by decide : 1 < (2 : ℕ)) hc)
+
+/-- The controller threshold retains the original concrete callee admission. -/
+theorem record_admitted {W n D g p A : ℕ} (hW : admissionWidth n D g p A ≤ W) :
+    RecordWitness.admissionWidth n D g p A ≤ W := (le_max_left _ _).trans hW
+
+/-- Before each actual return, both counters fit solely from original dimensions and the
+coarse visited-prefix bounds. This is not the charged false-positive estimate. -/
+theorem return_fits {W n D g p A M i S performed : ℕ}
+    (hW : admissionWidth n D g p A ≤ W) (hM : M ≤ p * n * n * n)
+    (hi : i < M) (hS : S ≤ i * (n * n + 1)) (hp : performed ≤ n * n + 1) :
+    Fits W (S + performed) ∧ Fits W (i + 1) := by
+  have hsum : S + performed ≤ (i + 1) * (n * n + 1) := by
+    rw [Nat.add_mul, Nat.one_mul]
+    omega
+  have hnext : i + 1 ≤ p * n * n * n + 1 := by omega
+  have hprod := Nat.mul_le_mul_right (n * n + 1) hnext
+  have hlinear : i + 1 ≤ (p * n * n * n + 1) * (n * n + 1) :=
+    hnext.trans (Nat.le_mul_of_pos_right _ (by omega))
+  exact ⟨(counter_fits hW).of_le (by unfold counterEnvelope; omega),
+    (counter_fits hW).of_le (by unfold counterEnvelope; omega)⟩
+
+/-- The additional counters do not increase the existing original-input logarithmic constant.
+All source-regime bounds remain explicit; this is not a bound for arbitrary scalar headers. -/
+theorem admissionWidth_le_log {n D g p A κ : ℕ} (hn : 1 ≤ n)
+    (hD : D ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) :
+    admissionWidth n D g p A ≤ (257 * κ + 5909) * Nat.clog 2 (n + 2) := by
+  let b := n + 2
+  have hb : 2 ≤ b := by dsimp only [b]; omega
+  have hb1 : 1 ≤ b := by omega
+  have hnB : n ≤ b := by dsimp only [b]; omega
+  have hfour : p * n * n * n ≤ b ^ 4 := by
+    calc
+      _ ≤ b * b * b * b := Nat.mul_le_mul
+        (Nat.mul_le_mul (Nat.mul_le_mul (hp.trans hnB) hnB) hnB) hnB
+      _ = b ^ 4 := by ring
+  have htwo : n * n ≤ b ^ 2 := by simpa only [pow_two] using Nat.mul_le_mul hnB hnB
+  have h4pos : 1 ≤ b ^ 4 := Nat.one_le_pow _ _ hb1
+  have h2pos : 1 ≤ b ^ 2 := Nat.one_le_pow _ _ hb1
+  have hleft : p * n * n * n + 1 ≤ b ^ 5 := by
+    calc
+      _ ≤ 2 * b ^ 4 := by omega
+      _ ≤ b * b ^ 4 := Nat.mul_le_mul_right _ hb
+      _ = b ^ 5 := by ring
+  have hright : n * n + 1 ≤ b ^ 3 := by
+    calc
+      _ ≤ 2 * b ^ 2 := by omega
+      _ ≤ b * b ^ 2 := Nat.mul_le_mul_right _ hb
+      _ = b ^ 3 := by ring
+  have hprod : (p * n * n * n + 1) * (n * n + 1) ≤ b ^ 8 :=
+    (Nat.mul_le_mul hleft hright).trans_eq (by ring)
+  have hn8 : n ≤ b ^ 8 := hnB.trans (Nat.le_self_pow (by decide) b)
+  have hc : 64 ≤ b ^ 8 := (show 64 ≤ (2 : ℕ) ^ 8 by decide).trans
+    (Nat.pow_le_pow_left hb 8)
+  have he : counterEnvelope n p ≤ b ^ 10 := by
+    calc
+      _ ≤ 3 * b ^ 8 := by unfold counterEnvelope; omega
+      _ ≤ b ^ 2 * b ^ 8 := Nat.mul_le_mul_right _
+        ((show 3 ≤ (2 : ℕ) ^ 2 by decide).trans (Nat.pow_le_pow_left hb 2))
+      _ = b ^ 10 := by ring
+  have hlogBound := he.trans (Nat.pow_le_pow_left
+    (Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) b) 10)
+  rw [← Nat.pow_mul] at hlogBound
+  have hlog := Nat.clog_le_of_le_pow hlogBound
+  have hpos : 1 ≤ Nat.clog 2 b := Nat.clog_pos (by decide) (by omega : 1 < b)
+  have hcounter : Nat.clog 2 (counterEnvelope n p) + 1 ≤
+      (257 * κ + 5909) * Nat.clog 2 b := by
+    nlinarith only [hlog, hpos, Nat.zero_le (κ * Nat.clog 2 b)]
+  exact max_le (RecordWitness.admissionWidth_le_log hn hD hg hp hA) hcounter
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationLocality.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationLocality.lean
new file mode 100644
index 000000000..8b1b5611b
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationLocality.lean
@@ -0,0 +1,114 @@
+/-
+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.Instances
+
+/-!
+# Prepared catalogue readback after workspace reuse
+
+Every catalogue, query, record and matrix word described by `Instances.Output` lies below its
+heap boundary. A consumer may change the workspace above that boundary while preserving all
+those words and the producer registers. The readback contract can then be framed against the
+current state. This does not assert that the producer ran again, or that its original external
+frame survived: the original producer execution and its initial state remain separate facts.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.Instances
+
+open Cslib.WordRAM Cslib.Algorithms.ExactTriangle
+
+/-- Transport the actual prepared readback through changes above the heap. The new frame is
+relative to the current state, not to the original producer input. No execution is asserted. -/
+theorem Output.reframe {n D g p : ℕ} (values : ℕ → ℤ) {initial y z : Data 64}
+    (h : Output n D g p values initial y) (hregs : z.regs = y.regs)
+    (hmem : Set.EqOn z.mem y.mem (Set.Iio (y.regs heap))) :
+    Output n D g p values z z := by
+  let N := n * n
+  let R := fun q => (values q % (p : ℤ)).toNat
+  let C := fun rho => Nat.count (fun q => R q = rho) N
+  let K := ChunkCatalogue.before C (queryCap n D) p
+  let H := numPieces n D g
+  let B := pieceSize D g
+  let desc := 5 + 6 * N + p + 2 * N * p
+  let out := desc + 3 * K
+  let stop := out + (K * H) * (6 + 2 * (n * D))
+  obtain ⟨hn, hD, hp, ho, hc, hh, hr, hcounts, hqueries, hdesc, hblocks, -⟩ := h
+  change y.regs heap = stop at hh
+  have mem_eq (a : ℕ) (ha : a < stop) : z.mem a = y.mem a :=
+    hmem (by simpa only [Set.mem_Iio, hh] using ha)
+  have hdescOut : desc ≤ out := by dsimp only [out]; omega
+  have houtStop : out ≤ stop := Nat.le_add_right _ _
+  have desc_lt (i : ℕ) (hi : i < K) : desc + 3 * i + 2 < stop := by
+    have hm := Nat.mul_le_mul_left 3 (Nat.succ_le_of_lt hi)
+    rw [Nat.mul_succ] at hm
+    dsimp only [out] at houtStop
+    omega
+  refine ⟨hregs ▸ hn, hregs ▸ hD, hregs ▸ hp, hregs ▸ ho, hregs ▸ hc,
+    hregs ▸ hh, ?_, ?_, ?_, ?_, ?_, fun _ _ => rfl⟩
+  · intro q hq
+    rw [mem_eq _ (by dsimp only [stop, out, desc]; omega)]
+    exact hr q hq
+  · intro rho hrho
+    rw [mem_eq _ (by dsimp only [stop, out, desc]; omega)]
+    exact hcounts rho hrho
+  · intro rho hrho q hq he
+    have hcount : Nat.count (fun k => R k = rho) q ≤ q := Nat.count_le _
+    have hm := Nat.mul_le_mul_left (2 * N) (Nat.succ_le_of_lt hrho)
+    rw [Nat.mul_succ] at hm
+    have hbound : 5 + 6 * N + p + 2 * N * rho +
+        2 * Nat.count (fun k => R k = rho) q + 1 < stop := by
+      dsimp only [stop, out, desc]
+      omega
+    rw [mem_eq (5 + 6 * N + p + 2 * N * rho +
+        2 * Nat.count (fun k => R k = rho) q) (by omega),
+      mem_eq _ hbound]
+    exact hqueries rho hrho q hq he
+  · intro rho hrho k hk
+    have hi := ChunkCatalogue.before_add_lt C (queryCap n D) hrho hk
+    have hb := desc_lt (ChunkCatalogue.before C (queryCap n D) rho + k) hi
+    rw [mem_eq (desc + 3 * (ChunkCatalogue.before C (queryCap n D) rho + k))
+        (by omega),
+      mem_eq (desc + 3 * (ChunkCatalogue.before C (queryCap n D) rho + k) + 1)
+        (by omega), mem_eq _ hb]
+    exact hdesc rho hrho k hk
+  · intro i hi
+    change i < K * H at hi
+    have hH : 0 < H := by
+      by_contra hzero
+      have hz : H = 0 := by omega
+      rw [hz, Nat.mul_zero] at hi
+      omega
+    have hchunk : i / H < K := (Nat.div_lt_iff_lt_mul hH).mpr hi
+    have hd := desc_lt (i / H) hchunk
+    have hm := Nat.mul_le_mul_right (6 + 2 * (n * D)) (Nat.succ_le_of_lt hi)
+    rw [Nat.succ_mul] at hm
+    have hb : out + i * (6 + 2 * (n * D)) + (6 + 2 * (n * D)) ≤ stop := by
+      dsimp only [stop]
+      omega
+    obtain ⟨hrecord, hleft, hright⟩ := hblocks i hi
+    dsimp only
+    rw [mem_eq _ (by omega : desc + 3 * (i / H) < stop),
+      mem_eq _ (by omega : desc + 3 * (i / H) + 1 < stop), mem_eq _ hd]
+    refine ⟨?_, ?_, ?_⟩
+    · intro j
+      change z.mem (out + i * (6 + 2 * (n * D)) + j.val) = _
+      rw [mem_eq _ (by have hj : j.val < 6 := j.isLt; omega)]
+      exact hrecord j
+    · intro j
+      change z.mem (out + i * (6 + 2 * (n * D)) + 6 + j.val) = _
+      rw [mem_eq _ (by have hj : j.val < n * D := j.isLt; omega)]
+      exact hleft j
+    · intro j
+      change z.mem (out + i * (6 + 2 * (n * D)) + 6 + n * D + j.val) = _
+      rw [mem_eq _ (by have hj : j.val < n * D := j.isLt; omega)]
+      exact hright j
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.Instances
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/FailureCount.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/FailureCount.lean
new file mode 100644
index 000000000..41d59078c
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/FailureCount.lean
@@ -0,0 +1,71 @@
+/-
+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.RecordProduct.Detection
+public import Complexity.Algorithms.WordRAM.ExactTriangle.WitnessScan.Finite
+
+/-!
+# Actual failed-query words and finite failed occurrences
+
+This value/readback rule keeps the per-record occurrence count before applying any global
+false-positive bound. An all-record controller can therefore add these distinct counts once
+and inject their union into the existing global failed scans. No execution is assumed here;
+actual native calls prove the answer-word and coordinate premises.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Actual failed accepted queries are bounded by their finite occurrence count, retaining
+the record's identity for a later global sum. Repetition assumptions are not needed here. -/
+theorem native_failed_count_le {m n g p : ℕ} (values : ℕ → ℤ)
+    (AB BC AC : ℕ → ℕ → ℤ) (wAB wBC wAC : Fin n → Fin n → ℤ)
+    (hD : 16 ≤ D m) (hg : 1 ≤ g)
+    (hAB : ∀ u v : Fin n, AB u.val v.val = wAB u v)
+    (hBC : ∀ u v : Fin n, BC u.val v.val = wBC u v)
+    (hAC : ∀ u v : Fin n, AC u.val v.val = wAC u v)
+    (idx : InstanceIndex p) (qs : List (Fin n × Fin n)) (default : Fin n × Fin n)
+    (a b : ℕ → ℕ) (hcoords : ∀ i : Fin qs.length,
+      a i.val = (qs.get i).1.val ∧ b i.val = (qs.get i).2.val)
+    (mem : ℕ → ℕ) (out : ℕ)
+    (hanswer : ∀ i : Fin qs.length, mem (out + i.val) = Signed.encode
+      ((RecordProduct.leftMatrix m n g p values idx *
+        RecordProduct.rightMatrix m n g p values idx) (qs.get i).1 (qs.get i).2)) :
+    let first := idx.2.2 * pieceSize (D m) g
+    let length := min (pieceSize (D m) g) (n - first)
+    Nat.count (fun i => mem (out + i) ≠ 0 ∧
+      ∀ c : Fin length, AB (a i) (b i) + BC (b i) (first + c.val) +
+        AC (a i) (first + c.val) ≠ 0) qs.length ≤
+      Nat.count (fun i =>
+        (RecordProduct.leftMatrix m n g p values idx *
+          RecordProduct.rightMatrix m n g p values idx)
+            (qs.getD i default).1 (qs.getD i default).2 ≠ 0 ∧
+        scanPiece wAB wBC wAC (D m) g idx.2.2
+          (qs.getD i default).1 (qs.getD i default).2 = none) qs.length := by
+  apply Nat.count_mono_left
+  intro i hi hn
+  let j : Fin qs.length := ⟨i, hi⟩
+  have hget : qs.getD i default = qs.get j := by
+    rw [List.getD_eq_getElem _ _ hi, List.get_eq_getElem]
+  rw [hget]
+  constructor
+  · intro hz
+    apply hn.1
+    rw [hanswer j, hz]
+    rfl
+  · apply (WitnessScan.fails_iff_scanPiece_eq_none AB BC AC wAB wBC wAC
+      hD hg hAB hBC hAC (qs.get j).1 (qs.get j).2).mp
+    obtain ⟨ha, hb⟩ := hcoords j
+    simpa only [j, ha, hb] using hn.2
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Failures.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Failures.lean
index 5618c23a4..6691c7ba5 100644
--- a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Failures.lean
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Failures.lean
@@ -7,8 +7,7 @@ Authors: Anthropic, PBC, Erik Demaine
 module
 -- upstream: candidate
 
-public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Detection
-public import Complexity.Algorithms.WordRAM.ExactTriangle.WitnessScan.Finite
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.FailureCount
 
 /-!
 # Original false positives bound the actual native failed occurrences
@@ -50,27 +49,10 @@ theorem native_failed_occurrences_le {m n g p : ℕ} (values : ℕ → ℤ)
     Nat.count (fun i => mem (out + i) ≠ 0 ∧
       ∀ c : Fin length, AB (a i) (b i) + BC (b i) (first + c.val) +
         AC (a i) (first + c.val) ≠ 0) qs.length ≤ falsePositiveCount wAB wBC wAC p := by
-  apply (Nat.count_mono_left (q := fun i =>
-    (RecordProduct.leftMatrix m n g p values idx * RecordProduct.rightMatrix m n g p values idx)
-        (qs.getD i default).1 (qs.getD i default).2 ≠ 0 ∧
-      scanPiece wAB wBC wAC (D m) g idx.2.2
-        (qs.getD i default).1 (qs.getD i default).2 = none) ?_).trans
+  exact (native_failed_count_le values AB BC AC wAB wBC wAC hD hg hAB hBC hAC
+    idx qs default a b hcoords mem out hanswer).trans
     (RecordProduct.failed_occurrences_le values wAB wBC wAC hD hg hp
       hvaluesBC hvaluesAC idx hidx qs default hqs hquery)
-  intro i hi hn
-  let j : Fin qs.length := ⟨i, hi⟩
-  have hget : qs.getD i default = qs.get j := by
-    rw [List.getD_eq_getElem _ _ hi, List.get_eq_getElem]
-  rw [hget]
-  constructor
-  · intro hz
-    apply hn.1
-    rw [hanswer j, hz]
-    rfl
-  · apply (WitnessScan.fails_iff_scanPiece_eq_none AB BC AC wAB wBC wAC
-      hD hg hAB hBC hAC (qs.get j).1 (qs.get j).2).mp
-    obtain ⟨ha, hb⟩ := hcoords j
-    simpa only [j, ha, hb] using hn.2
 
 /-- The actual native success condition is exactly an original zero triangle in the selected
 existing chunk and piece. The nonzero-product condition is derived for every genuine zero. -/
diff --git a/ComplexityTests/WordRAMExactTriangleFixedPrimeController.lean b/ComplexityTests/WordRAMExactTriangleFixedPrimeController.lean
new file mode 100644
index 000000000..cc228f78e
--- /dev/null
+++ b/ComplexityTests/WordRAMExactTriangleFixedPrimeController.lean
@@ -0,0 +1,66 @@
+/-
+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.FixedPrime.Controller
+import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime.Potential
+
+/-!
+# Concrete native catalogue controller regressions
+
+These executions check actual counter delivery, failed/successful returns and the real loop's
+exit guard. They are controller fixtures, not supplied-callee/full-solver execution examples.
+The initialized valid-geometry solver clients are checked in their separate test module.
+-/
+
+set_option linter.hashCommand false
+
+namespace ComplexityTests.WordRAMExactTriangleFixedPrimeController
+
+open Cslib.WordRAM
+open Cslib.Algorithms.WordRAM.ExactTriangle
+
+private def fixture (flag : ℕ) : Data 416 :=
+  { regs := fun j =>
+      if j.val = 40 then 7 else if j.val = 392 then flag else if j.val = 396 then 3
+      else if j.val = 400 then 2 else if j.val = 401 then 7 else if j.val = 403 then 5
+      else if j.val = 404 then 1 else 99
+    mem := fun a => if a = 17 then 123 else 0 }
+
+private def observe (code : Code .standard 416) (flag : ℕ) : Option (List ℕ × ℕ) :=
+  (code.eval 16 0 (fixture flag)).map fun (y, t) =>
+    ([y.regs FixedPrime.Reg.index, y.regs FixedPrime.Reg.limit,
+      y.regs FixedPrime.Reg.found, y.regs FixedPrime.Reg.scans, y.regs FixedPrime.Reg.one,
+      y.regs 392, y.mem 17], t)
+
+#guard observe FixedPrime.setup 1 == some ([0, 7, 0, 0, 1, 1, 123], 5)
+#guard observe FixedPrime.select 0 == some ([2, 7, 99, 5, 1, 0, 123], 1)
+#guard observe FixedPrime.receive 0 == some ([3, 7, 0, 8, 1, 0, 123], 6)
+#guard observe FixedPrime.receive 1 == some ([3, 3, 1, 8, 1, 1, 123], 5)
+
+-- A successful return closes the actual loop immediately, even with zero body fuel. The
+-- embedded body is the real record program, not a substitute solver.
+private def stopped : Option (ℕ × ℕ) := do
+  let (y, _) ← FixedPrime.receive.eval 16 0 (fixture 1)
+  let (z, t) ← (Code.loop (.lt FixedPrime.Reg.index FixedPrime.Reg.limit)
+    FixedPrime.step).eval 16 0 y
+  pure (z.regs FixedPrime.Reg.scans, t)
+
+#guard stopped == some (8, 2)
+
+-- A failed record leaves more work and therefore cannot exit with zero body fuel.
+private def pending : Option (Data 416 × ℕ) := do
+  let (y, _) ← FixedPrime.receive.eval 16 0 (fixture 0)
+  (Code.loop (.lt FixedPrime.Reg.index FixedPrime.Reg.limit) FixedPrime.step).eval 16 0 y
+
+#guard pending.isNone
+
+-- The single reserve pays exactly one actual success and none for an unsuccessful return.
+example : 20 + 2 + (11 + 7 * (5 + 1 - 1)) ≤ 8 + 11 + 7 * (1 + 5 + 1) :=
+  FixedPrime.pay_return (by decide) (by decide : 2 ≤ 1 + 1) (by decide)
+
+end ComplexityTests.WordRAMExactTriangleFixedPrimeController
diff --git a/ComplexityTests/WordRAMExactTriangleFixedPrimeInput.lean b/ComplexityTests/WordRAMExactTriangleFixedPrimeInput.lean
new file mode 100644
index 000000000..c058b56ee
--- /dev/null
+++ b/ComplexityTests/WordRAMExactTriangleFixedPrimeInput.lean
@@ -0,0 +1,156 @@
+/-
+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.FixedPrime
+import Mathlib.Data.List.GetD
+
+/-!
+# Fully admitted original-input fixed-prime decisions
+
+Both clients retain the actual same-state prefix and halt at valid positive thin geometry.
+The all-one negative input has modular false positives at prime three, 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.WordRAMExactTriangleFixedPrimeInput
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.WordRAM.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+private def side : ℕ := 16 ^ 18
+private def weights (N : ℕ) (z : ℤ) : List ℤ := List.replicate (3 * (N * N)) z
+private def width (N A : ℕ) : ℕ := FixedPrime.admissionWidth N (D 2) 1 3 A
+
+private theorem prime : 3 ∈ Nat.sqrtPrimeWindow (D 2) :=
+  Nat.mem_sqrtPrimeWindow_iff_sq.mpr ⟨by decide, by decide, by decide⟩
+
+/-- The complete actual program returns one and an original witness on all-zero input. -/
+private theorem initialized_zero (N : ℕ) (hgeo : D 2 ^ 18 ≤ N) : ∃ y : Data 416, ∃ t : ℕ,
+    Runs (width N 0) (FixedPrime.program.program FixedPrime.Reg.found)
+      (State.init (PreparationInput.input N (D 2) 1 3 (weights N 0)))
+      ⟨FixedPrime.program.size, y⟩ t ∧
+    Executes (width N 0) (FixedPrime.program.program FixedPrime.Reg.found)
+      (State.init (PreparationInput.input N (D 2) 1 3 (weights N 0))) 1 (t + 1) ∧
+    y.regs FixedPrime.Reg.found = 1 ∧ y.regs FixedPrime.Reg.scans ≤ 1 ∧
+    ∃ 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⟩ :=
+    FixedPrime.runs_input (m := 2) (n := N) (g := 1) (p := 3) (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 2 ^ 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))) 3 = 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))) 3 +
+          y.regs FixedPrime.Reg.found := ys
+    simpa only [hF, hf, zero_add] using hs
+
+/-- 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_one (N : ℕ) (hgeo : D 2 ^ 18 ≤ N) :
+    let V := fun q => (weights N 1).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))) 3
+    ∃ y : Data 416, ∃ t : ℕ,
+      Runs (width N 1) (FixedPrime.program.program FixedPrime.Reg.found)
+        (State.init (PreparationInput.input N (D 2) 1 3 (weights N 1)))
+        ⟨FixedPrime.program.size, y⟩ t ∧
+      Executes (width N 1) (FixedPrime.program.program FixedPrime.Reg.found)
+        (State.init (PreparationInput.input N (D 2) 1 3 (weights N 1))) 0 (t + 1) ∧
+      y.regs FixedPrime.Reg.found = 0 ∧ y.regs FixedPrime.Reg.scans ≤ F := by
+  have hmag : ∀ z ∈ weights N 1, z.natAbs ≤ 1 := 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⟩ :=
+    FixedPrime.runs_input (m := 2) (n := N) (g := 1) (p := 3) (A := 1)
+      (W := width N 1) (weights N 1) (by simp only [weights, List.length_replicate])
+      (by decide) (by decide) prime hgeo hmag le_rfl
+  let V := fun q => (weights N 1).getD q 0
+  have hval (q : ℕ) (hq : q < 3 * (N * N)) : V q = 1 :=
+    List.getD_replicate (1 : ℤ) 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) (FixedPrime.program.program FixedPrime.Reg.found)
+      (State.init (PreparationInput.input side (D 2) 1 3 (weights side 0)))
+      ⟨FixedPrime.program.size, y⟩ t ∧
+    Executes (width side 0) (FixedPrime.program.program FixedPrime.Reg.found)
+      (State.init (PreparationInput.input side (D 2) 1 3 (weights side 0))) 1 (t + 1) ∧
+    y.regs FixedPrime.Reg.found = 1 ∧ y.regs FixedPrime.Reg.scans ≤ 1 ∧
+    ∃ 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 1).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))) 3
+    ∃ y : Data 416, ∃ t : ℕ,
+      Runs (width side 1) (FixedPrime.program.program FixedPrime.Reg.found)
+        (State.init (PreparationInput.input side (D 2) 1 3 (weights side 1)))
+        ⟨FixedPrime.program.size, y⟩ t ∧
+      Executes (width side 1) (FixedPrime.program.program FixedPrime.Reg.found)
+        (State.init (PreparationInput.input side (D 2) 1 3 (weights side 1))) 0 (t + 1) ∧
+      y.regs FixedPrime.Reg.found = 0 ∧ y.regs FixedPrime.Reg.scans ≤ F :=
+  initialized_one side (by decide)
+
+end ComplexityTests.WordRAMExactTriangleFixedPrimeInput
diff --git a/ComplexityTests/WordRAMExactTrianglePreparationLocality.lean b/ComplexityTests/WordRAMExactTrianglePreparationLocality.lean
new file mode 100644
index 000000000..5dc732785
--- /dev/null
+++ b/ComplexityTests/WordRAMExactTrianglePreparationLocality.lean
@@ -0,0 +1,67 @@
+/-
+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.PreparationLocality
+import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationInput
+
+/-!
+# Actual prepared readback survives a dirty heap cell
+
+This small producer-only client distinguishes protected readback from the producer's original
+external frame. The full thin-solver clients retain their valid positive geometry elsewhere.
+-/
+
+namespace ComplexityTests.WordRAMExactTrianglePreparationLocality
+
+open Cslib.WordRAM
+open Cslib.Algorithms.WordRAM.ExactTriangle
+
+example : ∃ a z : Data 64,
+    ExecWithin (PreparationInput.width 1 1 1 2 0) Instances.program
+      (.init (PreparationInput.input 1 1 1 2 [0, 0, 0])) a
+      (Instances.timeBound 1 1 2 1 1 - 1) ∧
+    Instances.Output 1 1 1 2 (fun q => ([0, 0, 0] : List ℤ).getD q 0) z z ∧
+    z.mem (a.regs Instances.heap) = 77 ∧
+    ¬ Instances.Output 1 1 1 2 (fun q => ([0, 0, 0] : List ℤ).getD q 0)
+      (.init (PreparationInput.input 1 1 1 2 [0, 0, 0])) z := by
+  obtain ⟨a, ha, hout, _, _⟩ := PreparationInput.exec_input (n := 1) (D := 1) (g := 1)
+    (p := 2) (A := 0) (W := PreparationInput.width 1 1 1 2 0) [0, 0, 0]
+    (by decide) (by decide) (by decide) (by decide) (by decide)
+    (by intro v hv; simp only [List.mem_cons, List.not_mem_nil, or_false] at hv
+        rcases hv with h | h | h <;> subst v <;> decide) le_rfl
+  let z := a.write (a.regs Instances.heap) 77
+  have hmem : Set.EqOn z.mem a.mem (Set.Iio (a.regs Instances.heap)) := by
+    intro u hu
+    change Function.update a.mem (a.regs Instances.heap) 77 u = a.mem u
+    exact Function.update_of_ne (by change u < a.regs Instances.heap at hu; omega) _ _
+  have hnew := hout.reframe (z := z) (fun q => ([0, 0, 0] : List ℤ).getD q 0) rfl hmem
+  have dirty : z.mem (a.regs Instances.heap) = 77 := by
+    simp only [z, Data.write_mem, Function.update_self]
+  have hheap : 17 ≤ a.regs Instances.heap := by
+    have hh := hout.2.2.2.2.2.1
+    change a.regs Instances.heap = _ + _ at hh
+    omega
+  have old_zero : (Data.init (PreparationInput.input 1 1 1 2 [0, 0, 0]) : Data 64).mem
+      (a.regs Instances.heap) = 0 := by
+    cases he : a.regs Instances.heap with
+    | zero => omega
+    | succ u =>
+      change (PreparationInput.input 1 1 1 2 [0, 0, 0]).getD u 0 = 0
+      apply List.getD_eq_default
+      have hu : 7 ≤ u := by omega
+      exact hu
+  refine ⟨a, z, ?_, hnew, dirty, ?_⟩
+  · convert ha using 1
+    decide
+  · intro hbad
+    have he := hbad.2.2.2.2.2.2.2.2.2.2.2 (a.regs Instances.heap)
+      (Or.inr hout.2.2.2.2.2.1.ge)
+    rw [dirty, old_zero] at he
+    contradiction
+
+end ComplexityTests.WordRAMExactTrianglePreparationLocality
diff --git a/ROADMAP.md b/ROADMAP.md
index 1eb96901d..d087bc159 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -551,6 +551,15 @@ each statement against the numbered result. Organize modules by subject, not cha
   Root decoding, all control and original-weight scans are charged; positive logarithmic width
   and polynomial words/support hold at every wider admitted width. The outer instance loop,
   aggregate subcubic ET analysis and ordinary-3SUM 1.9992 composition remain open under [#1394].
+- **Fixed-prime native catalogue decision** ([#1662](https://github.com/cslib-community/complexitylib/issues/1662)):
+  the native continuation runs real preparation once and the actual product/witness callee
+  over every computed occupied ordinal, stopping on the first original witness. Its initialized
+  same-state prefix/halt verdict is equivalent to original ET, with dirty-workspace reuse and
+  one global `S≤F(p)+returnedFlag` scan budget. All-instance product savings, all native control
+  charges, original-input logarithmic admission and polynomial wider-prefix words/support are
+  derived. Validation, independent review and integration are tracked in #1662. Global
+  parameter/prime selection, unrestricted small geometry, the complete aggregate source exponent
+  and the ordinary-3SUM 1.9992 endpoint remain open under [#1394].
 - **Conditional Convolution-3SUM host** ([#1524]): the charged native host initializes from the
   ordinary input and runs every generated instance, conditional on a concrete solver's execution,
   correctness and frame theorem. This completes the conditional host milestone. Integrating the
diff --git a/UPSTREAM.md b/UPSTREAM.md
index f84aaa139..773a9cb55 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -421,6 +421,25 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   narrow `ExactTriangle.PieceBounds` module, reused by preparation and recovery. Parameter/prime
   choice, the outer ET loop, aggregate savings and the full #1394 endpoint remain open; no curated
   abstract changes.
+  The bounded fixed-prime continuation
+  [#1662](https://github.com/cslib-community/complexitylib/issues/1662) runs the producer once
+  and traverses every actual occupied ordinal using the full 400-register callee in a fixed
+  416-register program. Its initialized verdict decides original ET across all records;
+  protected readback survives dirty scratch via `Instances.Output.reframe`, which reframes
+  against the current state without asserting preservation of the old external frame.
+  Distinct record/query occurrences inject into the existing global `failedScans`; actual
+  total scans satisfy `S≤F(p)+returnedFlag`, with only one possible successful-return flag.
+  Native preparation, products, root/query/controller/loop/halt and original verification
+  costs are charged. Aggregate product work is bounded by
+  `138412032*(19m+1)*n³*g/D^(1/18)` under the unchanged positive thin geometry and prime window;
+  one-time `690n²Dg`, explicit query/root/controller work and one global failed-scan term remain
+  separate. The actual program has original-input logarithmic admission and polynomial
+  all-prefix words/support independently of every larger physical width. Validation and
+  integration are tracked in #1662; this is not a parameter/prime-selection host or a completed
+  aggregate source exponent. The source's Light host uses piece-major rounds and
+  per-round matrix construction; the native producer prepares the chunk-major catalogue once
+  and later products stop after success. No source-trace equivalence or Light simulation is
+  assumed. The full ordinary-3SUM 1.9992 objective remains open under #1394; no abstract changes.
   Stage `exec_*` lemmas are internal implementation APIs exported across proof modules;
   callers use the flat initialized runs, width theorem or pointer/epoch kernel. The narrow
   `WordRAM.ArrayAppend` and `WordRAM.InputArray` topic modules keep append/input dependencies