diff --git a/Complexity.lean b/Complexity.lean
index f59b96f223..ea6e35732b 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -3,6 +3,7 @@ module  -- shake: keep-all --deprecated_module: ignore
 public import Complexity.Algorithms.ExactTriangle.Defs
 public import Complexity.Algorithms.ExactTriangle.Hashing
 public import Complexity.Algorithms.ExactTriangle.Lopsided
+public import Complexity.Algorithms.ExactTriangle.PieceBounds
 public import Complexity.Algorithms.ExactTriangle.Splitting
 public import Complexity.Algorithms.ExactTriangle.Weights
 public import Complexity.Algorithms.ExactTriangle.Witnesses
@@ -107,6 +108,7 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Bounds
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Copy
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Decode
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Detection
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Entry
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Exec
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.First
@@ -118,9 +120,35 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Prepare
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Producer
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.ProducerQueries
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.QueryValues
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.RawInput
 public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.SourceBounds
+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.Failures
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Flat
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Header
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Kernel
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Original
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Pair
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Prepare
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Queries
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Readback
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.SourceBounds
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Spec
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Step
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.TimeBound
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Trace
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Width
 public import Complexity.Algorithms.WordRAM.ExactTriangle.ResidueClasses
+public import Complexity.Algorithms.WordRAM.ExactTriangle.WitnessScan.Cell
+public import Complexity.Algorithms.WordRAM.ExactTriangle.WitnessScan.Exec
+public import Complexity.Algorithms.WordRAM.ExactTriangle.WitnessScan.Finite
+public import Complexity.Algorithms.WordRAM.ExactTriangle.WitnessScan.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.WitnessScan.Setup
 public import Complexity.Algorithms.WordRAM.ExactTriangle.WriteMatrices
 public import Complexity.Algorithms.WordRAM.FusionTree.Binary
 public import Complexity.Algorithms.WordRAM.FusionTree.Boundary
diff --git a/Complexity/Algorithms/ExactTriangle/PieceBounds.lean b/Complexity/Algorithms/ExactTriangle/PieceBounds.lean
new file mode 100644
index 0000000000..ca9da0e095
--- /dev/null
+++ b/Complexity/Algorithms/ExactTriangle/PieceBounds.lean
@@ -0,0 +1,65 @@
+/-
+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.Splitting
+
+/-!
+# Numeric coordinates of ExactTriangle pieces
+
+These bounds connect the existing finite pieces with the truncated original-vertex intervals
+used by both native matrix preparation and witness recovery. They expose the same coordinate
+facts previously private to the prepared-adjacency consumer, without changing the finite pieces.
+-/
+
+public section
+
+namespace Cslib.Algorithms.ExactTriangle
+
+/-- The active piece/label rectangle fits in the source middle dimension. -/
+theorem pieceLength_mul_le_of_mem_sqrtPrimeWindow {D g p n k : ℕ} (hg : 1 ≤ g)
+    (hp : p ∈ Nat.sqrtPrimeWindow D) :
+    min (pieceSize D g) (n - k * pieceSize D g) * p ≤ D := by
+  have hpS : p ≤ sOf D := Nat.le_sqrt'.mpr (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).2.2.le
+  have hlen : min (pieceSize D g) (n - k * pieceSize D g) ≤ sOf D :=
+    (min_le_left _ _).trans (pieceSize_le_sOf hg)
+  exact (Nat.mul_le_mul hlen hpS).trans (Nat.sqrt_le D)
+
+/-- An original piece vertex has its computed local coordinate in the actual truncated interval. -/
+theorem piece_coordinate {n D g k : ℕ} (hD : 16 ≤ D) (hg : 1 ≤ g)
+    (c : Fin n) (hc : c ∈ piece n D g k) :
+    k * pieceSize D g + c.val % pieceSize D g = c.val ∧
+      c.val % pieceSize D g < min (pieceSize D g) (n - k * pieceSize D g) := by
+  have hB := pieceSize_pos hD hg
+  have hdiv := (mem_piece c).mp hc
+  have hsplit := Nat.div_add_mod c.val (pieceSize D g)
+  rw [hdiv, Nat.mul_comm] at hsplit
+  have hmod := Nat.mod_lt c.val hB
+  exact ⟨hsplit, lt_min hmod (by have := c.isLt; omega)⟩
+
+/-- The finite piece is precisely its original-coordinate truncated interval. -/
+theorem mem_piece_iff_interval {n D g k : ℕ} (hD : 16 ≤ D) (hg : 1 ≤ g) (c : Fin n) :
+    c ∈ piece n D g k ↔ k * pieceSize D g ≤ c.val ∧
+      c.val < k * pieceSize D g + min (pieceSize D g) (n - k * pieceSize D g) := by
+  constructor
+  · intro hc
+    obtain ⟨he, hv⟩ := piece_coordinate hD hg c hc
+    omega
+  · rintro ⟨hlo, hhi⟩
+    apply (mem_piece c).mpr
+    have hB := pieceSize_pos hD hg
+    have hsmall : c.val - k * pieceSize D g < pieceSize D g := by
+      have := min_le_left (pieceSize D g) (n - k * pieceSize D g)
+      omega
+    have he : c.val = k * pieceSize D g + (c.val - k * pieceSize D g) := by omega
+    have hsmall' : c.val - pieceSize D g * k < pieceSize D g := by
+      simpa only [Nat.mul_comm k (pieceSize D g)] using hsmall
+    rw [he, Nat.mul_comm k (pieceSize D g), Nat.mul_add_div hB,
+      Nat.div_eq_of_lt hsmall', Nat.add_zero]
+
+end Cslib.Algorithms.ExactTriangle
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationAdjacency.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationAdjacency.lean
index e28b7fb0ed..57437d9508 100644
--- a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationAdjacency.lean
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationAdjacency.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationSpec
+public import Complexity.Algorithms.ExactTriangle.PieceBounds
 
 /-!
 # Adjacency in prepared native ExactTriangle matrices
@@ -34,25 +35,6 @@ namespace Cslib.Algorithms.WordRAM.ExactTriangle.PreparationSpec
 
 open Cslib.WordRAM Cslib.Algorithms.ExactTriangle Cslib.Matrix
 
-private theorem prepared_middle_fits {D g p n k : ℕ} (hg : 1 ≤ g)
-    (hp : p ∈ Nat.sqrtPrimeWindow D) :
-    min (pieceSize D g) (n - k * pieceSize D g) * p ≤ D := by
-  have hpS : p ≤ sOf D := Nat.le_sqrt'.mpr (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).2.2.le
-  have hlen : min (pieceSize D g) (n - k * pieceSize D g) ≤ sOf D :=
-    (min_le_left _ _).trans (pieceSize_le_sOf hg)
-  exact (Nat.mul_le_mul hlen hpS).trans (Nat.sqrt_le D)
-
-private theorem piece_coordinate {n D g k : ℕ} (hD : 16 ≤ D) (hg : 1 ≤ g)
-    (c : Fin n) (hc : c ∈ piece n D g k) :
-    k * pieceSize D g + c.val % pieceSize D g = c.val ∧
-      c.val % pieceSize D g < min (pieceSize D g) (n - k * pieceSize D g) := by
-  have hB := pieceSize_pos hD hg
-  have hdiv := (mem_piece c).mp hc
-  have hsplit := Nat.div_add_mod c.val (pieceSize D g)
-  rw [hdiv, Nat.mul_comm] at hsplit
-  have hmod := Nat.mod_lt c.val hB
-  exact ⟨hsplit, lt_min hmod (by have := c.isLt; omega)⟩
-
 /-- The actual prepared matrix cells express the existing finite graph's adjacency, and the
 unused middle positions are zero. The prime-window and piece hypotheses discharge every
 padding and local-coordinate premise of the matrix-entry API. -/
@@ -100,7 +82,7 @@ theorem instance_adjacency {n D g p : ℕ} (values : ℕ → ℤ)
     (fun j => WriteMatrices.entry false A (fun q => R (2 * N + q)) j) at hL
   change (Block.mk A'.dst (n * D)).Realizes y.mem
     (fun j => WriteMatrices.entry true A' (fun q => R (N + q)) j) at hR
-  have hpad : A.length * A.p ≤ A.D := prepared_middle_fits hg hp
+  have hpad : A.length * A.p ≤ A.D := pieceLength_mul_le_of_mem_sqrtPrimeWindow hg hp
   change min B (n - idx.2.2 * B) * p ≤ D at hpad
   have hloadL (a c : Fin n) :
       R (2 * N + (a.val * n + c.val)) = (wAC a c).natMod p := by
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Detection.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Detection.lean
new file mode 100644
index 0000000000..425cce365c
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Detection.lean
@@ -0,0 +1,197 @@
+/-
+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.Producer
+public import Complexity.Algorithms.ExactTriangle.PieceBounds
+public import Complexity.Algorithms.ExactTriangle.Witnesses
+public import Mathlib.Data.Nat.Count
+import Complexity.Algorithms.WordRAM.ExactTriangle.MatrixSpec
+
+/-!
+# Actual record products detect the existing modular graph
+
+The zero/one value matrices used by the real product adapter have a nonzero product entry
+exactly at a common neighbor of the existing finite `lopInstance`. Active middle coordinates
+and zero padding follow from the original source prime window and piece geometry. Thus a
+consumer can derive detection semantics from the actual product, without an answer oracle.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct
+
+open Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- The value matrices written by the producer and consumed by the actual native product
+have precisely the common-neighbor semantics of the existing finite modular instance. -/
+theorem product_ne_zero_iff {m n g p : ℕ} (values : ℕ → ℤ)
+    (wAB wBC wAC : Fin n → Fin n → ℤ)
+    (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m))
+    (hBC : ∀ b c, values (n * n + pairIndex (b, c)) = wBC b c)
+    (hAC : ∀ a c, values (2 * (n * n) + pairIndex (a, c)) = wAC a c)
+    (idx : InstanceIndex p) (a b : Fin n) :
+    (leftMatrix m n g p values idx * rightMatrix m n g p values idx) a b ≠ 0 ↔
+      (lopInstance wAB wBC wAC (D m) g p idx).HasCommonNeighbor a b := by
+  classical
+  let X := leftMatrix m n g p values idx
+  let Y := rightMatrix m n g p values idx
+  let G := lopInstance wAB wBC wAC (D m) g p idx
+  let A := matrixArgs n (D m) g p idx.1.val idx.2.2
+  let Rleft (q : ℕ) := (values (2 * (n * n) + q) % (p : ℤ)).toNat
+  let Rright (q : ℕ) := (values (n * n + q) % (p : ℤ)).toNat
+  have hpad : A.length * p ≤ D m := pieceLength_mul_le_of_mem_sqrtPrimeWindow hg hp
+  have hp0 : 0 < p := (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.pos
+  have loadLeft (u c : Fin n) : Rleft (u.val * n + c.val) = (wAC u c).natMod p := by
+    change (values (2 * (n * n) + pairIndex (u, c)) % (p : ℤ)).toNat = _
+    rw [hAC]
+    rfl
+  have loadRight (u c : Fin n) : Rright (u.val * n + c.val) = (wBC u c).natMod p := by
+    change (values (n * n + pairIndex (u, c)) % (p : ℤ)).toNat = _
+    rw [hBC]
+    rfl
+  have edges (c : Fin n) (hc : c ∈ piece n (D m) g idx.2.2)
+      (v : Fin A.length) (label : Fin p) (j : Fin (D m))
+      (hv : A.first + v.val = c.val) (hj : j.val = v.val * p + label.val) :
+      (X a j = 1 ↔ G.adjA a (⟨c, hc⟩, label)) ∧
+      (Y j b = 1 ↔ G.adjB (⟨c, hc⟩, label) b) := by
+    have hl := MatrixSpec.left_lopInstance A Rleft wAB wBC wAC g idx.2.1 idx.2.2
+      idx.1 rfl a c v label hc hv hpad loadLeft
+    have hr := MatrixSpec.right_lopInstance A Rright wAB wBC wAC g idx.2.1 idx.2.2
+      idx.1 b c v label hc hv loadRight
+    constructor
+    · change (WriteMatrices.entry false A Rleft (a.val * D m + j.val) : ℤ) = 1 ↔ _
+      rw [hj]
+      exact_mod_cast hl
+    · change (WriteMatrices.entry true A Rright (j.val * n + b.val) : ℤ) = 1 ↔ _
+      rw [hj]
+      exact_mod_cast hr
+  obtain ⟨hX, hY⟩ := matrices_zero_one m n g p values idx
+  have hx : ∀ a j, X a j = 0 ∨ X a j = 1 := by
+    intro a j
+    have := hX a j
+    change 0 ≤ X a j ∧ X a j ≤ 1 at this
+    omega
+  have hy : ∀ j b, Y j b = 0 ∨ Y j b = 1 := by
+    intro j b
+    have := hY j b
+    change 0 ≤ Y j b ∧ Y j b ≤ 1 at this
+    omega
+  rw [LopsidedGraph.mul_apply_eq_commonNeighborCount_ofMatrices X Y ∅ hx hy]
+  have hnz := (LopsidedGraph.ofMatrices X Y ∅).commonNeighborCount_ne_zero_iff a b
+  rw [show ((LopsidedGraph.ofMatrices X Y ∅).commonNeighborCount a b : ℤ) ≠ 0 ↔
+      (LopsidedGraph.ofMatrices X Y ∅).commonNeighborCount a b ≠ 0 by exact_mod_cast Iff.rfl]
+  rw [hnz]
+  change (∃ j : Fin (D m), X a j = 1 ∧ Y j b = 1) ↔ G.HasCommonNeighbor a b
+  constructor
+  · rintro ⟨j, hleft, hright⟩
+    have hj : j.val / p < A.length := by
+      by_contra h
+      have hz := MatrixSpec.left_padding A Rleft a j (by change A.length ≤ j.val / p; omega)
+      change WriteMatrices.entry false A Rleft (a.val * D m + j.val) = 0 at hz
+      have hl : (WriteMatrices.entry false A Rleft (a.val * D m + j.val) : ℤ) = 1 := hleft
+      rw [hz] at hl
+      norm_num at hl
+    let v : Fin A.length := ⟨j.val / p, hj⟩
+    let label : Fin p := ⟨j.val % p, Nat.mod_lt _ hp0⟩
+    have hn : A.first + v.val < n := by
+      have hl := min_le_right (pieceSize (D m) g) (n - A.first)
+      have hv := v.isLt
+      change v.val < min (pieceSize (D m) g) (n - A.first) at hv
+      omega
+    let c : Fin n := ⟨A.first + v.val, hn⟩
+    have hc : c ∈ piece n (D m) g idx.2.2 := by
+      apply (mem_piece_iff_interval hD hg c).mpr
+      change idx.2.2 * pieceSize (D m) g ≤ A.first + v.val ∧
+        A.first + v.val < idx.2.2 * pieceSize (D m) g + A.length
+      change A.first ≤ A.first + v.val ∧ A.first + v.val < A.first + A.length
+      exact ⟨by omega, Nat.add_lt_add_left v.isLt _⟩
+    have he : j.val = v.val * p + label.val := by
+      simpa only [v, label, Nat.mul_comm] using (Nat.div_add_mod j.val p).symm
+    obtain ⟨heL, heR⟩ := edges c hc v label j rfl he
+    exact ⟨(⟨c, hc⟩, label), heL.mp hleft, heR.mp hright⟩
+  · rintro ⟨⟨⟨c, hc⟩, label⟩, hleft, hright⟩
+    obtain ⟨hv, hlen⟩ := piece_coordinate hD hg c hc
+    let v : Fin A.length := ⟨c.val % pieceSize (D m) g, hlen⟩
+    have hj : v.val * p + label.val < D m := by
+      have hm := Nat.mul_le_mul_right p v.isLt
+      rw [Nat.succ_mul] at hm
+      have hl := label.isLt
+      omega
+    let j : Fin (D m) := ⟨v.val * p + label.val, hj⟩
+    obtain ⟨heL, heR⟩ := edges c hc v label j hv rfl
+    exact ⟨j, heL.mpr hleft, heR.mpr hright⟩
+
+/-- The mathematical answers computed by the actual product discharge the finite recovery
+contract. Correct answers are a conclusion here, not a solver assumption. -/
+theorem product_answers_correct {m n g p : ℕ} (values : ℕ → ℤ)
+    (wAB wBC wAC : Fin n → Fin n → ℤ)
+    (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m))
+    (hBC : ∀ b c, values (n * n + pairIndex (b, c)) = wBC b c)
+    (hAC : ∀ a c, values (2 * (n * n) + pairIndex (a, c)) = wAC a c) :
+    AnswersCorrect wAB wBC wAC (D m) g p (fun idx q => decide
+      ((leftMatrix m n g p values idx * rightMatrix m n g p values idx) q.1 q.2 ≠ 0)) := by
+  intro idx _ q _
+  simp only [decide_eq_true_eq]
+  exact propext (product_ne_zero_iff values wAB wBC wAC hD hg hp hBC hAC idx q.1 q.2)
+
+/-- Distinct occurrences of one actual query chunk that are accepted by the product but
+have no original witness inject into the existing finite failed scans. Their number is
+therefore bounded by the existing original-weight false-positive count. -/
+theorem failed_occurrences_le {m n g p : ℕ} (values : ℕ → ℤ)
+    (wAB wBC wAC : Fin n → Fin n → ℤ)
+    (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m))
+    (hBC : ∀ b c, values (n * n + pairIndex (b, c)) = wBC b c)
+    (hAC : ∀ a c, values (2 * (n * n) + pairIndex (a, c)) = wAC a c)
+    (idx : InstanceIndex p) (hidx : idx ∈ instanceIndices wAB (D m) g p)
+    (qs : List (Fin n × Fin n)) (default : Fin n × Fin n) (hqs : qs.Nodup)
+    (hquery : ∀ q ∈ qs, q ∈ chunkOf wAB (D m) p idx.1 idx.2.1) :
+    Nat.count (fun i =>
+      (leftMatrix m n g p values idx * 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 ≤
+      falsePositiveCount wAB wBC wAC p := by
+  classical
+  let ans : InstanceIndex p → Fin n × Fin n → Bool := fun idx q => decide
+    ((leftMatrix m n g p values idx * rightMatrix m n g p values idx) q.1 q.2 ≠ 0)
+  let P (i : ℕ) : Prop :=
+    (leftMatrix m n g p values idx * 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
+  let := Nat.CountSet.fintype P qs.length
+  let failures := failedScans wAB wBC wAC (D m) g p ans
+  have hget (i : ℕ) (hi : i < qs.length) : qs.getD i default = qs.get ⟨i, hi⟩ := by
+    rw [List.getD_eq_getElem _ _ hi, List.get_eq_getElem]
+  let f : {i : ℕ // i < qs.length ∧ P i} → {s // s ∈ failures} := fun i =>
+    ⟨(idx, qs.get ⟨i.val, i.prop.1⟩), by
+      apply Finset.mem_filter.mpr
+      refine ⟨mem_acceptedPairs.mpr ⟨hidx, ?_, ?_⟩, ?_⟩
+      · exact hquery _ (List.get_mem _ _)
+      · have he := i.prop.2.1
+        simpa only [ans, decide_eq_true_eq, hget i.val i.prop.1] using he
+      · have he := i.prop.2.2
+        simpa only [scanOf, hget i.val i.prop.1] using he⟩
+  have hf : Function.Injective f := by
+    intro i j hij
+    have hpair : qs.get ⟨i.val, i.prop.1⟩ = qs.get ⟨j.val, j.prop.1⟩ :=
+      congrArg (fun s => s.val.2) hij
+    have hi := List.nodup_iff_injective_get.mp hqs hpair
+    exact Subtype.ext (congrArg Fin.val hi)
+  change Nat.count P qs.length ≤ _
+  rw [Nat.count_eq_card_fintype]
+  calc
+    _ ≤ 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
+      (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.ne_zero
+      (product_answers_correct values wAB wBC wAC hD hg hp hBC hAC)
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Producer.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Producer.lean
index 0876048cd6..253538c18a 100644
--- a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Producer.lean
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Producer.lean
@@ -46,11 +46,6 @@ open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
   (WriteMatrices.entry true (matrixArgs n (D m) g p idx.1.val idx.2.2)
     (fun q => (values (n * n + q) % (p : ℤ)).toNat) (k.val * n + a.val) : ℤ)
 
-/-- Both native writer value functions are raw zero/one words at every index. -/
-theorem entry_le_one (side : Bool) (A : WriteMatrices.Args) (R : ℕ → ℕ) (a : ℕ) :
-    WriteMatrices.entry side A R a ≤ 1 := by
-  cases side <;> dsimp only [WriteMatrices.entry] <;> split_ifs <;> omega
-
 /-- The readback matrices satisfy the raw callee's original-entry hypotheses. -/
 theorem matrices_zero_one (m n g p : ℕ) (values : ℕ → ℤ) (idx : InstanceIndex p) :
     (∀ a k, 0 ≤ leftMatrix m n g p values idx a k ∧
@@ -60,10 +55,10 @@ theorem matrices_zero_one (m n g p : ℕ) (values : ℕ → ℤ) (idx : Instance
   constructor <;> intro a k
   · exact ⟨Int.natCast_nonneg _, by
       dsimp only [leftMatrix]
-      exact_mod_cast entry_le_one false _ _ _⟩
+      exact_mod_cast WriteMatrices.entry_le_one false _ _ _⟩
   · exact ⟨Int.natCast_nonneg _, by
       dsimp only [rightMatrix]
-      exact_mod_cast entry_le_one true _ _ _⟩
+      exact_mod_cast WriteMatrices.entry_le_one true _ _ _⟩
 
 /-- The actual computed ordinal of an existing finite class/chunk/piece. This is a value
 specification for the caller's selection register, not a table supplied to the adapter. -/
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/QueryValues.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/QueryValues.lean
new file mode 100644
index 0000000000..f90c45d9fe
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/QueryValues.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.RecordProduct.Producer
+import Mathlib.Data.List.Nodup
+
+/-!
+# The value of an actual decoded producer query block
+
+The actual occurrence list is exactly the existing finite `chunkOf`, without repetitions,
+and its `i`-th pair has class rank `k*queryCap+i`. Consumers can use original ET pairs directly
+through this packaged readback; no alternative query notion or supplied routing table is added.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+
+/-- The actual decoded list consists of all pairs of the existing chunk, once each, in
+increasing class rank. The indexed equation specifies the order as well as set membership. -/
+theorem decodedQueries_chunkOf {n D g p : ℕ} (values : ℕ → ℤ)
+    (wAB : Fin n → Fin n → ℤ) (hn : 0 < n) (hp : p ≠ 0)
+    (hAB : ∀ a b, values (pairIndex (a, b)) = wAB a b)
+    (hD : 1 ≤ D) (hDn : D ≤ n)
+    {initial y : Data 64} (h : Instances.Output n D g p values initial y)
+    (rho : Fin p) (k : ℕ)
+    (hk : k < numChunks (residueClass wAB p rho) (queryCap n D)) :
+    let q := 5 + 6 * (n * n) + p + 2 * rho.val * (n * n) + 2 * (k * queryCap n D)
+    let Q := min (queryCap n D) ((residueClass wAB p rho).card - k * queryCap n D)
+    let qs := decodedQueries hn y.mem q Q
+    (∀ i : Fin qs.length, qs.get i ∈ chunkOf wAB D p rho k ∧
+      rankIn (residueClass wAB p rho) (qs.get i) = k * queryCap n D + i.val) ∧
+      qs.Nodup ∧ qs.toFinset = chunkOf wAB D p rho k := by
+  let S := residueClass wAB p rho
+  let cap := queryCap n D
+  let q := 5 + 6 * (n * n) + p + 2 * rho.val * (n * n) + 2 * (k * cap)
+  let Q := min cap (S.card - k * cap)
+  let qs := decodedQueries hn y.mem q Q
+  obtain ⟨-, hpair⟩ := output_query_coordinates values wAB hp hAB hD hDn h rho k hk
+  have hget (i : Fin qs.length) : qs.get i ∈ chunkOf wAB D p rho k ∧
+      rankIn S (qs.get i) = k * cap + i.val := by
+    have hi : i.val < Q := by simpa only [qs, decodedQueries_length] using i.isLt
+    obtain ⟨pair, hvalue, -⟩ := hpair i.val hi
+    have hvA : y.mem (q + 2 * i.val) = pair.1.val := hvalue.2.2.1
+    have hvB : y.mem (q + 2 * i.val + 1) = pair.2.val := hvalue.2.2.2
+    have hv := decodedQueries_get_val hn y.mem q Q i
+      (by rw [hvA]; exact pair.1.isLt) (by rw [hvB]; exact pair.2.isLt)
+    have he : qs.get i = pair := by
+      exact Prod.ext (Fin.ext (hv.1.trans hvA)) (Fin.ext (hv.2.trans hvB))
+    rw [he]
+    exact ⟨hvalue.1, hvalue.2.1⟩
+  refine ⟨hget, ?_, ?_⟩
+  · apply List.nodup_iff_injective_get.mpr
+    intro i j hij
+    have hi := (hget i).2
+    have hj := (hget j).2
+    exact Fin.ext (Nat.add_left_cancel
+      (hi.symm.trans ((congrArg (rankIn S) hij).trans hj)))
+  · apply Finset.ext
+    intro pair
+    rw [List.mem_toFinset]
+    constructor
+    · intro hm
+      obtain ⟨i, rfl⟩ := List.mem_iff_get.mp hm
+      exact (hget i).1
+    · intro hm
+      have hchunk : pair ∈ S ∧ rankIn S pair / cap = k := by
+        simpa only [chunkOf, chunk, Finset.mem_filter, S, cap] using hm
+      have hrank := rankIn_lt_card hchunk.1
+      have hcap : 0 < cap := one_le_queryCap hD hDn
+      have hrem := Nat.mod_lt (rankIn S pair) hcap
+      have hsplit := Nat.div_add_mod (rankIn S pair) cap
+      rw [hchunk.2] at hsplit
+      rw [Nat.mul_comm cap k] at hsplit
+      have hi : rankIn S pair % cap < Q := by dsimp only [Q]; omega
+      let i : Fin qs.length := ⟨rankIn S pair % cap, by
+        simpa only [qs, decodedQueries_length] using hi⟩
+      have hv := hget i
+      have hmem : qs.get i ∈ S := by
+        exact (Finset.mem_filter.mp hv.1).1
+      have he : qs.get i = pair := rankIn_injOn S hmem hchunk.1 (by
+        rw [hv.2]
+        simpa only [i] using hsplit)
+      exact List.mem_iff_get.mpr ⟨i, he⟩
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/RawInput.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/RawInput.lean
index bd86b23f73..113123c8c4 100644
--- a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/RawInput.lean
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/RawInput.lean
@@ -37,6 +37,21 @@ a total specification; actual producer coordinates are proved in range before us
 theorem decodedQueries_length {n : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) (q Q : ℕ) :
     (decodedQueries hn mem q Q).length = Q := List.length_ofFn
 
+/-- In-range actual query words are exactly the original coordinate values in the decoded
+occurrence. The total specification's modulo does not change valid producer words. -/
+theorem decodedQueries_get_val {n : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) (q Q : ℕ)
+    (i : Fin (decodedQueries hn mem q Q).length)
+    (ha : mem (q + 2 * i.val) < n) (hb : mem (q + 2 * i.val + 1) < n) :
+    ((decodedQueries hn mem q Q).get i).1.val = mem (q + 2 * i.val) ∧
+      ((decodedQueries hn mem q Q).get i).2.val = mem (q + 2 * i.val + 1) := by
+  constructor
+  · rw [List.get_eq_getElem]
+    simp only [decodedQueries, List.getElem_ofFn]
+    exact Nat.mod_eq_of_lt ha
+  · rw [List.get_eq_getElem]
+    simp only [decodedQueries, List.getElem_ofFn]
+    exact Nat.mod_eq_of_lt hb
+
 /-- Every actual in-range coordinate word reappears unchanged in the ordinary callee input. -/
 theorem decodedQueries_words {m n q Q : ℕ} (hn : 0 < n) (mem : ℕ → ℕ)
     (X : Matrix (Fin n) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin n) ℤ)
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness.lean
new file mode 100644
index 0000000000..0bc8f554d7
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness.lean
@@ -0,0 +1,59 @@
+/-
+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.TimeBound
+
+/-!
+# Native per-record ExactTriangle witness recovery
+
+One fixed standard unsigned WordRAM program starts from the existing original `(D,g,n,p)`
+headers and three canonical-signed weight arrays. It runs the real producer, selects the first
+occupied record, calls the actual native queried product, reads its actual answers/interleaved
+pairs and verifies the original signed sums. No catalogue, layout, execution, answer, witness,
+fit or time certificate is an algorithm input. The generic caller supports any occupied record.
+
+## Main definitions
+
+* `RecordWitness.program`, `RecordWitness.entryProgram`: caller and initialized code, using
+  400 fixed registers with the complete 320-register product bank and 32-register verifier.
+* `RecordWitness.admissionWidth`, `RecordWitness.wordBound`: original-input width and prefix
+  word/support envelopes, independent of every larger admitted physical width.
+
+## Main results
+
+* `RecordWitness.exec_of_output`: actual product and verification for a genuine producer output.
+* `RecordWitness.runs_input`: original `State.init`, same-state prefix `Runs`, charged halt,
+  finite chunk/piece correctness, original-coordinate witness and caller frame.
+* `RecordWitness.admissionWidth_le_log`, `RecordWitness.wordBound_le_pow`,
+  `RecordWitness.bounded_reachable_original`: positive logarithmic width and polynomial words
+  and memory support at every prefix, including physical dirty loads before normalization.
+* `RecordWitness.initialized_time_le`: preparation and actual product charges, plus all actual
+  root/query/control work and scans; unsuccessful records have no extra successful-scan term.
+
+The physical program is fixed and has at most 133120 flat slots including halt. Geometry is
+`D=4^m≥16`, `L=19m`, `n≥D^18`, `g≥1`, and `p` in the existing source prime window. The raw
+0/1 matrix words are converted exactly once by the reused real product. Native success is
+equivalent to an original zero in the selected chunk/piece. The actual scan counter satisfies
+`S≤falsePositiveCount+returnedFlag`, where the returned flag is raw unsigned 0/1. All memory
+outside the original product window and the low producer bank are preserved.
+
+This is a per-record component. Prime/global parameter selection, the outer ET instance loop,
+aggregate subcubic ET analysis and the full ordinary 3SUM 1.9992 endpoint remain open under #1394.
+No curated headline abstract is affected.
+
+## References
+
+The original-weight scan and short-circuit accounting adapt
+[Scan.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Witnesses/Scan.lean#L73-L89)
+and [ScanPairs.lean](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Witnesses/ScanPairs.lean#L69-L70).
+The native code, initialized composition, fits, frames and instruction constants are original;
+no Light-machine execution or resource bound is transferred by assumption. Finite `scanPiece`
+returns its first zero, while the native verifier returns its last zero in the same interval;
+their failure conditions agree, and every returned original-coordinate witness is verified.
+-/
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Consume.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Consume.lean
new file mode 100644
index 0000000000..3c1606b047
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Consume.lean
@@ -0,0 +1,100 @@
+/-
+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.Header
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Queries
+
+/-!
+# Complete per-record candidate consumption
+
+The real header reads the record and computes its piece interval. The real query loop then
+loads product answers and original pairs, verifies the original signed weights and returns a
+genuine original-coordinate witness when one exists among the selected pairs. All memory and
+the complete earlier producer/product register bank are preserved.
+
+The numerical component premises are discharged from original caller data by the initialized
+composition. In particular the record and answer words here are read from actual memory, not
+supplied witness or execution certificates.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Algorithms.ExactTriangle
+
+-- This checks the finite write sets of the fixed consumer, including the renamed scan bank.
+set_option maxRecDepth 4096 in
+private theorem consume_preserves : ∀ j : Fin 400, j.val < 320 → consume.Preserves j := by
+  decide
+
+/-- Execute the actual descriptor decoder and short-circuit verifier loop. The additional
+scan term uses the native counter, bounded by failed accepted pairs plus one success. -/
+theorem exec_consume {w U n D g i records heap out : ℕ}
+    (AB BC AC : ℕ → ℕ → ℤ) (a b : ℕ → ℕ) (x : Data 400) (v : Fin 6 → ℕ)
+    (hD : x.mem 1 = D) (hg : x.mem 2 = g) (hn : x.mem 3 = n)
+    (hi : x.regs (productBank RecordProduct.Reg.ordinal) = i)
+    (hrecords : x.regs (productBank (RecordProduct.producerBank Instances.output)) = records)
+    (hout : x.regs (productBank RecordProduct.Reg.result) = out)
+    (hrec : records + i * (6 + 2 * (n * D)) + 6 ≤ heap)
+    (hv : ∀ j : Fin 6, x.mem (records + i * (6 + 2 * (n * D)) + j.val) = v j)
+    (hfirst : v 1 * pieceSize D g ≤ n)
+    (hquery : ∀ j < v 3, x.mem (v 2 + 2 * j) = a j ∧
+      x.mem (v 2 + 2 * j + 1) = b j ∧ a j < n ∧ b j < n)
+    (hmem : ∀ u < n, ∀ z < n,
+      x.mem (5 + (u * n + z)) = Signed.encode (AB u z) ∧
+      x.mem (5 + n * n + (u * n + z)) = Signed.encode (BC u z) ∧
+      x.mem (5 + n * n + n * n + (u * n + z)) = Signed.encode (AC u z))
+    (hmag : ∀ u < n, ∀ z < n,
+      (AB u z).natAbs ≤ U ∧ (BC u z).natAbs ≤ U ∧ (AC u z).natAbs ≤ U)
+    (hU : GenericRAM.Signed.Fits w (2 * U : ℕ))
+    (hfit : Fits (w + 2) (heap + out + v 2 + 4 * v 3 + 4 * D +
+      2 * (n * D) + 9 * (n * n) + 4 * n + g + 2048)) :
+    let first := v 1 * pieceSize D g
+    let length := min (pieceSize D g) (n - first)
+    ∃ y S, ExecWithin (w + 2) consume x y
+        (5 * Nat.sqrt D + 8 * v 3 + (42 * length + 28) * S + 52) ∧
+      y.mem = x.mem ∧ y.regs Reg.scans = S ∧
+      S ≤ Nat.count (fun j => x.mem (out + j) ≠ 0 ∧
+        ∀ c : Fin length, AB (a j) (b j) + BC (b j) (first + c.val) +
+          AC (a j) (first + c.val) ≠ 0) (v 3) + y.regs Reg.found ∧
+      (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+      (y.regs Reg.found = 1 ↔ ∃ j < v 3, x.mem (out + j) ≠ 0 ∧
+        ∃ c, first ≤ c ∧ c < first + length ∧ AB (a j) (b j) + BC (b j) c + AC (a j) c = 0) ∧
+      (y.regs Reg.found = 1 → ∃ j < v 3,
+        x.mem (out + j) ≠ 0 ∧ y.regs Reg.witnessA = a j ∧ y.regs Reg.witnessB = b j ∧
+        first ≤ y.regs Reg.witnessC ∧ y.regs Reg.witnessC < first + length ∧
+        AB (a j) (b j) + BC (b j) (y.regs Reg.witnessC) +
+          AC (a j) (y.regs Reg.witnessC) = 0) ∧
+      ∀ j : Fin 400, j.val < 320 → y.regs j = x.regs j := by
+  let first := v 1 * pieceSize D g
+  let length := min (pieceSize D g) (n - first)
+  have hlength : first + length ≤ n := by
+    dsimp only [length, first]
+    have := min_le_right (pieceSize D g) (n - v 1 * pieceSize D g)
+    omega
+  obtain ⟨s, hs, sFixed, sm, sf, -, -, -, ss, si, -⟩ := exec_header x v hD hg hn hi
+    hrecords hout hrec hv hfirst (hfit.of_le (by omega))
+  obtain ⟨y, S, he, -, ym, -, ys, hS, yf, iffFound, yw⟩ := exec_queries
+    AB BC AC a b s sFixed si ss sf (by simpa only [sm] using hquery)
+    hlength (by simpa only [sm] using hmem) hmag hU
+    (hfit.of_le (by omega))
+  change ExecWithin (w + 2) (.loop (.lt Reg.index Reg.count) step) s y
+    (8 * v 3 + (42 * length + 28) * S + 2) at he
+  have hexe : ExecWithin (w + 2) consume x y
+      (5 * Nat.sqrt D + 8 * v 3 + (42 * length + 28) * S + 52) :=
+    (hs.seq he).mono (by omega)
+  refine ⟨y, S, hexe, ym.trans sm, ys, ?_, yf, ?_, ?_, ?_⟩
+  · simpa only [sm] using hS
+  · simpa only [sm] using iffFound
+  · simpa only [sm] using yw
+  · intro j hj
+    exact hexe.regs_eq (consume_preserves j hj)
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Entry.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Entry.lean
new file mode 100644
index 0000000000..c6ab79af30
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Entry.lean
@@ -0,0 +1,200 @@
+/-
+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.Prepare
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Original
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Failures
+
+/-!
+# Initialized producer, actual product and original-weight witness recovery
+
+The input contains only the original scalar headers and three signed arrays. The fixed native
+program constructs its real catalogue, selects its first actual record, computes its product,
+loads its real queries and verifies original weights. False-positive accounting is derived
+from the producer's actual repetition-free chunk. This is one record, not an outer ET solver.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+/-- Actual initialized structured execution, with original-coordinate soundness and complete
+coverage of the selected chunk/piece. Failed records incur no extra successful-scan charge. -/
+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 a b : Fin n => V (pairIndex (a, b))
+    let wBC := fun b c : Fin n => V (n * n + pairIndex (b, c))
+    let wAC := fun a c : Fin n => V (2 * (n * n) + pairIndex (a, c))
+    InputFits (w + 2) (PreparationInput.input n (D m) g p values) ∧
+    ∃ a : Data 64, ∃ idx : InstanceIndex p,
+      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 ∧
+      idx ∈ instanceIndices wAB (D m) g p ∧
+      RecordProduct.recordOrdinal n (D m) g p V idx = 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
+      let length := min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g)
+      ∃ y S, ExecWithin (w + 2) entryProgram
+          (.init (PreparationInput.input n (D m) g p values)) y
+          (RecordProduct.preparationTime n (D m) g p values +
+            RecordProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q +
+            (42 * length + 28) * S + 52) ∧
+        y.Bounded (w + 2) ∧ y.regs Reg.scans = S ∧
+        (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+        S ≤ falsePositiveCount wAB wBC wAC p + y.regs Reg.found ∧
+        (y.regs Reg.found = 1 ↔
+          ∃ q ∈ chunkOf wAB (D m) p idx.1 idx.2.1,
+            ∃ c ∈ piece n (D m) g idx.2.2, weightSum wAB wBC wAC q.1 q.2 c = 0) ∧
+        (y.regs Reg.found = 1 → ∃ u v c : Fin n,
+          y.regs Reg.witnessA = u.val ∧ y.regs Reg.witnessB = v.val ∧
+          y.regs Reg.witnessC = c.val ∧ (u, v) ∈ chunkOf wAB (D m) p idx.1 idx.2.1 ∧
+          c ∈ piece n (D m) g idx.2.2 ∧ weightSum wAB wBC wAC u v c = 0) ∧
+        (∀ u, u < a.regs Instances.heap ∨
+          a.regs Instances.heap + CallableProduct.windowSize n Q ≤ u → y.mem u = a.mem u) ∧
+        ∀ j : Fin 64, y.regs (productBank (RecordProduct.producerBank j)) = a.regs j := by
+  let V := fun q => values.getD q 0
+  let wAB := fun a b : Fin n => V (pairIndex (a, b))
+  let wBC := fun b c : Fin n => V (n * n + pairIndex (b, c))
+  let wAC := fun a c : Fin n => V (2 * (n * n) + pairIndex (a, c))
+  let AB := fun a b : ℕ => V (a * n + b)
+  let BC := fun b c : ℕ => V (n * n + (b * n + c))
+  let AC := fun a c : ℕ => V (2 * (n * n) + (a * n + 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.pos
+  obtain ⟨hinput, a, idx, z, ha, hout, hidx, hord, hz, zmap, zi, zheap⟩ :=
+    prepare_input values hlen hD hg hp0 hN hv hW
+  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 hlenQ : qs.length = Q := RecordProduct.decodedQueries_length hn a.mem q Q
+  have zmem : z.mem = a.mem := congrArg (fun d : Data 64 => d.mem) zmap
+  have hzout : Instances.Output n (D m) g p V
+      (.init (PreparationInput.input n (D m) g p values))
+      ((z.comap productBank).comap RecordProduct.producerBank) := by
+    rw [zmap]
+    exact hout
+  have hQ : Q ≤ n ^ 2 := by
+    unfold Q RecordProduct.recordQueryCount
+    rw [pow_two]
+    exact (min_le_right _ _).trans ((Nat.sub_le _ _).trans (Nat.count_le _))
+  have hmem : ∀ 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 hn := Nat.mul_le_mul_right n (Nat.succ_le_of_lt hu)
+    rw [Nat.succ_mul] at hn
+    refine ⟨original_word values a z hout zmap (by omega), ?_, ?_⟩
+    · simpa only [Nat.add_assoc] using
+        original_word (q := n * n + (u * n + v)) values a z hout zmap (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_word values a z hout zmap (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 hn := Nat.mul_le_mul_right n (Nat.succ_le_of_lt hu)
+    rw [Nat.succ_mul] at hn
+    exact ⟨original_magnitude values hlen hv (by omega),
+      original_magnitude values hlen hv (by omega), original_magnitude values hlen hv (by omega)⟩
+  obtain ⟨y, S, he, ys, yf, hS, yiff, answers, yw, frame, regs⟩ := exec_of_output
+    V AB BC AC (.init (PreparationInput.input n (D m) g p values)) z hzout hD hg
+    (by omega : p ≠ 0) hN rfl rfl rfl idx hidx (by rw [zi, hord]) hmem hmag
+    (signed_fits hW) (physical_fits zheap hQ hN hW)
+  simp only [zmem] at he hS yiff answers yw frame
+  rw [zmem] at answers
+  change ∀ j : Fin qs.length,
+    y.mem (y.regs (productBank RecordProduct.Reg.result) + j.val) = Signed.encode
+      ((RecordProduct.leftMatrix m n g p V idx * RecordProduct.rightMatrix m n g p V idx)
+        (qs.get j).1 (qs.get j).2) at answers
+  change ExecWithin (w + 2) program z y (RecordProduct.timeBound (m := m) qs +
+    5 * Nat.sqrt (D m) + 8 * Q +
+    (42 * min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g) + 28) * S + 52) at he
+  have hheap : z.regs (productBank 42) = a.regs Instances.heap :=
+    congrArg (fun d : Data 64 => d.regs Instances.heap) zmap
+  have hex : ExecWithin (w + 2) entryProgram
+      (.init (PreparationInput.input n (D m) g p values)) y
+      (RecordProduct.preparationTime n (D m) g p values +
+        RecordProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q +
+        (42 * min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g) + 28) * S + 52) := by
+    obtain ⟨t, ht, hpref⟩ := hz
+    cases hpref with
+    | seq hp hs => exact ((hp.within.seq (hs.within.seq he))).mono (by omega)
+  obtain ⟨-, -, -, hfirst, -, hcoords, -⟩ := record_view V
+    (.init (PreparationInput.input n (D m) g p values)) a hout hD hDn hg (by omega) idx hidx
+  change ∀ i < Q, a.mem (q + 2 * i) < n ∧ a.mem (q + 2 * i + 1) < n at hcoords
+  have card := QuerySpec.card_residueClass wAB (by omega : p ≠ 0)
+    (fun q => (V q % (p : ℤ)).toNat) (by intro pair; rfl) idx.1
+  obtain ⟨-, hnodup, hset⟩ := RecordProduct.decodedQueries_chunkOf V wAB hn (by omega)
+    (by intro u v; rfl) (by omega) hDn hout idx.1 idx.2.1 ((mem_instanceIndices wAB idx).mp hidx).1
+  rw [card] at hnodup hset
+  change qs.Nodup at hnodup
+  change qs.toFinset = chunkOf wAB (D m) p idx.1 idx.2.1 at hset
+  let argA := fun j => a.mem (q + 2 * j)
+  let argB := fun j => a.mem (q + 2 * j + 1)
+  have hcoordinate (i : Fin qs.length) :
+      argA i.val = (qs.get i).1.val ∧ argB i.val = (qs.get i).2.val := by
+    have hi : i.val < Q := by simpa only [hlenQ] using i.isLt
+    have hh := RecordProduct.decodedQueries_get_val hn a.mem q Q i
+      (hcoords i.val hi).1 (hcoords i.val hi).2
+    exact ⟨hh.1.symm, hh.2.symm⟩
+  have hquery : ∀ pair ∈ qs, pair ∈ chunkOf wAB (D m) p idx.1 idx.2.1 := by
+    intro pair hm
+    rw [← hset, List.mem_toFinset]
+    exact hm
+  let default : Fin n × Fin n := (⟨0, hn⟩, ⟨0, hn⟩)
+  have hfail := native_failed_occurrences_le 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 u v; rfl) (by intro u v; rfl) idx hidx qs default hnodup hquery
+    argA argB hcoordinate y.mem (y.regs (productBank RecordProduct.Reg.result)) answers
+  have hsuccess := 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 u v; rfl) (by intro u v; rfl) idx qs hset
+    argA argB hcoordinate y.mem (y.regs (productBank RecordProduct.Reg.result)) answers
+  rw [hlenQ] at hfail hsuccess
+  refine ⟨hinput, a, idx, ha, hout, hidx, hord, y, S, hex,
+    hex.bounded (Data.Bounded.init hinput), ys, yf, ?_, yiff.trans hsuccess, ?_, ?_, ?_⟩
+  · exact hS.trans (Nat.add_le_add_right hfail _)
+  · intro hy
+    obtain ⟨ha, hb, hlo, hhi, hz, j, hj, hwa, hwb⟩ := yw hy
+    have hc : y.regs Reg.witnessC < n := by
+      have := min_le_right (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g)
+      omega
+    let u : Fin n := ⟨y.regs Reg.witnessA, ha⟩
+    let v : Fin n := ⟨y.regs Reg.witnessB, hb⟩
+    let c : Fin n := ⟨y.regs Reg.witnessC, hc⟩
+    let i : Fin qs.length := ⟨j, by simpa only [hlenQ] using hj⟩
+    have hpq : (u, v) = qs.get i := Prod.ext (Fin.ext (hwa.trans (hcoordinate i).1))
+      (Fin.ext (hwb.trans (hcoordinate i).2))
+    refine ⟨u, v, c, rfl, rfl, rfl, ?_, ?_, hz⟩
+    · rw [hpq]
+      exact hquery _ (List.get_mem _ _)
+    · exact (mem_piece_iff_interval hD hg c).mpr ⟨hlo, hhi⟩
+  · intro u hu
+    exact frame u (by simpa only [hheap] using hu)
+  · intro j
+    rw [regs _ (by change j.val < 65; omega)]
+    exact congrArg (fun d : Data 64 => d.regs j) zmap
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Exec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Exec.lean
new file mode 100644
index 0000000000..6d0780e098
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Exec.lean
@@ -0,0 +1,206 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Consume
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Readback
+
+/-!
+# The real product followed by candidate verification
+
+The general caller selects any occupied record. The actual product is executed on its whole
+renamed 320-register bank; the consumer then reads its real answers and protected query words.
+The original signed arrays and caller catalogue remain untouched. The initialized entry derives
+the numerical premises from original input, rather than supplying an intermediate run contract.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+private theorem productBank_injective : Function.Injective productBank := by
+  intro i j h
+  exact Fin.ext (congrArg (fun k : Fin 400 => k.val) h)
+
+/-- Execute the actual product and verifier from one genuine producer output. No product
+execution, accepted-pair list, witness or time certificate is a hypothesis. -/
+theorem exec_of_output {w U m n g p : ℕ} (values : ℕ → ℤ)
+    (AB BC AC : ℕ → ℕ → ℤ) (initial : Data 64) (x : Data 400)
+    (h : Instances.Output n (D m) g p values initial
+      ((x.comap productBank).comap RecordProduct.producerBank))
+    (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ≠ 0) (hN : D m ^ 18 ≤ n)
+    (hheaderD : initial.mem 1 = D m) (hheaderG : initial.mem 2 = g)
+    (hheaderN : initial.mem 3 = n)
+    (idx : InstanceIndex p)
+    (hidx : idx ∈ instanceIndices (fun a b : Fin n => values (pairIndex (a, b))) (D m) g p)
+    (hi : x.regs (productBank RecordProduct.Reg.ordinal) =
+      RecordProduct.recordOrdinal n (D m) g p values idx)
+    (hmem : ∀ a < n, ∀ b < n,
+      x.mem (5 + (a * n + b)) = Signed.encode (AB a b) ∧
+      x.mem (5 + n * n + (a * n + b)) = Signed.encode (BC a b) ∧
+      x.mem (5 + n * n + n * n + (a * n + b)) = Signed.encode (AC a b))
+    (hmag : ∀ a < n, ∀ b < n,
+      (AB a b).natAbs ≤ U ∧ (BC a b).natAbs ≤ U ∧ (AC a b).natAbs ≤ U)
+    (hU : GenericRAM.Signed.Fits w (2 * U : ℕ))
+    (hfit : Fits (w + 2)
+      (4 * x.regs (productBank 42) +
+        4 * CallableProduct.windowSize n (RecordProduct.recordQueryCount n (D m) p values idx) +
+        QueriedProduct.outputBase (19 * m) m n
+          (RecordProduct.recordQueryCount n (D m) p values idx) +
+        4 * RecordProduct.recordQueryCount n (D m) p values idx + 4 * D m +
+        2 * (n * D m) + 9 * (n * n) + 4 * n + g + 4096)) :
+    let hn : 0 < n := lt_of_lt_of_le (by omega : 0 < D m)
+      ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN)
+    let q := RecordProduct.recordQueries n (D m) p idx
+    let Q := RecordProduct.recordQueryCount n (D m) p values idx
+    let qs := RecordProduct.decodedQueries hn x.mem q Q
+    let first := idx.2.2 * pieceSize (D m) g
+    let length := min (pieceSize (D m) g) (n - first)
+    ∃ y S, ExecWithin (w + 2) program x y
+        (RecordProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q +
+          (42 * length + 28) * S + 52) ∧
+      y.regs Reg.scans = S ∧ (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+      S ≤ Nat.count (fun j => y.mem (y.regs (productBank RecordProduct.Reg.result) + j) ≠ 0 ∧
+        ∀ c : Fin length,
+          AB (x.mem (q + 2 * j)) (x.mem (q + 2 * j + 1)) +
+            BC (x.mem (q + 2 * j + 1)) (first + c.val) +
+            AC (x.mem (q + 2 * j)) (first + c.val) ≠ 0) Q + y.regs Reg.found ∧
+      (y.regs Reg.found = 1 ↔ ∃ j < Q,
+        y.mem (y.regs (productBank RecordProduct.Reg.result) + j) ≠ 0 ∧
+        ∃ c, first ≤ c ∧ c < first + length ∧
+          AB (x.mem (q + 2 * j)) (x.mem (q + 2 * j + 1)) +
+            BC (x.mem (q + 2 * j + 1)) c + AC (x.mem (q + 2 * j)) c = 0) ∧
+      (∀ j : Fin qs.length,
+        y.mem (y.regs (productBank RecordProduct.Reg.result) + j.val) = Signed.encode
+          ((RecordProduct.leftMatrix m n g p values idx *
+            RecordProduct.rightMatrix m n g p values idx) (qs.get j).1 (qs.get j).2)) ∧
+      (y.regs Reg.found = 1 →
+        y.regs Reg.witnessA < n ∧ y.regs Reg.witnessB < n ∧
+        first ≤ y.regs Reg.witnessC ∧ y.regs Reg.witnessC < first + length ∧
+        AB (y.regs Reg.witnessA) (y.regs Reg.witnessB) +
+          BC (y.regs Reg.witnessB) (y.regs Reg.witnessC) +
+          AC (y.regs Reg.witnessA) (y.regs Reg.witnessC) = 0 ∧
+        ∃ j < Q, y.regs Reg.witnessA = x.mem (q + 2 * j) ∧
+          y.regs Reg.witnessB = x.mem (q + 2 * j + 1)) ∧
+      (∀ u, u < x.regs (productBank 42) ∨
+        x.regs (productBank 42) + CallableProduct.windowSize n Q ≤ u → y.mem u = x.mem u) ∧
+      (∀ j : Fin 320, j.val < 65 → y.regs (productBank j) = x.regs (productBank j)) := by
+  let x' := x.comap productBank
+  let produced := x'.comap RecordProduct.producerBank
+  let heap := x.regs (productBank 42)
+  let q := RecordProduct.recordQueries n (D m) p idx
+  let Q := RecordProduct.recordQueryCount n (D m) p values idx
+  let ord := RecordProduct.recordOrdinal n (D m) g p values idx
+  let base := x.regs (productBank (RecordProduct.producerBank Instances.output)) +
+    ord * (6 + 2 * (n * D m))
+  let out := heap + QueriedProduct.outputBase (19 * m) m n Q
+  change Fits (w + 2) (4 * heap + 4 * CallableProduct.windowSize n Q +
+    QueriedProduct.outputBase (19 * m) m n Q + 4 * Q + 4 * D m +
+    2 * (n * D m) + 9 * (n * n) + 4 * n + g + 4096) at hfit
+  have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN
+  have hn : 0 < n := lt_of_lt_of_le (by omega) hDn
+  let qs := RecordProduct.decodedQueries hn x.mem q Q
+  have hlen : qs.length = Q := RecordProduct.decodedQueries_length hn x.mem q Q
+  obtain ⟨hinputEnd, hrec, hq, hfirst, hv, hcoords, hprefix⟩ :=
+    record_view values initial produced h hD hDn hg hp idx hidx
+  change 5 + 3 * (n * n) ≤ heap at hinputEnd
+  change base + 6 ≤ heap at hrec
+  change q + 2 * Q ≤ heap at hq
+  change ∀ j : Fin 6, x.mem (base + j.val) =
+    ![idx.1.val, idx.2.2, q, Q, base + 6, base + 6 + n * D m] j at hv
+  change ∀ j < Q, x.mem (q + 2 * j) < n ∧ x.mem (q + 2 * j + 1) < n at hcoords
+  change ∀ j < 5 + 3 * (n * n), x.mem j = initial.mem j at hprefix
+  obtain ⟨r, hr, rr, rvalues, rmem, rregs, -⟩ := RecordProduct.exec_of_output values
+    initial x' h hD hg hp hN hheaderD hheaderN idx hidx hi (hfit.of_le (by
+      change 2 * heap + 4 * CallableProduct.windowSize n Q + 1024 ≤ _
+      omega))
+  change r.regs RecordProduct.Reg.result =
+    heap + QueriedProduct.outputBase (19 * m) m n qs.length at rr
+  change ∀ j : Fin qs.length,
+    r.mem (heap + (QueriedProduct.outputBase (19 * m) m n qs.length + j.val)) =
+      Signed.encode ((RecordProduct.leftMatrix m n g p values idx *
+        RecordProduct.rightMatrix m n g p values idx) (qs.get j).1 (qs.get j).2) at rvalues
+  simp only [RecordProduct.decodedQueries_length] at rmem
+  change ∀ u, u < heap ∨ heap + CallableProduct.windowSize n Q ≤ u →
+    r.mem u = x.mem u at rmem
+  let s := r.extend productBank x
+  have hs : ExecWithin (w + 2) (RecordProduct.program.rename productBank) x s
+      (RecordProduct.timeBound (m := m) qs) := hr.rename productBank_injective
+  have sr (j : Fin 320) : s.regs (productBank j) = r.regs j :=
+    productBank_injective.extend_apply _ _ j
+  have sm (u : ℕ) (hu : u < heap) : s.mem u = x.mem u := rmem u (Or.inl hu)
+  have snative (j : Fin 320) (hj : j.val < 65) :
+      s.regs (productBank j) = x.regs (productBank j) := (sr j).trans (rregs j hj)
+  have sout : s.regs (productBank RecordProduct.Reg.result) = out := by
+    simpa only [out, hlen] using (sr RecordProduct.Reg.result).trans rr
+  let v : Fin 6 → ℕ := ![idx.1.val, idx.2.2, q, Q, base + 6, base + 6 + n * D m]
+  have hread (j : Fin 6) : s.mem (base + j.val) = v j :=
+    (sm _ (by have := j.isLt; omega)).trans (hv j)
+  have hquery : ∀ j < Q, s.mem (q + 2 * j) = x.mem (q + 2 * j) ∧
+      s.mem (q + 2 * j + 1) = x.mem (q + 2 * j + 1) ∧
+      x.mem (q + 2 * j) < n ∧ x.mem (q + 2 * j + 1) < n := by
+    intro j hj
+    exact ⟨sm _ (by omega), sm _ (by omega), hcoords j hj⟩
+  have smem : ∀ a < n, ∀ b < n,
+      s.mem (5 + (a * n + b)) = Signed.encode (AB a b) ∧
+      s.mem (5 + n * n + (a * n + b)) = Signed.encode (BC a b) ∧
+      s.mem (5 + n * n + n * n + (a * n + b)) = Signed.encode (AC a b) := by
+    intro a ha b hb
+    have hn := Nat.mul_le_mul_right n (Nat.succ_le_of_lt ha)
+    rw [Nat.succ_mul] at hn
+    simpa only [sm _ (by omega : 5 + (a * n + b) < heap),
+      sm _ (by omega : 5 + n * n + (a * n + b) < heap),
+      sm _ (by omega : 5 + n * n + n * n + (a * n + b) < heap)] using hmem a ha b hb
+  obtain ⟨y, S, he, ym, ys, hS, yf, yiff, yw, frame⟩ := exec_consume AB BC AC
+    (fun j => x.mem (q + 2 * j)) (fun j => x.mem (q + 2 * j + 1)) s v
+    ((sm 1 (by omega)).trans ((hprefix 1 (by omega)).trans hheaderD))
+    ((sm 2 (by omega)).trans ((hprefix 2 (by omega)).trans hheaderG))
+    ((sm 3 (by omega)).trans ((hprefix 3 (by omega)).trans hheaderN))
+    ((snative _ (by decide)).trans hi) (snative _ (by decide)) sout hrec hread hfirst
+    hquery smem hmag hU (hfit.of_le (by
+      change heap + out + q + 4 * Q + 4 * D m + 2 * (n * D m) +
+        9 * (n * n) + 4 * n + g + 2048 ≤ _
+      dsimp only [out]
+      omega))
+  change ExecWithin (w + 2) consume s y
+    (5 * Nat.sqrt (D m) + 8 * Q +
+      (42 * min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g) + 28) * S + 52) at he
+  change S ≤ Nat.count (fun j => s.mem (out + j) ≠ 0 ∧
+    ∀ c : Fin (min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g)),
+      AB (x.mem (q + 2 * j)) (x.mem (q + 2 * j + 1)) +
+        BC (x.mem (q + 2 * j + 1)) (idx.2.2 * pieceSize (D m) g + c.val) +
+        AC (x.mem (q + 2 * j)) (idx.2.2 * pieceSize (D m) g + c.val) ≠ 0) Q + y.regs Reg.found at hS
+  simp_rw [show v 1 = idx.2.2 from rfl, show v 3 = Q from rfl] at yiff
+  have hexe : ExecWithin (w + 2) program x y
+      (RecordProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q +
+        (42 * min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g) + 28) * S + 52) :=
+    (hs.seq he).mono (by omega)
+  refine ⟨y, S, hexe, ys, yf, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · simpa only [ym, frame (productBank RecordProduct.Reg.result) (by decide), sout] using hS
+  · simpa only [ym, frame (productBank RecordProduct.Reg.result) (by decide), sout] using yiff
+  · intro j
+    have hv := rvalues j
+    rw [frame _ (by decide), sout, ym]
+    change r.mem (out + j.val) = _
+    simpa only [out, hlen, Nat.add_assoc] using hv
+  · intro hy
+    obtain ⟨j, hj, -, hwa, hwb, hlo, hhi, hz⟩ := yw hy
+    obtain ⟨ha, hb⟩ := hcoords j hj
+    exact ⟨by simpa only [hwa] using ha, by simpa only [hwb] using hb,
+      hlo, hhi, by simpa only [hwa, hwb] using hz, j, hj, hwa, hwb⟩
+  · intro u hu
+    rw [ym]
+    exact rmem u hu
+  · intro j hj
+    exact (frame _ (by change j.val < 320; omega)).trans (snative j hj)
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Failures.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Failures.lean
new file mode 100644
index 0000000000..5618c23a4f
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Failures.lean
@@ -0,0 +1,143 @@
+/-
+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
+
+/-!
+# Original false positives bound the actual native failed occurrences
+
+Actual answer words and original query coordinates determine the native failure predicate.
+For the producer's repetition-free chunk, these occurrences inject into the existing finite
+failed scans, whose distinct false-positive bound is already proved. This is a value/readback
+lemma: actual execution supplies its premises, with no assumed answer or witness oracle.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Interpret the native failure predicate on real product words. Each failed original query
+occurs only once, so its count is bounded by original-weight modular false positives. -/
+theorem native_failed_occurrences_le {m n g p : ℕ} (values : ℕ → ℤ)
+    (AB BC AC : ℕ → ℕ → ℤ) (wAB wBC wAC : Fin n → Fin n → ℤ)
+    (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m))
+    (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)
+    (hvaluesBC : ∀ b c, values (n * n + pairIndex (b, c)) = wBC b c)
+    (hvaluesAC : ∀ a c, values (2 * (n * n) + pairIndex (a, c)) = wAC a c)
+    (idx : InstanceIndex p) (hidx : idx ∈ instanceIndices wAB (D m) g p)
+    (qs : List (Fin n × Fin n)) (default : Fin n × Fin n) (hqs : qs.Nodup)
+    (hquery : ∀ q ∈ qs, q ∈ chunkOf wAB (D m) p idx.1 idx.2.1)
+    (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 ≤ 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
+    (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. -/
+theorem actual_success_iff {m n g p : ℕ} (values : ℕ → ℤ)
+    (AB BC AC : ℕ → ℕ → ℤ) (wAB wBC wAC : Fin n → Fin n → ℤ)
+    (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m))
+    (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)
+    (hvaluesBC : ∀ b c, values (n * n + pairIndex (b, c)) = wBC b c)
+    (hvaluesAC : ∀ a c, values (2 * (n * n) + pairIndex (a, c)) = wAC a c)
+    (idx : InstanceIndex p) (qs : List (Fin n × Fin n))
+    (hset : qs.toFinset = chunkOf wAB (D m) p idx.1 idx.2.1)
+    (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)
+    (∃ i < qs.length, mem (out + i) ≠ 0 ∧
+      ∃ c, first ≤ c ∧ c < first + length ∧ AB (a i) (b i) + BC (b i) c + AC (a i) c = 0) ↔
+      ∃ q ∈ chunkOf wAB (D m) p idx.1 idx.2.1,
+        ∃ c ∈ piece n (D m) g idx.2.2, weightSum wAB wBC wAC q.1 q.2 c = 0 := by
+  let first := idx.2.2 * pieceSize (D m) g
+  let length := min (pieceSize (D m) g) (n - first)
+  have pair_mem (i : Fin qs.length) : qs.get i ∈ chunkOf wAB (D m) p idx.1 idx.2.1 := by
+    rw [← hset, List.mem_toFinset]
+    exact List.get_mem _ _
+  constructor
+  · rintro ⟨i, hi, -, c, hlo, hhi, hz⟩
+    let j : Fin qs.length := ⟨i, hi⟩
+    have hl := min_le_right (pieceSize (D m) g) (n - first)
+    have hn : c < n := by change first ≤ c at hlo; change c < first + length at hhi; omega
+    let vertex : Fin n := ⟨c, hn⟩
+    have hc : vertex ∈ piece n (D m) g idx.2.2 :=
+      (mem_piece_iff_interval hD hg vertex).mpr ⟨hlo, hhi⟩
+    obtain ⟨ha, hb⟩ := hcoords j
+    have he : AB (a i) (b i) + BC (b i) c + AC (a i) c =
+        weightSum wAB wBC wAC (qs.get j).1 (qs.get j).2 vertex := by
+      rw [ha, hb]
+      change AB (qs.get j).1.val (qs.get j).2.val +
+        BC (qs.get j).2.val vertex.val + AC (qs.get j).1.val vertex.val = _
+      rw [hAB, hBC, hAC]
+      rfl
+    exact ⟨qs.get j, pair_mem j, vertex, hc, he.symm.trans hz⟩
+  · rintro ⟨q, hq, c, hc, hz⟩
+    have hmem : q ∈ qs := by rw [← List.mem_toFinset, hset]; exact hq
+    obtain ⟨j, hj⟩ := List.mem_iff_get.mp hmem
+    obtain ⟨ha, hb⟩ := hcoords j
+    have hpair : (lopInstance wAB wBC wAC (D m) g p idx).HasCommonNeighbor q.1 q.2 := by
+      apply (hasCommonNeighbor_lopInstance_iff wAB wBC wAC
+        (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.ne_zero hq).mpr
+      exact ⟨c, hc, by rw [hz]⟩
+    have hprod := (RecordProduct.product_ne_zero_iff values wAB wBC wAC hD hg hp
+      hvaluesBC hvaluesAC idx q.1 q.2).mpr hpair
+    refine ⟨j.val, j.isLt, ?_, c.val, ?_, ?_, ?_⟩
+    · intro hzero
+      apply hprod
+      have he := hanswer j
+      rw [hj] at he
+      apply Signed.encode_injective
+      exact he.symm.trans hzero
+    · exact ((mem_piece_iff_interval hD hg c).mp hc).1
+    · exact ((mem_piece_iff_interval hD hg c).mp hc).2
+    · rw [ha, hb, hj, hAB, hBC, hAC]
+      exact hz
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Flat.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Flat.lean
new file mode 100644
index 0000000000..7ca9c2f25d
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Flat.lean
@@ -0,0 +1,103 @@
+/-
+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.Entry
+
+/-!
+# Actual initialized flat witness-recovery runs
+
+One fixed standard unsigned program starts from the original input, computes the actual first
+record's product and verifies its accepted pairs. The same actual state witnesses the prefix
+run, final charged halt, original-coordinate result, false-positive accounting and caller frame.
+This is a per-record endpoint; choosing parameters and the outer ET record loop remain separate.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+/-- The complete initialized standard-native program uses 400 fixed registers, at most
+133120 flat instruction slots including halt, and never inspects physical word width. -/
+theorem entryProgram_fixed : (entryProgram.program Reg.found).length ≤ 133120 ∧
+    ¬(entryProgram.program Reg.found).ReadsWidth := by
+  constructor
+  · simp only [Code.program, List.length_append, Code.length_assemble,
+      List.length_singleton, entryProgram, Code.size, produce, RecordProduct.produce,
+      program, Code.size_rename]
+    have hc := RecordProduct.program_fixed.1
+    have hp := Instances.program_fixed.1
+    have hs := consume_fixed.1
+    omega
+  · apply Code.not_readsWidth_program
+    simp only [entryProgram, Code.ReadsWidth, produce, RecordProduct.produce,
+      Code.readsWidth_rename, Op.ReadsWidth, false_or, program]
+    exact not_or.mpr ⟨Instances.program_fixed.2,
+      not_or.mpr ⟨RecordProduct.program_fixed.2, consume_fixed.2⟩⟩
+
+/-- Every sufficiently wide physical word size executes the actual original-input program.
+Returned success is exactly an original zero in this actual selected chunk/piece, and every
+returned coordinate belongs to that original witness. The instruction bound includes halt. -/
+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 a b : Fin n => V (pairIndex (a, b))
+    let wBC := fun b c : Fin n => V (n * n + pairIndex (b, c))
+    let wAC := fun a c : Fin n => V (2 * (n * n) + pairIndex (a, c))
+    InputFits W (PreparationInput.input n (D m) g p values) ∧
+    ∃ a : Data 64, ∃ idx : InstanceIndex p,
+      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 ∧
+      idx ∈ instanceIndices wAB (D m) g p ∧
+      RecordProduct.recordOrdinal n (D m) g p V idx = 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
+      let length := min (pieceSize (D m) g) (n - idx.2.2 * pieceSize (D m) g)
+      ∃ y t S, t + 1 ≤ RecordProduct.preparationTime n (D m) g p values +
+          RecordProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * Q +
+          (42 * length + 28) * S + 53 ∧
+        Runs W (entryProgram.program Reg.found)
+          (State.init (PreparationInput.input n (D m) g p values)) ⟨entryProgram.size, y⟩ t ∧
+        Executes W (entryProgram.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.scans = S ∧
+        (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+        S ≤ falsePositiveCount wAB wBC wAC p + y.regs Reg.found ∧
+        (y.regs Reg.found = 1 ↔
+          ∃ q ∈ chunkOf wAB (D m) p idx.1 idx.2.1,
+            ∃ c ∈ piece n (D m) g idx.2.2, weightSum wAB wBC wAC q.1 q.2 c = 0) ∧
+        (y.regs Reg.found = 1 → ∃ u v c : Fin n,
+          y.regs Reg.witnessA = u.val ∧ y.regs Reg.witnessB = v.val ∧
+          y.regs Reg.witnessC = c.val ∧ (u, v) ∈ chunkOf wAB (D m) p idx.1 idx.2.1 ∧
+          c ∈ piece n (D m) g idx.2.2 ∧ weightSum wAB wBC wAC u v c = 0) ∧
+        (∀ u, u < a.regs Instances.heap ∨
+          a.regs Instances.heap + CallableProduct.windowSize n Q ≤ u → y.mem u = a.mem u) ∧
+        ∀ j : Fin 64, y.regs (productBank (RecordProduct.producerBank j)) = a.regs j := by
+  have htwo : 2 ≤ W := by unfold admissionWidth at hW; 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, idx, ha, hout, hidx, hord, y, S, he, yb, ys, yf, hS, yiff, yw, frame, regs⟩ := h
+  obtain ⟨t, ht, hex⟩ := he
+  refine ⟨hi, a, idx, ha, hout, hidx, hord, y, t, S, by omega,
+    ?_, ?_, yb, ys, yf, hS, yiff, yw, frame, regs⟩
+  · simpa only [Nat.zero_add, State.init] using hex.runs (pc := 0)
+      (p := entryProgram.program Reg.found) (Program.Contains.self _).append_left
+  · simpa only [State.init] using hex.executes Reg.found
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Header.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Header.lean
new file mode 100644
index 0000000000..3201d2b1b9
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Header.lean
@@ -0,0 +1,250 @@
+/-
+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.Spec
+import Complexity.Computability.WordRAM.RegisterFrame
+
+/-!
+# Actual record and interval-header execution
+
+These internal rules read the producer's real scalar/record words and run the existing native
+square-root loop. Record and piece metadata are never supplied as predecoded algorithm inputs.
+The original producer/product bank and all memory are preserved.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM
+open Cslib.Algorithms.ExactTriangle
+
+-- Closed preservation checks enumerate the four-hundred-register caller bank.
+set_option maxRecDepth 4096 in
+private theorem readRecord_preserves : ∀ i : Fin 400, i.val < 320 → readRecord.Preserves i := by
+  decide
+
+private theorem sqrtBank_injective : Function.Injective sqrtBank := by
+  intro i j h
+  apply Fin.ext
+  simpa only [sqrtBank, Nat.add_left_cancel_iff] using congrArg Fin.val h
+
+private theorem squareRoot_preserves (i : Fin 400) (hi : i.val < 336 ∨ 342 ≤ i.val) :
+    squareRoot.Preserves i := by
+  apply Code.preserves_rename_of_forall_ne
+  intro j hj
+  have hv := congrArg Fin.val hj
+  change 336 + j.val = i.val at hv
+  have hj := j.isLt
+  omega
+
+/-- Read the original dimension/divisor and this actual six-word record, then reset the
+per-record search state. The record address is computed from the native selected ordinal. -/
+theorem exec_readRecord {W n D g i records heap out : ℕ} (x : Data 400) (v : Fin 6 → ℕ)
+    (hD : x.mem 1 = D) (hg : x.mem 2 = g) (hn : x.mem 3 = n)
+    (hi : x.regs (productBank RecordProduct.Reg.ordinal) = i)
+    (hrecords : x.regs (productBank (RecordProduct.producerBank Instances.output)) = records)
+    (hout : x.regs (productBank RecordProduct.Reg.result) = out)
+    (hrec : records + i * (6 + 2 * (n * D)) + 6 ≤ heap)
+    (hv : ∀ j : Fin 6, x.mem (records + i * (6 + 2 * (n * D)) + j.val) = v j)
+    (hfit : Fits W (heap + 2 * (n * D) + D + n + g + 128)) :
+    ∃ y, ExecWithin W readRecord x y 28 ∧ y.mem = x.mem ∧
+      y.regs (sqrtBank NatSqrt.arg) = D ∧ y.regs Reg.size = n ∧
+      y.regs Reg.divisor = g ∧ y.regs Reg.output = out ∧
+      y.regs Reg.piece = v 1 ∧ y.regs Reg.queries = v 2 ∧ y.regs Reg.count = v 3 ∧
+      y.regs Reg.found = 0 ∧ y.regs Reg.witnessA = 0 ∧ y.regs Reg.witnessB = 0 ∧
+      y.regs Reg.witnessC = 0 ∧ y.regs Reg.scans = 0 ∧ y.regs Reg.index = 0 ∧
+      y.regs Reg.one = 1 ∧ y.regs Reg.zero = 0 ∧
+      ∀ j : Fin 400, j.val < 320 → y.regs j = x.regs j := by
+  let stride := n * D + n * D + 6
+  let r := records + i * stride
+  have heq : stride = 6 + 2 * (n * D) := by dsimp only [stride]; omega
+  have hrange : r + 6 ≤ heap := by simpa only [r, heq] using hrec
+  have h1 : Fits W 1 := hfit.of_le (by omega)
+  have h2 : Fits W 2 := hfit.of_le (by omega)
+  have h3 : Fits W 3 := hfit.of_le (by omega)
+  have h6 : Fits W 6 := hfit.of_le (by omega)
+  have harea : Fits W (n * D) := hfit.of_le (by omega)
+  have htwice : Fits W (n * D + n * D) := hfit.of_le (by omega)
+  have hstride : Fits W stride := hfit.of_le (by dsimp only [stride]; omega)
+  have hmul : Fits W (i * stride) := hfit.of_le (by dsimp only [r] at hrange; omega)
+  have hr : Fits W r := hfit.of_le (by omega)
+  have hr1 : Fits W (r + 1) := hfit.of_le (by omega)
+  have hr2 : Fits W (r + 1 + 1) := hfit.of_le (by omega)
+  have hr3 : Fits W (r + 1 + 1 + 1) := hfit.of_le (by omega)
+  have hv1 : x.mem (r + 1) = v 1 := by simpa +decide [r, heq] using hv ⟨1, by decide⟩
+  have hv2 : x.mem (r + 1 + 1) = v 2 := by
+    change x.mem (r + 2) = v 2
+    simpa +decide [r, heq] using hv ⟨2, by decide⟩
+  have hv3 : x.mem (r + 1 + 1 + 1) = v 3 := by
+    change x.mem (r + 3) = v 3
+    simpa +decide [r, heq] using hv ⟨3, by decide⟩
+  dsimp only [productBank, RecordProduct.producerBank, RecordProduct.Reg.ordinal,
+    RecordProduct.Reg.result, Instances.output, Fin.castLE] at hi hrecords hout
+  dsimp only [r, stride] at hstride hmul hr hr1 hr2 hr3 hv1 hv2 hv3
+  let y := x.set Reg.one 1 |>.set Reg.zero 0 |>.set Reg.address 3 |>.set Reg.size n
+    |>.set Reg.address 1 |>.set Reg.temp D |>.set (sqrtBank NatSqrt.arg) D
+    |>.set Reg.address 2 |>.set Reg.divisor g |>.set Reg.output out
+    |>.set Reg.temp (n * D) |>.set Reg.temp (n * D + n * D) |>.set Reg.piece 6
+    |>.set Reg.temp stride |>.set Reg.address (i * stride) |>.set Reg.address r
+    |>.set Reg.address (r + 1) |>.set Reg.piece (v 1)
+    |>.set Reg.address (r + 1 + 1) |>.set Reg.queries (v 2)
+    |>.set Reg.address (r + 1 + 1 + 1) |>.set Reg.count (v 3)
+    |>.set Reg.found 0 |>.set Reg.witnessA 0 |>.set Reg.witnessB 0 |>.set Reg.witnessC 0
+    |>.set Reg.scans 0 |>.set Reg.index 0
+  have he : ExecWithin W readRecord x y 28 := by
+    ram_eval [readRecord, y, r, stride, hD, hg, hn, hi, hrecords, hout, hv1, hv2, hv3,
+      h1, h2, h3, h6, harea, htwice, hstride, hmul, hr, hr1, hr2, hr3,
+      Reg.one, Reg.zero, Reg.address, Reg.size, Reg.temp, Reg.divisor, Reg.output,
+      Reg.piece, Reg.queries, Reg.count, Reg.found, Reg.witnessA, Reg.witnessB,
+      Reg.witnessC, Reg.scans, Reg.index, productBank, sqrtBank, RecordProduct.producerBank,
+      RecordProduct.Reg.ordinal, RecordProduct.Reg.result, Instances.output, NatSqrt.arg,
+      Fin.castLE]
+  refine ⟨y, he, rfl, ?_⟩
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  all_goals first
+    | exact fun j hj => he.regs_eq (readRecord_preserves j hj)
+    | simp +decide [y, Reg.one, Reg.zero, Reg.address, Reg.size, Reg.temp, Reg.divisor,
+        Reg.output, Reg.piece, Reg.queries, Reg.count, Reg.found, Reg.witnessA,
+        Reg.witnessB, Reg.witnessC, Reg.scans, Reg.index, sqrtBank, NatSqrt.arg]
+
+/-- The local interval decoder executes the actual square-root loop, preserving the complete
+old bank and controller registers. Its result is derived, not a square-root certificate. -/
+theorem exec_squareRoot {W D : ℕ} (x : Data 400)
+    (hD : x.regs (sqrtBank NatSqrt.arg) = D) (hfit : Fits W (4 * D + 4)) :
+    ∃ y, ExecWithin W squareRoot x y (5 * Nat.sqrt D + 7) ∧
+      y.regs (sqrtBank NatSqrt.root) = Nat.sqrt D ∧ y.mem = x.mem ∧
+      ∀ i : Fin 400, i.val < 336 ∨ 342 ≤ i.val → y.regs i = x.regs i := by
+  obtain ⟨y, hy, hr, -, hm, -⟩ := NatSqrt.exec_rename sqrtBank sqrtBank_injective x (by
+    rw [hD]; exact hfit)
+  refine ⟨y, ?_, ?_, hm, fun i hi => hy.regs_eq (squareRoot_preserves i hi)⟩
+  · simpa only [squareRoot, hD] using hy
+  · simpa only [hD] using hr
+
+-- Closed preservation over the finite controller and old product bank.
+set_option maxRecDepth 4096 in
+private theorem finishHeader_preserves : ∀ i : Fin 400,
+    i.val < 324 ∨ i = Reg.index ∨ i = Reg.one ∨ i = Reg.piece ∨
+      i = Reg.divisor ∨ 392 ≤ i.val → finishHeader.Preserves i := by decide
+
+/-- Compute the actual interval and original signed-array pointers after the real root loop.
+All query/output metadata and success/counter initialization are preserved. -/
+theorem exec_finishHeader {W n S g k : ℕ} (x : Data 400)
+    (hroot : x.regs (sqrtBank NatSqrt.root) = S) (hn : x.regs Reg.size = n)
+    (hg : x.regs Reg.divisor = g) (hk : x.regs Reg.piece = k)
+    (h1 : x.regs Reg.one = 1) (hc : k * (S ⌈/⌉ g) ≤ n)
+    (hfit : Fits W (S + g + 3 * (n * n) + n + 64)) :
+    let B := S ⌈/⌉ g
+    let first := k * B
+    let length := min B (n - first)
+    ∃ y, ExecWithin W finishHeader x y 15 ∧ y.mem = x.mem ∧
+      y.regs Reg.blockLength = B ∧ y.regs Reg.first = first ∧ y.regs Reg.length = length ∧
+      y.regs (scanBank WitnessScan.Reg.ab) = 5 ∧
+      y.regs (scanBank WitnessScan.Reg.bc) = 5 + n * n ∧
+      y.regs (scanBank WitnessScan.Reg.ac) = 5 + n * n + n * n ∧
+      y.regs (scanBank WitnessScan.Reg.size) = n ∧
+      y.regs (scanBank WitnessScan.Reg.first) = first ∧
+      y.regs (scanBank WitnessScan.Reg.length) = length ∧
+      ∀ i : Fin 400, i.val < 324 ∨ i = Reg.index ∨ i = Reg.one ∨ i = Reg.piece ∨
+        i = Reg.divisor ∨ 392 ≤ i.val → y.regs i = x.regs i := by
+  let B := S ⌈/⌉ g
+  let first := k * B
+  let length := min B (n - first)
+  have hquot : (S + g - 1) / g = B := by simp only [B, Nat.ceilDiv_eq_add_pred_div]
+  have hsum : Fits W (S + g) := hfit.of_le (by omega)
+  have hsub : Fits W (S + g - 1) := hsum.of_le (Nat.sub_le ..)
+  have hB : Fits W B := by rw [← hquot]; exact hsub.of_le (Nat.div_le_self ..)
+  have hfirst : Fits W first := hfit.of_le (by change k * B ≤ n at hc; dsimp only [first]; omega)
+  have hlen : Fits W (n - first) := hfit.of_le (by omega)
+  have harea : Fits W (n * n) := hfit.of_le (by omega)
+  have h5 : Fits W 5 := hfit.of_le (by omega)
+  have hbc : Fits W (5 + n * n) := hfit.of_le (by omega)
+  have hac : Fits W (5 + n * n + n * n) := hfit.of_le (by omega)
+  dsimp only [sqrtBank, NatSqrt.root] at hroot
+  let y := x.set Reg.blockLength (S + g) |>.set Reg.blockLength (S + g - 1)
+    |>.set Reg.blockLength B |>.set Reg.first first |>.set Reg.length (n - first)
+    |>.set Reg.length length |>.set (scanBank WitnessScan.Reg.ab) 5
+    |>.set Reg.temp (n * n) |>.set (scanBank WitnessScan.Reg.bc) (5 + n * n)
+    |>.set (scanBank WitnessScan.Reg.ac) (5 + n * n + n * n)
+    |>.set (scanBank WitnessScan.Reg.size) n |>.set (scanBank WitnessScan.Reg.first) first
+    |>.set (scanBank WitnessScan.Reg.length) length
+  have he : ExecWithin W finishHeader x y 15 := by
+    by_cases hlt : B < n - first
+    · have hl : length = B := min_eq_left hlt.le
+      ram_eval [finishHeader, y, hroot, hn, hg, hk, h1, hquot, hlt, hl,
+        hsum, hsub, hB, hfirst, hlen, harea, h5, hbc, hac, B, first, length,
+        Reg.blockLength, Reg.divisor, Reg.one, Reg.piece, Reg.first, Reg.length, Reg.size,
+        Reg.temp, scanBank, sqrtBank, WitnessScan.Reg.ab, WitnessScan.Reg.bc, WitnessScan.Reg.ac,
+        WitnessScan.Reg.size, WitnessScan.Reg.first, WitnessScan.Reg.length, NatSqrt.root]
+    · have hl : length = n - first := min_eq_right (by omega)
+      ram_eval [finishHeader, y, hroot, hn, hg, hk, h1, hquot, hlt, hl,
+        hsum, hsub, hB, hfirst, hlen, harea, h5, hbc, hac, B, first, length,
+        Reg.blockLength, Reg.divisor, Reg.one, Reg.piece, Reg.first, Reg.length, Reg.size,
+        Reg.temp, scanBank, sqrtBank, WitnessScan.Reg.ab, WitnessScan.Reg.bc, WitnessScan.Reg.ac,
+        WitnessScan.Reg.size, WitnessScan.Reg.first, WitnessScan.Reg.length, NatSqrt.root]
+  refine ⟨y, he, rfl, ?_⟩
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  all_goals first
+    | exact fun i hi => he.regs_eq (finishHeader_preserves i hi)
+    | rfl
+
+/-- Complete charged local setup from real scalar and descriptor reads. The computed original
+piece interval and all verifier arguments are conclusions of the actual code. -/
+theorem exec_header {W n D g i records heap out : ℕ} (x : Data 400) (v : Fin 6 → ℕ)
+    (hD : x.mem 1 = D) (hg : x.mem 2 = g) (hn : x.mem 3 = n)
+    (hi : x.regs (productBank RecordProduct.Reg.ordinal) = i)
+    (hrecords : x.regs (productBank (RecordProduct.producerBank Instances.output)) = records)
+    (hout : x.regs (productBank RecordProduct.Reg.result) = out)
+    (hrec : records + i * (6 + 2 * (n * D)) + 6 ≤ heap)
+    (hv : ∀ j : Fin 6, x.mem (records + i * (6 + 2 * (n * D)) + j.val) = v j)
+    (hfirst : v 1 * pieceSize D g ≤ n)
+    (hfit : Fits W (heap + 4 * D + 2 * (n * D) + 3 * (n * n) + n + g + 512)) :
+    let first := v 1 * pieceSize D g
+    let length := min (pieceSize D g) (n - first)
+    ∃ y, ExecWithin W header x y (5 * Nat.sqrt D + 50) ∧
+      Fixed n first length out (v 2) (v 3) y ∧ y.mem = x.mem ∧
+      y.regs Reg.found = 0 ∧ y.regs Reg.witnessA = 0 ∧ y.regs Reg.witnessB = 0 ∧
+      y.regs Reg.witnessC = 0 ∧ y.regs Reg.scans = 0 ∧ y.regs Reg.index = 0 ∧
+      ∀ j : Fin 400, j.val < 320 → y.regs j = x.regs j := by
+  obtain ⟨a, ha, am, aD, an, ag, ao, ak, aq, aQ, af, aa, ab, ac, as, ai, a1, a0, ar⟩ :=
+    exec_readRecord x v hD hg hn hi hrecords hout hrec hv (hfit.of_le (by omega))
+  obtain ⟨b, hb, bS, bm, br⟩ := exec_squareRoot a aD (hfit.of_le (by omega))
+  have bn : b.regs Reg.size = n := (br _ (by decide)).trans an
+  have bg : b.regs Reg.divisor = g := (br _ (by decide)).trans ag
+  have bk : b.regs Reg.piece = v 1 := (br _ (by decide)).trans ak
+  have b1 : b.regs Reg.one = 1 := (br _ (by decide)).trans a1
+  have hsqrt := Nat.sqrt_le_self D
+  obtain ⟨y, hy, ym, yB, yf, yl, yab, ybc, yac, yn, yfirst, ylength, yr⟩ :=
+    exec_finishHeader b bS bn bg bk b1 hfirst (hfit.of_le (by omega))
+  refine ⟨y, (ha.seq (hb.seq hy)).mono (by omega), ?_, ym.trans (bm.trans am),
+    (yr _ (by decide)).trans ((br _ (by decide)).trans af),
+    (yr _ (by decide)).trans ((br _ (by decide)).trans aa),
+    (yr _ (by decide)).trans ((br _ (by decide)).trans ab),
+    (yr _ (by decide)).trans ((br _ (by decide)).trans ac),
+    (yr _ (by decide)).trans ((br _ (by decide)).trans as),
+    (yr _ (by decide)).trans ((br _ (by decide)).trans ai), ?_⟩
+  · exact
+      { output := (yr _ (by decide)).trans ((br _ (by decide)).trans ao)
+        queries := (yr _ (by decide)).trans ((br _ (by decide)).trans aq)
+        count := (yr _ (by decide)).trans ((br _ (by decide)).trans aQ)
+        size := (yr _ (by decide)).trans bn
+        first := yf
+        length := yl
+        one := (yr _ (by decide)).trans b1
+        zero := (yr _ (by decide)).trans ((br _ (by decide)).trans a0)
+        ab := yab
+        bc := ybc
+        ac := yac
+        scanSize := yn
+        scanFirst := yfirst
+        scanLength := ylength }
+  · intro j hj
+    exact (yr j (Or.inl (by omega))).trans ((br j (Or.inl (by omega))).trans (ar j hj))
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Kernel.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Kernel.lean
new file mode 100644
index 0000000000..3a6e504766
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Kernel.lean
@@ -0,0 +1,188 @@
+/-
+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.Spec
+import Complexity.Computability.WordRAM.RegisterFrame
+
+/-!
+# Real coordinate delivery, verifier calls and witness returns
+
+The internal call rule invokes the complete native signed-weight verifier, preserves the
+controller and old product bank, and returns its original zero-sum vertex. Query delivery
+loads the actual interleaved words and increments the actual scan counter. No run or witness
+routine is supplied by a caller.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM
+
+private abbrev Stable (i : Fin 400) : Prop :=
+  i.val < 326 ∨ i = Reg.one ∨ i = Reg.zero ∨
+    (345 ≤ i.val ∧ i.val ≤ 348) ∨ (351 ≤ i.val ∧ i.val ≤ 352)
+
+-- These closed checks enumerate only the finite caller bank and loop-free delivery/return code.
+set_option maxRecDepth 4096 in
+private theorem deliverPair_preserves : ∀ i : Fin 400, Stable i → deliverPair.Preserves i := by
+  decide
+
+-- The same finite controller-frame check, without unfolding the verifier program.
+set_option maxRecDepth 4096 in
+private theorem receiveWitness_preserves : ∀ i : Fin 400, Stable i →
+    receiveWitness.Preserves i := by decide
+
+private theorem scanBank_injective : Function.Injective scanBank := by
+  intro i j h
+  apply Fin.ext
+  simpa only [scanBank, Nat.add_left_cancel_iff] using congrArg Fin.val h
+
+/-- Execute the real original-weight verifier on the disjoint bank. Every scanned weight
+comes from the original arrays; a nonzero product answer supplies no original-weight witness. -/
+theorem exec_scan {w U n first length out queries count a b : ℕ}
+    (AB BC AC : ℕ → ℕ → ℤ) (x : Data 400)
+    (hx : Fixed n first length out queries count x)
+    (hargA : x.regs (scanBank WitnessScan.Reg.a) = a)
+    (hargB : x.regs (scanBank WitnessScan.Reg.b) = b)
+    (ha : a < n) (hb : b < n) (hc : first + length ≤ n)
+    (hmem : ∀ i < n, ∀ j < n,
+      x.mem (5 + (i * n + j)) = Signed.encode (AB i j) ∧
+      x.mem (5 + n * n + (i * n + j)) = Signed.encode (BC i j) ∧
+      x.mem (5 + n * n + n * n + (i * n + j)) = Signed.encode (AC i j))
+    (hmag : ∀ i < n, ∀ j < n,
+      (AB i j).natAbs ≤ U ∧ (BC i j).natAbs ≤ U ∧ (AC i j).natAbs ≤ U)
+    (hU : GenericRAM.Signed.Fits w (2 * U : ℕ))
+    (hfit : Fits (w + 2) (6 * (n * n) + n + first + length + 24)) :
+    ∃ y, ExecWithin (w + 2) scan x y (42 * length + 17) ∧
+      Fixed n first length out queries count y ∧ y.mem = x.mem ∧
+      y.regs (scanBank WitnessScan.Reg.a) = a ∧
+      y.regs (scanBank WitnessScan.Reg.b) = b ∧
+      (y.regs (scanBank WitnessScan.Reg.found) = 0 ∨
+        y.regs (scanBank WitnessScan.Reg.found) = 1) ∧
+      (y.regs (scanBank WitnessScan.Reg.found) = 1 ↔
+        ∃ c, first ≤ c ∧ c < first + length ∧ AB a b + BC b c + AC a c = 0) ∧
+      (y.regs (scanBank WitnessScan.Reg.found) = 1 →
+        first ≤ y.regs (scanBank WitnessScan.Reg.witness) ∧
+        y.regs (scanBank WitnessScan.Reg.witness) < first + length ∧
+        AB a b + BC b (y.regs (scanBank WitnessScan.Reg.witness)) +
+          AC a (y.regs (scanBank WitnessScan.Reg.witness)) = 0) ∧
+      ∀ i : Fin 400, i.val < 336 ∨ 368 ≤ i.val → y.regs i = x.regs i := by
+  let A : WitnessScan.Args := ⟨5, 5 + n * n, 5 + n * n + n * n, n, a, b, first, length⟩
+  have hargs : A.InRegisters (x.comap scanBank) :=
+    ⟨hx.ab, hx.bc, hx.ac, hx.scanSize, hargA, hargB, hx.scanFirst, hx.scanLength⟩
+  obtain ⟨s, hs, sa, sm, sf, si, sw⟩ := WitnessScan.exec A AB BC AC (x.comap scanBank)
+    hargs ha hb hc hmem hmag hU (hfit.of_le (by
+      dsimp only [A, WitnessScan.Args.addressBound]; omega))
+  let y := s.extend scanBank x
+  have he : ExecWithin (w + 2) scan x y (42 * length + 17) := hs.rename scanBank_injective
+  have yr (i : Fin 32) : y.regs (scanBank i) = s.regs i :=
+    scanBank_injective.extend_apply _ _ i
+  have frame (i : Fin 400) (hi : i.val < 336 ∨ 368 ≤ i.val) : y.regs i = x.regs i := by
+    apply he.regs_eq
+    apply Code.preserves_rename_of_forall_ne
+    intro j hj
+    have hv := congrArg Fin.val hj
+    change 336 + j.val = i.val at hv
+    have hj := j.isLt
+    omega
+  obtain ⟨sab, sbc, sac, sn, sa', sb', sfirst, slength⟩ := sa
+  refine ⟨y, he, ?_, sm, (yr _).trans sa', (yr _).trans sb', ?_, ?_, ?_, frame⟩
+  · exact
+      { output := (frame _ (by decide)).trans hx.output
+        queries := (frame _ (by decide)).trans hx.queries
+        count := (frame _ (by decide)).trans hx.count
+        size := (frame _ (by decide)).trans hx.size
+        first := (frame _ (by decide)).trans hx.first
+        length := (frame _ (by decide)).trans hx.length
+        one := (frame _ (by decide)).trans hx.one
+        zero := (frame _ (by decide)).trans hx.zero
+        ab := (yr _).trans sab
+        bc := (yr _).trans sbc
+        ac := (yr _).trans sac
+        scanSize := (yr _).trans sn
+        scanFirst := (yr _).trans sfirst
+        scanLength := (yr _).trans slength }
+  · simpa only [yr] using sf
+  · simpa only [yr] using si
+  · simpa only [yr] using sw
+
+/-- Load the actual query occurrence into the verifier arguments and increment the native
+scan count. No query enumeration or pair supplied as an algorithm argument replaces the loads. -/
+theorem exec_deliverPair {W n first length out queries count i scans a b : ℕ} (x : Data 400)
+    (hx : Fixed n first length out queries count x)
+    (hi : x.regs Reg.index = i) (hs : x.regs Reg.scans = scans)
+    (ha : x.mem (queries + 2 * i) = a) (hb : x.mem (queries + 2 * i + 1) = b)
+    (hfit : Fits W (queries + 2 * i + scans + 8)) :
+    ∃ y, ExecWithin W deliverPair x y 6 ∧ Fixed n first length out queries count y ∧
+      y.mem = x.mem ∧ y.regs (scanBank WitnessScan.Reg.a) = a ∧
+      y.regs (scanBank WitnessScan.Reg.b) = b ∧ y.regs Reg.scans = scans + 1 ∧
+      y.regs Reg.index = i ∧ y.regs Reg.found = x.regs Reg.found ∧
+      ∀ j : Fin 400, j.val < 326 ∨ j = Reg.one ∨ j = Reg.zero ∨
+        (345 ≤ j.val ∧ j.val ≤ 348) ∨ (351 ≤ j.val ∧ j.val ≤ 352) →
+        y.regs j = x.regs j := by
+  have hd : Fits W (i + i) := hfit.of_le (by omega)
+  have hp : Fits W (i + i + queries) := hfit.of_le (by omega)
+  have hp1 : Fits W (i + i + queries + 1) := hfit.of_le (by omega)
+  have hs1 : Fits W (scans + 1) := hfit.of_le (by omega)
+  have hreadA : x.mem (i + i + queries) = a := by simpa only [two_mul, Nat.add_comm] using ha
+  have hreadB : x.mem (i + i + queries + 1) = b := by
+    simpa only [two_mul, Nat.add_comm] using hb
+  let y := x.set Reg.address (i + i) |>.set Reg.address (i + i + queries)
+    |>.set (scanBank WitnessScan.Reg.a) a |>.set Reg.address (i + i + queries + 1)
+    |>.set (scanBank WitnessScan.Reg.b) b |>.set Reg.scans (scans + 1)
+  have he : ExecWithin W deliverPair x y 6 := by
+    ram_eval [deliverPair, y, hi, hs, hx.queries, hx.one, hreadA, hreadB,
+      hd, hp, hp1, hs1, Reg.address, Reg.index, Reg.queries, Reg.one, Reg.scans,
+      scanBank, WitnessScan.Reg.a, WitnessScan.Reg.b]
+  have frame (j : Fin 400) (hj : Stable j) : y.regs j = x.regs j :=
+    he.regs_eq (deliverPair_preserves j hj)
+  refine ⟨y, he, hx.of_frame frame, rfl, ?_, ?_, ?_, ?_, ?_, frame⟩
+  · rfl
+  · rfl
+  · rfl
+  · exact (he.regs_eq (by decide)).trans hi
+  · exact he.regs_eq (by decide)
+
+/-- Copy back only a genuinely reported verifier success and its actual original coordinates.
+This is a charged native branch, preserving all fixed arguments, memory and the scan count. -/
+theorem exec_receiveWitness {W n first length out queries count flag a b c : ℕ} (x : Data 400)
+    (hx : Fixed n first length out queries count x)
+    (hf : x.regs (scanBank WitnessScan.Reg.found) = flag)
+    (ha : x.regs (scanBank WitnessScan.Reg.a) = a)
+    (hb : x.regs (scanBank WitnessScan.Reg.b) = b)
+    (hc : x.regs (scanBank WitnessScan.Reg.witness) = c) :
+    ∃ y, ExecWithin W receiveWitness x y 5 ∧ Fixed n first length out queries count y ∧
+      y.mem = x.mem ∧ y.regs Reg.found = (if flag = 1 then 1 else x.regs Reg.found) ∧
+      y.regs Reg.witnessA = (if flag = 1 then a else x.regs Reg.witnessA) ∧
+      y.regs Reg.witnessB = (if flag = 1 then b else x.regs Reg.witnessB) ∧
+      y.regs Reg.witnessC = (if flag = 1 then c else x.regs Reg.witnessC) ∧
+      y.regs Reg.scans = x.regs Reg.scans ∧ y.regs Reg.index = x.regs Reg.index ∧
+      ∀ j : Fin 400, j.val < 326 ∨ j = Reg.one ∨ j = Reg.zero ∨
+        (345 ≤ j.val ∧ j.val ≤ 348) ∨ (351 ≤ j.val ∧ j.val ≤ 352) →
+        y.regs j = x.regs j := by
+  let y := if flag = 1 then x.set Reg.found 1 |>.set Reg.witnessA a
+      |>.set Reg.witnessB b |>.set Reg.witnessC c
+    else x.set Reg.found (x.regs Reg.found)
+  dsimp only [scanBank, WitnessScan.Reg.found, WitnessScan.Reg.a,
+    WitnessScan.Reg.b, WitnessScan.Reg.witness] at hf ha hb hc
+  have he : ExecWithin W receiveWitness x y 5 := by
+    by_cases h : flag = 1 <;>
+      ram_eval [receiveWitness, y, h, hf, ha, hb, hc, hx.one, Reg.one, Reg.found,
+        Reg.witnessA, Reg.witnessB, Reg.witnessC, scanBank, WitnessScan.Reg.found,
+        WitnessScan.Reg.a, WitnessScan.Reg.b, WitnessScan.Reg.witness]
+  have frame (j : Fin 400) (hj : Stable j) : y.regs j = x.regs j :=
+    he.regs_eq (receiveWitness_preserves j hj)
+  refine ⟨y, he, hx.of_frame frame, ?_, ?_, ?_, ?_, ?_,
+    he.regs_eq (by decide), he.regs_eq (by decide), frame⟩
+  all_goals
+    dsimp only [y]
+    split_ifs <;> rfl
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Original.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Original.lean
new file mode 100644
index 0000000000..7f7ea3d07d
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Original.lean
@@ -0,0 +1,46 @@
+/-
+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.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationInput
+
+/-!
+# Original signed arrays after real preparation
+
+The producer's existing prefix frame retains every original signed input word. These internal
+readback rules relate the recovery bank to those same words and to their original magnitude
+bound; they do not assume intermediate signed fits or add a second input encoding.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM
+
+/-- Each original payload word survives preparation in the unchanged caller prefix. -/
+theorem original_word {n D g p q : ℕ} (values : List ℤ) (a : Data 64) (z : Data 400)
+    (hout : Instances.Output n D g p (fun q => values.getD q 0)
+      (.init (PreparationInput.input n D g p values)) a)
+    (hmap : (z.comap productBank).comap RecordProduct.producerBank = a)
+    (hq : q < 3 * (n * n)) : z.mem (5 + q) = Signed.encode (values.getD q 0) := by
+  have hm : z.mem = a.mem := congrArg (fun d : Data 64 => d.mem) hmap
+  rw [hm, hout.2.2.2.2.2.2.2.2.2.2.2 (5 + q) (Or.inl (by omega))]
+  exact PreparationInput.input_word n D g p values q
+
+/-- Original magnitude bounds supply every original array entry, not merely a fitting
+intermediate machine state. The implicit index equation is the producer's existing layout. -/
+theorem original_magnitude {n A q : ℕ} (values : List ℤ)
+    (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A)
+    (hq : q < 3 * (n * n)) : (values.getD q 0).natAbs ≤ A := by
+  have hi : q < values.length := by omega
+  rw [List.getD_eq_getElem _ _ hi]
+  exact hv _ (List.getElem_mem hi)
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Pair.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Pair.lean
new file mode 100644
index 0000000000..6048bc7760
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Pair.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.RecordWitness.Kernel
+
+/-!
+# One actual product-selected original-weight verification
+
+The coordinate words are loaded from the original interleaved query block. The full renamed
+native verifier reads the original three signed arrays, and its result is returned to the
+controller. This internal call rule charges delivery, the complete scan and witness return.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM
+
+/-- Execute one selected candidate from its actual query words. A reported witness satisfies
+the original integer equation, independently of whether the modular candidate was genuine. -/
+theorem exec_scanPair {w U n first length out queries count i scans a b : ℕ}
+    (AB BC AC : ℕ → ℕ → ℤ) (x : Data 400)
+    (hx : Fixed n first length out queries count x)
+    (hi : x.regs Reg.index = i) (hs : x.regs Reg.scans = scans)
+    (hf : x.regs Reg.found = 0)
+    (haWord : x.mem (queries + 2 * i) = a)
+    (hbWord : x.mem (queries + 2 * i + 1) = b)
+    (ha : a < n) (hb : b < n) (hc : first + length ≤ n)
+    (hmem : ∀ u < n, ∀ v < n,
+      x.mem (5 + (u * n + v)) = Signed.encode (AB u v) ∧
+      x.mem (5 + n * n + (u * n + v)) = Signed.encode (BC u v) ∧
+      x.mem (5 + n * n + n * n + (u * n + v)) = Signed.encode (AC u v))
+    (hmag : ∀ u < n, ∀ v < n,
+      (AB u v).natAbs ≤ U ∧ (BC u v).natAbs ≤ U ∧ (AC u v).natAbs ≤ U)
+    (hU : GenericRAM.Signed.Fits w (2 * U : ℕ))
+    (hfit : Fits (w + 2)
+      (queries + 2 * i + scans + 6 * (n * n) + n + first + length + 32)) :
+    ∃ y, ExecWithin (w + 2) scanPair x y (42 * length + 28) ∧
+      Fixed n first length out queries count y ∧ y.mem = x.mem ∧
+      y.regs Reg.index = i ∧ y.regs Reg.scans = scans + 1 ∧
+      (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+      (y.regs Reg.found = 1 ↔
+        ∃ c, first ≤ c ∧ c < first + length ∧ AB a b + BC b c + AC a c = 0) ∧
+      (y.regs Reg.found = 1 →
+        y.regs Reg.witnessA = a ∧ y.regs Reg.witnessB = b ∧
+        first ≤ y.regs Reg.witnessC ∧ y.regs Reg.witnessC < first + length ∧
+        AB a b + BC b (y.regs Reg.witnessC) + AC a (y.regs Reg.witnessC) = 0) := by
+  obtain ⟨d, hd, dFixed, dm, da, db, ds, di, df, -⟩ :=
+    exec_deliverPair x hx hi hs haWord hbWord (hfit.of_le (by omega))
+  obtain ⟨s, he, sFixed, sm, sa, sb, sf, iffFound, sw, frame⟩ :=
+    exec_scan AB BC AC d dFixed da db ha hb hc (by simpa only [dm] using hmem)
+      hmag hU (hfit.of_le (by omega))
+  obtain ⟨y, hy, yFixed, ym, yf, ya, yb, yc, ys, yi, -⟩ :=
+    exec_receiveWitness s sFixed rfl sa sb rfl
+  have sIndex : s.regs Reg.index = i := (frame _ (by decide)).trans di
+  have sScans : s.regs Reg.scans = scans + 1 := (frame _ (by decide)).trans ds
+  have sFound : s.regs Reg.found = 0 := (frame _ (by decide)).trans (df.trans hf)
+  have hexe : ExecWithin (w + 2) scanPair x y (42 * length + 28) :=
+    (hd.seq (he.seq hy)).mono (by omega)
+  have yflag : y.regs Reg.found = s.regs (scanBank WitnessScan.Reg.found) := by
+    rcases sf with sf | sf <;> simp only [yf, sf, sFound, Nat.zero_ne_one, ↓reduceIte]
+  refine ⟨y, hexe, yFixed, ym.trans (sm.trans dm), yi.trans sIndex, ys.trans sScans,
+    ?_, ?_, ?_⟩
+  · simpa only [yflag] using sf
+  · simpa only [yflag] using iffFound
+  · intro hfound
+    have hsfound : s.regs (scanBank WitnessScan.Reg.found) = 1 := yflag.symm.trans hfound
+    obtain ⟨lo, hi, hz⟩ := sw hsfound
+    refine ⟨?_, ?_, ?_, ?_, ?_⟩
+    · simpa only [hsfound, ↓reduceIte] using ya
+    · simpa only [hsfound, ↓reduceIte] using yb
+    · simpa only [yc, hsfound, ↓reduceIte] using lo
+    · simpa only [yc, hsfound, ↓reduceIte] using hi
+    · simpa only [yc, hsfound, ↓reduceIte] using hz
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Prepare.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Prepare.lean
new file mode 100644
index 0000000000..d69d7b429b
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Prepare.lean
@@ -0,0 +1,113 @@
+/-
+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.Width
+
+/-!
+# Real initialized preparation for candidate recovery
+
+This internal composition rule executes the existing producer on its complete renamed bank,
+then selects ordinal zero with one real instruction. Nonemptiness and the producer's original
+word bound are derived from the original input and actual execution. No prepared catalogue,
+index, run or intermediate fit certificate is an input to this rule.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- Actual preparation and charged first-record selection, from the original initialized
+input. All later structured/flat clients reuse this same producer state and selected record. -/
+theorem prepare_input {w m n g p A : ℕ} (values : List ℤ)
+    (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m)
+    (hg : 1 ≤ g) (hp : 0 < p) (hN : D m ^ 18 ≤ n)
+    (hv : ∀ z ∈ values, z.natAbs ≤ A)
+    (hW : admissionWidth n (D m) g p A ≤ w + 2) :
+    InputFits (w + 2) (PreparationInput.input n (D m) g p values) ∧
+      ∃ a : Data 64, ∃ idx : InstanceIndex p, ∃ z : Data 400,
+        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 (fun q => values.getD q 0)
+          (.init (PreparationInput.input n (D m) g p values)) a ∧
+        idx ∈ instanceIndices (fun a b : Fin n => values.getD (pairIndex (a, b)) 0) (D m) g p ∧
+        RecordProduct.recordOrdinal n (D m) g p (fun q => values.getD q 0) idx = 0 ∧
+        ExecWithin (w + 2)
+          (.seq produce (.op (.const (productBank RecordProduct.Reg.ordinal) 0)))
+          (.init (PreparationInput.input n (D m) g p values)) z
+          (RecordProduct.preparationTime n (D m) g p values) ∧
+        (z.comap productBank).comap RecordProduct.producerBank = a ∧
+        z.regs (productBank RecordProduct.Reg.ordinal) = 0 ∧
+        z.regs (productBank 42) ≤ PreparationInput.wordBound n (D m) g p A := by
+  have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN
+  have hw : PreparationInput.width n (D m) g p A ≤ w + 2 := by
+    unfold admissionWidth RecordProduct.admissionWidth at hW
+    omega
+  obtain ⟨a, ha, hout, hi, -⟩ := PreparationInput.exec_input values hlen
+    (by omega) hDn hg hp 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 productBank := by
+    intro i j h
+    exact Fin.ext (congrArg (fun k : Fin 400 => k.val) h)
+  let x₀ : Data 320 := .init (PreparationInput.input n (D m) g p values)
+  let x := a.extend RecordProduct.producerBank x₀
+  have hx : ExecWithin (w + 2) RecordProduct.produce x₀ x
+      (RecordProduct.preparationTime n (D m) g p values - 1) := ha'.rename hf
+  let y₀ : Data 400 := .init (PreparationInput.input n (D m) g p values)
+  let y := x.extend productBank y₀
+  have hy : ExecWithin (w + 2) produce y₀ y
+      (RecordProduct.preparationTime n (D m) g p values - 1) := hx.rename hf'
+  let z := y.set (productBank RecordProduct.Reg.ordinal) 0
+  have hz : ExecWithin (B := .standard) (w + 2)
+      (.op (.const (productBank RecordProduct.Reg.ordinal) 0)) y z 1 :=
+    ExecWithin.const (fits_zero _)
+  have low (j : Fin 64) : y.regs (productBank (RecordProduct.producerBank j)) = a.regs j :=
+    (hf'.extend_apply _ _ _).trans (hf.extend_apply _ _ _)
+  have zmap : (z.comap productBank).comap RecordProduct.producerBank = a := by
+    ext j
+    · change Function.update y.regs (productBank RecordProduct.Reg.ordinal) 0
+        (productBank (RecordProduct.producerBank j)) = a.regs j
+      have hne : productBank (RecordProduct.producerBank j) ≠
+          productBank RecordProduct.Reg.ordinal := by
+        intro he
+        have hh := congrArg (fun k : Fin 400 => k.val) he
+        change j.val = 64 at hh
+        omega
+      rw [Function.update_of_ne hne]
+      exact low j
+    · rfl
+  obtain ⟨idx, hidx, hord⟩ := RecordProduct.first_index (fun q => values.getD q 0)
+    hD hDn hg (by omega : p ≠ 0)
+  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
+  have hb := PreparationInput.bounded_reachable values hlen (by omega) hDn hg hp hv hw
+    ⟨Instances.program.size, a⟩ t hr
+  refine ⟨hi, a, idx, z, ⟨t, ht, he⟩, hout, hidx, hord, ?_, zmap, rfl, ?_⟩
+  · have hpos : 1 ≤ RecordProduct.preparationTime n (D m) g p values := by
+      dsimp only [RecordProduct.preparationTime, Instances.timeBound]
+      omega
+    exact (hy.seq hz).mono (by omega)
+  · have hheap : z.regs (productBank 42) = a.regs Instances.heap :=
+      congrArg (fun d : Data 64 => d.regs Instances.heap) zmap
+    rw [hheap]
+    exact (hb.1 Instances.heap).le
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Program.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Program.lean
new file mode 100644
index 0000000000..83d4be514c
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Program.lean
@@ -0,0 +1,190 @@
+/-
+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
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.QueryValues
+public import Complexity.Algorithms.WordRAM.ExactTriangle.WitnessScan.Exec
+public import Complexity.Algorithms.WordRAM.NatSqrt
+
+/-!
+# Native consumption of one prepared record's product answers
+
+The existing 320-register producer/product bank stays in place. A disjoint controller reads
+the actual record, derives the original piece interval with charged square-root/ceiling code,
+and reads nonzero encoded product answers and their raw interleaved coordinates. Each accepted
+pair invokes the real original-weight verifier. Once a witness is found, later scans are skipped.
+All memory is read-only in this phase; no result, catalogue or window snapshot is needed.
+
+The consumer adapts the control of the pinned `ScanPairs.lean` procedure in the
+proof of Theorem 17 at `anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`.
+The native ABI, code and charged constants are original. These stage definitions are internal
+implementation interfaces. The outer instance loop and prime/global parameter choice are separate.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM
+
+namespace Reg
+
+/-- Absolute product-answer pointer. -/
+abbrev output : Fin 400 := 320
+/-- Protected interleaved query-pair pointer. -/
+abbrev queries : Fin 400 := 321
+/-- Actual number of query occurrences. -/
+abbrev count : Fin 400 := 322
+/-- Original outer dimension. -/
+abbrev size : Fin 400 := 323
+/-- First original vertex of this piece. -/
+abbrev first : Fin 400 := 324
+/-- Actual number of original vertices in this piece. -/
+abbrev length : Fin 400 := 325
+/-- Number of query occurrences already treated. -/
+abbrev index : Fin 400 := 326
+/-- Constant one. -/
+abbrev one : Fin 400 := 327
+/-- Actual memory-address temporary. -/
+abbrev address : Fin 400 := 328
+/-- Loaded canonical-signed product answer. -/
+abbrev answer : Fin 400 := 329
+/-- Actual piece ordinal read from the prepared record. -/
+abbrev piece : Fin 400 := 332
+/-- Computed maximum piece length. -/
+abbrev blockLength : Fin 400 := 333
+/-- Original positive piece divisor. -/
+abbrev divisor : Fin 400 := 334
+/-- Index/product temporary. -/
+abbrev temp : Fin 400 := 335
+/-- Raw unsigned success flag. -/
+abbrev found : Fin 400 := 392
+/-- Original first coordinate of a verified triangle. -/
+abbrev witnessA : Fin 400 := 393
+/-- Original second coordinate of a verified triangle. -/
+abbrev witnessB : Fin 400 := 394
+/-- Original third coordinate of a verified triangle. -/
+abbrev witnessC : Fin 400 := 395
+/-- Actual number of original-weight interval scans performed. -/
+abbrev scans : Fin 400 := 396
+/-- Constant zero, disjoint from both procedure banks. -/
+abbrev zero : Fin 400 := 399
+
+end Reg
+
+/-- Preserve the complete existing producer/product register bank. -/
+@[expose] def productBank : Fin 320 → Fin 400 := Fin.castLE (by decide)
+
+/-- The entire thirty-two-register original-weight verifier moves together. -/
+@[expose] def scanBank (i : Fin 32) : Fin 400 := ⟨336 + i.val, by omega⟩
+
+/-- The root computation temporarily reuses the first six verifier registers. -/
+@[expose] def sqrtBank (i : Fin 6) : Fin 400 := ⟨336 + i.val, by omega⟩
+
+/-- Actual charged square root for the local piece-size decoder. -/
+@[expose] def squareRoot : Code .standard 400 := NatSqrt.program.rename sqrtBank
+
+open Reg in
+/-- Read original scalar words and the selected record's piece/query fields. -/
+@[expose] def readRecord : Code .standard 400 :=
+  let sqrtArg := sqrtBank NatSqrt.arg
+  let productResult := productBank RecordProduct.Reg.result
+  let ordinal := productBank RecordProduct.Reg.ordinal
+  let records := productBank (RecordProduct.producerBank Instances.output)
+  ram[
+  one ← #1; zero ← #0; address ← #3; size ← *address;
+  address ← #1; temp ← *address; sqrtArg ← temp;
+  address ← #2; divisor ← *address; output ← productResult;
+  temp ← size * temp; temp ← temp + temp; piece ← #6; temp ← temp + piece;
+  address ← ordinal * temp;
+  address ← records + address; address ← address + one; piece ← *address;
+  address ← address + one; queries ← *address; address ← address + one; count ← *address;
+  found ← #0; witnessA ← #0; witnessB ← #0; witnessC ← #0; scans ← #0; index ← #0 ]
+
+open Reg in
+/-- Compute the original interval and deliver the unchanged signed-array pointers once. -/
+@[expose] def finishHeader : Code .standard 400 :=
+  let root := sqrtBank NatSqrt.root
+  let scanAB := scanBank WitnessScan.Reg.ab
+  let scanBC := scanBank WitnessScan.Reg.bc
+  let scanAC := scanBank WitnessScan.Reg.ac
+  let scanN := scanBank WitnessScan.Reg.size
+  let scanFirst := scanBank WitnessScan.Reg.first
+  let scanLength := scanBank WitnessScan.Reg.length
+  ram[
+  blockLength ← root + divisor; blockLength ← blockLength - one;
+  blockLength ← blockLength / divisor; first ← piece * blockLength; length ← size - first;
+  if blockLength < length then [ length ← blockLength ] else [ length ← length ];
+  scanAB ← #5; temp ← size * size;
+  scanBC ← scanAB + temp;
+  scanAC ← scanBC + temp;
+  scanN ← size; scanFirst ← first;
+  scanLength ← length ]
+
+/-- Complete actual local descriptor and interval decoding. -/
+@[expose] def header : Code .standard 400 :=
+  .seq readRecord (.seq squareRoot finishHeader)
+
+/-- Actual original signed-weight scan, with the complete bank renamed together. -/
+@[expose] def scan : Code .standard 400 := WitnessScan.program.rename scanBank
+
+open Reg in
+/-- Load the real original coordinate pair and charge this invocation in the native counter. -/
+@[expose] def deliverPair : Code .standard 400 :=
+  let scanA := scanBank WitnessScan.Reg.a
+  let scanB := scanBank WitnessScan.Reg.b
+  ram[
+  address ← index + index; address ← address + queries;
+  scanA ← *address; address ← address + one;
+  scanB ← *address; scans ← scans + one ]
+
+open Reg in
+/-- A verifier success returns its original vertex together with the actual pair that was read. -/
+@[expose] def receiveWitness : Code .standard 400 :=
+  let scanFound := scanBank WitnessScan.Reg.found
+  let scanA := scanBank WitnessScan.Reg.a
+  let scanB := scanBank WitnessScan.Reg.b
+  let scanC := scanBank WitnessScan.Reg.witness
+  ram[
+  if scanFound = one then [
+    found ← one; witnessA ← scanA; witnessB ← scanB;
+    witnessC ← scanC ] else [ found ← found ] ]
+
+/-- The accepted-candidate branch contains the real verifier, not a supplied witness routine. -/
+@[expose] def scanPair : Code .standard 400 :=
+  .seq deliverPair (.seq scan receiveWitness)
+
+open Reg in
+/-- Read a product answer only while searching, and skip all later scans after a success. -/
+@[expose] def step : Code .standard 400 :=
+  .seq (.branch (.eq found zero)
+    (.seq (ram[ address ← output + index; answer ← *address ])
+      (.branch (.eq answer zero) (.op (.copy answer answer)) scanPair))
+    (.op (.copy answer answer))) (.op (.bin .add index index one))
+
+/-- Consume one actual product-answer slice without modifying any memory. -/
+@[expose] def consume : Code .standard 400 :=
+  .seq header (.loop (.lt Reg.index Reg.count) step)
+
+/-- Actual product calculation followed immediately by original-weight verification. -/
+@[expose] def program : Code .standard 400 :=
+  .seq (RecordProduct.program.rename productBank) consume
+
+/-- The real producer occupies the existing low bank of the larger caller. -/
+@[expose] def produce : Code .standard 400 := RecordProduct.produce.rename productBank
+
+/-- Original initialized producer, actual first-record selection and actual product/verifier.
+The selected ordinal is preserved by the real product, so no later reset is needed. -/
+@[expose] def entryProgram : Code .standard 400 :=
+  .seq produce (.seq (.op (.const (productBank RecordProduct.Reg.ordinal) 0)) program)
+
+/-- The consumer is one fixed finite instruction graph and never reads the physical width. -/
+theorem consume_fixed : consume.size ≤ 512 ∧ ¬consume.ReadsWidth := by decide
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Queries.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Queries.lean
new file mode 100644
index 0000000000..9299161816
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Queries.lean
@@ -0,0 +1,235 @@
+/-
+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.Step
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Trace
+
+/-!
+# The actual short-circuit query loop
+
+The proof derives its scan trace from the original answer words and the verifier's integer
+equation. Runtime execution receives neither trace nor witness function. Variable-cost loop
+accounting charges a complete scan exactly when the native controller actually invokes it.
+The finite scan bound follows the counting argument of pinned `ScanPairs.lean`;
+the native code, ABI and instruction constants are original.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM
+
+private theorem potential_step (active : ℕ → Prop) [DecidablePred active]
+    {i Q T : ℕ} (hi : i < Q) :
+    (if active i then T + 6 else 6) + 2 +
+        (8 * (Q - (i + 1)) + T * (Nat.count active Q - Nat.count active (i + 1))) ≤
+      8 * (Q - i) + T * (Nat.count active Q - Nat.count active i) := by
+  have hcount : Nat.count active (i + 1) = Nat.count active i +
+      (if active i then 1 else 0) := Nat.count_succ active i
+  have hle := Nat.count_monotone active (Nat.succ_le_of_lt hi)
+  change Nat.count active (i + 1) ≤ Nat.count active Q at hle
+  have hindex : Q - i = Q - (i + 1) + 1 := by omega
+  by_cases h : active i
+  · rw [ite_eq_left h] at hcount ⊢
+    rw [hcount] at hle
+    have hd : Nat.count active Q - Nat.count active i =
+        (Nat.count active Q - Nat.count active (i + 1)) + 1 := by omega
+    rw [hindex, hd, Nat.mul_add, Nat.mul_add]
+    omega
+  · rw [ite_eq_right h] at hcount ⊢
+    simp only [Nat.add_zero] at hcount
+    rw [hindex, hcount, Nat.mul_add, Nat.mul_one]
+    omega
+
+/-- Run the actual answer/query loop. Every query coordinate is read from the protected
+interleaved block, and every success is verified against the original three integer arrays.
+Only accepted pairs without an original witness contribute to the failure count. -/
+theorem exec_queries {w U n first length out queries Q : ℕ}
+    (AB BC AC : ℕ → ℕ → ℤ) (a b : ℕ → ℕ) (x : Data 400)
+    (hx : Fixed n first length out queries Q x)
+    (hi : x.regs Reg.index = 0) (hs : x.regs Reg.scans = 0)
+    (hf : x.regs Reg.found = 0)
+    (hquery : ∀ i < Q, x.mem (queries + 2 * i) = a i ∧
+      x.mem (queries + 2 * i + 1) = b i ∧ a i < n ∧ b i < n)
+    (hc : first + length ≤ n)
+    (hmem : ∀ u < n, ∀ v < n,
+      x.mem (5 + (u * n + v)) = Signed.encode (AB u v) ∧
+      x.mem (5 + n * n + (u * n + v)) = Signed.encode (BC u v) ∧
+      x.mem (5 + n * n + n * n + (u * n + v)) = Signed.encode (AC u v))
+    (hmag : ∀ u < n, ∀ v < n,
+      (AB u v).natAbs ≤ U ∧ (BC u v).natAbs ≤ U ∧ (AC u v).natAbs ≤ U)
+    (hU : GenericRAM.Signed.Fits w (2 * U : ℕ))
+    (hfit : Fits (w + 2)
+      (out + queries + 4 * Q + 6 * (n * n) + n + first + length + 64)) :
+    ∃ y S, ExecWithin (w + 2) (.loop (.lt Reg.index Reg.count) step) x y
+        (8 * Q + (42 * length + 28) * S + 2) ∧
+      Fixed n first length out queries Q y ∧ y.mem = x.mem ∧
+      y.regs Reg.index = Q ∧ y.regs Reg.scans = S ∧
+      S ≤ Nat.count (fun i => x.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) Q + y.regs Reg.found ∧
+      (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+      (y.regs Reg.found = 1 ↔ ∃ i < Q, x.mem (out + i) ≠ 0 ∧
+        ∃ c, first ≤ c ∧ c < first + length ∧ AB (a i) (b i) + BC (b i) c + AC (a i) c = 0) ∧
+      (y.regs Reg.found = 1 → ∃ i < Q,
+        x.mem (out + i) ≠ 0 ∧ y.regs Reg.witnessA = a i ∧ y.regs Reg.witnessB = b i ∧
+        first ≤ y.regs Reg.witnessC ∧ y.regs Reg.witnessC < first + length ∧
+        AB (a i) (b i) + BC (b i) (y.regs Reg.witnessC) +
+          AC (a i) (y.regs Reg.witnessC) = 0) := by
+  let accept (i : ℕ) : Bool := decide (x.mem (out + i) ≠ 0)
+  let hit (i : ℕ) : Bool := decide (∃ c : Fin length,
+    AB (a i) (b i) + BC (b i) (first + c.val) + AC (a i) (first + c.val) = 0)
+  let active (i : ℕ) : Prop := (accept i && !foundBefore accept hit i) = true
+  have hit_iff (i : ℕ) : hit i = true ↔ ∃ c, first ≤ c ∧ c < first + length ∧
+      AB (a i) (b i) + BC (b i) c + AC (a i) c = 0 := by
+    simp only [hit, decide_eq_true_eq]
+    constructor
+    · rintro ⟨c, hz⟩
+      exact ⟨first + c.val, by omega, by have := c.isLt; omega, hz⟩
+    · rintro ⟨c, hlo, hhi, hz⟩
+      refine ⟨⟨c - first, by omega⟩, ?_⟩
+      simpa only [Nat.add_sub_of_le hlo] using hz
+  let I (y : Data 400) : Prop :=
+    Fixed n first length out queries Q y ∧ y.mem = x.mem ∧ y.regs Reg.index ≤ Q ∧
+    y.regs Reg.found = (foundBefore accept hit (y.regs Reg.index)).toNat ∧
+    y.regs Reg.scans = Nat.count active (y.regs Reg.index) ∧
+    (y.regs Reg.found = 1 → ∃ i < y.regs Reg.index,
+      x.mem (out + i) ≠ 0 ∧ y.regs Reg.witnessA = a i ∧ y.regs Reg.witnessB = b i ∧
+      first ≤ y.regs Reg.witnessC ∧ y.regs Reg.witnessC < first + length ∧
+      AB (a i) (b i) + BC (b i) (y.regs Reg.witnessC) +
+        AC (a i) (y.regs Reg.witnessC) = 0)
+  let Φ (y : Data 400) := 8 * (Q - y.regs Reg.index) +
+    (42 * length + 28) * (Nat.count active Q - Nat.count active (y.regs Reg.index))
+  have hstart : I x := by
+    refine ⟨hx, rfl, by omega, ?_, ?_, ?_⟩
+    · simp only [hi, hf, foundBefore_zero, Bool.toNat_false]
+    · simp only [hi, hs, Nat.count_zero]
+    · intro h; omega
+  have body (y : Data 400) (hy : I y) (hcond : (Cond.lt Reg.index Reg.count).Holds y) :
+      ∃ z T, ExecWithin (w + 2) step y z T ∧ I z ∧ T + 2 + Φ z ≤ Φ y := by
+    obtain ⟨yFixed, ym, yi, yf, ys, yw⟩ := hy
+    let i := y.regs Reg.index
+    change y.regs Reg.found = (foundBefore accept hit i).toNat at yf
+    have hilt : i < Q := by simpa only [Cond.holds_lt, yFixed.count] using hcond
+    have hscans : y.regs Reg.scans ≤ Q := by
+      rw [ys]
+      exact (Nat.count_le active).trans yi
+    have hstepfit : Fits (w + 2)
+        (out + queries + 3 * i + y.regs Reg.scans + 6 * (n * n) + n + first + length + 40) :=
+      hfit.of_le (by dsimp only [i]; omega)
+    by_cases hact : active i
+    · have hinfo : accept i = true ∧ foundBefore accept hit i = false := by
+        simpa only [active, Bool.and_eq_true, Bool.not_eq_true_eq_eq_false] using hact
+      have yzero : y.regs Reg.found = 0 := by rw [yf, hinfo.2]; rfl
+      have hanswer : y.mem (out + i) ≠ 0 := by
+        rw [ym]
+        exact of_decide_eq_true hinfo.1
+      obtain ⟨haWord, hbWord, ha, hb⟩ := hquery i hilt
+      obtain ⟨z, he, zFixed, zm, zi, zs, zf, zh, zw⟩ := exec_step_scan (i := i) AB BC AC y yFixed
+        rfl rfl yzero hanswer (by simpa only [ym] using haWord)
+        (by simpa only [ym] using hbWord) ha hb hc (by simpa only [ym] using hmem)
+        hmag hU hstepfit
+      have zflag : z.regs Reg.found = (hit i).toNat := by
+        cases hh : hit i
+        · have hn : z.regs Reg.found ≠ 1 := by
+            intro h
+            have := (hit_iff i).mpr (zh.mp h)
+            simp only [hh, Bool.false_eq_true] at this
+          rcases zf with hz | hz
+          · simpa only [hh, Bool.toNat_false] using hz
+          · exact (hn hz).elim
+        · simpa only [hh, Bool.toNat_true] using zh.mpr ((hit_iff i).mp hh)
+      have zI : I z := by
+        refine ⟨zFixed, zm.trans ym, by omega, ?_, ?_, ?_⟩
+        · rw [zi, foundBefore_succ, hinfo.1, hinfo.2]
+          simpa only [Bool.true_and, Bool.false_or] using zflag
+        · rw [zi, Nat.count_succ, ite_eq_left hact, ← ys]
+          exact zs
+        · intro hz
+          obtain ⟨za, zb, zlo, zhi, zeq⟩ := zw hz
+          exact ⟨i, by omega, by simpa only [ym] using hanswer, za, zb, zlo, zhi, zeq⟩
+      refine ⟨z, 42 * length + 34, he, zI, ?_⟩
+      have hp := potential_step active (T := 42 * length + 28) hilt
+      simpa only [ite_eq_left hact, Φ, zi, i] using hp
+    · have hskip : y.regs Reg.found ≠ 0 ∨ y.mem (out + i) = 0 := by
+        by_cases hz : y.regs Reg.found = 0
+        · right
+          by_contra hn
+          apply hact
+          have ha : accept i = true := decide_eq_true (by simpa only [ym] using hn)
+          have hb : foundBefore accept hit i = false := by
+            have hz' : (foundBefore accept hit i).toNat = 0 := yf.symm.trans hz
+            cases h : foundBefore accept hit i
+            · rfl
+            · simp only [h, Bool.toNat_true, Nat.one_ne_zero] at hz'
+          simp only [active, ha, hb, Bool.not_false, Bool.true_and]
+        · exact Or.inl hz
+      obtain ⟨z, he, zFixed, zm, zi, frame⟩ := exec_step_skip (i := i) y yFixed rfl hskip
+        (hfit.of_le (by dsimp only [i]; omega))
+      have zfound : z.regs Reg.found = y.regs Reg.found :=
+        frame _ (by decide) (by decide) (by decide)
+      have zscans : z.regs Reg.scans = y.regs Reg.scans :=
+        frame _ (by decide) (by decide) (by decide)
+      have hnext : foundBefore accept hit (i + 1) = foundBefore accept hit i := by
+        rw [foundBefore_succ]
+        cases ha : accept i
+        · simp only [Bool.false_and, Bool.or_false]
+        · cases hb : foundBefore accept hit i
+          · exact (hact (by simp [active, ha, hb])).elim
+          · simp only [Bool.true_or]
+      have zI : I z := by
+        refine ⟨zFixed, zm.trans ym, by omega, ?_, ?_, ?_⟩
+        · rw [zi, hnext, zfound]
+          exact yf
+        · rw [zi, Nat.count_succ, ite_eq_right hact, Nat.add_zero, zscans]
+          exact ys
+        · intro hz
+          obtain ⟨j, hj, hm, hwa, hwb, hlo, hhi, hzsum⟩ := yw (zfound.symm.trans hz)
+          have za := frame Reg.witnessA (by decide) (by decide) (by decide)
+          have zb := frame Reg.witnessB (by decide) (by decide) (by decide)
+          have zc := frame Reg.witnessC (by decide) (by decide) (by decide)
+          exact ⟨j, by omega, hm, za.trans hwa, zb.trans hwb,
+            by simpa only [zc] using hlo, by simpa only [zc] using hhi,
+            by simpa only [zc] using hzsum⟩
+      refine ⟨z, 6, he, zI, ?_⟩
+      have hp := potential_step active (T := 42 * length + 28) hilt
+      simpa only [ite_eq_right hact, Φ, zi, i] using hp
+  obtain ⟨y, he, hIy, hend⟩ := ExecWithin.loop_potential I Φ body hstart
+  obtain ⟨yFixed, ym, yi, yf, ys, yw⟩ := hIy
+  have yindex : y.regs Reg.index = Q := by
+    have hh : ¬ y.regs Reg.index < Q := by
+      simpa only [Cond.holds_lt, yFixed.count] using hend
+    omega
+  have hcount := scan_count_le accept hit Q
+  have hfail : Nat.count (fun i => (accept i && !hit i) = true) Q =
+      Nat.count (fun i => x.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) Q := by
+    congr 1
+    funext i
+    simp only [accept, hit, Bool.and_eq_true, decide_eq_true_eq,
+      Bool.not_eq_true_eq_eq_false, decide_eq_false_iff_not, not_exists]
+  refine ⟨y, Nat.count active Q, ?_, yFixed, ym, yindex, ?_, ?_, ?_, ?_, ?_⟩
+  · simpa only [Φ, hi, Nat.sub_zero, Nat.count_zero, Nat.mul_zero, Nat.add_zero] using he
+  · simpa only [yindex] using ys
+  · rw [← hfail, yf, yindex]
+    exact hcount
+  · rw [yf, yindex]
+    cases foundBefore accept hit Q <;> simp
+  · rw [yf, yindex]
+    simp only [Bool.toNat_eq_one, foundBefore_eq_true, accept, decide_eq_true_eq]
+    constructor
+    · rintro ⟨i, hi, ha, hh⟩
+      exact ⟨i, hi, ha, (hit_iff i).mp hh⟩
+    · rintro ⟨i, hi, ha, hh⟩
+      exact ⟨i, hi, ha, (hit_iff i).mpr hh⟩
+  · simpa only [yindex] using yw
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Readback.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Readback.lean
new file mode 100644
index 0000000000..dd61118b8f
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Readback.lean
@@ -0,0 +1,113 @@
+/-
+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.RecordProduct.QueryValues
+public import Complexity.Algorithms.ExactTriangle.PieceBounds
+
+/-!
+# Protected original data for a real record consumer
+
+The original arrays, selected record and original interleaved queries all precede the actual
+producer heap. These bounds are derived from `Instances.Output` and membership in the existing
+finite instance family. A product execution can therefore preserve the actual words needed
+by candidate recovery without copying the catalogue or snapshotting its workspace.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+
+/-- Read the real selected record and prove every subsequent read is in the protected prefix.
+The native program obtains these fields by loads; this theorem only derives their meaning. -/
+theorem record_view {n D g p : ℕ} (values : ℕ → ℤ) (initial y : Data 64)
+    (h : Instances.Output n D g p values initial y)
+    (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ≠ 0)
+    (idx : InstanceIndex p)
+    (hidx : idx ∈ instanceIndices (fun a b : Fin n => values (pairIndex (a, b))) D g p) :
+    let ord := RecordProduct.recordOrdinal n D g p values idx
+    let base := y.regs Instances.output + ord * (6 + 2 * (n * D))
+    let q := RecordProduct.recordQueries n D p idx
+    let Q := RecordProduct.recordQueryCount n D p values idx
+    5 + 3 * (n * n) ≤ y.regs Instances.heap ∧
+      base + 6 ≤ y.regs Instances.heap ∧ q + 2 * Q ≤ y.regs Instances.heap ∧
+      idx.2.2 * pieceSize D g ≤ n ∧
+      (∀ j : Fin 6, y.mem (base + j.val) =
+        ![idx.1.val, idx.2.2, q, Q, base + 6, base + 6 + n * D] j) ∧
+      (∀ j < Q, y.mem (q + 2 * j) < n ∧ y.mem (q + 2 * j + 1) < n) ∧
+      (∀ j < 5 + 3 * (n * n), y.mem j = initial.mem j) := by
+  let wAB := fun a b : Fin n => values (pairIndex (a, b))
+  let N := n * n
+  let C := fun rho => Nat.count (fun q => (values q % (p : ℤ)).toNat = rho) N
+  let H := numPieces n D g
+  let K := ChunkCatalogue.before C (queryCap n D) p
+  let ord := RecordProduct.recordOrdinal n D g p values idx
+  let base := y.regs Instances.output + ord * (6 + 2 * (n * D))
+  let q := RecordProduct.recordQueries n D p idx
+  let Q := RecordProduct.recordQueryCount n D p values idx
+  obtain ⟨hk, hj⟩ := (mem_instanceIndices wAB idx).mp hidx
+  have hcard : (residueClass wAB p idx.1).card = C idx.1.val :=
+    QuerySpec.card_residueClass wAB hp _ (by intro pair; rfl) idx.1
+  have hchunk : idx.2.1 < C idx.1.val ⌈/⌉ queryCap n D := by
+    simpa only [numChunks, hcard] using hk
+  have hord := ChunkCatalogue.before_add_lt C (queryCap n D) idx.1.isLt hchunk
+  have hiCount : ord < K * H := by
+    have hh := Nat.mul_le_mul_right H (Nat.succ_le_of_lt hord)
+    change (ChunkCatalogue.before C (queryCap n D) idx.1.val + idx.2.1) * H + idx.2.2 < K * H
+    change (ChunkCatalogue.before C (queryCap n D) idx.1.val + idx.2.1 + 1) * H ≤ K * H at hh
+    change idx.2.2 < H at hj
+    rw [Nat.add_mul, Nat.one_mul] at hh
+    omega
+  have hout : y.regs Instances.output = 5 + 6 * N + p + 2 * N * p + 3 * K := h.2.2.2.1
+  have hheap : y.regs Instances.heap = y.regs Instances.output + K * H * (6 + 2 * (n * D)) :=
+    h.2.2.2.2.2.1.trans (congrArg (fun v => v + K * H * (6 + 2 * (n * D))) hout.symm)
+  have hbase : base + 6 ≤ y.regs Instances.heap := by
+    have hh := Nat.mul_le_mul_right (6 + 2 * (n * D)) (Nat.succ_le_of_lt hiCount)
+    rw [hheap]
+    dsimp only [base]
+    nlinarith only [hh]
+  have hQ : idx.2.1 * queryCap n D + Q ≤ N := by
+    have hc : C idx.1.val ≤ N := Nat.count_le _
+    have hpositive := RecordProduct.recordQueryCount_pos values hp (by omega) hDn idx hidx
+    change 0 < min (queryCap n D) (C idx.1.val - idx.2.1 * queryCap n D) at hpositive
+    dsimp only [Q, RecordProduct.recordQueryCount]
+    change idx.2.1 * queryCap n D +
+      min (queryCap n D) (C idx.1.val - idx.2.1 * queryCap n D) ≤ N
+    omega
+  have hqEnd : q + 2 * Q ≤ y.regs Instances.heap := by
+    have hrho := Nat.mul_le_mul_right (2 * N) (Nat.succ_le_of_lt idx.1.isLt)
+    dsimp only [q, RecordProduct.recordQueries]
+    change 5 + 6 * N + p + 2 * idx.1.val * N +
+      2 * (idx.2.1 * queryCap n D) + 2 * Q ≤ _
+    rw [hheap, hout]
+    nlinarith only [hQ, hrho, Nat.zero_le (3 * K),
+      Nat.zero_le (K * H * (6 + 2 * (n * D)))]
+  have hfirst : idx.2.2 * pieceSize D g ≤ n := by
+    have hB := pieceSize_pos hD hg
+    by_contra hh
+    have hc : numPieces n D g ≤ idx.2.2 := (Nat.ceilDiv_le_iff hB).mpr (by omega)
+    change idx.2.2 < numPieces n D g at hj
+    omega
+  obtain ⟨hdr, -, -⟩ := PreparationSpec.instance_readback values wAB hp
+    (by intro a b; rfl) hD hDn hg h idx hidx
+  have hcoord := (RecordProduct.output_query_coordinates values wAB hp (by intro a b; rfl)
+    (by omega) hDn h idx.1 idx.2.1 hk).1
+  rw [hcard] at hcoord
+  dsimp only
+  refine ⟨?_, hbase, hqEnd, hfirst, ?_, hcoord, ?_⟩
+  · rw [hheap, hout]
+    dsimp only [N]
+    omega
+  · simpa only [base, ord, RecordProduct.recordOrdinal, Q, RecordProduct.recordQueryCount,
+      q, RecordProduct.recordQueries, hout, N, K, C, hcard, Block.Realizes, Block.read] using hdr
+  · intro j hj
+    exact h.2.2.2.2.2.2.2.2.2.2.2 j (Or.inl hj)
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/SourceBounds.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/SourceBounds.lean
new file mode 100644
index 0000000000..2ce7025ac8
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/SourceBounds.lean
@@ -0,0 +1,151 @@
+/-
+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.Flat
+
+/-!
+# Original-size width and prefix bounds for candidate recovery
+
+The complete initialized producer/product/verifier has one positive logarithmic physical-width
+threshold for polynomial original scalars and weights. Its words and memory support at every
+prefix have a polynomial bound independent of any larger physical width. These are consequences
+of the actual minimum-width halting run and existing native width transport.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+/-- Every admitted physical width can be chosen logarithmic in original size. The positive
+constant is explicit for each original magnitude exponent; geometry is not weakened. -/
+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
+  let E := 2 * κ + 512
+  have hb : 2 ≤ b := by dsimp only [b]; omega
+  have hb1 : 1 ≤ b := le_trans (by decide : 1 ≤ (2 : ℕ)) hb
+  have hP : PreparationInput.wordBound n D g p A ≤ b ^ E := by
+    exact (PreparationInput.wordBound_le_pow hn hD hg hp hA).trans
+      (Nat.pow_le_pow_right hb1 (by dsimp only [E]; omega))
+  have hfour : 2 * (n + n ^ 2 + 3) ≤ b ^ 4 := by
+    dsimp only [b]
+    nlinarith only [Nat.zero_le (n ^ 4), Nat.zero_le (n ^ 3), Nat.zero_le (n ^ 2),
+      Nat.zero_le n]
+  have hfour' : 2 * (n + n ^ 2 + 3) ≤ (b ^ 2) ^ 2 := hfour.trans_eq (Nat.pow_mul b 2 2)
+  have hM : CallableProduct.windowSize n (n ^ 2) ≤ b ^ E := by
+    calc
+      _ ≤ (2 * (n + n ^ 2 + 3)) ^ 128 := CallableProduct.windowSize_le n (n ^ 2)
+      _ ≤ ((b ^ 2) ^ 2) ^ 128 := Nat.pow_le_pow_left hfour' _
+      _ = (b ^ 2) ^ 256 := (Nat.pow_mul (b ^ 2) 2 128).symm
+      _ ≤ (b ^ 2) ^ (κ + 256) := Nat.pow_le_pow_right (Nat.pow_pos hb1)
+        (Nat.le_add_left 256 κ)
+      _ = b ^ E := by
+        rw [← Nat.pow_mul]
+        exact congrArg (fun j : ℕ => b ^ j)
+          (by dsimp only [E]; omega : 2 * (κ + 256) = E)
+  have hn2 : n ^ 2 ≤ b ^ E := (Nat.pow_le_pow_left (by dsimp only [b]; omega : n ≤ b) 2).trans
+    (Nat.pow_le_pow_right hb1 (by dsimp only [E]; omega))
+  have hnE : n ≤ b ^ E := (show n ≤ n ^ 2 by nlinarith only [hn]).trans hn2
+  have hprod : n * D ≤ b ^ E := (Nat.mul_le_mul_left n hD).trans
+    (by simpa only [pow_two] using hn2)
+  have hAE : A ≤ b ^ E := hA.trans
+    (Nat.pow_le_pow_right hb1 (by dsimp only [E]; omega))
+  have hconst : 4096 ≤ b ^ E := (show 4096 ≤ (2 : ℕ) ^ 12 by decide).trans
+    ((Nat.pow_le_pow_left hb 12).trans
+      (Nat.pow_le_pow_right hb1 (by dsimp only [E]; omega)))
+  have hsum : envelope n D g p A ≤ 576 * b ^ E := by
+    unfold envelope
+    have hgE := hg.trans hnE
+    have hDE := hD.trans hnE
+    omega
+  have henvelope : envelope n D g p A ≤ b ^ (2 * κ + 522) := by
+    calc
+      _ ≤ 576 * b ^ E := hsum
+      _ ≤ b ^ 10 * b ^ E := Nat.mul_le_mul_right _
+        ((show 576 ≤ (2 : ℕ) ^ 10 by decide).trans (Nat.pow_le_pow_left hb 10))
+      _ = b ^ (2 * κ + 522) := by
+        rw [← Nat.pow_add]
+        exact congrArg (fun j : ℕ => b ^ j) (by dsimp only [E]; omega : 10 + E = 2 * κ + 522)
+  have hbase := Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) b
+  have hlogBound := henvelope.trans (Nat.pow_le_pow_left hbase (2 * κ + 522))
+  rw [← Nat.pow_mul] at hlogBound
+  have hlog := Nat.clog_le_of_le_pow hlogBound
+  change Nat.clog 2 (envelope n D g p A) ≤ Nat.clog 2 b * (2 * κ + 522) at hlog
+  have hrecord := RecordProduct.admissionWidth_le_log hn hD hg hp hA
+  have hlog' : Nat.clog 2 (envelope n D g p A) ≤ (257 * κ + 5906) * Nat.clog 2 b := by
+    nlinarith only [hlog, Nat.zero_le (κ * Nat.clog 2 b)]
+  have hmax := max_le hrecord hlog'
+  have hpositive : 1 ≤ Nat.clog 2 b := Nat.clog_pos (by decide) (by omega : 1 < b)
+  unfold admissionWidth
+  dsimp only [b] at hmax hpositive
+  nlinarith only [hmax, hpositive]
+
+/-- Original-input prefix word/address envelope, independent of the caller's larger width. -/
+@[expose] def wordBound (n D g p A : ℕ) : ℕ := 2 ^ admissionWidth n D g p A
+
+/-- All prefix words and memory support have a fixed polynomial envelope for each κ. -/
+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 : 1 < b := by dsimp only [b]; omega
+  have hc := Nat.clog_pos (by decide : 1 < (2 : ℕ)) hb
+  have hp2 := Nat.pow_pred_clog_lt_self (by decide : 1 < (2 : ℕ)) hb
+  have he : Nat.clog 2 b = (Nat.clog 2 b).pred + 1 := (Nat.succ_pred_eq_of_pos hc).symm
+  have hbase : 2 ^ Nat.clog 2 b ≤ b ^ 2 := by
+    rw [he, pow_succ]
+    nlinarith only [hp2, show 2 ≤ b by omega]
+  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)
+
+/-- At every admitted wider width, every actual prefix has original-input polynomial words
+and zero memory above the same original-input envelope. Dirty pre-normalization loads are
+included because the entire actual native execution is compared with its minimum-width 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 400} (hr : Runs W (entryProgram.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, idx, ha, hout, hidx, hord, y, t, S, ht, hpref, he, -⟩ :=
+    runs_input values hlen hD hg hp hN hv le_rfl
+  have hlow := Runs.prefix_at_smaller_width entryProgram_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.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Spec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Spec.lean
new file mode 100644
index 0000000000..ab9f73f4ba
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Spec.lean
@@ -0,0 +1,79 @@
+/-
+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.Program
+
+/-!
+# Fixed registers of the per-record witness controller
+
+This internal invariant contains only ordinary runtime register equalities. It packages
+neither execution nor witness, fit, sparse-count or time certificates. The actual header
+establishes it from the original scalar words and record; the query loop preserves it.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM
+
+/-- The controller's fixed arguments and the verifier's shared array/interval arguments. -/
+structure Fixed (n firstVertex spanLen out queryBase queryCount : ℕ) (x : Data 400) : Prop where
+  /-- Absolute answer pointer. -/
+  output : x.regs Reg.output = out
+  /-- Original interleaved query pointer. -/
+  queries : x.regs Reg.queries = queryBase
+  /-- Actual occurrence count. -/
+  count : x.regs Reg.count = queryCount
+  /-- Original outer dimension. -/
+  size : x.regs Reg.size = n
+  /-- Original first piece vertex. -/
+  first : x.regs Reg.first = firstVertex
+  /-- Number of original piece vertices. -/
+  length : x.regs Reg.length = spanLen
+  /-- Constant one. -/
+  one : x.regs Reg.one = 1
+  /-- Constant zero. -/
+  zero : x.regs Reg.zero = 0
+  /-- Original signed A–B pointer delivered to the verifier. -/
+  ab : x.regs (scanBank WitnessScan.Reg.ab) = 5
+  /-- Original signed B–C pointer delivered to the verifier. -/
+  bc : x.regs (scanBank WitnessScan.Reg.bc) = 5 + n * n
+  /-- Original signed A–C pointer delivered to the verifier. -/
+  ac : x.regs (scanBank WitnessScan.Reg.ac) = 5 + n * n + n * n
+  /-- Verifier outer dimension. -/
+  scanSize : x.regs (scanBank WitnessScan.Reg.size) = n
+  /-- Verifier original first vertex. -/
+  scanFirst : x.regs (scanBank WitnessScan.Reg.first) = firstVertex
+  /-- Verifier interval length. -/
+  scanLength : x.regs (scanBank WitnessScan.Reg.length) = spanLen
+
+/-- Reuse the fixed ABI under a frame that excludes the query cursor, loaded coordinates,
+verifier scratch and result/counter registers. -/
+theorem Fixed.of_frame {n first length out queries count : ℕ} {x y : Data 400}
+    (hx : Fixed n first length out queries count x)
+    (he : ∀ i : Fin 400, i.val < 326 ∨ i = Reg.one ∨ i = Reg.zero ∨
+      (345 ≤ i.val ∧ i.val ≤ 348) ∨ (351 ≤ i.val ∧ i.val ≤ 352) →
+      y.regs i = x.regs i) : Fixed n first length out queries count y where
+  output := (he _ (by decide)).trans hx.output
+  queries := (he _ (by decide)).trans hx.queries
+  count := (he _ (by decide)).trans hx.count
+  size := (he _ (by decide)).trans hx.size
+  first := (he _ (by decide)).trans hx.first
+  length := (he _ (by decide)).trans hx.length
+  one := (he _ (by decide)).trans hx.one
+  zero := (he _ (by decide)).trans hx.zero
+  ab := (he _ (by decide)).trans hx.ab
+  bc := (he _ (by decide)).trans hx.bc
+  ac := (he _ (by decide)).trans hx.ac
+  scanSize := (he _ (by decide)).trans hx.scanSize
+  scanFirst := (he _ (by decide)).trans hx.scanFirst
+  scanLength := (he _ (by decide)).trans hx.scanLength
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Step.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Step.lean
new file mode 100644
index 0000000000..1d1a37f98c
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Step.lean
@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordWitness.Pair
+
+/-!
+# Charged query-controller steps
+
+An accepted step reads the actual answer word and invokes the actual original-weight verifier.
+The separate skipped-step rule accounts for both zero answers and the already-successful
+short circuit. These are internal execution rules, not additional algorithm inputs.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM
+
+/-- A nonzero actual product word, while still searching, causes exactly one native scan.
+The six additional instructions include both branches, answer access and cursor advancement. -/
+theorem exec_step_scan {w U n first length out queries count i scans a b : ℕ}
+    (AB BC AC : ℕ → ℕ → ℤ) (x : Data 400)
+    (hx : Fixed n first length out queries count x)
+    (hi : x.regs Reg.index = i) (hs : x.regs Reg.scans = scans)
+    (hf : x.regs Reg.found = 0) (hanswer : x.mem (out + i) ≠ 0)
+    (haWord : x.mem (queries + 2 * i) = a)
+    (hbWord : x.mem (queries + 2 * i + 1) = b)
+    (ha : a < n) (hb : b < n) (hc : first + length ≤ n)
+    (hmem : ∀ u < n, ∀ v < n,
+      x.mem (5 + (u * n + v)) = Signed.encode (AB u v) ∧
+      x.mem (5 + n * n + (u * n + v)) = Signed.encode (BC u v) ∧
+      x.mem (5 + n * n + n * n + (u * n + v)) = Signed.encode (AC u v))
+    (hmag : ∀ u < n, ∀ v < n,
+      (AB u v).natAbs ≤ U ∧ (BC u v).natAbs ≤ U ∧ (AC u v).natAbs ≤ U)
+    (hU : GenericRAM.Signed.Fits w (2 * U : ℕ))
+    (hfit : Fits (w + 2)
+      (out + queries + 3 * i + scans + 6 * (n * n) + n + first + length + 40)) :
+    ∃ y, ExecWithin (w + 2) step x y (42 * length + 34) ∧
+      Fixed n first length out queries count y ∧ y.mem = x.mem ∧
+      y.regs Reg.index = i + 1 ∧ y.regs Reg.scans = scans + 1 ∧
+      (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+      (y.regs Reg.found = 1 ↔
+        ∃ c, first ≤ c ∧ c < first + length ∧ AB a b + BC b c + AC a c = 0) ∧
+      (y.regs Reg.found = 1 →
+        y.regs Reg.witnessA = a ∧ y.regs Reg.witnessB = b ∧
+        first ≤ y.regs Reg.witnessC ∧ y.regs Reg.witnessC < first + length ∧
+        AB a b + BC b (y.regs Reg.witnessC) + AC a (y.regs Reg.witnessC) = 0) := by
+  let d := x.set Reg.address (out + i) |>.set Reg.answer (x.mem (out + i))
+  have hd : ExecWithin (w + 2)
+      (ram[ Reg.address ← Reg.output + Reg.index; Reg.answer ← *Reg.address ]) x d 2 := by
+    ram_eval [d, hx.output, hi, Reg.address, Reg.output, Reg.index, Reg.answer,
+      hfit.of_le (by omega : out + i ≤
+        out + queries + 3 * i + scans + 6 * (n * n) + n + first + length + 40)]
+  have dFixed : Fixed n first length out queries count d := hx.of_frame (by
+    intro j hj
+    have haddr : j ≠ Reg.address := by
+      intro he
+      subst j
+      norm_num [Reg.address, Reg.one, Reg.zero] at hj
+    have hans : j ≠ Reg.answer := by
+      intro he
+      subst j
+      norm_num [Reg.answer, Reg.one, Reg.zero] at hj
+    simp [d, haddr, hans])
+  obtain ⟨s, he, sFixed, sm, si, ss, sf, sh, sw⟩ := exec_scanPair AB BC AC d dFixed
+    (by simpa +decide [d, Reg.address, Reg.answer, Reg.index] using hi)
+    (by simpa +decide [d, Reg.address, Reg.answer, Reg.scans] using hs)
+    (by simpa +decide [d, Reg.address, Reg.answer, Reg.found] using hf)
+    haWord hbWord ha hb hc hmem hmag hU
+    (hfit.of_le (by omega))
+  have hb : ExecWithin (w + 2)
+      (.branch (.eq Reg.found Reg.zero)
+        (.seq (ram[ Reg.address ← Reg.output + Reg.index; Reg.answer ← *Reg.address ])
+          (.branch (.eq Reg.answer Reg.zero) (.op (.copy Reg.answer Reg.answer)) scanPair))
+        (.op (.copy Reg.answer Reg.answer))) x s (42 * length + 33) := by
+    apply ExecWithin.branch_pos (by simp only [Cond.holds_eq, hf, hx.zero])
+    exact (hd.seq (ExecWithin.branch_neg (cond := .eq Reg.answer Reg.zero) (by
+      simpa +decide [Cond.holds_eq, d, Reg.answer, Reg.address, Reg.zero,
+        show x.regs 399 = 0 from hx.zero] using hanswer) he)).mono (by omega)
+  let y := s.set Reg.index (i + 1)
+  have hy : ExecWithin (w + 2) (.op (.bin .add Reg.index Reg.index Reg.one)) s y 1 := by
+    ram_eval [y, si, sFixed.one, Reg.index, Reg.one,
+      hfit.of_le (by omega : i + 1 ≤
+        out + queries + 3 * i + scans + 6 * (n * n) + n + first + length + 40)]
+  have yFixed : Fixed n first length out queries count y := sFixed.of_frame (by
+    intro j hj
+    have hne : j ≠ Reg.index := by
+      intro he
+      subst j
+      norm_num [Reg.index, Reg.one, Reg.zero] at hj
+    simp [y, hne])
+  refine ⟨y, hb.seq hy, yFixed, sm, rfl, ?_, ?_, ?_, ?_⟩
+  · simpa +decide [y, Reg.index, Reg.scans] using ss
+  · simpa +decide [y, Reg.index, Reg.found] using sf
+  · simpa +decide [y, Reg.index, Reg.found] using sh
+  · simpa +decide [y, Reg.index, Reg.found, Reg.witnessA, Reg.witnessB,
+      Reg.witnessC] using sw
+
+/-- Zero answers and an already successful flag incur no verifier call. In particular the
+actual scan counter and all returned witness coordinates are preserved. -/
+theorem exec_step_skip {W n first length out queries count i : ℕ} (x : Data 400)
+    (hx : Fixed n first length out queries count x) (hi : x.regs Reg.index = i)
+    (hskip : x.regs Reg.found ≠ 0 ∨ x.mem (out + i) = 0)
+    (hfit : Fits W (out + i + 2)) :
+    ∃ y, ExecWithin W step x y 6 ∧ Fixed n first length out queries count y ∧
+      y.mem = x.mem ∧ y.regs Reg.index = i + 1 ∧
+      ∀ j : Fin 400, j ≠ Reg.index → j ≠ Reg.address → j ≠ Reg.answer →
+        y.regs j = x.regs j := by
+  let y := if x.regs Reg.found = 0 then
+      (x.set Reg.address (out + i) |>.set Reg.answer 0 |>.set Reg.answer 0)
+        |>.set Reg.index (i + 1)
+    else (x.set Reg.answer (x.regs Reg.answer)).set Reg.index (i + 1)
+  have ha : Fits W (out + i) := hfit.of_le (by omega)
+  have ht : Fits W (i + 1) := hfit.of_le (by omega)
+  have he : ExecWithin W step x y 6 := by
+    by_cases hf : x.regs Reg.found = 0
+    · have hz : x.mem (out + i) = 0 := hskip.resolve_left (not_not_intro hf)
+      ram_eval [step, y, hf, hz, hi, hx.output, hx.zero, hx.one, ha, ht,
+        Reg.found, Reg.zero, Reg.address, Reg.output, Reg.index, Reg.answer, Reg.one]
+    · ram_eval [step, y, hf, hi, hx.zero, hx.one, ht,
+        Reg.found, Reg.zero, Reg.answer, Reg.index, Reg.one]
+  have frame (j : Fin 400) (hj : j ≠ Reg.index) (ha : j ≠ Reg.address)
+      (hb : j ≠ Reg.answer) : y.regs j = x.regs j := by
+    by_cases hf : x.regs Reg.found = 0 <;> simp [y, hf, hj, ha, hb]
+  have yFixed : Fixed n first length out queries count y := hx.of_frame (by
+    intro j hj
+    have hindex : j ≠ Reg.index := by
+      intro he; subst j; norm_num [Reg.index, Reg.one, Reg.zero] at hj
+    have haddr : j ≠ Reg.address := by
+      intro he; subst j; norm_num [Reg.address, Reg.one, Reg.zero] at hj
+    have hans : j ≠ Reg.answer := by
+      intro he; subst j; norm_num [Reg.answer, Reg.one, Reg.zero] at hj
+    exact frame j hindex haddr hans)
+  refine ⟨y, he, yFixed, ?_, ?_, frame⟩
+  · by_cases hf : x.regs Reg.found = 0 <;> simp [y, hf]
+  · by_cases hf : x.regs Reg.found = 0 <;> simp [y, hf]
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/TimeBound.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/TimeBound.lean
new file mode 100644
index 0000000000..262c0d0a1c
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/TimeBound.lean
@@ -0,0 +1,84 @@
+/-
+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.SourceBounds
+
+/-!
+# Charged per-record witness-recovery bound
+
+The actual producer chunk derives the required occurrence sparsity. Preparation and the thin
+product retain their already proved charges, and recovery adds actual root/query/control work
+plus full interval scans. The scan surplus is the returned native flag, so unsuccessful records
+have no additive successful-scan term. This does not sum the outer instance loop or choose a
+prime, and it establishes neither aggregate subcubic ET nor the ordinary 3SUM endpoint.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM Cslib.Algorithms.ExactTriangle Cslib.Matrix
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+
+/-- The quantitative bound applied to the actual initialized execution. Occurrence sparsity
+is derived from its computed query count. The scan/count and interval premises are conclusions
+of `runs_input`; they are not algorithm inputs or supplied solver/time certificates. -/
+theorem initialized_time_le {m n g p length S flag : ℕ} (values : List ℤ)
+    (idx : InstanceIndex p) (qs : List (Fin n × Fin n))
+    (hcount : qs.length = RecordProduct.recordQueryCount n (D m) p
+      (fun q => values.getD q 0) idx)
+    (hD : 16 ≤ D m) (hN : D m ^ 18 ≤ n) (hg : 1 ≤ g)
+    (hp : p ∈ Nat.sqrtPrimeWindow (D m))
+    (hlength : length ≤ pieceSize (D m) g)
+    (hS : S ≤ falsePositiveCount
+      (fun a b : Fin n => values.getD (pairIndex (a, b)) 0)
+      (fun b c : Fin n => values.getD (n * n + pairIndex (b, c)) 0)
+      (fun a c : Fin n => values.getD (2 * (n * n) + pairIndex (a, c)) 0) p + flag) :
+    let F := falsePositiveCount
+      (fun a b : Fin n => values.getD (pairIndex (a, b)) 0)
+      (fun b c : Fin n => values.getD (n * n + pairIndex (b, c)) 0)
+      (fun a c : Fin n => values.getD (2 * (n * n) + pairIndex (a, c)) 0) p
+    ((RecordProduct.preparationTime n (D m) g p values +
+      RecordProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * qs.length +
+      (42 * length + 28) * S + 53 : ℕ) : ℝ) ≤
+      690 * (n : ℝ) ^ 2 * D m * g +
+        34603008 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 2 /
+          (D m : ℝ) ^ (1 / 18 : ℝ) +
+        ((5 * Nat.sqrt (D m) + 8 * qs.length +
+          (42 * pieceSize (D m) g + 28) * (F + flag) + 52 : ℕ) : ℝ) := by
+  let F := falsePositiveCount
+    (fun a b : Fin n => values.getD (pairIndex (a, b)) 0)
+    (fun b c : Fin n => values.getD (n * n + pairIndex (b, c)) 0)
+    (fun a c : Fin n => values.getD (2 * (n * n) + pairIndex (a, c)) 0) p
+  change S ≤ F + flag at hS
+  have hQ : qs.length * 2 ^ m ≤ n ^ 2 := by
+    rw [hcount]
+    exact (Nat.mul_le_mul_right (2 ^ m) (min_le_left _ _)).trans
+      (RecordProduct.queryCap_mul_two_pow_le n m)
+  have hbase := RecordProduct.initialized_time_le values qs hD hN hg hp hQ
+  have hscan : (42 * length + 28) * S ≤
+      (42 * pieceSize (D m) g + 28) * (F + flag) :=
+    Nat.mul_le_mul (by omega) hS
+  let extra := 5 * Nat.sqrt (D m) + 8 * qs.length +
+    (42 * pieceSize (D m) g + 28) * (F + flag) + 52
+  have htotal : RecordProduct.preparationTime n (D m) g p values +
+      RecordProduct.timeBound (m := m) qs + 5 * Nat.sqrt (D m) + 8 * qs.length +
+      (42 * length + 28) * S + 53 ≤
+      RecordProduct.preparationTime n (D m) g p values +
+        RecordProduct.timeBound (m := m) qs + 1 + extra := by
+    dsimp only [extra]
+    omega
+  calc
+    _ ≤ ((RecordProduct.preparationTime n (D m) g p values +
+        RecordProduct.timeBound (m := m) qs + 1 + extra : ℕ) : ℝ) := Nat.cast_le.mpr htotal
+    _ = ((RecordProduct.preparationTime n (D m) g p values +
+        RecordProduct.timeBound (m := m) qs + 1 : ℕ) : ℝ) + (extra : ℝ) := Nat.cast_add _ _
+    _ ≤ _ := add_le_add hbase (le_rfl : (extra : ℝ) ≤ extra)
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Trace.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Trace.lean
new file mode 100644
index 0000000000..9af3ab238b
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Trace.lean
@@ -0,0 +1,62 @@
+/-
+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.Init
+public import Mathlib.Data.Nat.Count
+public import Mathlib.Data.List.Range
+
+/-!
+# The actual witness controller's short-circuit scan trace
+
+`foundBefore` specifies the cached native flag after an input prefix. It is not a witness
+oracle or an extra runtime computation: the execution invariant derives it from the actual
+loads and verifier calls. Scan and failure counts use Mathlib's `Nat.count` directly.
+
+The argument follows the scan-accounting portion of pinned `ScanPairs.lean`,
+`anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`. This controller starts
+with a false flag; the source's optional already-successful incoming flag is not needed.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+/-- Pure value of the cached flag: an earlier accepted pair has a genuine original witness. -/
+@[expose] def foundBefore (accept hit : ℕ → Bool) (i : ℕ) : Bool :=
+  (List.range i).any fun j => accept j && hit j
+
+/-- Before reading any answer, the native success flag is false. -/
+theorem foundBefore_zero (accept hit : ℕ → Bool) : foundBefore accept hit 0 = false := rfl
+
+/-- One actual query extends the previous success flag by its own accepted witness result. -/
+theorem foundBefore_succ (accept hit : ℕ → Bool) (i : ℕ) :
+    foundBefore accept hit (i + 1) = (foundBefore accept hit i || (accept i && hit i)) := by
+  simp [foundBefore, List.range_succ]
+
+/-- The cached success flag records an actually accepted earlier query. -/
+theorem foundBefore_eq_true (accept hit : ℕ → Bool) (i : ℕ) :
+    foundBefore accept hit i = true ↔ ∃ j < i, accept j = true ∧ hit j = true := by
+  simp [foundBefore, List.any_eq_true, List.mem_range]
+
+/-- Every actual scan except at most the successful one is a failed accepted candidate.
+The functions describe original input values; no such function is an algorithm argument. -/
+theorem scan_count_le (accept hit : ℕ → Bool) (Q : ℕ) :
+    Nat.count (fun i => (accept i && !foundBefore accept hit i) = true) Q ≤
+      Nat.count (fun i => (accept i && !hit i) = true) Q +
+        (foundBefore accept hit Q).toNat := by
+  induction Q with
+  | zero => simp [foundBefore]
+  | succ Q ih =>
+    rw [Nat.count_succ, Nat.count_succ, foundBefore_succ]
+    rcases ha : accept Q <;> rcases hh : hit Q <;> rcases hf : foundBefore accept hit Q <;>
+      simp_all only [Bool.not_false, Bool.not_true, Bool.and_false, Bool.and_true,
+        Bool.or_false, Bool.or_true, Bool.toNat_false, Bool.toNat_true,
+        Bool.false_eq_true, ↓reduceIte] <;> omega
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Width.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Width.lean
new file mode 100644
index 0000000000..24c43619fa
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordWitness/Width.lean
@@ -0,0 +1,100 @@
+/-
+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.Exec
+
+/-!
+# Original-input admission for product-selected witness recovery
+
+One positive width threshold covers the original producer/product admission, all real
+descriptor/query/address arithmetic and both signed additions of original weights. It depends
+on the original scalar headers and magnitude envelope, not on the physical width chosen by
+the caller. The reserved product window is an address bound, not a charged clearing operation.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
+
+open Cslib.WordRAM
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+/-- Numerical envelope in original dimensions and weight magnitude; it covers all recovery
+setup and calls after the genuine producer has established its own word/address bound. -/
+@[expose] def envelope (n D g p A : ℕ) : ℕ :=
+  64 * (PreparationInput.wordBound n D g p A + CallableProduct.windowSize n (n ^ 2) +
+    n * D + n ^ 2 + n + g + D + A + 4096)
+
+/-- Physical width for the same fixed native program at every larger admitted word size. -/
+@[expose] def admissionWidth (n D g p A : ℕ) : ℕ :=
+  max (RecordProduct.admissionWidth n D g p A) (Nat.clog 2 (envelope n D g p A)) + 3
+
+/-- The initialized native threshold is positive for every original scalar tuple. -/
+theorem admissionWidth_pos (n D g p A : ℕ) : 0 < admissionWidth n D g p A := by
+  unfold admissionWidth
+  omega
+
+/-- The existing product's output slice precedes its admitted virtual-window boundary. -/
+theorem outputBase_lt_window {m n Q : ℕ} (hN : D m ^ 18 ≤ n) :
+    QueriedProduct.outputBase (19 * m) m n Q < CallableProduct.windowSize n Q := by
+  have hout : QueriedProduct.outputBase (19 * m) m n Q ≤
+      QueriedProduct.memoryEnd (19 * m) m n Q := by
+    unfold QueriedProduct.memoryEnd QueriedProduct.stampBase QueriedProduct.scratchBase
+    have hten := Nat.zero_le (10 ^ (19 * m))
+    have hframes := Nat.zero_le (2 * (19 * m + 1) * 10 ^ (19 * m))
+    omega
+  have hword : QueriedProduct.memoryEnd (19 * m) m n Q ≤
+      QueriedProduct.wordBudget (19 * m) m n Q := by
+    unfold QueriedProduct.wordBudget
+    omega
+  exact (hout.trans hword).trans_lt (CallableProduct.source_admission hN).2.2
+
+/-- Every pointer and temporary of the actual per-record caller fits from the original
+producer word bound and the actual chunk count. No intermediate fit certificate is supplied. -/
+theorem physical_fits {w m n g p A heap Q : ℕ}
+    (hheap : heap ≤ PreparationInput.wordBound n (D m) g p A)
+    (hQ : Q ≤ n ^ 2) (hN : D m ^ 18 ≤ n)
+    (hW : admissionWidth n (D m) g p A ≤ w + 2) :
+    Fits (w + 2) (4 * heap + 4 * CallableProduct.windowSize n Q +
+      QueriedProduct.outputBase (19 * m) m n Q + 4 * Q + 4 * D m +
+      2 * (n * D m) + 9 * (n * n) + 4 * n + g + 4096) := by
+  have hwindow : CallableProduct.windowSize n Q ≤ CallableProduct.windowSize n (n ^ 2) := by
+    unfold CallableProduct.windowSize CallableProduct.sourceWidth
+    apply Nat.pow_le_pow_right (by decide)
+    exact Nat.mul_le_mul_left 128 (Nat.clog_mono_right 2 (by omega))
+  have hout := (outputBase_lt_window (Q := Q) hN).le.trans hwindow
+  have he : Fits (w + 2) (envelope n (D m) g p A) := by
+    have hn := Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) (envelope n (D m) g p A)
+    have hw : Nat.clog 2 (envelope n (D m) g p A) < w + 2 := by
+      unfold admissionWidth at hW
+      omega
+    exact hn.trans_lt (Nat.pow_lt_pow_right (by decide : 1 < (2 : ℕ)) hw)
+  apply he.of_le
+  unfold envelope
+  rw [pow_two] at hQ hwindow hout ⊢
+  omega
+
+/-- Two signed additions use the original envelope `2A`; the physical compiler extension
+is included in the same original-input threshold. -/
+theorem signed_fits {w n D g p A : ℕ} (hW : admissionWidth n D g p A ≤ w + 2) :
+    GenericRAM.Signed.Fits w (2 * A : ℕ) := by
+  have hw : Nat.clog 2 (envelope n D g p A) + 1 ≤ w := by
+    unfold admissionWidth at hW
+    omega
+  have he : 2 * A < envelope n D g p A := by unfold envelope; omega
+  have hp := Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) (envelope n D g p A)
+  have ht : 2 * A < 2 ^ (w - 1) := he.trans_le
+    (hp.trans (Nat.pow_le_pow_right (by decide) (by omega)))
+  refine ⟨by omega, ?_, by exact_mod_cast ht⟩
+  have hz : (0 : ℤ) ≤ (2 * A : ℕ) := by exact_mod_cast Nat.zero_le (2 * A)
+  have hp : (0 : ℤ) ≤ 2 ^ (w - 1) := by positivity
+  omega
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordWitness
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Cell.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Cell.lean
new file mode 100644
index 0000000000..8936a7c1f3
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Cell.lean
@@ -0,0 +1,74 @@
+/-
+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.WitnessScan.Program
+
+/-!
+# Charged original-weight zero-sum test
+
+The internal cell rule composes the actual two loads, their address calculations and both
+existing signed additions. Its result is the exact sum of the three original weights; no
+modular product or candidate certificate can make a nonzero original sum pass this test.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
+
+open Cslib.WordRAM
+
+private theorem loads_preserve : ∀ i : Fin 32, 9 ≤ i.val → i ≠ Reg.address →
+    loadBC.Preserves i ∧ loadAC.Preserves i := by decide
+
+/-- Actual signed verification of one original candidate vertex, with every address and
+arithmetic instruction charged. The first partial sum must fit the next kernel's signed
+source range; the complete initialized caller derives this from the original weight bound. -/
+theorem exec_testVertex {w rb ra c : ℕ} {ab bc ac : ℤ} (x : Data 32)
+    (hrowB : x.regs Reg.rowB = rb) (hrowA : x.regs Reg.rowA = ra)
+    (hindex : x.regs Reg.index = c) (hwab : x.regs Reg.wab = Signed.encode ab)
+    (hBC : x.mem (rb + c) = Signed.encode bc)
+    (hAC : x.mem (ra + c) = Signed.encode ac)
+    (haddr : Fits (w + 2) (rb + ra + c + 1))
+    (hab : GenericRAM.Signed.Fits w ab) (hbc : GenericRAM.Signed.Fits w bc)
+    (hac : GenericRAM.Signed.Fits w ac) (hpartial : GenericRAM.Signed.Fits w (ab + bc)) :
+    ∃ y, ExecWithin (w + 2) testVertex x y 36 ∧
+      y.regs Signed.result = Signed.encode (ab + bc + ac) ∧ y.mem = x.mem ∧
+      ∀ i : Fin 32, 9 ≤ i.val → i ≠ Reg.address → y.regs i = x.regs i := by
+  let a := x.set Signed.left (Signed.encode ab) |>.set Reg.address (rb + c)
+    |>.set Signed.right (Signed.encode bc)
+  have hloadB : ExecWithin (w + 2) loadBC x a 3 := by
+    have hf : Fits (w + 2) (rb + c) := haddr.of_le (by omega)
+    ram_eval [loadBC, a, hrowB, hindex, hwab, hBC, hf,
+      Reg.address, Reg.rowB, Reg.index, Reg.wab, Signed.left, Signed.right, Fin.mk.injEq]
+  obtain ⟨b, hsumB, bsum, bframe⟩ := Signed.exec_add hab hbc a
+    (by simp +decide [a, Signed.left, Signed.right, Reg.address])
+    (by simp +decide [a, Signed.left, Signed.right, Reg.address])
+  change b.regs Signed.result = Signed.encode (ab + bc) at bsum
+  have bmeta (i : Fin 32) (hi : 9 ≤ i.val) (hne : i ≠ Reg.address) :
+      b.regs i = x.regs i :=
+    (bframe.2 i (Or.inr hi)).trans (hloadB.regs_eq (loads_preserve i hi hne).1)
+  have bra : b.regs Reg.rowA = ra := (bmeta _ (by decide) (by decide)).trans hrowA
+  have bindex : b.regs Reg.index = c := (bmeta _ (by decide) (by decide)).trans hindex
+  have bmem : b.mem = x.mem := bframe.1
+  let d := b.set Signed.left (Signed.encode (ab + bc)) |>.set Reg.address (ra + c)
+    |>.set Signed.right (Signed.encode ac)
+  have hloadA : ExecWithin (w + 2) loadAC b d 3 := by
+    have hf : Fits (w + 2) (ra + c) := haddr.of_le (by omega)
+    ram_eval [loadAC, d, bra, bindex, bsum, bmem, hAC, hf,
+      Reg.address, Reg.rowA, Reg.index, Signed.left, Signed.right, Signed.result, Fin.mk.injEq]
+  obtain ⟨y, hsumA, ysum, yframe⟩ := Signed.exec_add hpartial hac d
+    (by simp +decide [d, Signed.left, Signed.right, Reg.address])
+    (by simp +decide [d, Signed.left, Signed.right, Reg.address])
+  refine ⟨y, hloadB.seq (hsumB.seq (hloadA.seq hsumA)), ysum, ?_, ?_⟩
+  · exact yframe.1.trans bmem
+  · intro i hi hne
+    exact (yframe.2 i (Or.inr hi)).trans
+      ((hloadA.regs_eq (loads_preserve i hi hne).2).trans (bmeta i hi hne))
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Exec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Exec.lean
new file mode 100644
index 0000000000..dbc618745e
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Exec.lean
@@ -0,0 +1,231 @@
+/-
+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.WitnessScan.Cell
+public import Complexity.Algorithms.WordRAM.ExactTriangle.WitnessScan.Setup
+public import Complexity.Computability.GenericRAM.Signed.Fits
+
+/-!
+# Complete native original-weight interval verification
+
+Every interval vertex is tested by actual charged code. The returned flag characterizes
+existence of an original zero sum, and a successful run returns an original-coordinate witness.
+Arguments and all memory are preserved. The magnitude and address bounds here are numerical
+component premises; the producer/product consumer derives them from its original input.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
+
+open Cslib.WordRAM
+
+private theorem args_of_eq (A : Args) {x y : Data 32} (hx : A.InRegisters x)
+    (h : ∀ i : Fin 32, 9 ≤ i.val → i.val < 17 → y.regs i = x.regs i) :
+    A.InRegisters y := by
+  simpa only [Args.InRegisters, h Reg.ab (by decide) (by decide),
+    h Reg.bc (by decide) (by decide), h Reg.ac (by decide) (by decide),
+    h Reg.size (by decide) (by decide), h Reg.a (by decide) (by decide),
+    h Reg.b (by decide) (by decide), h Reg.first (by decide) (by decide),
+    h Reg.length (by decide) (by decide)] using hx
+
+private theorem finish_preserves : ∀ i : Fin 32,
+    (9 ≤ i.val ∧ i.val < 20) ∨ i = Reg.one ∨ i = Reg.zero →
+      finishVertex.Preserves i := by decide
+
+/-- Read and verify the original signed arrays, preserving the argument bank and all memory.
+The bound excludes only a final halt. The success flag is raw unsigned 0/1; the witness is an
+original vertex, not a middle-label or modular candidate. -/
+theorem exec {w U : ℕ} (A : Args) (AB BC AC : ℕ → ℕ → ℤ) (x : Data 32)
+    (hx : A.InRegisters x) (ha : A.a < A.n) (hb : A.b < A.n)
+    (hc : A.first + A.length ≤ A.n)
+    (hmem : ∀ i < A.n, ∀ j < A.n,
+      x.mem (A.ab + (i * A.n + j)) = Signed.encode (AB i j) ∧
+      x.mem (A.bc + (i * A.n + j)) = Signed.encode (BC i j) ∧
+      x.mem (A.ac + (i * A.n + j)) = Signed.encode (AC i j))
+    (hmag : ∀ i < A.n, ∀ j < A.n,
+      (AB i j).natAbs ≤ U ∧ (BC i j).natAbs ≤ U ∧ (AC i j).natAbs ≤ U)
+    (hU : GenericRAM.Signed.Fits w (2 * U : ℕ))
+    (hfit : Fits (w + 2) A.addressBound) :
+    ∃ y, ExecWithin (w + 2) program x y (42 * A.length + 17) ∧
+      A.InRegisters y ∧ y.mem = x.mem ∧ (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+      (y.regs Reg.found = 1 ↔ ∃ c, A.first ≤ c ∧ c < A.first + A.length ∧
+        AB A.a A.b + BC A.b c + AC A.a c = 0) ∧
+      (y.regs Reg.found = 1 → A.first ≤ y.regs Reg.witness ∧
+        y.regs Reg.witness < A.first + A.length ∧
+        AB A.a A.b + BC A.b (y.regs Reg.witness) + AC A.a (y.regs Reg.witness) = 0) := by
+  let total (c : ℕ) := AB A.a A.b + BC A.b c + AC A.a c
+  obtain ⟨s, hs, sargs, smem, sone, szero, sfound, sindex, srowB, srowA, swab⟩ :=
+    exec_setup A x (AB A.a A.b) hx ha hb hc (hmem A.a ha A.b hb).1 hfit
+  let I (y : Data 32) : Prop := A.InRegisters y ∧ y.mem = x.mem ∧
+    y.regs Reg.one = 1 ∧ y.regs Reg.zero = 0 ∧
+    y.regs Reg.rowB = A.bc + A.b * A.n + A.first ∧
+    y.regs Reg.rowA = A.ac + A.a * A.n + A.first ∧
+    y.regs Reg.wab = Signed.encode (AB A.a A.b) ∧ y.regs Reg.index ≤ A.length ∧
+    (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+    (y.regs Reg.found = 1 ↔ ∃ j < y.regs Reg.index, total (A.first + j) = 0) ∧
+    (y.regs Reg.found = 1 → A.first ≤ y.regs Reg.witness ∧
+      y.regs Reg.witness < A.first + y.regs Reg.index ∧ total (y.regs Reg.witness) = 0)
+  have hstart : I s := by
+    refine ⟨sargs, smem, sone, szero, srowB, srowA, swab, by omega,
+      Or.inl sfound, ?_, ?_⟩
+    · constructor
+      · intro h; omega
+      · rintro ⟨j, hj, -⟩; omega
+    · intro h; omega
+  have hrowB : A.b * A.n + A.first ≤ A.n * A.n := by
+    have hstep := Nat.mul_le_mul_right A.n (Nat.succ_le_of_lt hb)
+    rw [Nat.succ_mul] at hstep
+    omega
+  have hrowA : A.a * A.n + A.first ≤ A.n * A.n := by
+    have hstep := Nat.mul_le_mul_right A.n (Nat.succ_le_of_lt ha)
+    rw [Nat.succ_mul] at hstep
+    omega
+  have hbody (y : Data 32) (hy : I y) (hc' : (Cond.lt Reg.index Reg.length).Holds y) :
+      ∃ z, ExecWithin (w + 2) step y z 40 ∧ I z ∧
+        A.length - z.regs Reg.index < A.length - y.regs Reg.index := by
+    obtain ⟨yargs, ymem, yone, yzero, yrowB, yrowA, ywab, yindex, yflag, yiff, ywit⟩ := hy
+    have yl : y.regs Reg.length = A.length := yargs.2.2.2.2.2.2.2
+    have hi : y.regs Reg.index < A.length := by
+      simpa only [Cond.holds_lt, yl] using hc'
+    let i := y.regs Reg.index
+    have hcurrent : A.first + i < A.n := by dsimp only [i]; omega
+    have hreadB : y.mem (A.bc + A.b * A.n + A.first + i) =
+        Signed.encode (BC A.b (A.first + i)) := by
+      rw [ymem]
+      simpa only [Nat.add_assoc] using (hmem A.b hb (A.first + i) hcurrent).2.1
+    have hreadA : y.mem (A.ac + A.a * A.n + A.first + i) =
+        Signed.encode (AC A.a (A.first + i)) := by
+      rw [ymem]
+      simpa only [Nat.add_assoc] using (hmem A.a ha (A.first + i) hcurrent).2.2
+    have habmag := (hmag A.a ha A.b hb).1
+    have hbcmag := (hmag A.b hb (A.first + i) hcurrent).2.1
+    have hacmag := (hmag A.a ha (A.first + i) hcurrent).2.2
+    have habfit := hU.of_natAbs_le (habmag.trans (by omega : U ≤ 2 * U))
+    have hbcfit := hU.of_natAbs_le (hbcmag.trans (by omega : U ≤ 2 * U))
+    have hacfit := hU.of_natAbs_le (hacmag.trans (by omega : U ≤ 2 * U))
+    have hsumMag : (AB A.a A.b + BC A.b (A.first + i)).natAbs ≤ 2 * U := by
+      have := Int.natAbs_add_le (AB A.a A.b) (BC A.b (A.first + i))
+      omega
+    have hsumfit := hU.of_natAbs_le hsumMag
+    obtain ⟨b, hbtest, bsum, bmem, bmeta⟩ := exec_testVertex y yrowB yrowA rfl ywab
+      hreadB hreadA (hfit.of_le (by dsimp only [Args.addressBound]; omega))
+      habfit hbcfit hacfit hsumfit
+    change b.regs Signed.result = Signed.encode (total (A.first + i)) at bsum
+    have bone : b.regs Reg.one = 1 := (bmeta _ (by decide) (by decide)).trans yone
+    have bzero : b.regs Reg.zero = 0 := (bmeta _ (by decide) (by decide)).trans yzero
+    have bfirst : b.regs Reg.first = A.first :=
+      (bmeta _ (by decide) (by decide)).trans yargs.2.2.2.2.2.2.1
+    have bindex : b.regs Reg.index = i := bmeta _ (by decide) (by decide)
+    have bfound : b.regs Reg.found = y.regs Reg.found := bmeta _ (by decide) (by decide)
+    have bwit : b.regs Reg.witness = y.regs Reg.witness := bmeta _ (by decide) (by decide)
+    let z := (if total (A.first + i) = 0 then
+        b.set Reg.found 1 |>.set Reg.witness (A.first + i)
+      else b.set Reg.witness (b.regs Reg.witness)).set Reg.index (i + 1)
+    have hfinish : ExecWithin (w + 2) finishVertex b z 4 := by
+      have hinc : Fits (w + 2) (i + 1) := hfit.of_le (by
+        dsimp only [Args.addressBound]; dsimp only [i]; omega)
+      have hpos : Fits (w + 2) (A.first + i) := hfit.of_le (by
+        dsimp only [Args.addressBound]; omega)
+      by_cases hz : total (A.first + i) = 0
+      · have hresult : b.regs Signed.result = 0 := by rw [bsum]; rw [hz]; rfl
+        simp only [z, ite_eq_left hz]
+        ram_eval [finishVertex, hresult, bone, bzero, bfirst, bindex, hinc, hpos,
+          Reg.found, Reg.one, Reg.zero, Reg.witness, Reg.index, Reg.first,
+          Signed.result, Fin.mk.injEq]
+      · have hresult : b.regs Signed.result ≠ 0 := by
+          intro he
+          apply hz
+          apply Signed.encode_injective
+          exact bsum.symm.trans he
+        simp only [z, ite_eq_right hz]
+        ram_eval [finishVertex, hresult, bone, bzero, bfirst, bindex, hinc,
+          Reg.found, Reg.one, Reg.zero, Reg.witness, Reg.index, Reg.first,
+          Signed.result, Fin.mk.injEq]
+    have zindex : z.regs Reg.index = i + 1 := by simp [z]
+    have zflag : z.regs Reg.found = if total (A.first + i) = 0 then 1 else y.regs Reg.found := by
+      by_cases hz : total (A.first + i) = 0 <;>
+        simp +decide [z, hz, Reg.index, Reg.witness, Reg.found, bfound]
+    have zwit : z.regs Reg.witness =
+        if total (A.first + i) = 0 then A.first + i else y.regs Reg.witness := by
+      by_cases hz : total (A.first + i) = 0 <;>
+        simp +decide [z, hz, Reg.index, Reg.witness, bwit]
+    have keep (j : Fin 32)
+        (hj : (9 ≤ j.val ∧ j.val < 20) ∨ j = Reg.one ∨ j = Reg.zero) :
+        z.regs j = y.regs j := by
+      have hj9 : 9 ≤ j.val := by
+        rcases hj with h | rfl | rfl
+        · exact h.1
+        · decide
+        · decide
+      have hjaddr : j ≠ Reg.address := by
+        rcases hj with h | rfl | rfl
+        · intro he
+          have hv := congrArg Fin.val he
+          change j.val = 24 at hv
+          omega
+        · decide
+        · decide
+      exact (hfinish.regs_eq (finish_preserves j hj)).trans (bmeta j hj9 hjaddr)
+    have zmem : z.mem = b.mem := by
+      by_cases hz : total (A.first + i) = 0 <;> simp [z, hz]
+    refine ⟨z, hbtest.seq hfinish, ?_, ?_⟩
+    · refine ⟨args_of_eq A yargs (fun j hj hj' => keep j (Or.inl ⟨hj, by omega⟩)),
+        zmem.trans (bmem.trans ymem), (keep _ (Or.inr (Or.inl rfl))).trans yone,
+        (keep _ (Or.inr (Or.inr rfl))).trans yzero,
+        (keep _ (Or.inl ⟨by decide, by decide⟩)).trans yrowB,
+        (keep _ (Or.inl ⟨by decide, by decide⟩)).trans yrowA,
+        (keep _ (Or.inl ⟨by decide, by decide⟩)).trans ywab,
+        by rw [zindex]; dsimp only [i]; omega, ?_, ?_, ?_⟩
+      · rw [zflag]
+        split_ifs <;> omega
+      · rw [zflag, zindex]
+        by_cases hz : total (A.first + i) = 0
+        · rw [ite_eq_left hz]
+          exact ⟨fun _ => ⟨i, by omega, hz⟩, fun _ => rfl⟩
+        · rw [ite_eq_right hz, yiff]
+          constructor
+          · rintro ⟨j, hj, hzero⟩
+            exact ⟨j, by dsimp only [i]; omega, hzero⟩
+          · rintro ⟨j, hj, hzero⟩
+            refine ⟨j, ?_, hzero⟩
+            have hne : j ≠ i := by intro he; subst j; exact hz hzero
+            dsimp only [i] at *
+            omega
+      · intro hfound
+        by_cases hz : total (A.first + i) = 0
+        · rw [zwit, ite_eq_left hz, zindex]
+          exact ⟨by omega, by omega, hz⟩
+        · rw [zflag, ite_eq_right hz] at hfound
+          obtain ⟨hlo, hhi, hzero⟩ := ywit hfound
+          rw [zwit, ite_eq_right hz, zindex]
+          exact ⟨hlo, by dsimp only [i]; omega, hzero⟩
+    · rw [zindex]
+      dsimp only [i]
+      omega
+  obtain ⟨y, hloop, hy, hdone⟩ := ExecWithin.loop_invariant I
+    (fun y => A.length - y.regs Reg.index) hbody hstart
+  obtain ⟨yargs, ymem, yone, yzero, yrowB, yrowA, ywab, yindex, yflag, yiff, ywit⟩ := hy
+  have ylen : y.regs Reg.length = A.length := yargs.2.2.2.2.2.2.2
+  have yend : y.regs Reg.index = A.length := by
+    simp only [Cond.holds_lt, ylen] at hdone
+    omega
+  refine ⟨y, (hs.seq hloop).mono (by rw [sindex]; omega), yargs, ymem, yflag, ?_, ?_⟩
+  · constructor
+    · intro hfound
+      obtain ⟨j, hj, hz⟩ := yiff.mp hfound
+      exact ⟨A.first + j, by omega, by rw [yend] at hj; omega, hz⟩
+    · rintro ⟨c, hlo, hhi, hz⟩
+      apply yiff.mpr
+      refine ⟨c - A.first, by rw [yend]; omega, ?_⟩
+      simpa only [Nat.add_sub_of_le hlo] using hz
+  · intro hfound
+    simpa only [yend] using ywit hfound
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Finite.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Finite.lean
new file mode 100644
index 0000000000..8dd68e0630
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Finite.lean
@@ -0,0 +1,67 @@
+/-
+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.WitnessScan.Exec
+public import Complexity.Algorithms.ExactTriangle.PieceBounds
+public import Complexity.Algorithms.ExactTriangle.Witnesses
+
+/-!
+# Native interval failure and existing finite witness scans
+
+The actual verifier reports the last zero it reads, whereas `scanPiece` returns the first.
+Their failure conditions agree: both exhaust precisely the original vertices in the existing
+finite piece. This value lemma connects native failure accounting to the existing finite
+false-positive theory without identifying the two witness-order conventions.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
+
+open Cslib.Algorithms.ExactTriangle
+
+/-- Native interval exhaustion is exactly failure of the existing finite piece scan. The
+array equations describe the same original integer weights; no witness routine is assumed. -/
+theorem fails_iff_scanPiece_eq_none {n D g k : ℕ}
+    (AB BC AC : ℕ → ℕ → ℤ) (wAB wBC wAC : Fin n → Fin n → ℤ)
+    (hD : 16 ≤ D) (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)
+    (a b : Fin n) :
+    let first := k * pieceSize D g
+    let length := min (pieceSize D g) (n - first)
+    (∀ c : Fin length, AB a.val b.val + BC b.val (first + c.val) +
+      AC a.val (first + c.val) ≠ 0) ↔ scanPiece wAB wBC wAC D g k a b = none := by
+  let first := k * pieceSize D g
+  let length := min (pieceSize D g) (n - first)
+  have heq (c : Fin n) : AB a.val b.val + BC b.val c.val + AC a.val c.val =
+      weightSum wAB wBC wAC a b c := by rw [hAB, hBC, hAC]; rfl
+  rw [scanPiece_eq_none_iff]
+  constructor
+  · intro hfail c hc
+    have hinterval := (mem_piece_iff_interval hD hg c).mp hc
+    change first ≤ c.val ∧ c.val < first + length at hinterval
+    let j : Fin length := ⟨c.val - first, by omega⟩
+    have he : first + j.val = c.val := by dsimp only [j]; omega
+    have hz := hfail j
+    rw [he, heq] at hz
+    exact hz
+  · intro hfail j
+    have hj := j.isLt
+    have hl := min_le_right (pieceSize D g) (n - first)
+    have hn : first + j.val < n := by change j.val < length at hj; omega
+    let c : Fin n := ⟨first + j.val, hn⟩
+    have hc : c ∈ piece n D g k := by
+      apply (mem_piece_iff_interval hD hg c).mpr
+      exact ⟨Nat.le_add_right _ _, Nat.add_lt_add_left j.isLt _⟩
+    have hz := hfail c hc
+    simpa only [← heq c] using hz
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Program.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Program.lean
new file mode 100644
index 0000000000..855fd10b95
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Program.lean
@@ -0,0 +1,139 @@
+/-
+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.Computability.WordRAM.Signed.Arithmetic
+
+/-!
+# Native original-weight verification in one vertex interval
+
+The program reads the original canonical-signed A–B, B–C and A–C arrays, tests each vertex
+in the supplied interval using two actual signed-addition kernels, and returns a flag and
+an original vertex witnessing a zero sum. It writes no memory and preserves all arguments.
+This is the inner verifier used after a nonzero product answer, not a product or ET oracle.
+
+The interval scan follows the pinned `Scan.lean` procedure in the proof of Theorem 17
+at `anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5`. The native code,
+register layout and charged constants are rebuilt against the existing WordRAM APIs.
+The stage definitions are internal implementation interfaces.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
+
+open Cslib.WordRAM
+
+namespace Reg
+
+/-- Original canonical-signed A–B array pointer. -/
+abbrev ab : Fin 32 := 9
+/-- Original canonical-signed B–C array pointer. -/
+abbrev bc : Fin 32 := 10
+/-- Original canonical-signed A–C array pointer. -/
+abbrev ac : Fin 32 := 11
+/-- Outer matrix dimension. -/
+abbrev size : Fin 32 := 12
+/-- Original first query coordinate. -/
+abbrev a : Fin 32 := 13
+/-- Original second query coordinate. -/
+abbrev b : Fin 32 := 14
+/-- First original vertex of the scanned interval. -/
+abbrev first : Fin 32 := 15
+/-- Number of vertices in the interval. -/
+abbrev length : Fin 32 := 16
+/-- B–C row pointer at the first interval vertex. -/
+abbrev rowB : Fin 32 := 17
+/-- A–C row pointer at the first interval vertex. -/
+abbrev rowA : Fin 32 := 18
+/-- Cached canonical-signed A–B weight. -/
+abbrev wab : Fin 32 := 19
+/-- Number of interval vertices already tested. -/
+abbrev index : Fin 32 := 20
+/-- Unsigned success flag. -/
+abbrev found : Fin 32 := 21
+/-- Original vertex of the most recently verified zero sum. -/
+abbrev witness : Fin 32 := 22
+/-- Constant one. -/
+abbrev one : Fin 32 := 23
+/-- Actual load-address temporary. -/
+abbrev address : Fin 32 := 24
+/-- Constant zero, preserved by the signed arithmetic bank. -/
+abbrev zero : Fin 32 := 25
+
+end Reg
+
+/-- Ordinary runtime arguments of the original-weight interval verifier. This stores no
+execution, fit, witness or time certificate. -/
+structure Args where
+  /-- Original canonical-signed A–B array base. -/
+  ab : ℕ
+  /-- Original canonical-signed B–C array base. -/
+  bc : ℕ
+  /-- Original canonical-signed A–C array base. -/
+  ac : ℕ
+  /-- Matrix dimension. -/
+  n : ℕ
+  /-- First query coordinate. -/
+  a : ℕ
+  /-- Second query coordinate. -/
+  b : ℕ
+  /-- First interval vertex. -/
+  first : ℕ
+  /-- Number of interval vertices. -/
+  length : ℕ
+
+/-- The eight scalar arguments occupy their actual native registers. -/
+@[expose] def Args.InRegisters (A : Args) (x : Data 32) : Prop :=
+  x.regs Reg.ab = A.ab ∧ x.regs Reg.bc = A.bc ∧ x.regs Reg.ac = A.ac ∧
+    x.regs Reg.size = A.n ∧ x.regs Reg.a = A.a ∧ x.regs Reg.b = A.b ∧
+    x.regs Reg.first = A.first ∧ x.regs Reg.length = A.length
+
+/-- A concrete numerical envelope for all address/index arithmetic in this verifier. -/
+@[expose] def Args.addressBound (A : Args) : ℕ :=
+  A.ab + A.bc + A.ac + 3 * (A.n * A.n) + A.n + A.first + A.length + 8
+
+open Reg in
+/-- Load the fixed A–B weight and compute the two row pointers with actual instructions. -/
+@[expose] def setup : Code .standard 32 := ram[
+  one ← #1; zero ← #0; found ← #0; index ← #0; witness ← first;
+  address ← a * size; address ← address + b; address ← address + ab; wab ← *address;
+  rowB ← b * size; rowB ← rowB + first; rowB ← rowB + bc;
+  rowA ← a * size; rowA ← rowA + first; rowA ← rowA + ac ]
+
+open Reg in
+/-- First two original signed weights, read from the original memory. -/
+@[expose] def loadBC : Code .standard 32 := ram[
+  Signed.left ← wab; address ← rowB + index; Signed.right ← *address ]
+
+open Reg in
+/-- The true partial sum and the original A–C weight. -/
+@[expose] def loadAC : Code .standard 32 := ram[
+  Signed.left ← Signed.result; address ← rowA + index; Signed.right ← *address ]
+
+/-- Two charged standard-native signed additions, with no extra machine operation. -/
+@[expose] def testVertex : Code .standard 32 :=
+  .seq loadBC (.seq Signed.add (.seq loadAC Signed.add))
+
+open Reg in
+/-- Remember a genuine zero-sum vertex, then advance the interval counter. -/
+@[expose] def finishVertex : Code .standard 32 := ram[
+  if Signed.result = zero then [ found ← one; witness ← first + index ]
+  else [ witness ← witness ]; index ← index + one ]
+
+/-- One complete verification step. -/
+@[expose] def step : Code .standard 32 := .seq testVertex finishVertex
+
+/-- Fixed native interval verifier; only the actual loop count depends on input. -/
+@[expose] def program : Code .standard 32 :=
+  .seq setup (.loop (.lt Reg.index Reg.length) step)
+
+/-- Fixed instruction graph, independent of dimensions and physical width. -/
+theorem program_fixed : program.size ≤ 160 ∧ ¬program.ReadsWidth := by decide
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Setup.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Setup.lean
new file mode 100644
index 0000000000..fde58d47c6
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/WitnessScan/Setup.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.WitnessScan.Program
+
+/-!
+# Native interval-verifier initialization
+
+The actual header caches one original weight and computes two original row pointers. Its
+numeric address bound covers every intermediate product/sum, including empty intervals at
+the one-past-end boundary. These are internal rules for composing the verifier loop.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
+
+open Cslib.WordRAM
+
+/-- Initialize the actual verifier in fifteen instructions, preserving the original arguments
+and memory. In particular the weight is loaded from the original A–B array, not supplied as
+an accepted modular candidate. -/
+theorem exec_setup {W : ℕ} (A : Args) (x : Data 32) (v : ℤ)
+    (hx : A.InRegisters x) (ha : A.a < A.n) (hb : A.b < A.n)
+    (hc : A.first + A.length ≤ A.n)
+    (hread : x.mem (A.ab + (A.a * A.n + A.b)) = Signed.encode v)
+    (hfit : Fits W A.addressBound) :
+    ∃ y, ExecWithin W setup x y 15 ∧ A.InRegisters y ∧ y.mem = x.mem ∧
+      y.regs Reg.one = 1 ∧ y.regs Reg.zero = 0 ∧ y.regs Reg.found = 0 ∧
+      y.regs Reg.index = 0 ∧ y.regs Reg.rowB = A.bc + A.b * A.n + A.first ∧
+      y.regs Reg.rowA = A.ac + A.a * A.n + A.first ∧
+      y.regs Reg.wab = Signed.encode v := by
+  obtain ⟨hab, hbc, hac, hn, ha', hb', hf, hl⟩ := hx
+  have hstepA : A.a * A.n + A.n ≤ A.n * A.n := by
+    simpa only [Nat.succ_mul] using Nat.mul_le_mul_right A.n (Nat.succ_le_of_lt ha)
+  have hstepB : A.b * A.n + A.n ≤ A.n * A.n := by
+    simpa only [Nat.succ_mul] using Nat.mul_le_mul_right A.n (Nat.succ_le_of_lt hb)
+  have hiab : A.a * A.n + A.b < A.n * A.n := by omega
+  have hrowB : A.b * A.n + A.first ≤ A.n * A.n := by omega
+  have hrowA : A.a * A.n + A.first ≤ A.n * A.n := by omega
+  have hmulA : A.a * A.n ≤ A.n * A.n := Nat.mul_le_mul_right _ ha.le
+  have hmulB : A.b * A.n ≤ A.n * A.n := Nat.mul_le_mul_right _ hb.le
+  have h1 : Fits W 1 := hfit.of_le (by unfold Args.addressBound; omega)
+  have hfirst : Fits W A.first := hfit.of_le (by unfold Args.addressBound; omega)
+  have hmA : Fits W (A.a * A.n) := hfit.of_le (by unfold Args.addressBound; omega)
+  have hmB : Fits W (A.b * A.n) := hfit.of_le (by unfold Args.addressBound; omega)
+  have hpair : Fits W (A.a * A.n + A.b) := hfit.of_le (by unfold Args.addressBound; omega)
+  have hpaddr : Fits W (A.a * A.n + A.b + A.ab) :=
+    hfit.of_le (by unfold Args.addressBound; omega)
+  have hrB : Fits W (A.b * A.n + A.first) :=
+    hfit.of_le (by unfold Args.addressBound; omega)
+  have hrA : Fits W (A.a * A.n + A.first) :=
+    hfit.of_le (by unfold Args.addressBound; omega)
+  have hpB : Fits W (A.b * A.n + A.first + A.bc) :=
+    hfit.of_le (by unfold Args.addressBound; omega)
+  have hpA : Fits W (A.a * A.n + A.first + A.ac) :=
+    hfit.of_le (by unfold Args.addressBound; omega)
+  have hread' : x.mem (A.a * A.n + A.b + A.ab) = Signed.encode v := by
+    simpa only [Nat.add_comm] using hread
+  let y := x.set Reg.one 1 |>.set Reg.zero 0 |>.set Reg.found 0 |>.set Reg.index 0
+    |>.set Reg.witness A.first |>.set Reg.address (A.a * A.n)
+    |>.set Reg.address (A.a * A.n + A.b) |>.set Reg.address (A.a * A.n + A.b + A.ab)
+    |>.set Reg.wab (Signed.encode v) |>.set Reg.rowB (A.b * A.n)
+    |>.set Reg.rowB (A.b * A.n + A.first) |>.set Reg.rowB (A.b * A.n + A.first + A.bc)
+    |>.set Reg.rowA (A.a * A.n) |>.set Reg.rowA (A.a * A.n + A.first)
+    |>.set Reg.rowA (A.a * A.n + A.first + A.ac)
+  have he : ExecWithin W setup x y 15 := by
+    ram_eval [setup, y, hab, hbc, hac, hn, ha', hb', hf, hl, hread',
+      h1, hfirst, hmA, hmB, hpair, hpaddr, hrA, hrB, hpA, hpB,
+      Reg.one, Reg.zero, Reg.found, Reg.index, Reg.witness, Reg.address, Reg.ab, Reg.bc,
+      Reg.ac, Reg.a, Reg.b, Reg.size, Reg.first, Reg.rowA, Reg.rowB, Reg.wab, Reg.length,
+      Fin.mk.injEq]
+  refine ⟨y, he, ?_, rfl, ?_⟩
+  · simpa +decide [Args.InRegisters, y, Reg.one, Reg.zero, Reg.found, Reg.index, Reg.witness,
+      Reg.address, Reg.ab, Reg.bc, Reg.ac, Reg.a, Reg.b, Reg.size, Reg.first, Reg.rowA,
+      Reg.rowB, Reg.wab, Reg.length] using
+      (show Args.InRegisters A x from ⟨hab, hbc, hac, hn, ha', hb', hf, hl⟩)
+  · simp +decide [y, Reg.one, Reg.zero, Reg.found, Reg.index, Reg.witness, Reg.address,
+      Reg.rowA, Reg.rowB, Reg.wab, Nat.add_comm, Nat.add_left_comm]
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.WitnessScan
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/WriteMatrices.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/WriteMatrices.lean
index 6ee0235e5d..6425557ce7 100644
--- a/Complexity/Algorithms/WordRAM/ExactTriangle/WriteMatrices.lean
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/WriteMatrices.lean
@@ -77,6 +77,11 @@ def entry (rightSide : Bool) (A : Args) (R : ℕ → ℕ) (q : ℕ) : ℕ :=
     if label = wanted then 1 else 0
   else 0
 
+/-- Every raw adjacency entry is a zero/one word, including padding. -/
+theorem entry_le_one (side : Bool) (A : Args) (R : ℕ → ℕ) (q : ℕ) :
+    entry side A R q ≤ 1 := by
+  cases side <;> dsimp only [entry] <;> split_ifs <;> omega
+
 /-- Residue input pointer. -/
 abbrev src : Fin 17 := 0
 /-- Output matrix pointer. -/
diff --git a/ComplexityTests/WordRAMExactTriangleQueryValues.lean b/ComplexityTests/WordRAMExactTriangleQueryValues.lean
new file mode 100644
index 0000000000..3f436d0775
--- /dev/null
+++ b/ComplexityTests/WordRAMExactTriangleQueryValues.lean
@@ -0,0 +1,86 @@
+/-
+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.RecordProduct.QueryValues
+import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationInput
+
+/-!
+# Original pairs from an actual producer query block
+
+The small concrete producer instance tests the readback API independently of thin-product
+geometry. The kernel client starts with the original scalar headers and twelve zero weights;
+neither a prepared query list nor a layout certificate is supplied as input.
+-/
+
+set_option linter.hashCommand false
+
+namespace ComplexityTests.WordRAMExactTriangleQueryValues
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.WordRAM.ExactTriangle
+
+private def values : List ℤ := List.replicate 12 0
+private def zeroAB : Fin 2 → Fin 2 → ℤ := fun _ _ => 0
+
+-- The actual producer writes all four original coordinate pairs in row-major rank order.
+#guard (Instances.program.eval 256 64 (Data.init (PreparationInput.input 2 1 1 2 values))).map
+    (fun (y, _) => (List.range 8).map (fun j => y.mem (31 + j))) ==
+  some [0, 0, 0, 1, 1, 0, 1, 1]
+
+/-- Fully admitted initialized producer execution, connected to the new query-value API.
+The original pairs occur once each and their order is the existing finite class rank. -/
+example : ∃ T : ℕ, ∃ y : Data 64,
+    ExecWithin 256 Instances.program (Data.init (PreparationInput.input 2 1 1 2 values)) y T ∧
+    let qs := RecordProduct.decodedQueries (by decide : 0 < 2) y.mem 31 4
+    qs.Nodup ∧ qs.toFinset = Finset.univ ∧
+      ∀ i : Fin qs.length, rankIn (Finset.univ : Finset (Fin 2 × Fin 2)) (qs.get i) = i.val := by
+  obtain ⟨y, he, hout, -, -⟩ := PreparationInput.exec_input
+    (n := 2) (D := 1) (g := 1) (p := 2) (A := 0) (W := 256) values
+    (by decide) (by decide) (by decide) (by decide) (by decide)
+    (by intro z hz; exact le_of_eq (congrArg Int.natAbs (List.eq_of_mem_replicate hz)))
+    (by decide)
+  have hAB : ∀ a b, values.getD (pairIndex (a, b)) 0 = zeroAB a b := by
+    intro a b
+    change (List.replicate 12 (0 : ℤ))[pairIndex (a, b)]?.getD 0 = 0
+    exact List.getElem?_getD_replicate_default_eq _ _ _
+  have hcap : queryCap 2 1 = 4 := by
+    have hl : 4 ≤ Nat.sqrt 16 := Nat.le_sqrt.mpr (by decide)
+    have hu : Nat.sqrt 16 < 5 := Nat.sqrt_lt.mpr (by decide)
+    change Nat.sqrt 16 = 4
+    omega
+  have hclass : residueClass zeroAB 2 0 = Finset.univ := by decide
+  have hk : 0 < numChunks (residueClass zeroAB 2 0) (queryCap 2 1) := by
+    rw [hcap, hclass]
+    decide
+  obtain ⟨hget, hnodup, hset⟩ := RecordProduct.decodedQueries_chunkOf
+    (fun q => values.getD q 0) zeroAB (by decide) (by decide) hAB
+    (by decide) (by decide) hout 0 0 hk
+  have hchunk : chunkOf zeroAB 1 2 0 0 = Finset.univ := by
+    rw [chunkOf, chunk, hclass, hcap]
+    ext pair
+    simp only [Finset.mem_filter, Finset.mem_univ, true_and, rankIn_univ]
+    apply iff_true_intro
+    apply Nat.div_eq_of_lt
+    have ha := pair.1.isLt
+    have hb := pair.2.isLt
+    dsimp only [pairIndex]
+    omega
+  simp_rw [hcap, hclass] at hget
+  simp only [hcap, hclass] at hnodup hset
+  simp only [Nat.reduceAdd, Nat.reduceMul, Fin.val_zero, zero_mul, Nat.add_zero,
+    Nat.sub_zero, Finset.card_univ, Fintype.card_prod, Fintype.card_fin,
+    min_self] at hget hnodup hset
+  refine ⟨_, y, he, ?_⟩
+  refine ⟨?_, ?_, ?_⟩
+  · exact hnodup
+  · exact hset.trans hchunk
+  · intro i
+    simpa [hcap, hclass] using (hget ⟨i.val, by
+      simpa [RecordProduct.decodedQueries_length, hcap, hclass] using i.isLt⟩).2
+
+end ComplexityTests.WordRAMExactTriangleQueryValues
diff --git a/ComplexityTests/WordRAMExactTriangleRecordWitness.lean b/ComplexityTests/WordRAMExactTriangleRecordWitness.lean
new file mode 100644
index 0000000000..97908121e2
--- /dev/null
+++ b/ComplexityTests/WordRAMExactTriangleRecordWitness.lean
@@ -0,0 +1,147 @@
+/-
+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.RecordWitness.SourceBounds
+
+/-!
+# Actual candidate-consumer executions at valid thin geometry
+
+These sparse-memory fixtures execute the full descriptor/root/query/verifier consumer at
+`D=16`, `n=16^18`. They supply a post-product memory fixture, not a full producer/product run.
+The initialized composition client is separate. No enormous encoder run is evaluated here.
+-/
+
+set_option linter.hashCommand false
+
+namespace ComplexityTests.WordRAMExactTriangleRecordWitness
+
+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 queryBase : ℕ := 8 + 6 * (side * side)
+private def records : ℕ := 23 + 12 * (side * side)
+private def heap : ℕ := records + 6 + 2 * (side * 16)
+private def answers : ℕ := heap + 100
+
+private def fixture (success zeroAnswers : Bool) : Data 400 :=
+  { regs := fun i => if i.val = 39 then records else if i.val = 42 then heap
+      else if i.val = 64 then 0 else if i.val = 65 then answers else 77
+    mem := fun a =>
+      if a = 1 then 16 else if a = 2 then 1 else if a = 3 then side else if a = 4 then 3
+      else if 5 ≤ a && a < 5 + side * side then
+        if a = 5 + (side - 1) * side + (side - 2) ||
+            a = 5 + (side - 1) * side + (side - 1) then 0 else Signed.encode 1
+      else if 5 + side * side ≤ a && a < 5 + 2 * (side * side) then
+        if success then 0 else Signed.encode 3
+      else if records ≤ a && a < records + 6 then
+        [0, 0, queryBase, 2, records + 6, records + 6 + side * 16].getD (a - records) 0
+      else if a = queryBase then side - 1 else if a = queryBase + 1 then side - 2
+      else if a = queryBase + 2 then side - 1 else if a = queryBase + 3 then side - 1
+      else if a = answers || a = answers + 1 then if zeroAnswers then 0 else Signed.encode 4
+      else if a = answers + 2 then 99 else 0 }
+
+private def observe (success zeroAnswers : Bool) : Option (List ℕ × Bool × Bool) :=
+  (RecordWitness.consume.eval 512 64 (fixture success zeroAnswers)).map fun (y, t) =>
+    ([y.regs RecordWitness.Reg.found, y.regs RecordWitness.Reg.witnessA,
+      y.regs RecordWitness.Reg.witnessB, y.regs RecordWitness.Reg.witnessC,
+      y.regs RecordWitness.Reg.scans, y.regs RecordWitness.Reg.index, y.mem (answers + 2)],
+      decide (t ≤ 20 + 16 + 196 * y.regs RecordWitness.Reg.scans + 52),
+      decide (∀ j : Fin 320, y.regs (RecordWitness.productBank j) =
+        (fixture success zeroAnswers).regs (RecordWitness.productBank j)))
+
+-- The first pair succeeds; the second candidate incurs no further original-weight scan.
+#guard observe true false == some ([1, side - 1, side - 2, 3, 1, 2, 99], true, true)
+
+-- Both accepted modular candidates have original sum three, and both scans fail.
+#guard observe false false == some ([0, 0, 0, 0, 2, 2, 99], true, true)
+
+-- Zero answer words produce no verifier call, even though original weights have zero sums.
+#guard observe true true == some ([0, 0, 0, 0, 0, 2, 99], true, true)
+
+#guard side ≥ 16 ^ 18
+#guard ¬(16 ≥ 16 ^ 18)
+
+private def zeroWeights (N : ℕ) : List ℤ := List.replicate (3 * (N * N)) 0
+private def width (N : ℕ) : ℕ := RecordWitness.admissionWidth N (D 2) 1 3 0
+
+/-- All original-input premises are discharged at valid positive depth. The real initialized
+producer/product/verifier returns an actual original witness in the same state as prefix and
+halt. This symbolic kernel proof does not evaluate the enormous positive-depth encoder. -/
+private theorem initialized_zero (N : ℕ) (hgeo : D 2 ^ 18 ≤ N) :
+    ∃ y : Data 400, ∃ t S : ℕ,
+      Runs (width N) (RecordWitness.entryProgram.program RecordWitness.Reg.found)
+        (State.init (PreparationInput.input N (D 2) 1 3 (zeroWeights N)))
+        ⟨RecordWitness.entryProgram.size, y⟩ t ∧
+      Executes (width N) (RecordWitness.entryProgram.program RecordWitness.Reg.found)
+        (State.init (PreparationInput.input N (D 2) 1 3 (zeroWeights N))) 1 (t + 1) ∧
+      y.regs RecordWitness.Reg.found = 1 ∧ y.regs RecordWitness.Reg.scans = S ∧ S ≤ 1 ∧
+      ∃ u v c : Fin N, y.regs RecordWitness.Reg.witnessA = u.val ∧
+        y.regs RecordWitness.Reg.witnessB = v.val ∧ y.regs RecordWitness.Reg.witnessC = c.val := by
+  have hprime : 3 ∈ Nat.sqrtPrimeWindow (D 2) :=
+    Nat.mem_sqrtPrimeWindow_iff_sq.mpr ⟨by decide, by decide, by decide⟩
+  have hmag : ∀ z ∈ zeroWeights N, z.natAbs ≤ 0 := by
+    intro z hz
+    have he : z = 0 := List.eq_of_mem_replicate hz
+    subst z
+    decide
+  obtain ⟨hi, a, idx, ha, hout, hidx, hord, y, t, S, ht, hr, he, yb, ys, yf,
+    hS, yiff, yw, frame, regs⟩ := RecordWitness.runs_input (m := 2) (n := N)
+      (g := 1) (p := 3) (A := 0) (W := width N) (zeroWeights N)
+      (by simp only [zeroWeights, List.length_replicate]) (by decide) (by decide)
+      hprime hgeo hmag le_rfl
+  let V := fun q => (zeroWeights N).getD q 0
+  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 hvalues (q : ℕ) : V q = 0 := by
+    change (List.replicate (3 * (N * N)) (0 : ℤ))[q]?.getD 0 = 0
+    exact List.getElem?_getD_replicate_default_eq _ _ _
+  have hN : D 2 ≤ N := (Nat.le_self_pow (by decide : 18 ≠ 0) (D 2)).trans hgeo
+  have hn : 0 < N := lt_of_lt_of_le (by decide : 0 < D 2) hN
+  have hk := ((mem_instanceIndices wAB idx).mp hidx).1
+  have hQ := RecordProduct.recordQueryCount_pos V (by decide : 3 ≠ 0)
+    (by decide : 1 ≤ D 2) hN idx hidx
+  have hcard := QuerySpec.card_residueClass wAB (by decide : 3 ≠ 0)
+    (fun q => (V q % (3 : ℤ)).toNat) (by intro pair; rfl) idx.1
+  have hpairs := (RecordProduct.output_query_coordinates V wAB (by decide)
+    (by intro u v; rfl) (by decide) hN hout idx.1 idx.2.1 hk).2
+  rw [hcard] at hpairs
+  obtain ⟨pair, hpair, -⟩ := hpairs 0 hQ
+  have hkzero : idx.2.2 = 0 := by
+    exact (Nat.add_eq_zero_iff.mp hord).2
+  let c : Fin N := ⟨0, hn⟩
+  have hc : c ∈ piece N (D 2) 1 idx.2.2 := by
+    rw [mem_piece, hkzero]
+    exact Nat.zero_div _
+  have hz : weightSum wAB wBC wAC pair.1 pair.2 c = 0 := by
+    simp only [weightSum, wAB, wBC, wAC, hvalues, zero_add]
+  have hfound : y.regs RecordWitness.Reg.found = 1 := yiff.mpr
+    ⟨pair, hpair.1, c, hc, hz⟩
+  have hfalse : falsePositiveCount wAB wBC wAC 3 = 0 := by
+    simp only [falsePositiveCount, IsFalsePositive, weightSum, wAB, wBC, wAC, hvalues,
+      zero_add, ne_eq, not_true_eq_false, false_and, Finset.filter_false, Finset.card_empty]
+  obtain ⟨u, v, c, hu, hv, hc, -⟩ := yw hfound
+  change S ≤ falsePositiveCount wAB wBC wAC 3 + y.regs RecordWitness.Reg.found at hS
+  refine ⟨y, t, S, hr, ?_, hfound, ys, ?_, u, v, c, hu, hv, hc⟩
+  · simpa only [hfound] using he
+  · simpa only [hfalse, hfound, zero_add] using hS
+
+example : ∃ y : Data 400, ∃ t S : ℕ,
+    Runs (width side) (RecordWitness.entryProgram.program RecordWitness.Reg.found)
+      (State.init (PreparationInput.input side (D 2) 1 3 (zeroWeights side)))
+      ⟨RecordWitness.entryProgram.size, y⟩ t ∧
+    Executes (width side) (RecordWitness.entryProgram.program RecordWitness.Reg.found)
+      (State.init (PreparationInput.input side (D 2) 1 3 (zeroWeights side))) 1 (t + 1) ∧
+    y.regs RecordWitness.Reg.found = 1 ∧ y.regs RecordWitness.Reg.scans = S ∧ S ≤ 1 ∧
+    ∃ u v c : Fin side, y.regs RecordWitness.Reg.witnessA = u.val ∧
+      y.regs RecordWitness.Reg.witnessB = v.val ∧ y.regs RecordWitness.Reg.witnessC = c.val :=
+  initialized_zero side le_rfl
+
+end ComplexityTests.WordRAMExactTriangleRecordWitness
diff --git a/ComplexityTests/WordRAMExactTriangleWitnessScan.lean b/ComplexityTests/WordRAMExactTriangleWitnessScan.lean
new file mode 100644
index 0000000000..9e9472e656
--- /dev/null
+++ b/ComplexityTests/WordRAMExactTriangleWitnessScan.lean
@@ -0,0 +1,88 @@
+/-
+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.WitnessScan.Exec
+import Mathlib.Tactic.IntervalCases
+import Mathlib.Tactic.NormNum
+
+/-!
+# Signed original-weight verifier executions
+
+These test the interval verifier on small original arrays; they do not assert the much larger
+thin-product geometry. The complete producer/product/recovery client is a separate test.
+-/
+
+set_option linter.hashCommand false
+
+namespace ComplexityTests.WordRAMExactTriangleWitnessScan
+
+open Cslib.WordRAM Cslib.Algorithms.WordRAM.ExactTriangle
+
+private def weights (last : ℤ) : List ℤ := [2, 5, 7, 8, -1, 3, 0, 0, 4, last, 0, 0]
+
+private def args (first length : ℕ) : WitnessScan.Args := ⟨1, 5, 9, 2, 0, 0, first, length⟩
+
+private def fixture (last : ℤ) (first length : ℕ) : Data 32 :=
+  ((Data.init ((weights last).map Signed.encode)).write 20 99)
+    |>.set WitnessScan.Reg.ab 1 |>.set WitnessScan.Reg.bc 5 |>.set WitnessScan.Reg.ac 9
+    |>.set WitnessScan.Reg.size 2 |>.set WitnessScan.Reg.a 0 |>.set WitnessScan.Reg.b 0
+    |>.set WitnessScan.Reg.first first |>.set WitnessScan.Reg.length length
+
+private def observe (last : ℤ) (first length : ℕ) : Option (ℕ × ℕ × ℕ × Bool) :=
+  (WitnessScan.program.eval 10 8 (fixture last first length)).map fun (y, t) =>
+    (y.regs WitnessScan.Reg.found, y.regs WitnessScan.Reg.witness, y.mem 20,
+      decide (t ≤ 42 * length + 17))
+
+-- c=0 fails (2-1+4=5), then the original signed weights at c=1 give 2+3-5=0.
+#guard observe (-5) 0 2 == some (1, 1, 99, true)
+
+-- A nonzero product candidate cannot turn 2+3+1 into an original zero sum.
+#guard observe 1 0 2 == some (0, 0, 99, true)
+
+-- An empty interval performs no candidate-vertex read and cannot report a witness.
+#guard observe (-5) 2 0 == some (0, 2, 99, true)
+
+-- Restricting the scan to c=0 excludes the later true witness.
+#guard observe (-5) 0 1 == some (0, 0, 99, true)
+
+private def AB (i j : ℕ) : ℤ := (weights (-5)).getD (i * 2 + j) 0
+private def BC (i j : ℕ) : ℤ := (weights (-5)).getD (4 + (i * 2 + j)) 0
+private def AC (i j : ℕ) : ℤ := (weights (-5)).getD (8 + (i * 2 + j)) 0
+
+/-- Closed kernel client: every runtime, address, signed-fit and input-array premise is
+discharged. The actual successful execution observes the unique original witness c=1. -/
+example : ∃ y, ExecWithin 10 WitnessScan.program (fixture (-5) 0 2) y 101 ∧
+    y.regs WitnessScan.Reg.found = 1 ∧ y.regs WitnessScan.Reg.witness = 1 ∧
+    y.mem = (fixture (-5) 0 2).mem := by
+  have hm : ∀ i < 2, ∀ j < 2,
+      (fixture (-5) 0 2).mem (1 + (i * 2 + j)) = Signed.encode (AB i j) ∧
+      (fixture (-5) 0 2).mem (5 + (i * 2 + j)) = Signed.encode (BC i j) ∧
+      (fixture (-5) 0 2).mem (9 + (i * 2 + j)) = Signed.encode (AC i j) := by
+    intro i hi j hj
+    interval_cases i <;> interval_cases j <;> decide
+  have hb : ∀ i < 2, ∀ j < 2,
+      (AB i j).natAbs ≤ 8 ∧ (BC i j).natAbs ≤ 8 ∧ (AC i j).natAbs ≤ 8 := by
+    intro i hi j hj
+    interval_cases i <;> interval_cases j <;> decide
+  obtain ⟨y, he, hy, hmem, hflag, hiff, hwit⟩ := WitnessScan.exec
+    (w := 8) (U := 8) (args 0 2) AB BC AC (fixture (-5) 0 2)
+    (by unfold WitnessScan.Args.InRegisters; decide)
+    (by decide) (by decide) (by decide) hm hb (by decide) (by decide)
+  have hf : y.regs WitnessScan.Reg.found = 1 := hiff.mpr ⟨1, by decide, by decide, by decide⟩
+  obtain ⟨hlo, hhi, hz⟩ := hwit hf
+  have hc : y.regs WitnessScan.Reg.witness = 1 := by
+    change 0 ≤ y.regs WitnessScan.Reg.witness at hlo
+    change y.regs WitnessScan.Reg.witness < 2 at hhi
+    have hzero : y.regs WitnessScan.Reg.witness ≠ 0 := by
+      intro h
+      rw [h] at hz
+      norm_num [AB, BC, AC, weights, args] at hz
+    omega
+  exact ⟨y, he, hf, hc, hmem⟩
+
+end ComplexityTests.WordRAMExactTriangleWitnessScan
diff --git a/ROADMAP.md b/ROADMAP.md
index e3f209eca6..1eb96901db 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -543,6 +543,14 @@ each statement against the numbered result. Organize modules by subject, not cha
   `34603008*(19m+1)*n²/D^(1/18)` at `D=4^m`, `L=19m`, `D^18≤n`.
   The outer instance loop, aggregate subcubic ET bound, backend/witness reconstruction and
   the full [#1394] ordinary-3SUM 1.9992 endpoint remain open.
+- **Per-record native witness recovery** ([#1639](https://github.com/cslib-community/complexitylib/issues/1639)):
+  actual initialized producer/product calls now feed real answer/query loads and original signed
+  weight verification. The fixed 400-register program returns original-coordinate witnesses and
+  decides zeros in the selected existing chunk/piece. Its actual scan counter satisfies
+  `S≤falsePositiveCount+returnedFlag`, so unsuccessful records have no successful-scan surplus.
+  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].
 - **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 7f5575c79e..f84aaa139e 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -404,6 +404,23 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   initialized prefixes have a positive logarithmic width threshold and polynomial words/support
   independent of the physical width. Outer parameter/prime selection and instance iteration,
   aggregate solving/witness reconstruction and the whole #1394 endpoint remain separate.
+  The original-weight consumer in
+  [#1639](https://github.com/cslib-community/complexitylib/issues/1639) composes actual producer,
+  product and verification code in 400 registers. It reads original interleaved pairs, computes
+  the piece interval with the native square-root kernel, and invokes the entire renamed
+  32-register signed verifier only while searching and on nonzero actual answers. The native
+  scan counter is at most existing finite false positives plus the returned 0/1 flag. Thus a
+  failed record has no additive successful-scan charge. Caller memory outside the original
+  product window and the complete producer bank are framed; widths and all-prefix words/support
+  are derived from original headers/weights at every sufficiently wide physical word size.
+  Source Light semantics and costs are not imported or simulated by assumption. The native
+  verifier returns its last zero, while finite `scanPiece` returns its first; failure and
+  original-weight soundness agree. The existing decoded queries now expose chunk membership,
+  nonrepetition and rank order, with an actual initialized client. The general raw writer bound
+  is placed at `WriteMatrices.entry_le_one`, and shared finite piece coordinates are in the
+  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.
   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