diff --git a/Complexity.lean b/Complexity.lean
index 7a59c84db8..353f64fa31 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -102,6 +102,9 @@ public import Complexity.Algorithms.WordRAM.Karger.FastCut
 public import Complexity.Algorithms.WordRAM.Karger.Graph
 public import Complexity.Algorithms.WordRAM.KargerMinCut
 public import Complexity.Algorithms.WordRAM.KargerStein
+public import Complexity.Algorithms.WordRAM.NatClog
+public import Complexity.Algorithms.WordRAM.NatLog
+public import Complexity.Algorithms.WordRAM.NatSqrt
 public import Complexity.Algorithms.WordRAM.PrefixSums.Dynamic
 public import Complexity.Algorithms.WordRAM.PrefixSums.Query
 public import Complexity.Algorithms.WordRAM.PrefixSums.Tree
@@ -134,8 +137,13 @@ public import Complexity.Algorithms.WordRAM.Stack.Controller
 public import Complexity.Algorithms.WordRAM.ThreeSum.Cell
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Collisions
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Count
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Residues
 public import Complexity.Algorithms.WordRAM.ThreeSum.Fill
+public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Loop
+public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Prepare
+public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Program
+public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Width
 public import Complexity.Algorithms.WordRAM.ThreeSum.Memory
 public import Complexity.Algorithms.WordRAM.ThreeSum.Weight
 public import Complexity.Algorithms.WordRAM.VanEmdeBoas.Call
@@ -1698,6 +1706,7 @@ public import Complexity.Computability.WordRAM.Randomized.Defs
 public import Complexity.Computability.WordRAM.Randomized.Expected
 public import Complexity.Computability.WordRAM.Randomized.LoopSegment
 public import Complexity.Computability.WordRAM.Randomized.Structured
+public import Complexity.Computability.WordRAM.RegisterFrame
 public import Complexity.Computability.WordRAM.Signed.Arithmetic
 public import Complexity.Computability.WordRAM.Signed.Comparison
 public import Complexity.Computability.WordRAM.Signed.Compile
diff --git a/Complexity/Algorithms/WordRAM/FusionTree/Node/Registers.lean b/Complexity/Algorithms/WordRAM/FusionTree/Node/Registers.lean
index f5903b8169..30b798fbaa 100644
--- a/Complexity/Algorithms/WordRAM/FusionTree/Node/Registers.lean
+++ b/Complexity/Algorithms/WordRAM/FusionTree/Node/Registers.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Algorithms.WordRAM.FusionTree.Parameters
 public import Complexity.Algorithms.WordRAM.FusionTree.ReadHeader
+public import Complexity.Computability.WordRAM.RegisterFrame
 
 /-!
 # Register banks for fusion-node queries
@@ -75,25 +76,12 @@ theorem bank_injective {k offset : ℕ} (hk : offset + k ≤ registers) :
   dsimp only [bank] at this
   omega
 
-/-- A renamed subroutine cannot write a register outside its embedding. This proof treats
-the subroutine structurally and does not expand its instruction graph. -/
-private theorem preserves_rename {k : ℕ} {f : Fin k → Fin registers} (c : Code .standard k)
-    (i : Fin registers) (hi : ∀ j, f j ≠ i) : (c.rename f).Preserves i := by
-  induction c with
-  | op o =>
-    cases o <;> simp only [Code.rename, Code.Preserves, Op.rename, Op.dest,
-      ne_eq, Option.some.injEq, reduceCtorEq, not_false_eq_true] <;> apply hi
-  | seq a b iha ihb => exact ⟨iha, ihb⟩
-  | branch cond pos neg ihp ihn => exact ⟨ihp, ihn⟩
-  | loop cond body ih => exact ih
-  | rand dst src => simpa only [Code.rename, Code.Preserves] using hi dst
-
 /-- In particular, a contiguous bank frames every physical register outside its interval. -/
 theorem preserves_bank {k offset : ℕ} (hk : offset + k ≤ registers)
     (c : Code .standard k) (i : Fin registers)
     (hi : i.val < offset ∨ offset + k ≤ i.val) :
     (c.rename (bank offset hk)).Preserves i := by
-  apply preserves_rename
+  apply Code.preserves_rename_of_forall_ne
   intro j he
   have := congrArg Fin.val he
   dsimp only [bank] at this
diff --git a/Complexity/Algorithms/WordRAM/NatClog.lean b/Complexity/Algorithms/WordRAM/NatClog.lean
new file mode 100644
index 0000000000..215117b054
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/NatClog.lean
@@ -0,0 +1,116 @@
+/-
+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.Computability.WordRAM.Notation
+public import Mathlib.Data.Nat.Log
+
+/-!
+# A charged native ceiling binary logarithm
+
+## Main definitions
+
+* `NatClog.program`: successive ceiling division by two.
+
+## Main results
+
+* `NatClog.exec`: the ceiling logarithm with a logarithmic charged instruction bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.NatClog
+
+open Cslib.WordRAM
+
+/-- Quotient, initially the input. -/
+abbrev arg : Fin 4 := 0
+/-- Ceiling logarithm output. -/
+abbrev result : Fin 4 := 1
+/-- Constant one. -/
+abbrev one : Fin 4 := 2
+/-- Constant two. -/
+abbrev two : Fin 4 := 3
+
+/-- Divide the quotient by two and increment the answer. -/
+def body : Code .standard 4 := ram[ arg ← arg + one; arg ← arg / two; result ← result + one ]
+
+/-- Fixed code for `Nat.clog 2`, including its value zero at input zero. -/
+def program : Code .standard 4 :=
+  .seq (ram[ result ← #0; one ← #1; two ← #2 ]) (.loop (.lt one arg) body)
+
+/-- Compute the ceiling binary logarithm in at most `5 ⌈log₂ n⌉ + 5` instructions.
+Memory is untouched and the input quotient is consumed. -/
+theorem exec {w : ℕ} (x : Data 4) (h2 : Fits w 2) (hn : Fits w (x.regs arg + 1))
+    (hout : Fits w (Nat.clog 2 (x.regs arg) + 1)) :
+    ∃ y, ExecWithin w program x y (5 * Nat.clog 2 (x.regs arg) + 5) ∧
+      y.regs result = Nat.clog 2 (x.regs arg) ∧ y.mem = x.mem ∧
+      y.regs one = 1 ∧ y.regs two = 2 := by
+  let I (y : Data 4) : Prop := y.regs one = 1 ∧ y.regs two = 2 ∧
+    y.regs arg ≤ x.regs arg ∧
+    y.regs result + Nat.clog 2 (y.regs arg) = Nat.clog 2 (x.regs arg) ∧ y.mem = x.mem
+  have hbody (y : Data 4) (hy : I y) (hc : (Cond.lt one arg).Holds y) :
+      ∃ z, ExecWithin w body y z 3 ∧ I z ∧
+        Nat.clog 2 (z.regs arg) < Nat.clog 2 (y.regs arg) := by
+    obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+    have hgt : 1 < y.regs arg := by simpa only [Cond.holds_lt, ho] using hc
+    have hpos : 0 < Nat.clog 2 (y.regs arg) := Nat.clog_pos (by decide) (by omega)
+    have hadd : Fits w (y.regs arg + 1) := hn.of_le (by omega)
+    have hdiv : Fits w ((y.regs arg + 1) / 2) :=
+      hn.of_le ((Nat.div_le_self _ _).trans (by omega))
+    have hinc : Fits w (y.regs result + 1) := hout.of_le (by omega)
+    refine ⟨?z, ?run, ?inv, ?decrease⟩
+    case run => ram_eval [body, ho, ht, hadd, hdiv, hinc, arg, result, one, two, Fin.mk.injEq]
+    case inv =>
+      refine ⟨?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [Function.update_apply] using ho
+      · simpa +decide [Function.update_apply] using ht
+      · simpa +decide [Function.update_apply] using
+          (show (y.regs arg + 1) / 2 ≤ x.regs arg from by omega)
+      · change y.regs result + 1 + Nat.clog 2 ((y.regs arg + 1) / 2) = Nat.clog 2 (x.regs arg)
+        have h := Nat.clog_of_two_le (b := 2) (by decide) (by omega : 2 ≤ y.regs arg)
+        simp only [show y.regs arg + 2 - 1 = y.regs arg + 1 by omega] at h
+        omega
+      · exact hm
+    case decrease =>
+      change Nat.clog 2 ((y.regs arg + 1) / 2) < Nat.clog 2 (y.regs arg)
+      have h := Nat.clog_of_two_le (b := 2) (by decide) (by omega : 2 ≤ y.regs arg)
+      simp only [show y.regs arg + 2 - 1 = y.regs arg + 1 by omega] at h
+      omega
+  let x₀ := ((x.set result 0).set one 1).set two 2
+  have hx₀ : I x₀ := by simp +decide [I, x₀, arg, result, one, two]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => Nat.clog 2 (y.regs arg)) hbody hx₀
+  obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+  have hzero : Nat.clog 2 (y.regs arg) = 0 := by
+    have hle : y.regs arg ≤ 1 := by simpa only [Cond.holds_lt, ho, not_lt] using hc
+    exact Nat.clog_of_right_le_one hle 2
+  refine ⟨y, ?_, by omega, hm, ho, ht⟩
+  have h1 : Fits w 1 := h2.of_le (by decide)
+  have hinit : ExecWithin (B := .standard) w (ram[ result ← #0; one ← #1; two ← #2 ]) x x₀ 3 := by
+    ram_eval [x₀, h1, h2]
+  convert hinit.seq he using 1
+  · rfl
+  · simp +decide only [x₀, Data.set_regs, Function.update_apply, arg, result, one, two,
+      ↓reduceIte]
+    omega
+
+/-- Run the routine on any injectively chosen registers. -/
+theorem exec_rename {r w : ℕ} (f : Fin 4 → Fin r) (hf : f.Injective) (x : Data r)
+    (h2 : Fits w 2) (hn : Fits w (x.regs (f arg) + 1))
+    (hout : Fits w (Nat.clog 2 (x.regs (f arg)) + 1)) :
+    ∃ y, ExecWithin w (program.rename f) x y (5 * Nat.clog 2 (x.regs (f arg)) + 5) ∧
+      y.regs (f result) = Nat.clog 2 (x.regs (f arg)) ∧ y.mem = x.mem ∧
+      y.regs (f one) = 1 ∧ y.regs (f two) = 2 := by
+  obtain ⟨a, ha, hr, hm, ho, ht⟩ := exec (x.comap f) h2 hn hout
+  refine ⟨a.extend f x, ha.rename hf, ?_, hm, ?_, ?_⟩
+  · exact (hf.extend_apply _ _ result).trans hr
+  · exact (hf.extend_apply _ _ one).trans ho
+  · exact (hf.extend_apply _ _ two).trans ht
+
+end Cslib.Algorithms.WordRAM.NatClog
diff --git a/Complexity/Algorithms/WordRAM/NatLog.lean b/Complexity/Algorithms/WordRAM/NatLog.lean
new file mode 100644
index 0000000000..eb229076e6
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/NatLog.lean
@@ -0,0 +1,111 @@
+/-
+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.Computability.WordRAM.Notation
+public import Mathlib.Data.Nat.Log
+
+/-!
+# A charged native binary logarithm
+
+## Main definitions
+
+* `NatLog.program`: successive division by two.
+
+## Main results
+
+* `NatLog.exec`: the floor logarithm with a logarithmic charged instruction bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.NatLog
+
+open Cslib.WordRAM
+
+/-- Quotient, initially the input. -/
+abbrev arg : Fin 4 := 0
+/-- Floor logarithm output. -/
+abbrev result : Fin 4 := 1
+/-- Constant one. -/
+abbrev one : Fin 4 := 2
+/-- Constant two. -/
+abbrev two : Fin 4 := 3
+
+/-- Divide the quotient by two and increment the answer. -/
+def body : Code .standard 4 := ram[ arg ← arg / two; result ← result + one ]
+
+/-- Fixed code for `Nat.log 2`, including its value zero at input zero. -/
+def program : Code .standard 4 :=
+  .seq (ram[ result ← #0; one ← #1; two ← #2 ]) (.loop (.lt one arg) body)
+
+/-- Compute the floor binary logarithm in at most `4 log₂ n + 5` instructions.
+Memory is untouched and the input quotient is consumed. -/
+theorem exec {w : ℕ} (x : Data 4) (h2 : Fits w 2) (hn : Fits w (x.regs arg))
+    (hout : Fits w (Nat.log 2 (x.regs arg) + 1)) :
+    ∃ y, ExecWithin w program x y (4 * Nat.log 2 (x.regs arg) + 5) ∧
+      y.regs result = Nat.log 2 (x.regs arg) ∧ y.mem = x.mem ∧
+      y.regs one = 1 ∧ y.regs two = 2 := by
+  let I (y : Data 4) : Prop := y.regs one = 1 ∧ y.regs two = 2 ∧
+    y.regs arg ≤ x.regs arg ∧
+    y.regs result + Nat.log 2 (y.regs arg) = Nat.log 2 (x.regs arg) ∧ y.mem = x.mem
+  have hbody (y : Data 4) (hy : I y) (hc : (Cond.lt one arg).Holds y) :
+      ∃ z, ExecWithin w body y z 2 ∧ I z ∧
+        Nat.log 2 (z.regs arg) < Nat.log 2 (y.regs arg) := by
+    obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+    have hgt : 1 < y.regs arg := by simpa only [Cond.holds_lt, ho] using hc
+    have hpos : 0 < Nat.log 2 (y.regs arg) := Nat.log_pos (by decide) (by omega)
+    have hdiv : Fits w (y.regs arg / 2) := hn.of_le ((Nat.div_le_self _ _).trans harg)
+    have hinc : Fits w (y.regs result + 1) := hout.of_le (by omega)
+    refine ⟨?z, ?run, ?inv, ?decrease⟩
+    case run => ram_eval [body, ho, ht, hdiv, hinc, arg, result, one, two, Fin.mk.injEq]
+    case inv =>
+      refine ⟨?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [Function.update_apply] using ho
+      · simpa +decide [Function.update_apply] using ht
+      · simpa +decide [Function.update_apply] using (Nat.div_le_self (y.regs arg) 2).trans harg
+      · change y.regs result + 1 + Nat.log 2 (y.regs arg / 2) = Nat.log 2 (x.regs arg)
+        rw [Nat.log_div_base]
+        omega
+      · exact hm
+    case decrease =>
+      change Nat.log 2 (y.regs arg / 2) < Nat.log 2 (y.regs arg)
+      rw [Nat.log_div_base]
+      omega
+  let x₀ := ((x.set result 0).set one 1).set two 2
+  have hx₀ : I x₀ := by simp +decide [I, x₀, arg, result, one, two]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => Nat.log 2 (y.regs arg)) hbody hx₀
+  obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+  have hzero : Nat.log 2 (y.regs arg) = 0 := by
+    have hle : y.regs arg ≤ 1 := by simpa only [Cond.holds_lt, ho, not_lt] using hc
+    exact Nat.log_eq_zero_iff.mpr (Or.inl (by omega))
+  refine ⟨y, ?_, by omega, hm, ho, ht⟩
+  have h1 : Fits w 1 := h2.of_le (by decide)
+  have hinit : ExecWithin (B := .standard) w (ram[ result ← #0; one ← #1; two ← #2 ]) x x₀ 3 := by
+    ram_eval [x₀, h1, h2]
+  convert hinit.seq he using 1
+  · rfl
+  · simp +decide only [x₀, Data.set_regs, Function.update_apply, arg, result, one, two,
+      ↓reduceIte]
+    omega
+
+/-- Run the routine on any injectively chosen registers. -/
+theorem exec_rename {r w : ℕ} (f : Fin 4 → Fin r) (hf : f.Injective) (x : Data r)
+    (h2 : Fits w 2) (hn : Fits w (x.regs (f arg)))
+    (hout : Fits w (Nat.log 2 (x.regs (f arg)) + 1)) :
+    ∃ y, ExecWithin w (program.rename f) x y (4 * Nat.log 2 (x.regs (f arg)) + 5) ∧
+      y.regs (f result) = Nat.log 2 (x.regs (f arg)) ∧ y.mem = x.mem ∧
+      y.regs (f one) = 1 ∧ y.regs (f two) = 2 := by
+  obtain ⟨a, ha, hr, hm, ho, ht⟩ := exec (x.comap f) h2 hn hout
+  refine ⟨a.extend f x, ha.rename hf, ?_, hm, ?_, ?_⟩
+  · exact (hf.extend_apply _ _ result).trans hr
+  · exact (hf.extend_apply _ _ one).trans ho
+  · exact (hf.extend_apply _ _ two).trans ht
+
+end Cslib.Algorithms.WordRAM.NatLog
diff --git a/Complexity/Algorithms/WordRAM/NatSqrt.lean b/Complexity/Algorithms/WordRAM/NatSqrt.lean
new file mode 100644
index 0000000000..98b3ad67ed
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/NatSqrt.lean
@@ -0,0 +1,129 @@
+/-
+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.Computability.WordRAM.Notation
+public import Mathlib.Data.Nat.Sqrt
+import Mathlib.Tactic.Linarith
+
+/-!
+# A charged native integer square root
+
+## Main definitions
+
+* `NatSqrt.program`: successive squares.
+
+## Main results
+
+* `NatSqrt.exec`: integer square root in a square-root number of native instructions.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.NatSqrt
+
+open Cslib.WordRAM
+
+/-- Input integer, preserved. -/
+abbrev arg : Fin 6 := 0
+/-- Current root and output. -/
+abbrev root : Fin 6 := 1
+/-- Successor of the current root. -/
+abbrev next : Fin 6 := 2
+/-- Square of the successor. -/
+abbrev square : Fin 6 := 3
+/-- Constant one. -/
+abbrev one : Fin 6 := 4
+/-- Input plus one. -/
+abbrev bound : Fin 6 := 5
+
+/-- Advance the root and compute the next square. -/
+def body : Code .standard 6 := ram[
+  root ← next; next ← next + one; square ← next * next ]
+
+/-- A fixed program for the integer square root, with all square computations charged. -/
+def program : Code .standard 6 :=
+  .seq (ram[ root ← #0; next ← #1; square ← #1; one ← #1; bound ← arg + one ])
+    (.loop (.lt square bound) body)
+
+/-- Compute `Nat.sqrt n` in at most `5 sqrt(n) + 7` instructions, preserving input and memory.
+The linear bound `4n + 4` covers the final unsuccessful square as well as all counters. -/
+theorem exec {w : ℕ} (x : Data 6) (hfit : Fits w (4 * x.regs arg + 4)) :
+    ∃ y, ExecWithin w program x y (5 * Nat.sqrt (x.regs arg) + 7) ∧
+      y.regs root = Nat.sqrt (x.regs arg) ∧ y.regs arg = x.regs arg ∧ y.mem = x.mem ∧
+      y.regs one = 1 := by
+  let n := x.regs arg
+  let I (y : Data 6) : Prop := y.regs arg = n ∧ y.regs one = 1 ∧
+    y.regs bound = n + 1 ∧ y.regs next = y.regs root + 1 ∧
+    y.regs square = y.regs next * y.regs next ∧
+    y.regs root ≤ Nat.sqrt n ∧ y.mem = x.mem
+  have hbody (y : Data 6) (hy : I y) (hc : (Cond.lt square bound).Holds y) :
+      ∃ z, ExecWithin w body y z 3 ∧ I z ∧
+        Nat.sqrt n - z.regs root < Nat.sqrt n - y.regs root := by
+    obtain ⟨ha, ho, hb, hn, hsq, hr, hm⟩ := hy
+    have hsmall : y.regs next * y.regs next ≤ n := by
+      simp only [Cond.holds_lt, hsq, hb] at hc
+      omega
+    have hnext : y.regs next ≤ Nat.sqrt n := Nat.le_sqrt.mpr hsmall
+    have hsl := Nat.sqrt_le n
+    have hsle := Nat.sqrt_le_self n
+    have hstep : Fits w (y.regs next + 1) := hfit.of_le (by dsimp [n] at *; omega)
+    have hsquare : Fits w ((y.regs next + 1) * (y.regs next + 1)) := hfit.of_le (by
+      change (y.regs next + 1) * (y.regs next + 1) ≤ 4 * n + 4
+      have hnn : y.regs next ≤ n := hnext.trans hsle
+      nlinarith)
+    refine ⟨?z, ?run, ?inv, ?decrease⟩
+    case run => ram_eval [body, ho, hstep, hsquare, root, next, square, one, Fin.mk.injEq]
+    case inv =>
+      refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [Function.update_apply] using ha
+      · simpa +decide [Function.update_apply] using ho
+      · simpa +decide [Function.update_apply] using hb
+      · rfl
+      · rfl
+      · exact hnext
+      · exact hm
+    case decrease =>
+      change Nat.sqrt n - y.regs next < Nat.sqrt n - y.regs root
+      omega
+  let x₀ := ((((x.set root 0).set next 1).set square 1).set one 1).set bound (n + 1)
+  have hx₀ : I x₀ := by simp +decide [I, x₀, n, root, next, square, one, bound, arg]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => Nat.sqrt n - y.regs root) hbody hx₀
+  obtain ⟨ha, ho, hb, hn, hsq, hr, hm⟩ := hy
+  have hlarge : n < (y.regs root + 1) * (y.regs root + 1) := by
+    simp only [Cond.holds_lt, hsq, hn, hb] at hc
+    omega
+  have hout : y.regs root = Nat.sqrt n := by
+    have h := Nat.sqrt_lt.mpr hlarge
+    omega
+  have h1 : Fits w 1 := hfit.of_le (by omega)
+  have hbfit : Fits w (x.regs arg + 1) := hfit.of_le (by omega)
+  have hinit : ExecWithin (B := .standard) w
+      (ram[ root ← #0; next ← #1; square ← #1; one ← #1; bound ← arg + one ]) x x₀ 5 := by
+    ram_eval [x₀, n, h1, hbfit, root, next, square, one, bound, arg, Fin.mk.injEq]
+  refine ⟨y, ?_, hout, ha, hm, ho⟩
+  convert hinit.seq he using 1
+  · rfl
+  · simp +decide only [x₀, Data.set_regs, Function.update_apply, root, next, square, one,
+      bound, arg, n, ↓reduceIte, Nat.sub_zero]
+    omega
+
+/-- Run successive squares on any injectively chosen registers. -/
+theorem exec_rename {r w : ℕ} (f : Fin 6 → Fin r) (hf : f.Injective) (x : Data r)
+    (hfit : Fits w (4 * x.regs (f arg) + 4)) :
+    ∃ y, ExecWithin w (program.rename f) x y (5 * Nat.sqrt (x.regs (f arg)) + 7) ∧
+      y.regs (f root) = Nat.sqrt (x.regs (f arg)) ∧
+      y.regs (f arg) = x.regs (f arg) ∧ y.mem = x.mem ∧ y.regs (f one) = 1 := by
+  obtain ⟨a, ha, hr, hn, hm, ho⟩ := exec (x.comap f) hfit
+  refine ⟨a.extend f x, ha.rename hf, ?_, ?_, hm, ?_⟩
+  · exact (hf.extend_apply _ _ root).trans hr
+  · exact (hf.extend_apply _ _ arg).trans hn
+  · exact (hf.extend_apply _ _ one).trans ho
+
+end Cslib.Algorithms.WordRAM.NatSqrt
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Parameters.lean b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Parameters.lean
new file mode 100644
index 0000000000..26812d6412
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Parameters.lean
@@ -0,0 +1,892 @@
+/-
+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.ThreeSum.ChanHe.Defs
+public import Complexity.Algorithms.WordRAM.NatLog
+public import Complexity.Algorithms.WordRAM.NatClog
+public import Complexity.Algorithms.WordRAM.NatSqrt
+public import Complexity.Computability.WordRAM.Compile
+public import Complexity.Computability.WordRAM.Signed.Encoding
+import Mathlib.Tactic.Linarith
+
+/-!
+# Native parameters for Chan–He preprocessing
+
+Original native programs and proofs. The parameter meanings are the existing finite mathematical
+Chan–He definitions, with magnitude bound `2U` after the distinct-position frontend.
+All loops and arithmetic are instructions; the program is fixed for each exponent `κ`.
+
+## Main definitions
+
+* `Parameters.program`: read the input header and compute the exact parameters.
+* `Parameters.Output`: identify the unsigned output registers.
+
+## Main results
+
+* `Parameters.runs_input`: native execution from signed-encoded input with derived fits.
+
+## References
+
+* [T. M. Chan and Q. He, *Reducing 3SUM to Convolution-3SUM*][ChanHe2020]
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
+
+open Cslib.WordRAM
+
+namespace Math
+open Cslib.Algorithms.ThreeSum
+
+/-- A bound covering arithmetic, unsuccessful loop tests, and all output words. -/
+def budget (n U : ℕ) : ℕ := 8 * (ChanHe.mPar n (2 * U) + 1) ^ 2 + 8 * U + 4 * n + 64
+
+private theorem want_le (n U : ℕ) : ChanHe.wPar n (2 * U) + 1 ≤ ChanHe.mPar n (2 * U) :=
+  Nat.le_mul_of_pos_right _ (by omega)
+
+private theorem digits_le (n U : ℕ) : 5 * labelBits (2 * U) ≤ ChanHe.wPar n (2 * U) :=
+  Nat.le_mul_of_pos_right _ (Nat.succ_pos _)
+
+private theorem factor_le (n U : ℕ) :
+    2 * Nat.log 2 (ChanHe.wPar n (2 * U) + 1) + 4 ≤ ChanHe.mPar n (2 * U) :=
+  Nat.le_mul_of_pos_left _ (Nat.succ_pos _)
+
+private theorem height_le (n : ℕ) : ChanHe.height n ≤ Nat.log 2 n + 2 :=
+  Nat.clog_le_of_le_pow Nat.lt_two_pow_self.le
+
+end Math
+
+/-- Unsigned input length. -/
+abbrev len : Fin 24 := 0
+/-- Original magnitude bound U. -/
+abbrev magnitude : Fin 24 := 1
+/-- Label bits for magnitude bound 2U. -/
+abbrev digits : Fin 24 := 2
+/-- Recursion height. -/
+abbrev height : Fin 24 := 3
+/-- Recursion fuel. -/
+abbrev fuel : Fin 24 := 4
+/-- Number of desired primes. -/
+abbrev want : Fin 24 := 5
+/-- Upper bound on candidate primes. -/
+abbrev primeBound : Fin 24 := 6
+/-- Common packed convolution length, 8m². -/
+abbrev packedLen : Fin 24 := 7
+/-- Magnitude of the padding for the doubled frontend bound, 4U+1. -/
+abbrev padding : Fin 24 := 8
+/-- Constant one. -/
+abbrev one : Fin 24 := 9
+/-- Constant two. -/
+abbrev two : Fin 24 := 10
+/-- Constant three. -/
+abbrev three : Fin 24 := 11
+/-- Constant four. -/
+abbrev four : Fin 24 := 12
+/-- Constant five. -/
+abbrev five : Fin 24 := 13
+/-- Constant eight. -/
+abbrev eight : Fin 24 := 14
+/-- Input length plus two. -/
+abbrev base : Fin 24 := 15
+/-- Consumed logarithm argument. -/
+abbrev quotient : Fin 24 := 16
+/-- Floor logarithm of input length. -/
+abbrev logLen : Fin 24 := 17
+/-- Integer square root of input length. -/
+abbrev root : Fin 24 := 18
+/-- Number of desired primes plus one. -/
+abbrev wantSucc : Fin 24 := 19
+/-- Arithmetic scratch. -/
+abbrev temp : Fin 24 := 20
+/-- Successor square-root counter. -/
+abbrev nextRoot : Fin 24 := 21
+/-- Square of that counter. -/
+abbrev square : Fin 24 := 22
+/-- Square-root test bound. -/
+abbrev rootBound : Fin 24 := 23
+
+/-- Exact mathematical outputs; every output is an ordinary unsigned word. -/
+structure Output (n U : ℕ) (x : Data 24) : Prop where
+  len : x.regs len = n
+  magnitude : x.regs magnitude = U
+  digits : x.regs digits = Cslib.Algorithms.ThreeSum.labelBits (2 * U)
+  height : x.regs height = Cslib.Algorithms.ThreeSum.ChanHe.height n
+  fuel : x.regs fuel = Cslib.Algorithms.ThreeSum.ChanHe.fuel n
+  want : x.regs want = Cslib.Algorithms.ThreeSum.ChanHe.wPar n (2 * U)
+  primeBound : x.regs primeBound = Cslib.Algorithms.ThreeSum.ChanHe.mPar n (2 * U)
+  packedLen : x.regs packedLen = 8 * Cslib.Algorithms.ThreeSum.ChanHe.mPar n (2 * U) ^ 2
+  padding : x.regs padding = 4 * U + 1
+
+/-- One header load, constants, and the polynomial base. -/
+def setup : Code .standard 24 := ram[
+  quotient ← #0; len ← *quotient; one ← #1; two ← #2; three ← #3;
+  four ← #4; five ← #5; eight ← #8; base ← len + two ]
+
+/-- Unroll only the fixed exponent, never the input length or word width. -/
+def power : ℕ → Code .standard 24
+  | 0 => ram[ magnitude ← #1 ]
+  | κ + 1 => .seq (power κ) (ram[ magnitude ← magnitude * base ])
+
+/-- Register selection for a floor/ceiling logarithm with output `dst`. -/
+def logRegisters (dst : Fin 24) : Fin 4 → Fin 24 := ![quotient, dst, one, two]
+
+/-- Register selection for successive squares. -/
+def sqrtRegisters : Fin 6 → Fin 24 := ![len, root, nextRoot, square, one, rootBound]
+
+private theorem sqrt_injective : sqrtRegisters.Injective := by decide
+
+/-- The instruction sequence after the power computation. -/
+def calculate : Code .standard 24 :=
+  .seq (ram[ quotient ← four * magnitude; padding ← quotient + one ])
+    (.seq (NatLog.program.rename (logRegisters digits))
+    (.seq (ram[ digits ← digits + one ])
+    (.seq (NatSqrt.program.rename sqrtRegisters)
+    (.seq (ram[ temp ← root + one; want ← five * digits; want ← want * temp;
+      wantSucc ← want + one; quotient ← wantSucc ])
+    (.seq (NatLog.program.rename (logRegisters temp))
+    (.seq (ram[ temp ← two * temp; temp ← temp + four; primeBound ← wantSucc * temp ])
+    (.seq (ram[ quotient ← len ])
+    (.seq (NatLog.program.rename (logRegisters logLen))
+    (.seq (ram[ quotient ← logLen + two ])
+    (.seq (NatClog.program.rename (logRegisters height))
+    (ram[ fuel ← three * height; fuel ← fuel - two; packedLen ← primeBound * primeBound;
+      packedLen ← eight * packedLen ])))))))))))
+
+/-- Fixed 24-register native code for each fixed polynomial magnitude exponent. -/
+def program (κ : ℕ) : Code .standard 24 := .seq setup (.seq (power κ) calculate)
+
+private theorem exec_power {w : ℕ} (κ : ℕ) (x : Data 24) (hb : 1 ≤ x.regs base)
+    (hfit : Fits w (x.regs base ^ κ)) :
+    ExecWithin w (power κ) x (x.set magnitude (x.regs base ^ κ)) (κ + 1) := by
+  induction κ with
+  | zero => simpa only [power, pow_zero] using ExecWithin.const hfit
+  | succ κ ih =>
+    have hprev : Fits w (x.regs base ^ κ) :=
+      hfit.of_le (Nat.pow_le_pow_right hb (by omega))
+    have he := ih hprev
+    have hm : ExecWithin w (ram[ magnitude ← magnitude * base ])
+        (x.set magnitude (x.regs base ^ κ))
+        (x.set magnitude (x.regs base ^ (κ + 1))) 1 := by
+      have hp : Fits w (x.regs base ^ κ * x.regs base) := by
+        simpa only [pow_succ] using hfit
+      apply ExecWithin.of_eval (fuel := 0) (n := 1) ?_ (by decide)
+      simp +decide [Code.eval, Op.eval_bin, Data.put,
+        BinOp.eval, hp, magnitude, base, pow_succ, Data.set, Function.update_idem]
+    exact (he.seq hm).mono (by omega)
+
+/-- An explicit charged bound, including all header reads, copies and setup. Halt adds one. -/
+def time (κ n U : ℕ) : ℕ := κ + 64 + 5 * Nat.sqrt n + 4 * Nat.log 2 (4 * U) +
+  4 * Nat.log 2 (Cslib.Algorithms.ThreeSum.ChanHe.wPar n (2 * U) + 1) +
+  4 * Nat.log 2 n + 5 * Cslib.Algorithms.ThreeSum.ChanHe.height n
+
+private theorem time_zero (n U : ℕ) : time 0 n U - 20 = 44 + 5 * Nat.sqrt n +
+    4 * Nat.log 2 (4 * U) +
+    4 * Nat.log 2 (Cslib.Algorithms.ThreeSum.ChanHe.wPar n (2 * U) + 1) +
+    4 * Nat.log 2 n + 5 * Cslib.Algorithms.ThreeSum.ChanHe.height n := by
+  dsimp [time]
+  omega
+
+set_option maxHeartbeats 300000 in
+-- Measured 256376 heartbeats for the twelve native segments and explicit register frames.
+private theorem exec_calculate {w n U : ℕ} (x : Data 24)
+    (hlen : x.regs len = n) (hU : x.regs magnitude = U)
+    (h1 : x.regs one = 1) (h2 : x.regs two = 2) (h3 : x.regs three = 3)
+    (h4 : x.regs four = 4) (h5 : x.regs five = 5) (h8 : x.regs eight = 8)
+    (hfit : Fits w (Math.budget n U)) :
+    ∃ y, ExecWithin w calculate x y (time 0 n U - 20) ∧ Output n U y ∧ y.mem = x.mem := by
+  let Λ := Cslib.Algorithms.ThreeSum.labelBits (2 * U)
+  let h := Cslib.Algorithms.ThreeSum.ChanHe.height n
+  let wp := Cslib.Algorithms.ThreeSum.ChanHe.wPar n (2 * U)
+  let m := Cslib.Algorithms.ThreeSum.ChanHe.mPar n (2 * U)
+  have eΛ : Λ = Nat.log 2 (4 * U) + 1 := by
+    dsimp [Λ, Cslib.Algorithms.ThreeSum.labelBits]
+    congr 2
+    omega
+  have ew : wp = 5 * Λ * (Nat.sqrt n + 1) := rfl
+  have em : m = (wp + 1) * (2 * Nat.log 2 (wp + 1) + 4) := rfl
+  have eh : Cslib.Algorithms.ThreeSum.ChanHe.fuel n = 3 * h - 2 := rfl
+  have hd : 5 * Λ ≤ wp := Math.digits_le n U
+  have hw : wp + 1 ≤ m := Math.want_le n U
+  have hf : 2 * Nat.log 2 (wp + 1) + 4 ≤ m := Math.factor_le n U
+  have hh : h ≤ Nat.log 2 n + 2 := Math.height_le n
+  have hl := Nat.log_le_self 2 n
+  have hroot := Nat.sqrt_le_self n
+  have hml : Fits w m := hfit.of_le (by dsimp [Math.budget]; nlinarith)
+  have fitm (v : ℕ) (hv : v ≤ m) : Fits w v := hml.of_le hv
+  have fitu (v : ℕ) (hv : v ≤ 8 * U + 64) : Fits w v :=
+    hfit.of_le (by dsimp [Math.budget]; omega)
+  have fitn (v : ℕ) (hv : v ≤ 4 * n + 64) : Fits w v :=
+    hfit.of_le (by dsimp [Math.budget]; omega)
+  have f1 : Fits w 1 := fitu _ (by omega)
+  have f2 : Fits w 2 := fitu _ (by omega)
+  have f4U : Fits w (4 * U) := fitu _ (by omega)
+  have fpad : Fits w (4 * U + 1) := fitu _ (by omega)
+  have fΛ : Fits w Λ := fitm _ (by omega)
+  have flogU : Fits w (Nat.log 2 (4 * U) + 1) :=
+    fitu _ (by have := Nat.log_le_self 2 (4 * U); omega)
+  have fsqrt : Fits w (4 * n + 4) := fitn _ (by omega)
+  have fr : Fits w (Nat.sqrt n + 1) := fitn _ (by omega)
+  have f5Λ : Fits w (5 * Λ) := fitm _ (by omega)
+  have fwp : Fits w wp := fitm _ (by omega)
+  have fwps : Fits w (wp + 1) := fitm _ hw
+  have flogwp : Fits w (Nat.log 2 (wp + 1) + 1) := fitm _ (by omega)
+  have f2log : Fits w (2 * Nat.log 2 (wp + 1)) := fitm _ (by omega)
+  have ff : Fits w (2 * Nat.log 2 (wp + 1) + 4) := fitm _ hf
+  have fn : Fits w n := fitn _ (by omega)
+  have flogn : Fits w (Nat.log 2 n + 1) := fitn _ (by omega)
+  have flog2 : Fits w (Nat.log 2 n + 2) := fitn _ (by omega)
+  have flog3 : Fits w (Nat.log 2 n + 2 + 1) := fitn _ (by omega)
+  have fh : Fits w (h + 1) := fitn _ (by omega)
+  have f3h : Fits w (3 * h) := fitn _ (by omega)
+  have ffuel : Fits w (Cslib.Algorithms.ThreeSum.ChanHe.fuel n) :=
+    fitn _ (by dsimp [Cslib.Algorithms.ThreeSum.ChanHe.fuel]; omega)
+  have fm2 : Fits w (m * m) := hfit.of_le (by dsimp [Math.budget]; nlinarith)
+  have fN : Fits w (8 * m ^ 2) := hfit.of_le (by dsimp [Math.budget]; nlinarith)
+  have fNm : Fits w (8 * (m * m)) := by simpa only [pow_two] using fN
+  let a := ((x.set quotient (4 * U)).set padding (4 * U + 1))
+  have ea : ExecWithin w (ram[ quotient ← four * magnitude; padding ← quotient + one ]) x a 2 := by
+    ram_eval [a, h4, hU, h1, f4U, fpad, four, magnitude, one, quotient, padding,
+      Fin.mk.injEq]
+  have a_len : a.regs len = n := by
+    simpa +decide [a, quotient, padding, len] using hlen
+  have a_magnitude : a.regs magnitude = U := by
+    simpa +decide [a, quotient, padding, magnitude] using hU
+  have a_one : a.regs one = 1 := by
+    simpa +decide [a, quotient, padding, one] using h1
+  have a_two : a.regs two = 2 := by
+    simpa +decide [a, quotient, padding, two] using h2
+  have a_three : a.regs three = 3 := by
+    simpa +decide [a, quotient, padding, three] using h3
+  have a_four : a.regs four = 4 := by
+    simpa +decide [a, quotient, padding, four] using h4
+  have a_five : a.regs five = 5 := by
+    simpa +decide [a, quotient, padding, five] using h5
+  have a_eight : a.regs eight = 8 := by
+    simpa +decide [a, quotient, padding, eight] using h8
+  have a_quotient : a.regs quotient = 4 * U := by
+    simp +decide [a, quotient, padding]
+  have a_padding : a.regs padding = 4 * U + 1 := by
+    simp +decide [a, quotient, padding]
+  have a_mem : a.mem = x.mem := rfl
+  obtain ⟨b, eb, b_digits, b_mem, b_one, b_two⟩ :=
+    NatLog.exec_rename (logRegisters digits) (by decide) a f2
+      (by simpa only [logRegisters, NatLog.arg, Matrix.cons_val_zero, a_quotient] using f4U)
+      (by simpa only [logRegisters, NatLog.arg, Matrix.cons_val_zero, a_quotient, h] using flogU)
+  simp only [logRegisters, NatLog.arg, NatLog.result, NatLog.one, NatLog.two,
+    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val,
+      a_quotient] at eb b_digits b_one b_two
+  have b_len : b.regs len = n := (eb.regs_eq (by decide)).trans a_len
+  have b_magnitude : b.regs magnitude = U := (eb.regs_eq (by decide)).trans a_magnitude
+  have b_three : b.regs three = 3 := (eb.regs_eq (by decide)).trans a_three
+  have b_four : b.regs four = 4 := (eb.regs_eq (by decide)).trans a_four
+  have b_five : b.regs five = 5 := (eb.regs_eq (by decide)).trans a_five
+  have b_eight : b.regs eight = 8 := (eb.regs_eq (by decide)).trans a_eight
+  have b_padding : b.regs padding = 4 * U + 1 := (eb.regs_eq (by decide)).trans a_padding
+  have b_memory : b.mem = x.mem := b_mem.trans a_mem
+  let c := (b.set digits (Λ))
+  have ec : ExecWithin w (ram[ digits ← digits + one ]) b c 1 := by
+    ram_eval [c, b_digits, b_one, ← eΛ, fΛ, digits, one, Fin.mk.injEq]
+  have c_len : c.regs len = n := by
+    simpa +decide [c, digits, len] using b_len
+  have c_magnitude : c.regs magnitude = U := by
+    simpa +decide [c, digits, magnitude] using b_magnitude
+  have c_three : c.regs three = 3 := by
+    simpa +decide [c, digits, three] using b_three
+  have c_four : c.regs four = 4 := by
+    simpa +decide [c, digits, four] using b_four
+  have c_five : c.regs five = 5 := by
+    simpa +decide [c, digits, five] using b_five
+  have c_eight : c.regs eight = 8 := by
+    simpa +decide [c, digits, eight] using b_eight
+  have c_padding : c.regs padding = 4 * U + 1 := by
+    simpa +decide [c, digits, padding] using b_padding
+  have c_digits : c.regs digits = Λ := by
+    simp +decide [c, digits]
+  have c_one : c.regs one = 1 := by
+    simpa +decide [c, digits, one] using b_one
+  have c_two : c.regs two = 2 := by
+    simpa +decide [c, digits, two] using b_two
+  have c_mem : c.mem = x.mem := b_memory
+  obtain ⟨d, ed, d_root, d_len, d_mem, d_one⟩ := NatSqrt.exec_rename
+    sqrtRegisters sqrt_injective c (by simpa [sqrtRegisters, NatSqrt.arg, c_len] using fsqrt)
+  simp only [sqrtRegisters, NatSqrt.arg, NatSqrt.root, NatSqrt.one,
+    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val, c_len] at ed d_root d_len d_one
+  have d_magnitude : d.regs magnitude = U := (ed.regs_eq (by decide)).trans c_magnitude
+  have d_three : d.regs three = 3 := (ed.regs_eq (by decide)).trans c_three
+  have d_four : d.regs four = 4 := (ed.regs_eq (by decide)).trans c_four
+  have d_five : d.regs five = 5 := (ed.regs_eq (by decide)).trans c_five
+  have d_eight : d.regs eight = 8 := (ed.regs_eq (by decide)).trans c_eight
+  have d_padding : d.regs padding = 4 * U + 1 := (ed.regs_eq (by decide)).trans c_padding
+  have d_digits : d.regs digits = Λ := (ed.regs_eq (by decide)).trans c_digits
+  have d_two : d.regs two = 2 := (ed.regs_eq (by decide)).trans c_two
+  have d_memory : d.mem = x.mem := d_mem.trans c_mem
+  let e := (((((d.set temp (Nat.sqrt n + 1)).set want (5 * Λ)).set want (wp)).set wantSucc
+    (wp + 1)).set quotient (wp + 1))
+  have ee : ExecWithin w (ram[ temp ← root + one; want ← five * digits; want ← want * temp;
+    wantSucc ← want + one; quotient ← wantSucc ]) d e 5 := by
+    ram_eval [e, d_root, d_one, d_five, d_digits, ← ew, fr, f5Λ, fwp, fwps, temp, root, one,
+      want, five, digits, wantSucc, quotient, Fin.mk.injEq, Data.set, Function.update_idem]
+  have e_magnitude : e.regs magnitude = U := by
+    simpa +decide [e, temp, want, wantSucc, quotient, magnitude] using d_magnitude
+  have e_three : e.regs three = 3 := by
+    simpa +decide [e, temp, want, wantSucc, quotient, three] using d_three
+  have e_four : e.regs four = 4 := by
+    simpa +decide [e, temp, want, wantSucc, quotient, four] using d_four
+  have e_five : e.regs five = 5 := by
+    simpa +decide [e, temp, want, wantSucc, quotient, five] using d_five
+  have e_eight : e.regs eight = 8 := by
+    simpa +decide [e, temp, want, wantSucc, quotient, eight] using d_eight
+  have e_padding : e.regs padding = 4 * U + 1 := by
+    simpa +decide [e, temp, want, wantSucc, quotient, padding] using d_padding
+  have e_digits : e.regs digits = Λ := by
+    simpa +decide [e, temp, want, wantSucc, quotient, digits] using d_digits
+  have e_two : e.regs two = 2 := by
+    simpa +decide [e, temp, want, wantSucc, quotient, two] using d_two
+  have e_root : e.regs root = Nat.sqrt n := by
+    simpa +decide [e, temp, want, wantSucc, quotient, root] using d_root
+  have e_one : e.regs one = 1 := by
+    simpa +decide [e, temp, want, wantSucc, quotient, one] using d_one
+  have e_len : e.regs len = n := by
+    simpa +decide [e, temp, want, wantSucc, quotient, len] using d_len
+  have e_temp : e.regs temp = Nat.sqrt n + 1 := by
+    simp +decide [e, temp, want, wantSucc, quotient]
+  have e_want : e.regs want = wp := by
+    simp +decide [e, temp, want, wantSucc, quotient]
+  have e_wantSucc : e.regs wantSucc = wp + 1 := by
+    simp +decide [e, temp, want, wantSucc, quotient]
+  have e_quotient : e.regs quotient = wp + 1 := by
+    simp +decide [e, temp, want, wantSucc, quotient]
+  have e_mem : e.mem = x.mem := d_memory
+  obtain ⟨f, ef, f_temp, f_mem, f_one, f_two⟩ :=
+    NatLog.exec_rename (logRegisters temp) (by decide) e f2
+      (by simpa only [logRegisters, NatLog.arg, Matrix.cons_val_zero, e_quotient] using fwps)
+      (by simpa only [logRegisters, NatLog.arg, Matrix.cons_val_zero, e_quotient, h] using flogwp)
+  simp only [logRegisters, NatLog.arg, NatLog.result, NatLog.one, NatLog.two,
+    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val, e_quotient] at ef f_temp f_one f_two
+  have f_magnitude : f.regs magnitude = U := (ef.regs_eq (by decide)).trans e_magnitude
+  have f_three : f.regs three = 3 := (ef.regs_eq (by decide)).trans e_three
+  have f_four : f.regs four = 4 := (ef.regs_eq (by decide)).trans e_four
+  have f_five : f.regs five = 5 := (ef.regs_eq (by decide)).trans e_five
+  have f_eight : f.regs eight = 8 := (ef.regs_eq (by decide)).trans e_eight
+  have f_padding : f.regs padding = 4 * U + 1 := (ef.regs_eq (by decide)).trans e_padding
+  have f_digits : f.regs digits = Λ := (ef.regs_eq (by decide)).trans e_digits
+  have f_root : f.regs root = Nat.sqrt n := (ef.regs_eq (by decide)).trans e_root
+  have f_len : f.regs len = n := (ef.regs_eq (by decide)).trans e_len
+  have f_want : f.regs want = wp := (ef.regs_eq (by decide)).trans e_want
+  have f_wantSucc : f.regs wantSucc = wp + 1 := (ef.regs_eq (by decide)).trans e_wantSucc
+  have f_memory : f.mem = x.mem := f_mem.trans e_mem
+  let g := (((f.set temp (2 * Nat.log 2 (wp + 1))).set temp
+    (2 * Nat.log 2 (wp + 1) + 4)).set primeBound m)
+  have eg : ExecWithin w (ram[ temp ← two * temp; temp ← temp + four;
+    primeBound ← wantSucc * temp ]) f g 3 := by
+    ram_eval [g, f_two, f_temp, f_four, f_wantSucc, ← em, f2log, ff, hml, temp, two, four,
+      primeBound, wantSucc, Fin.mk.injEq, Data.set, Function.update_idem]
+  have g_magnitude : g.regs magnitude = U := by
+    simpa +decide [g, temp, primeBound, magnitude] using f_magnitude
+  have g_three : g.regs three = 3 := by
+    simpa +decide [g, temp, primeBound, three] using f_three
+  have g_four : g.regs four = 4 := by
+    simpa +decide [g, temp, primeBound, four] using f_four
+  have g_five : g.regs five = 5 := by
+    simpa +decide [g, temp, primeBound, five] using f_five
+  have g_eight : g.regs eight = 8 := by
+    simpa +decide [g, temp, primeBound, eight] using f_eight
+  have g_padding : g.regs padding = 4 * U + 1 := by
+    simpa +decide [g, temp, primeBound, padding] using f_padding
+  have g_digits : g.regs digits = Λ := by
+    simpa +decide [g, temp, primeBound, digits] using f_digits
+  have g_root : g.regs root = Nat.sqrt n := by
+    simpa +decide [g, temp, primeBound, root] using f_root
+  have g_len : g.regs len = n := by
+    simpa +decide [g, temp, primeBound, len] using f_len
+  have g_want : g.regs want = wp := by
+    simpa +decide [g, temp, primeBound, want] using f_want
+  have g_wantSucc : g.regs wantSucc = wp + 1 := by
+    simpa +decide [g, temp, primeBound, wantSucc] using f_wantSucc
+  have g_temp : g.regs temp = 2 * Nat.log 2 (wp + 1) + 4 := by
+    simp +decide [g, temp, primeBound]
+  have g_one : g.regs one = 1 := by
+    simpa +decide [g, temp, primeBound, one] using f_one
+  have g_two : g.regs two = 2 := by
+    simpa +decide [g, temp, primeBound, two] using f_two
+  have g_primeBound : g.regs primeBound = m := by
+    simp +decide [g, temp, primeBound]
+  have g_mem : g.mem = x.mem := f_memory
+  let j := (g.set quotient (n))
+  have ej : ExecWithin (B := .standard) w (ram[ quotient ← len ]) g j 1 := by
+    ram_eval [j, g_len]
+  have j_magnitude : j.regs magnitude = U := by
+    simpa +decide [j, quotient, magnitude] using g_magnitude
+  have j_three : j.regs three = 3 := by
+    simpa +decide [j, quotient, three] using g_three
+  have j_four : j.regs four = 4 := by
+    simpa +decide [j, quotient, four] using g_four
+  have j_five : j.regs five = 5 := by
+    simpa +decide [j, quotient, five] using g_five
+  have j_eight : j.regs eight = 8 := by
+    simpa +decide [j, quotient, eight] using g_eight
+  have j_padding : j.regs padding = 4 * U + 1 := by
+    simpa +decide [j, quotient, padding] using g_padding
+  have j_digits : j.regs digits = Λ := by
+    simpa +decide [j, quotient, digits] using g_digits
+  have j_root : j.regs root = Nat.sqrt n := by
+    simpa +decide [j, quotient, root] using g_root
+  have j_len : j.regs len = n := by
+    simpa +decide [j, quotient, len] using g_len
+  have j_want : j.regs want = wp := by
+    simpa +decide [j, quotient, want] using g_want
+  have j_wantSucc : j.regs wantSucc = wp + 1 := by
+    simpa +decide [j, quotient, wantSucc] using g_wantSucc
+  have j_temp : j.regs temp = 2 * Nat.log 2 (wp + 1) + 4 := by
+    simpa +decide [j, quotient, temp] using g_temp
+  have j_one : j.regs one = 1 := by
+    simpa +decide [j, quotient, one] using g_one
+  have j_two : j.regs two = 2 := by
+    simpa +decide [j, quotient, two] using g_two
+  have j_primeBound : j.regs primeBound = m := by
+    simpa +decide [j, quotient, primeBound] using g_primeBound
+  have j_quotient : j.regs quotient = n := by
+    simp +decide [j, quotient]
+  have j_mem : j.mem = x.mem := g_mem
+  obtain ⟨k, ek, k_logLen, k_mem, k_one, k_two⟩ :=
+    NatLog.exec_rename (logRegisters logLen) (by decide) j f2
+      (by simpa only [logRegisters, NatLog.arg, Matrix.cons_val_zero, j_quotient] using fn)
+      (by simpa only [logRegisters, NatLog.arg, Matrix.cons_val_zero, j_quotient, h] using flogn)
+  simp only [logRegisters, NatLog.arg, NatLog.result, NatLog.one, NatLog.two,
+    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val,
+      j_quotient] at ek k_logLen k_one k_two
+  have k_magnitude : k.regs magnitude = U := (ek.regs_eq (by decide)).trans j_magnitude
+  have k_three : k.regs three = 3 := (ek.regs_eq (by decide)).trans j_three
+  have k_four : k.regs four = 4 := (ek.regs_eq (by decide)).trans j_four
+  have k_five : k.regs five = 5 := (ek.regs_eq (by decide)).trans j_five
+  have k_eight : k.regs eight = 8 := (ek.regs_eq (by decide)).trans j_eight
+  have k_padding : k.regs padding = 4 * U + 1 := (ek.regs_eq (by decide)).trans j_padding
+  have k_digits : k.regs digits = Λ := (ek.regs_eq (by decide)).trans j_digits
+  have k_root : k.regs root = Nat.sqrt n := (ek.regs_eq (by decide)).trans j_root
+  have k_len : k.regs len = n := (ek.regs_eq (by decide)).trans j_len
+  have k_want : k.regs want = wp := (ek.regs_eq (by decide)).trans j_want
+  have k_wantSucc : k.regs wantSucc = wp + 1 := (ek.regs_eq (by decide)).trans j_wantSucc
+  have k_temp : k.regs temp = 2 * Nat.log 2 (wp + 1) + 4 := (ek.regs_eq (by decide)).trans j_temp
+  have k_primeBound : k.regs primeBound = m := (ek.regs_eq (by decide)).trans j_primeBound
+  have k_memory : k.mem = x.mem := k_mem.trans j_mem
+  let l := (k.set quotient (Nat.log 2 n + 2))
+  have el : ExecWithin w (ram[ quotient ← logLen + two ]) k l 1 := by
+    ram_eval [l, k_logLen, k_two, flog2, quotient, logLen, two, Fin.mk.injEq]
+  have l_magnitude : l.regs magnitude = U := by
+    simpa +decide [l, quotient, magnitude] using k_magnitude
+  have l_three : l.regs three = 3 := by
+    simpa +decide [l, quotient, three] using k_three
+  have l_four : l.regs four = 4 := by
+    simpa +decide [l, quotient, four] using k_four
+  have l_five : l.regs five = 5 := by
+    simpa +decide [l, quotient, five] using k_five
+  have l_eight : l.regs eight = 8 := by
+    simpa +decide [l, quotient, eight] using k_eight
+  have l_padding : l.regs padding = 4 * U + 1 := by
+    simpa +decide [l, quotient, padding] using k_padding
+  have l_digits : l.regs digits = Λ := by
+    simpa +decide [l, quotient, digits] using k_digits
+  have l_root : l.regs root = Nat.sqrt n := by
+    simpa +decide [l, quotient, root] using k_root
+  have l_len : l.regs len = n := by
+    simpa +decide [l, quotient, len] using k_len
+  have l_want : l.regs want = wp := by
+    simpa +decide [l, quotient, want] using k_want
+  have l_wantSucc : l.regs wantSucc = wp + 1 := by
+    simpa +decide [l, quotient, wantSucc] using k_wantSucc
+  have l_temp : l.regs temp = 2 * Nat.log 2 (wp + 1) + 4 := by
+    simpa +decide [l, quotient, temp] using k_temp
+  have l_primeBound : l.regs primeBound = m := by
+    simpa +decide [l, quotient, primeBound] using k_primeBound
+  have l_logLen : l.regs logLen = Nat.log 2 n := by
+    simpa +decide [l, quotient, logLen] using k_logLen
+  have l_one : l.regs one = 1 := by
+    simpa +decide [l, quotient, one] using k_one
+  have l_two : l.regs two = 2 := by
+    simpa +decide [l, quotient, two] using k_two
+  have l_quotient : l.regs quotient = Nat.log 2 n + 2 := by
+    simp +decide [l, quotient]
+  have l_mem : l.mem = x.mem := k_memory
+  obtain ⟨o, eo, o_height, o_mem, o_one, o_two⟩ :=
+    NatClog.exec_rename (logRegisters height) (by decide) l f2
+      (by simpa only [logRegisters, NatClog.arg, Matrix.cons_val_zero, l_quotient] using flog3)
+      (by simpa only [logRegisters, NatClog.arg, Matrix.cons_val_zero, l_quotient, h,
+        Cslib.Algorithms.ThreeSum.ChanHe.height] using fh)
+  simp only [logRegisters, NatClog.arg, NatClog.result, NatClog.one, NatClog.two,
+    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val,
+      l_quotient] at eo o_height o_one o_two
+  change o.regs height = h at o_height
+  change ExecWithin w _ l o (5 * h + 5) at eo
+  have o_magnitude : o.regs magnitude = U := (eo.regs_eq (by decide)).trans l_magnitude
+  have o_three : o.regs three = 3 := (eo.regs_eq (by decide)).trans l_three
+  have o_four : o.regs four = 4 := (eo.regs_eq (by decide)).trans l_four
+  have o_five : o.regs five = 5 := (eo.regs_eq (by decide)).trans l_five
+  have o_eight : o.regs eight = 8 := (eo.regs_eq (by decide)).trans l_eight
+  have o_padding : o.regs padding = 4 * U + 1 := (eo.regs_eq (by decide)).trans l_padding
+  have o_digits : o.regs digits = Λ := (eo.regs_eq (by decide)).trans l_digits
+  have o_root : o.regs root = Nat.sqrt n := (eo.regs_eq (by decide)).trans l_root
+  have o_len : o.regs len = n := (eo.regs_eq (by decide)).trans l_len
+  have o_want : o.regs want = wp := (eo.regs_eq (by decide)).trans l_want
+  have o_wantSucc : o.regs wantSucc = wp + 1 := (eo.regs_eq (by decide)).trans l_wantSucc
+  have o_temp : o.regs temp = 2 * Nat.log 2 (wp + 1) + 4 := (eo.regs_eq (by decide)).trans l_temp
+  have o_primeBound : o.regs primeBound = m := (eo.regs_eq (by decide)).trans l_primeBound
+  have o_logLen : o.regs logLen = Nat.log 2 n := (eo.regs_eq (by decide)).trans l_logLen
+  have o_memory : o.mem = x.mem := o_mem.trans l_mem
+  let p := ((((o.set fuel (3 * h)).set fuel (Cslib.Algorithms.ThreeSum.ChanHe.fuel n)).set packedLen
+    (m * m)).set packedLen (8 * m ^ 2))
+  have ep : ExecWithin w (ram[ fuel ← three * height; fuel ← fuel - two;
+    packedLen ← primeBound * primeBound; packedLen ← eight * packedLen ]) o p 4 := by
+    ram_eval [p, o_three, o_height, o_two, o_primeBound, o_eight, ← eh, f3h, ffuel, fm2, fNm,
+      fuel, three, height, two, packedLen, primeBound, eight, Fin.mk.injEq, pow_two, Data.set,
+      Function.update_idem]
+  have p_magnitude : p.regs magnitude = U := by
+    simpa +decide [p, fuel, packedLen, magnitude] using o_magnitude
+  have p_three : p.regs three = 3 := by
+    simpa +decide [p, fuel, packedLen, three] using o_three
+  have p_four : p.regs four = 4 := by
+    simpa +decide [p, fuel, packedLen, four] using o_four
+  have p_five : p.regs five = 5 := by
+    simpa +decide [p, fuel, packedLen, five] using o_five
+  have p_eight : p.regs eight = 8 := by
+    simpa +decide [p, fuel, packedLen, eight] using o_eight
+  have p_padding : p.regs padding = 4 * U + 1 := by
+    simpa +decide [p, fuel, packedLen, padding] using o_padding
+  have p_digits : p.regs digits = Λ := by
+    simpa +decide [p, fuel, packedLen, digits] using o_digits
+  have p_root : p.regs root = Nat.sqrt n := by
+    simpa +decide [p, fuel, packedLen, root] using o_root
+  have p_len : p.regs len = n := by
+    simpa +decide [p, fuel, packedLen, len] using o_len
+  have p_want : p.regs want = wp := by
+    simpa +decide [p, fuel, packedLen, want] using o_want
+  have p_wantSucc : p.regs wantSucc = wp + 1 := by
+    simpa +decide [p, fuel, packedLen, wantSucc] using o_wantSucc
+  have p_temp : p.regs temp = 2 * Nat.log 2 (wp + 1) + 4 := by
+    simpa +decide [p, fuel, packedLen, temp] using o_temp
+  have p_primeBound : p.regs primeBound = m := by
+    simpa +decide [p, fuel, packedLen, primeBound] using o_primeBound
+  have p_logLen : p.regs logLen = Nat.log 2 n := by
+    simpa +decide [p, fuel, packedLen, logLen] using o_logLen
+  have p_height : p.regs height = h := by
+    simpa +decide [p, fuel, packedLen, height] using o_height
+  have p_one : p.regs one = 1 := by
+    simpa +decide [p, fuel, packedLen, one] using o_one
+  have p_two : p.regs two = 2 := by
+    simpa +decide [p, fuel, packedLen, two] using o_two
+  have p_fuel : p.regs fuel = Cslib.Algorithms.ThreeSum.ChanHe.fuel n := by
+    simp +decide [p, fuel, packedLen]
+  have p_packedLen : p.regs packedLen = 8 * m ^ 2 := by
+    simp +decide [p, fuel, packedLen]
+  have p_mem : p.mem = x.mem := o_memory
+  refine ⟨p, ?_, ?_, p_mem⟩
+  · exact (ea.seq
+      (eb.seq
+      (ec.seq
+      (ed.seq
+      (ee.seq
+      (ef.seq
+      (eg.seq
+      (ej.seq
+      (ek.seq
+      (el.seq
+      (eo.seq
+      (ep)))))))))))).mono (by
+      rw [time_zero]
+      dsimp only [wp, h]
+      exact le_of_eq (by ring))
+  · exact ⟨p_len, p_magnitude, p_digits, p_height, p_fuel, p_want, p_primeBound, p_packedLen,
+    p_padding⟩
+
+/-- Read the native unsigned header and compute all parameters, preserving every memory cell.
+This local theorem is discharged from a logarithmic width in `runs_input`. -/
+theorem exec {w : ℕ} (κ : ℕ) (x : Data 24)
+    (hfit : Fits w (Math.budget (x.mem 0) ((x.mem 0 + 2) ^ κ))) :
+    ∃ y, ExecWithin w (program κ) x y (time κ (x.mem 0) ((x.mem 0 + 2) ^ κ)) ∧
+      Output (x.mem 0) ((x.mem 0 + 2) ^ κ) y ∧ y.mem = x.mem := by
+  let n := x.mem 0
+  let U := (n + 2) ^ κ
+  have fit (v : ℕ) (hv : v ≤ 8 * U + 4 * n + 64) : Fits w v :=
+    hfit.of_le (by change v ≤ Math.budget n U; dsimp [Math.budget]; omega)
+  have f1 : Fits w 1 := fit _ (by omega)
+  have f2 : Fits w 2 := fit _ (by omega)
+  have f3 : Fits w 3 := fit _ (by omega)
+  have f4 : Fits w 4 := fit _ (by omega)
+  have f5 : Fits w 5 := fit _ (by omega)
+  have f8 : Fits w 8 := fit _ (by omega)
+  have fb : Fits w (n + 2) := fit _ (by omega)
+  have fU : Fits w U := fit _ (by omega)
+  let a := (((((((((x.set quotient 0).set len n).set one 1).set two 2).set three 3).set
+    four 4).set five 5).set eight 8).set base (n + 2))
+  have ha : ExecWithin w setup x a 9 := by
+    ram_eval [setup, a, n, f1, f2, f3, f4, f5, f8, fb,
+      quotient, len, one, two, three, four, five, eight, base, Fin.mk.injEq]
+  have hab : a.regs base = n + 2 := by simp [a]
+  have hp := exec_power κ a (by rw [hab]; omega) (by simpa only [hab] using fU)
+  let b := a.set magnitude U
+  have hpb : ExecWithin w (power κ) a b (κ + 1) := by simpa only [hab] using hp
+  obtain ⟨y, hy, hout, hm⟩ := exec_calculate b
+    (by simp +decide [b, a, n, magnitude, len, base, one, two, three, four, five, eight, quotient])
+    (by simp [b, U, n])
+    (by simp +decide [b, a, magnitude, one, base, two, three, four, five, eight])
+    (by simp +decide [b, a, magnitude, two, base, three, four, five, eight])
+    (by simp +decide [b, a, magnitude, three, base, four, five, eight])
+    (by simp +decide [b, a, magnitude, four, base, five, eight])
+    (by simp +decide [b, a, magnitude, five, base, eight])
+    (by simp +decide [b, a, magnitude, eight, base]) hfit
+  refine ⟨y, (ha.seq (hpb.seq hy)).mono ?_, hout, hm⟩
+  dsimp only [time]
+  omega
+
+namespace Math
+
+open Cslib.Algorithms.ThreeSum
+
+/-- A polynomial scale for bounding every parameter intermediate. -/
+def scale (n U : ℕ) : ℕ := 16 * (n + 2) * (U + 1)
+
+private theorem scale_bounds (n U : ℕ) :
+    16 ≤ scale n U ∧ n + 2 ≤ scale n U ∧ 4 * U + 2 ≤ scale n U := by
+  have h := Nat.mul_le_mul_left 16 (Nat.mul_le_mul
+    (show 1 ≤ n + 2 by omega) (show 1 ≤ U + 1 by omega))
+  have hn := Nat.le_mul_of_pos_right (n + 2) (show 0 < 16 * (U + 1) by positivity)
+  have hU := Nat.le_mul_of_pos_right (U + 1) (show 0 < n + 2 by omega)
+  dsimp [scale]
+  have hnu := Nat.zero_le (n * U)
+  refine ⟨?_, ?_, ?_⟩ <;> nlinarith
+
+private theorem scale_pow_mono {b : ℕ} (hb : 1 ≤ b) {i j : ℕ} (hij : i ≤ j) :
+    b ^ i ≤ b ^ j := Nat.pow_le_pow_right hb hij
+
+/-- A coarse polynomial bound; it also covers final unsuccessful root/log iterations. -/
+theorem budget_le_scale (n U : ℕ) : budget n U ≤ scale n U ^ 20 := by
+  let b := scale n U
+  obtain ⟨hb, hn, hU⟩ := scale_bounds n U
+  change 16 ≤ b at hb
+  change n + 2 ≤ b at hn
+  change 4 * U + 2 ≤ b at hU
+  have hb1 : 1 ≤ b := by omega
+  have hΛ : labelBits (2 * U) ≤ b := by
+    have hl := Nat.log_le_self 2 (4 * U)
+    dsimp [labelBits]
+    have he : 2 * (2 * U) = 4 * U := by omega
+    rw [he]
+    omega
+  have hr : Nat.sqrt n + 1 ≤ b := by have := Nat.sqrt_le_self n; omega
+  have hw : ChanHe.wPar n (2 * U) ≤ b ^ 3 := by
+    calc
+      _ ≤ b * b * b := by
+        dsimp [ChanHe.wPar]
+        exact Nat.mul_le_mul (Nat.mul_le_mul (by omega) hΛ) hr
+      _ = b ^ 3 := by ring
+  have hws : ChanHe.wPar n (2 * U) + 1 ≤ b ^ 4 := by
+    have hp : 1 ≤ b ^ 3 := Nat.one_le_pow _ _ hb1
+    calc
+      _ ≤ 2 * b ^ 3 := by omega
+      _ ≤ b * b ^ 3 := Nat.mul_le_mul_right _ (by omega)
+      _ = b ^ 4 := by ring
+  have hfac : 2 * Nat.log 2 (ChanHe.wPar n (2 * U) + 1) + 4 ≤ b ^ 5 := by
+    have hl := Nat.log_le_self 2 (ChanHe.wPar n (2 * U) + 1)
+    have hp : 1 ≤ b ^ 4 := Nat.one_le_pow _ _ hb1
+    calc
+      _ ≤ 6 * b ^ 4 := by omega
+      _ ≤ b * b ^ 4 := Nat.mul_le_mul_right _ (by omega)
+      _ = b ^ 5 := by ring
+  have hm : ChanHe.mPar n (2 * U) ≤ b ^ 9 := by
+    calc
+      _ ≤ b ^ 4 * b ^ 5 := Nat.mul_le_mul hws hfac
+      _ = b ^ 9 := by ring
+  have hms : ChanHe.mPar n (2 * U) + 1 ≤ 2 * b ^ 9 := by
+    have hp : 1 ≤ b ^ 9 := Nat.one_le_pow _ _ hb1
+    omega
+  have hsq : (ChanHe.mPar n (2 * U) + 1) ^ 2 ≤ (2 * b ^ 9) ^ 2 :=
+    Nat.pow_le_pow_left hms 2
+  have hsmall : 8 * U + 4 * n + 64 ≤ 16 * b := by omega
+  have hp18 : b ≤ b ^ 18 := by
+    simpa only [pow_one] using scale_pow_mono hb1 (show 1 ≤ 18 by decide)
+  have hbudget : budget n U ≤ 48 * b ^ 18 := by
+    dsimp only [budget]
+    nlinarith
+  calc
+    _ ≤ 48 * b ^ 18 := hbudget
+    _ ≤ b ^ 2 * b ^ 18 := Nat.mul_le_mul_right _ (by nlinarith)
+    _ = b ^ 20 := by ring
+
+/-- A single polynomial bound, with exponent affine in the fixed magnitude exponent. -/
+theorem budget_polynomial (κ n : ℕ) : budget n ((n + 2) ^ κ) ≤ (n + 2) ^ (20 * κ + 120) := by
+  let a := n + 2
+  have ha : 2 ≤ a := by dsimp [a]; omega
+  have hpow : 1 ≤ a ^ κ := Nat.one_le_pow _ _ (by omega)
+  have hs : scale n (a ^ κ) ≤ a ^ (κ + 6) := by
+    calc
+      _ = 16 * a * (a ^ κ + 1) := rfl
+      _ ≤ 32 * a * a ^ κ := by nlinarith
+      _ ≤ a ^ 5 * a * a ^ κ := by
+        exact Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ (by
+          have := Nat.pow_le_pow_left ha 5
+          norm_num at this ⊢
+          omega))
+      _ = a ^ (κ + 6) := by ring
+  calc
+    _ ≤ scale n (a ^ κ) ^ 20 := budget_le_scale n (a ^ κ)
+    _ ≤ (a ^ (κ + 6)) ^ 20 := Nat.pow_le_pow_left hs 20
+    _ = a ^ (20 * κ + 120) := by ring
+
+end Math
+/-- Positive logarithmic word-width threshold for the complete parameter computation. -/
+def width (κ n : ℕ) : ℕ := (20 * κ + 121) * Nat.clog 2 (n + 2)
+
+/-- The width requirement is satisfiable even at empty input and exponent zero. -/
+theorem width_pos (κ n : ℕ) : 0 < width κ n := by
+  have := Nat.clog_pos (b := 2) (by decide) (show 1 < n + 2 by omega)
+  dsimp [width]
+  positivity
+
+private theorem budget_le_two_pow (κ n : ℕ) :
+    Math.budget n ((n + 2) ^ κ) ≤ 2 ^ ((20 * κ + 120) * Nat.clog 2 (n + 2)) := by
+  calc
+    _ ≤ (n + 2) ^ (20 * κ + 120) := Math.budget_polynomial κ n
+    _ ≤ (2 ^ Nat.clog 2 (n + 2)) ^ (20 * κ + 120) :=
+      Nat.pow_le_pow_left (Nat.le_pow_clog (by decide) _) _
+    _ = _ := by rw [← pow_mul]; congr 1; ring
+
+/-- Every local fit premise follows from the positive logarithmic width. -/
+theorem budget_fits {κ n w : ℕ} (hw : width κ n ≤ w) :
+    Fits w (Math.budget n ((n + 2) ^ κ)) := by
+  have hl := Nat.clog_pos (b := 2) (by decide) (show 1 < n + 2 by omega)
+  apply Fits.mono (w := width κ n) _ hw
+  apply (budget_le_two_pow κ n).trans_lt
+  apply Nat.pow_lt_pow_right (by decide)
+  dsimp [width]
+  nlinarith
+
+/-- Signed-encoded inputs and the unsigned length header fit at the same width. -/
+theorem inputFits {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w)
+    (hvalues : ∀ z ∈ input, |z| ≤ ((input.length + 2) ^ κ : ℕ)) :
+    InputFits w (input.map Signed.encode) := by
+  have hf := budget_fits hw
+  refine ⟨?_, ?_⟩
+  · simp only [List.length_map]
+    apply hf.of_le
+    dsimp [Math.budget]
+    omega
+  · intro v hv
+    obtain ⟨z, hz, rfl⟩ := List.mem_map.mp hv
+    have habs : z.natAbs ≤ (input.length + 2) ^ κ := by
+      have hc : (z.natAbs : ℤ) ≤ ((input.length + 2) ^ κ : ℕ) := by
+        simpa only [Int.natCast_natAbs] using hvalues z hz
+      exact_mod_cast hc
+    apply hf.of_le
+    dsimp [Math.budget, Signed.encode]
+    split_ifs <;> omega
+
+/-- Explicit `Oκ(√n + log(n+2))` instruction bound, valid also at `n = 0,1,2`. -/
+theorem time_bound (κ n : ℕ) :
+    time κ n ((n + 2) ^ κ) ≤
+      5 * Nat.sqrt n + (400 * κ + 3000) * Nat.clog 2 (n + 2) := by
+  let U := (n + 2) ^ κ
+  let L := Nat.clog 2 (n + 2)
+  let E := 20 * κ + 120
+  have hL : 1 ≤ L := Nat.clog_pos (by decide) (show 1 < n + 2 by omega)
+  have hB : Nat.log 2 (Math.budget n U) ≤ E * L := by
+    calc
+      _ ≤ Nat.log 2 (2 ^ (E * L)) := Nat.log_mono_right (budget_le_two_pow κ n)
+      _ = _ := Nat.log_pow (by decide) _
+  have hlogU : Nat.log 2 (4 * U) ≤ E * L :=
+    (Nat.log_mono_right (show 4 * U ≤ Math.budget n U by dsimp [Math.budget]; omega)).trans hB
+  have hw := Math.want_le n U
+  have hlogw : Nat.log 2 (Cslib.Algorithms.ThreeSum.ChanHe.wPar n (2 * U) + 1) ≤ E * L := by
+    apply (Nat.log_mono_right ?_).trans hB
+    dsimp [Math.budget]
+    nlinarith
+  have hlogn : Nat.log 2 n ≤ E * L :=
+    (Nat.log_mono_right (show n ≤ Math.budget n U by dsimp [Math.budget]; omega)).trans hB
+  have hh := Math.height_le n
+  change time κ n U ≤ _
+  dsimp only [time]
+  dsimp only [E, L] at *
+  nlinarith
+
+/-- Native run from actual signed input initialization. No parameters or arithmetic routines
+are supplied as advice. The returned state identifies all outputs and keeps *all* input memory.
+The flat program has 24 registers and depends only on `κ`; halting adds one instruction. -/
+theorem runs_input {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w)
+    (hvalues : ∀ z ∈ input, |z| ≤ ((input.length + 2) ^ κ : ℕ)) :
+    ∃ y t, t ≤ 5 * Nat.sqrt input.length +
+        (400 * κ + 3000) * Nat.clog 2 (input.length + 2) ∧
+      Runs w ((program κ).program packedLen) (State.init (input.map Signed.encode))
+        ⟨(program κ).size, y⟩ t ∧
+      Output input.length ((input.length + 2) ^ κ) y ∧
+      y.mem = (Data.init (input.map Signed.encode) : Data 24).mem ∧ y.Bounded w := by
+  have hi := inputFits input hw hvalues
+  obtain ⟨y, hy, ho, hm⟩ := exec κ (Data.init (input.map Signed.encode))
+    (by simpa only [Data.init_mem_zero, List.length_map] using budget_fits hw)
+  simp only [Data.init_mem_zero, List.length_map] at hy ho
+  obtain ⟨t, ht, he⟩ := hy
+  have hr := he.runs (pc := 0) (p := (program κ).program packedLen)
+    (Program.Contains.self _).append_left
+  simp only [Nat.zero_add] at hr
+  refine ⟨y, t, ht.trans (time_bound κ input.length), hr, ho, hm, ?_⟩
+  exact hr.bounded_init hi
+
+/-- The number of native instructions in the finite structured code is affine in `κ`. -/
+theorem size_program (κ : ℕ) : (program κ).size = κ + 71 := by
+  have hp : (power κ).size = κ + 1 := by
+    induction κ with
+    | zero => rfl
+    | succ κ ih => simp [power, ih]
+  simp only [program, setup, calculate, NatLog.program, NatLog.body, NatSqrt.program,
+    NatSqrt.body, NatClog.program, NatClog.body, Code.size.eq_2, Code.size, Nat.reduceAdd, hp,
+    Code.size_rename]
+  omega
+
+/-- The code is the same at every word width. -/
+theorem not_readsWidth (κ : ℕ) : ¬(program κ).ReadsWidth := by
+  have hs : ¬setup.ReadsWidth := by decide
+  have hc : ¬calculate.ReadsWidth := by decide
+  have hp : ¬(power κ).ReadsWidth := by
+    induction κ with
+    | zero => decide
+    | succ κ ih =>
+      change ¬((power κ).ReadsWidth ∨
+        (Code.op (Op.bin BinOp.mul magnitude magnitude base) : Code .standard 24).ReadsWidth)
+      exact not_or.mpr ⟨ih, by decide⟩
+  simpa only [program, Code.ReadsWidth, not_or] using And.intro hs (And.intro hp hc)
+
+/-- Canonical-width executions use only polynomially bounded integers, including memory
+addresses, loop counters, and final unsuccessful tests. -/
+theorem intermediates_polynomial {κ : ℕ} (input : List ℤ)
+    (hvalues : ∀ z ∈ input, |z| ≤ ((input.length + 2) ^ κ : ℕ))
+    {s : State 24} {t : ℕ}
+    (hr : Runs (width κ input.length) ((program κ).program packedLen)
+      (State.init (input.map Signed.encode)) s t) :
+    (∀ i, s.data.regs i < (input.length + 2) ^ (40 * κ + 242)) ∧
+      ∀ a, s.data.mem a < (input.length + 2) ^ (40 * κ + 242) := by
+  let n := input.length
+  let L := Nat.clog 2 (n + 2)
+  have hL : 0 < L := Nat.clog_pos (by decide) (by omega)
+  have hpred : 2 ^ (L - 1) < n + 2 :=
+    Nat.pow_pred_clog_lt_self (b := 2) (x := n + 2) (by decide) (by omega)
+  have he : 2 ^ L = 2 * 2 ^ (L - 1) := by
+    conv_lhs => rw [show L = (L - 1) + 1 by omega]
+    rw [pow_succ, Nat.mul_comm]
+  have hceil : 2 ^ L ≤ (n + 2) ^ 2 := by rw [he]; nlinarith
+  have hpoly : 2 ^ width κ n ≤ (n + 2) ^ (40 * κ + 242) := by
+    calc
+      _ = (2 ^ L) ^ (20 * κ + 121) := by
+        dsimp only [width, L]
+        rw [← pow_mul]
+        congr 1
+        ring
+      _ ≤ ((n + 2) ^ 2) ^ (20 * κ + 121) := Nat.pow_le_pow_left hceil _
+      _ = _ := by rw [← pow_mul]; congr 1; omega
+  have hb := hr.bounded_init (inputFits input le_rfl hvalues)
+  exact ⟨fun i => (hb.1 i).trans_le hpoly, fun a => (hb.2 a).trans_le hpoly⟩
+
+end Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/Host/Loop.lean b/Complexity/Algorithms/WordRAM/ThreeSum/Host/Loop.lean
new file mode 100644
index 0000000000..853b3a1b32
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/Host/Loop.lean
@@ -0,0 +1,457 @@
+/-
+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.ThreeSum.Host.Prepare
+
+/-!
+# The native Convolution-3SUM instance loop
+
+The supplied solver is an actual finite structured program. Its six input registers hold the
+side, weight bound, three matrix pointers and workspace pointer; its seventh register returns
+an unsigned Boolean. Solver registers are disjoint from the host bank. The host writes each
+instance using `Fill.program`, copies its arguments, executes the solver and accumulates the
+verdict. The execution theorem requires the concrete solver's execution/correctness/frame proof;
+it does not establish a fast solver by assuming one.
+
+The construction directly adapts Anthropic's pinned
+[`c3Round` and `c3Body`](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/Convolution/Host.lean).
+
+## Main definitions
+
+* `Host.instanceArgs`: the concrete generated instance and layout.
+* `Host.hit`: the mathematical verdict for one instance.
+* `Host.round`: fill, invoke the solver and advance one instance.
+* `Host.loop`: the complete instance loop.
+
+## References
+
+* [V. Vassilevska Williams and R. Williams, *Finding, minimizing, and counting weighted
+  subgraphs*][VassilevskaWilliamsWilliams2013]
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.Host
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.ThreeSum
+
+/-- The generated matrices follow the input and precede the solver's workspace. -/
+def instanceArgs (N U s : ℕ) (μ : ℕ → ℤ) : Fill.Args :=
+  ⟨N, sideLength N, s, 1, N + 1,
+    N + 1 + sideLength N * sideLength N,
+    N + 1 + 2 * (sideLength N * sideLength N), μ, 2 * U + 1⟩
+
+/-- The exact-triangle answer for one instance of the explicit reduction. -/
+def hit (N U s : ℕ) (μ : ℕ → ℤ) : Prop :=
+  Cslib.Algorithms.ExactTriangle.HasZeroTriangle
+    (weightAB (t := sideLength N) N μ (2 * U + 1))
+    (weightBC N s μ (2 * U + 1)) (weightAC N s μ (2 * U + 1))
+
+/-- Embed the fixed matrix-builder register bank. -/
+def fillRegisters (i : Fin 28) : Fin 64 := ⟨i.val, by omega⟩
+
+/-- Copy every matrix-builder argument; the builder bank occupies the first 28 registers. -/
+def fillSetup : Code .standard 64 :=
+  let fLen := fillRegisters Cell.len
+  let fBase := fillRegisters Cell.base
+  let fFiller := fillRegisters Cell.filler
+  let fSide := fillRegisters Cell.side
+  let fInst := fillRegisters Cell.inst
+  let fAB := fillRegisters Cell.matAB
+  let fBC := fillRegisters Cell.matBC
+  let fAC := fillRegisters Cell.matAC
+  ram[ fLen ← len; fBase ← base; fFiller ← encodedFiller;
+    fSide ← side; fInst ← inst; fAB ← matAB; fBC ← matBC; fAC ← matAC ]
+
+/-- Matrix construction, including its argument copies. -/
+def fill : Code .standard 64 := .seq fillSetup (Fill.program.rename fillRegisters)
+
+/-- Host registers precede the solver bank. -/
+def hostRegisters {r : ℕ} (i : Fin 64) : Fin (64 + r) := ⟨i.val, by omega⟩
+
+/-- The solver bank is disjoint from every host register. -/
+def solverRegisters {r : ℕ} (i : Fin r) : Fin (64 + r) := ⟨64 + i.val, by omega⟩
+
+/-- One of the seven fixed protocol registers in the solver bank. -/
+def solverArg {r : ℕ} (i : Fin 7) : Fin (r + 7) := ⟨i.val, by omega⟩
+
+/-- Protocol registers after placing the solver after the host. -/
+def callRegisters {r : ℕ} (i : Fin 7) : Fin (64 + (r + 7)) :=
+  solverRegisters (solverArg i)
+
+/-- Prepare the solver's side, unsigned bound, AB/BC/AC pointers and free pointer. -/
+def solverSetup {r : ℕ} : Code .standard (64 + (r + 7)) :=
+  .seq (.op (.copy (callRegisters 0) (hostRegisters side)))
+  (.seq (.op (.copy (callRegisters 1) (hostRegisters filler)))
+  (.seq (.op (.copy (callRegisters 2) (hostRegisters matAB)))
+  (.seq (.op (.copy (callRegisters 3) (hostRegisters matBC)))
+  (.seq (.op (.copy (callRegisters 4) (hostRegisters matAC)))
+    (.op (.copy (callRegisters 5) (hostRegisters free)))))))
+
+/-- Accumulate the unsigned Boolean result and advance the instance counter. -/
+def finish {r : ℕ} : Code .standard (64 + (r + 7)) :=
+  .seq (.branch (.eq (callRegisters 6) (hostRegisters one))
+    (.op (.copy (hostRegisters found) (hostRegisters one)))
+    (.op (.copy (hostRegisters found) (hostRegisters found))))
+    (.op (.bin .add (hostRegisters inst) (hostRegisters inst) (hostRegisters one)))
+
+/-- One complete instance, invoking the supplied finite solver in its own register bank. -/
+def round {r : ℕ} (solver : Code .standard (r + 7)) : Code .standard (64 + (r + 7)) :=
+  .seq (fill.rename hostRegisters)
+    (.seq solverSetup (.seq (solver.rename solverRegisters) finish))
+
+/-- Every one of the `2t` instances is examined, without an uncharged early-exit operation. -/
+def loop {r : ℕ} (solver : Code .standard (r + 7)) : Code .standard (64 + (r + 7)) :=
+  .loop (.lt (hostRegisters inst) (hostRegisters stop)) (round solver)
+
+private theorem fill_injective : fillRegisters.Injective := by
+  intro i j h
+  exact Fin.ext (congrArg (fun k : Fin 64 => k.val) h)
+
+private theorem parameters_of_regs {N U : ℕ} {x y : Data 64}
+    (hx : Parameters N U x)
+    (h : ∀ i : Fin 64, 34 ≤ i.val → i ≠ inst → i ≠ found → y.regs i = x.regs i) :
+    Parameters N U y := by
+  exact ⟨(h len (by decide) (by decide) (by decide)).trans hx.len,
+    (h upper (by decide) (by decide) (by decide)).trans hx.upper,
+    (h base (by decide) (by decide) (by decide)).trans hx.base,
+    (h matAB (by decide) (by decide) (by decide)).trans hx.ab,
+    (h matBC (by decide) (by decide) (by decide)).trans hx.bc,
+    (h matAC (by decide) (by decide) (by decide)).trans hx.ac,
+    (h free (by decide) (by decide) (by decide)).trans hx.free,
+    (h side (by decide) (by decide) (by decide)).trans hx.side,
+    (h stop (by decide) (by decide) (by decide)).trans hx.stop,
+    (h filler (by decide) (by decide) (by decide)).trans hx.filler,
+    (h encodedFiller (by decide) (by decide) (by decide)).trans hx.encodedFiller,
+    (h one (by decide) (by decide) (by decide)).trans hx.one⟩
+
+/-- All eight argument copies and the complete matrix builder are charged. Memory before
+the matrix blocks is preserved; the result contains the three actual serialized matrices. -/
+theorem exec_fill {w N U s : ℕ} (μ : ℕ → ℤ) (x : Data 64)
+    (hp : Parameters N U x) (hs : x.regs inst = s)
+    (hmem : ∀ i < N, x.mem (1 + i) = encode (μ i))
+    (hidx : GenericRAM.Signed.Fits w ((2 * (sideLength N * sideLength N) + s + 1 : ℕ) : ℤ))
+    (hF : GenericRAM.Signed.Fits w (2 * (U : ℤ) + 1))
+    (hnF : GenericRAM.Signed.Fits w (-(2 * (U : ℤ) + 1)))
+    (hμ : ∀ i < N, GenericRAM.Signed.Fits w (μ i))
+    (hsize : Fits (w + 2) (N + 1 + 3 * (sideLength N * sideLength N))) :
+    ∃ y, ExecWithin (w + 2) fill x y (131 * (sideLength N * sideLength N) + 13) ∧
+      Parameters N U y ∧ y.regs inst = s ∧ y.regs found = x.regs found ∧
+      y.mem = (instanceArgs N U s μ).filled x.mem (sideLength N * sideLength N) ∧
+      (∀ a < N + 1, y.mem a = x.mem a) := by
+  let b := x.set (fillRegisters Cell.len) N |>.set (fillRegisters Cell.base) 1
+    |>.set (fillRegisters Cell.filler) (4 * U + 2)
+    |>.set (fillRegisters Cell.side) (sideLength N) |>.set (fillRegisters Cell.inst) s
+    |>.set (fillRegisters Cell.matAB) (N + 1)
+    |>.set (fillRegisters Cell.matBC) (N + 1 + sideLength N * sideLength N)
+    |>.set (fillRegisters Cell.matAC) (N + 1 + 2 * (sideLength N * sideLength N))
+  have hb : ExecWithin (w + 2) fillSetup x b 8 := by
+    ram_eval [fillSetup, b, hp.len, hp.base, hp.encodedFiller, hp.side, hs,
+      hp.ab, hp.bc, hp.ac, fillRegisters, Cell.len, Cell.base, Cell.filler, Cell.side,
+      Cell.inst, Cell.matAB, Cell.matBC, Cell.matAC, len, base, encodedFiller, side, inst,
+      matAB, matBC, matAC, Fin.mk.injEq]
+  have hbregs (i : Fin 64) (hi : 34 ≤ i.val) : b.regs i = x.regs i := by
+    have hne (j : Fin 28) : i ≠ fillRegisters j := by
+      intro he
+      have hv := congrArg Fin.val he
+      dsimp only [fillRegisters] at hv
+      have := j.isLt
+      omega
+    simp only [b, Data.set_regs, Function.update_of_ne (hne _)]
+  have hbf : (b.comap fillRegisters).regs Cell.filler = encode (instanceArgs N U s μ).filler := by
+    simp +decide [b, instanceArgs, fillRegisters, Cell.filler, Cell.side, Cell.inst,
+      Cell.matAB, Cell.matBC, Cell.matAC, encode,
+      show ¬(2 * (U : ℤ) + 1 < 0) from by omega]
+    omega
+  obtain ⟨p, he, hm, -⟩ := Fill.exec (instanceArgs N U s μ) (b.comap fillRegisters)
+    (by simp +decide [b, instanceArgs, fillRegisters, Cell.side, Cell.inst,
+      Cell.matAB, Cell.matBC, Cell.matAC])
+    (by simp +decide [b, instanceArgs, fillRegisters, Cell.inst,
+      Cell.matAB, Cell.matBC, Cell.matAC])
+    (by simp +decide [b, instanceArgs, fillRegisters, Cell.matAB, Cell.matBC, Cell.matAC])
+    (by simp +decide [b, instanceArgs, fillRegisters, Cell.matBC, Cell.matAC])
+    (by simp [b, instanceArgs])
+    (by simp +decide [b, instanceArgs, fillRegisters, Cell.len, Cell.base, Cell.filler,
+      Cell.side, Cell.inst, Cell.matAB, Cell.matBC, Cell.matAC])
+    (by simp +decide [b, instanceArgs, fillRegisters, Cell.base, Cell.filler,
+      Cell.side, Cell.inst, Cell.matAB, Cell.matBC, Cell.matAC]) hbf
+    hmem hidx hF hnF hμ
+    (hsize.of_le (by dsimp [instanceArgs]; omega))
+    (hsize.of_le (by dsimp [instanceArgs]; omega))
+    (hsize.of_le (by dsimp [instanceArgs]; omega))
+    (hsize.of_le (by dsimp [instanceArgs]; omega))
+    (by dsimp [instanceArgs]; omega) (by dsimp [instanceArgs]; omega)
+    (by dsimp [instanceArgs]; omega)
+  let y := p.extend fillRegisters b
+  have hy : ExecWithin (w + 2) (Fill.program.rename fillRegisters) b y
+      (131 * (sideLength N * sideLength N) + 5) := he.rename fill_injective
+  have hyr (i : Fin 64) (hi : 34 ≤ i.val) : y.regs i = x.regs i := by
+    refine (hy.regs_eq ?_).trans (hbregs i hi)
+    apply Code.preserves_rename_of_forall_ne
+    intro j heq
+    have hv := congrArg Fin.val heq
+    dsimp only [fillRegisters] at hv
+    have := j.isLt
+    omega
+  refine ⟨y, ?_, parameters_of_regs hp (fun i hi _ _ => hyr i hi), (hyr inst (by decide)).trans hs,
+    hyr found (by decide), hm, ?_⟩
+  · convert hb.seq hy using 1 <;> first | rfl | omega
+  · intro a ha
+    change p.mem a = x.mem a
+    rw [hm]
+    apply Fill.Args.outside_filled
+    all_goals dsimp [instanceArgs]; omega
+
+/-- The host register bank is embedded injectively. -/
+theorem hostRegisters_injective {r : ℕ} : (hostRegisters (r := r)).Injective := by
+  intro i j h
+  exact Fin.ext (congrArg (fun k : Fin (64 + r) => k.val) h)
+
+private theorem solver_injective {r : ℕ} : (solverRegisters (r := r)).Injective := by
+  intro i j h
+  apply Fin.ext
+  have := congrArg Fin.val h
+  dsimp only [solverRegisters] at this
+  omega
+
+private theorem exec_solverSetup {w r : ℕ} (x : Data (64 + (r + 7))) :
+    ∃ y, ExecWithin w solverSetup x y 6 ∧
+      (∀ i, y.regs (hostRegisters i) = x.regs (hostRegisters i)) ∧ y.mem = x.mem ∧
+      y.regs (callRegisters 0) = x.regs (hostRegisters side) ∧
+      y.regs (callRegisters 1) = x.regs (hostRegisters filler) ∧
+      y.regs (callRegisters 2) = x.regs (hostRegisters matAB) ∧
+      y.regs (callRegisters 3) = x.regs (hostRegisters matBC) ∧
+      y.regs (callRegisters 4) = x.regs (hostRegisters matAC) ∧
+      y.regs (callRegisters 5) = x.regs (hostRegisters free) := by
+  refine ⟨?y, ?exec, ?frame, ?mem, ?side, ?bound, ?ab, ?bc, ?ac, ?free⟩
+  case exec => ram_eval [solverSetup, callRegisters, solverArg, solverRegisters,
+    hostRegisters, side, filler,
+    matAB, matBC, matAC, free, Fin.mk.injEq]
+  case frame =>
+    intro i
+    have hlt := i.isLt
+    simp only [Data.set_regs, Function.update_apply, hostRegisters, Fin.mk.injEq]
+    split_ifs <;> omega
+  all_goals simp +decide [Data.set_regs, callRegisters, solverArg, solverRegisters, hostRegisters]
+
+private theorem exec_finish {w r s : ℕ} (x : Data (64 + (r + 7)))
+    (ho : x.regs (hostRegisters one) = 1) (hi : x.regs (hostRegisters inst) = s)
+    (hfit : Fits w (s + 1)) :
+    ∃ y, ExecWithin w finish x y 4 ∧
+      y.regs (hostRegisters inst) = s + 1 ∧
+      y.regs (hostRegisters found) =
+        (if x.regs (callRegisters 6) = 1 then 1 else x.regs (hostRegisters found)) ∧
+      (∀ i : Fin 64, i ≠ inst → i ≠ found →
+        y.regs (hostRegisters i) = x.regs (hostRegisters i)) ∧ y.mem = x.mem := by
+  change x.regs ⟨45, by omega⟩ = 1 at ho
+  change x.regs ⟨42, by omega⟩ = s at hi
+  by_cases ha : x.regs (callRegisters 6) = 1
+  · change x.regs ⟨70, by omega⟩ = 1 at ha
+    refine ⟨(x.set (hostRegisters found) 1).set (hostRegisters inst) (s + 1),
+      ?exec, ?inst, ?found, ?frame, ?mem⟩
+    case exec =>
+      apply ExecWithin.of_eval (fuel := 0) (n := 3)
+      · simp +decide [finish, Code.eval, Op.eval_copy, Op.eval_bin, Data.put,
+          Data.set_regs, Cond.holds_eq, BinOp.eval,
+          callRegisters, solverArg, solverRegisters, hostRegisters, one, inst, found,
+          ho, hi, ha, hfit]
+      · omega
+    case inst => simp
+    case found =>
+      simp +decide [ha, callRegisters, solverArg, solverRegisters, hostRegisters, inst, found]
+    case frame =>
+      intro i hi hf
+      have hni := (hostRegisters_injective (r := r + 7)).ne hi
+      have hnf := (hostRegisters_injective (r := r + 7)).ne hf
+      simp only [Data.set_regs, Function.update_of_ne hni, Function.update_of_ne hnf]
+    case mem => rfl
+  · change ¬x.regs ⟨70, by omega⟩ = 1 at ha
+    refine ⟨(x.set (hostRegisters found) (x.regs (hostRegisters found))).set
+      (hostRegisters inst) (s + 1), ?exec, ?inst, ?found, ?frame, ?mem⟩
+    case exec =>
+      apply ExecWithin.of_eval (fuel := 0) (n := 4)
+      · simp +decide [finish, Code.eval, Op.eval_copy, Op.eval_bin, Data.put,
+          Data.set_regs, Cond.holds_eq, BinOp.eval,
+          callRegisters, solverArg, solverRegisters, hostRegisters, one, inst, found,
+          ho, hi, ha, hfit]
+      · omega
+    case inst => simp
+    case found =>
+      simp +decide [ha, callRegisters, solverArg, solverRegisters, hostRegisters, inst, found]
+    case frame =>
+      intro i hi hf
+      have hni := (hostRegisters_injective (r := r + 7)).ne hi
+      have hnf := (hostRegisters_injective (r := r + 7)).ne hf
+      simp only [Data.set_regs, Function.update_of_ne hni, Function.update_of_ne hnf]
+    case mem => rfl
+
+/-- One generated instance, with the concrete solver's native execution proof supplied by the
+caller. The solver may overwrite matrices and scratch, but preserves the length header and input.
+The matrices in its premise are produced by the native builder, with no supplied layout oracle. -/
+theorem exec_round {w r N U s T : ℕ} (μ : ℕ → ℤ)
+    (solver : Code .standard (r + 7)) (x : Data (64 + (r + 7)))
+    (hp : Parameters N U (x.comap hostRegisters))
+    (hs : x.regs (hostRegisters inst) = s) (hslt : s < 2 * sideLength N)
+    (hf : x.regs (hostRegisters found) ≤ 1)
+    (hmem : ∀ i < N, x.mem (1 + i) = encode (μ i))
+    (hidx : GenericRAM.Signed.Fits w ((2 * (sideLength N * sideLength N) + s + 1 : ℕ) : ℤ))
+    (hF : GenericRAM.Signed.Fits w (2 * (U : ℤ) + 1))
+    (hnF : GenericRAM.Signed.Fits w (-(2 * (U : ℤ) + 1)))
+    (hμ : ∀ i < N, GenericRAM.Signed.Fits w (μ i))
+    (hsize : Fits (w + 2) (N + 1 + 3 * (sideLength N * sideLength N)))
+    (hsolver : ∀ (a : Data (r + 7)) (mem : ℕ → ℕ),
+      a.regs (solverArg 0) = sideLength N → a.regs (solverArg 1) = 2 * U + 1 →
+      a.regs (solverArg 2) = N + 1 →
+      a.regs (solverArg 3) = N + 1 + sideLength N * sideLength N →
+      a.regs (solverArg 4) = N + 1 + 2 * (sideLength N * sideLength N) →
+      a.regs (solverArg 5) = N + 1 + 3 * (sideLength N * sideLength N) →
+      a.mem = (instanceArgs N U s μ).filled mem (sideLength N * sideLength N) →
+      ∃ b, ExecWithin (w + 2) solver a b T ∧ b.regs (solverArg 6) ≤ 1 ∧
+        (b.regs (solverArg 6) = 1 ↔ hit N U s μ) ∧
+        (∀ a < N + 1, b.mem a = mem a)) :
+    ∃ y, ExecWithin (w + 2) (round solver) x y
+        (131 * (sideLength N * sideLength N) + T + 23) ∧
+      Parameters N U (y.comap hostRegisters) ∧ y.regs (hostRegisters inst) = s + 1 ∧
+      y.regs (hostRegisters found) ≤ 1 ∧
+      (y.regs (hostRegisters found) = 1 ↔ x.regs (hostRegisters found) = 1 ∨ hit N U s μ) ∧
+      (∀ a < N + 1, y.mem a = x.mem a) := by
+  obtain ⟨a, ha, hap, hasi, haf, ham, -⟩ :=
+    exec_fill μ (x.comap hostRegisters) hp hs hmem hidx hF hnF hμ hsize
+  let y := a.extend hostRegisters x
+  have hy : ExecWithin (w + 2) (fill.rename hostRegisters) x y
+      (131 * (sideLength N * sideLength N) + 13) := ha.rename hostRegisters_injective
+  have hyc : y.comap hostRegisters = a := Data.comap_extend hostRegisters_injective _ _
+  have hyp : Parameters N U (y.comap hostRegisters) := by rw [hyc]; exact hap
+  have hysi : y.regs (hostRegisters inst) = s :=
+    (hostRegisters_injective.extend_apply _ _ inst).trans hasi
+  have hyf : y.regs (hostRegisters found) = x.regs (hostRegisters found) :=
+    (hostRegisters_injective.extend_apply _ _ found).trans haf
+  obtain ⟨b, hb, hbr, hbm, hb0, hb1, hb2, hb3, hb4, hb5⟩ := exec_solverSetup (w := w + 2) y
+  have hbp : Parameters N U (b.comap hostRegisters) :=
+    parameters_of_regs hyp (fun i _ _ _ => hbr i)
+  obtain ⟨c, hc, hcans, hchit, hcm⟩ := hsolver (b.comap solverRegisters) x.mem
+    (hb0.trans hyp.side) (hb1.trans hyp.filler) (hb2.trans hyp.ab)
+    (hb3.trans hyp.bc) (hb4.trans hyp.ac) (hb5.trans hyp.free)
+    (hbm.trans ham)
+  let z := c.extend solverRegisters b
+  have hz : ExecWithin (w + 2) (solver.rename solverRegisters) b z T :=
+    hc.rename solver_injective
+  have hzr (i : Fin 64) : z.regs (hostRegisters i) = b.regs (hostRegisters i) := by
+    apply hz.regs_eq
+    apply Code.preserves_rename_of_forall_ne
+    intro j he
+    have hv := congrArg Fin.val he
+    dsimp only [solverRegisters, hostRegisters] at hv
+    have := i.isLt
+    omega
+  have hzp : Parameters N U (z.comap hostRegisters) :=
+    parameters_of_regs hbp (fun i _ _ _ => hzr i)
+  have hzsi : z.regs (hostRegisters inst) = s :=
+    (hzr inst).trans ((hbr inst).trans hysi)
+  have hzf : z.regs (hostRegisters found) = x.regs (hostRegisters found) :=
+    (hzr found).trans ((hbr found).trans hyf)
+  have hza : z.regs (callRegisters 6) = c.regs (solverArg 6) :=
+    solver_injective.extend_apply _ _ _
+  have hinc : Fits (w + 2) (s + 1) := hsize.of_le (by
+    have := Nat.le_mul_self (sideLength N)
+    omega)
+  obtain ⟨q, hq, hqi, hqf, hqr, hqm⟩ := exec_finish z hzp.one hzsi hinc
+  have hqp : Parameters N U (q.comap hostRegisters) :=
+    parameters_of_regs hzp (fun i _ hi hf => hqr i hi hf)
+  refine ⟨q, ?_, hqp, hqi, ?_, ?_, ?_⟩
+  · exact (hy.seq (hb.seq (hz.seq hq))).mono (by omega)
+  · rw [hqf, hza, hzf]
+    split_ifs <;> omega
+  · rw [hqf, hza, hzf]
+    by_cases h : c.regs (solverArg 6) = 1
+    · simp only [h, ↓reduceIte, hchit.mp h, or_true]
+    · simp only [h, ↓reduceIte, hchit.not.mp h, or_false]
+  · intro a ha
+    rw [hqm]
+    exact hcm a ha
+
+/-- The complete native instance loop. Its invariant records exactly the instances already
+examined, retains the original input, and charges every solver call and loop instruction. -/
+theorem exec_loop {w r N U T : ℕ} (μ : ℕ → ℤ)
+    (solver : Code .standard (r + 7)) (x : Data (64 + (r + 7)))
+    (hp : Parameters N U (x.comap hostRegisters))
+    (hi : x.regs (hostRegisters inst) = 0) (hf : x.regs (hostRegisters found) = 0)
+    (hmem : ∀ i < N, x.mem (1 + i) = encode (μ i))
+    (hidx : ∀ s < 2 * sideLength N,
+      GenericRAM.Signed.Fits w ((2 * (sideLength N * sideLength N) + s + 1 : ℕ) : ℤ))
+    (hF : GenericRAM.Signed.Fits w (2 * (U : ℤ) + 1))
+    (hnF : GenericRAM.Signed.Fits w (-(2 * (U : ℤ) + 1)))
+    (hμ : ∀ i < N, GenericRAM.Signed.Fits w (μ i))
+    (hsize : Fits (w + 2) (N + 1 + 3 * (sideLength N * sideLength N)))
+    (hsolver : ∀ s < 2 * sideLength N, ∀ (a : Data (r + 7)) (mem : ℕ → ℕ),
+      a.regs (solverArg 0) = sideLength N → a.regs (solverArg 1) = 2 * U + 1 →
+      a.regs (solverArg 2) = N + 1 →
+      a.regs (solverArg 3) = N + 1 + sideLength N * sideLength N →
+      a.regs (solverArg 4) = N + 1 + 2 * (sideLength N * sideLength N) →
+      a.regs (solverArg 5) = N + 1 + 3 * (sideLength N * sideLength N) →
+      a.mem = (instanceArgs N U s μ).filled mem (sideLength N * sideLength N) →
+      ∃ b, ExecWithin (w + 2) solver a b T ∧ b.regs (solverArg 6) ≤ 1 ∧
+        (b.regs (solverArg 6) = 1 ↔ hit N U s μ) ∧
+        (∀ a < N + 1, b.mem a = mem a)) :
+    ∃ y, ExecWithin (w + 2) (loop solver) x y
+        (2 * sideLength N * (131 * (sideLength N * sideLength N) + T + 25) + 2) ∧
+      Parameters N U (y.comap hostRegisters) ∧
+      y.regs (hostRegisters inst) = 2 * sideLength N ∧
+      y.regs (hostRegisters found) ≤ 1 ∧
+      (y.regs (hostRegisters found) = 1 ↔ ∃ s < 2 * sideLength N, hit N U s μ) ∧
+      (∀ a < N + 1, y.mem a = x.mem a) := by
+  let I (y : Data (64 + (r + 7))) : Prop :=
+    Parameters N U (y.comap hostRegisters) ∧
+      y.regs (hostRegisters inst) ≤ 2 * sideLength N ∧
+      y.regs (hostRegisters found) ≤ 1 ∧
+      (y.regs (hostRegisters found) = 1 ↔ ∃ s < y.regs (hostRegisters inst), hit N U s μ) ∧
+      (∀ a < N + 1, y.mem a = x.mem a)
+  have hbody (y : Data (64 + (r + 7))) (hy : I y)
+      (hc : (Cond.lt (hostRegisters inst) (hostRegisters stop)).Holds y) :
+      ∃ z, ExecWithin (w + 2) (round solver) y z
+          (131 * (sideLength N * sideLength N) + T + 23) ∧ I z ∧
+        2 * sideLength N - z.regs (hostRegisters inst) <
+          2 * sideLength N - y.regs (hostRegisters inst) := by
+    obtain ⟨hyp, hys, hyf, hyans, hym⟩ := hy
+    have hlt : y.regs (hostRegisters inst) < 2 * sideLength N := by
+      change y.regs (hostRegisters inst) < y.regs (hostRegisters stop) at hc
+      exact hc.trans_eq hyp.stop
+    have hyinput : ∀ i < N, y.mem (1 + i) = encode (μ i) := by
+      intro i hi
+      rw [hym _ (by omega)]
+      exact hmem i hi
+    obtain ⟨z, hz, hzp, hzsi, hzf, hzans, hzm⟩ := exec_round μ solver y hyp rfl hlt
+      hyf hyinput (hidx _ hlt) hF hnF hμ hsize (hsolver _ hlt)
+    refine ⟨z, hz, ⟨hzp, by omega, hzf, ?_, ?_⟩, by omega⟩
+    · rw [hzans, hyans, hzsi]
+      constructor
+      · rintro (⟨s, hs, hh⟩ | hh)
+        · exact ⟨s, by omega, hh⟩
+        · exact ⟨_, by omega, hh⟩
+      · rintro ⟨s, hs, hh⟩
+        by_cases h : s < y.regs (hostRegisters inst)
+        · exact Or.inl ⟨s, h, hh⟩
+        · have he : s = y.regs (hostRegisters inst) := by omega
+          exact Or.inr (he ▸ hh)
+    · intro a ha
+      exact (hzm a ha).trans (hym a ha)
+  have hx : I x := ⟨hp, by omega, by omega, by simp [hi, hf], fun _ _ => rfl⟩
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => 2 * sideLength N - y.regs (hostRegisters inst)) hbody hx
+  obtain ⟨hyp, hyi, hyf, hyans, hym⟩ := hy
+  have hend : y.regs (hostRegisters inst) = 2 * sideLength N := by
+    change ¬y.regs (hostRegisters inst) < y.regs (hostRegisters stop) at hc
+    have hstop : y.regs (hostRegisters stop) = 2 * sideLength N := hyp.stop
+    omega
+  refine ⟨y, ?_, hyp, hend, hyf, ?_, hym⟩
+  · simpa only [loop, hi, Nat.sub_zero, Nat.add_assoc, Nat.reduceAdd] using he
+  · simpa only [hend] using hyans
+
+end Cslib.Algorithms.WordRAM.ThreeSum.Host
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/Host/Prepare.lean b/Complexity/Algorithms/WordRAM/ThreeSum/Host/Prepare.lean
new file mode 100644
index 0000000000..4c1806cb83
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/Host/Prepare.lean
@@ -0,0 +1,249 @@
+/-
+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.ThreeSum.ChanHe.Parameters
+public import Complexity.Algorithms.WordRAM.ThreeSum.Fill
+public import Complexity.Computability.WordRAM.RegisterFrame
+
+/-!
+# Preparing the native Convolution-3SUM host
+
+The host reads the standard length header and computes a polynomial magnitude bound using the
+existing native parameter program. It then computes the matrix side and consecutive matrix
+addresses. The parameter program's additional computations are included in the instruction count.
+
+This directly adapts the setup of Anthropic's pinned
+[`c3Body`](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/Convolution/Host.lean).
+The complete reduction must also fill every instance and invoke a concrete certified solver.
+
+## Main definitions
+
+* `Host.Parameters`: the prepared register interface.
+* `Host.prepare`: native header, magnitude, square-root and layout computation.
+
+## Main results
+
+* `Host.exec_prepare`: exact prepared parameters and a charged setup bound.
+
+## References
+
+* [V. Vassilevska Williams and R. Williams, *Finding, minimizing, and counting weighted
+  subgraphs*][VassilevskaWilliamsWilliams2013]
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.Host
+
+open Cslib.WordRAM
+
+/-- Input length. -/
+abbrev len : Fin 64 := 34
+/-- Polynomial magnitude bound. -/
+abbrev upper : Fin 64 := 35
+/-- Input base address. -/
+abbrev base : Fin 64 := 36
+/-- AB matrix base address. -/
+abbrev matAB : Fin 64 := 37
+/-- BC matrix base address. -/
+abbrev matBC : Fin 64 := 38
+/-- AC matrix base address. -/
+abbrev matAC : Fin 64 := 39
+/-- Solver workspace starts after the three matrices. -/
+abbrev free : Fin 64 := 40
+/-- Number of vertices per part. -/
+abbrev side : Fin 64 := 41
+/-- Current instance number. -/
+abbrev inst : Fin 64 := 42
+/-- Number of instances. -/
+abbrev stop : Fin 64 := 43
+/-- Accumulated Boolean verdict. -/
+abbrev found : Fin 64 := 44
+/-- Constant one. -/
+abbrev one : Fin 64 := 45
+/-- Unsigned filler magnitude. -/
+abbrev filler : Fin 64 := 47
+/-- Signed-encoded positive filler. -/
+abbrev encodedFiller : Fin 64 := 48
+/-- Number of entries per matrix. -/
+abbrev area : Fin 64 := 49
+/-- Square-root argument. -/
+abbrev sqrtArg : Fin 64 := 28
+/-- Square-root output. -/
+abbrev sqrtRoot : Fin 64 := 29
+
+/-- Register embedding for the existing parameter routine. -/
+def parameterRegisters (i : Fin 24) : Fin 64 := ⟨i.val, by omega⟩
+
+/-- Register embedding for successive squares. -/
+def sqrtRegisters (i : Fin 6) : Fin 64 := ⟨28 + i.val, by omega⟩
+
+private theorem parameter_injective : parameterRegisters.Injective := by
+  intro i j h
+  exact Fin.ext (congrArg (fun k : Fin 64 => k.val) h)
+
+private theorem sqrt_injective : sqrtRegisters.Injective := by
+  intro i j h
+  apply Fin.ext
+  have := congrArg Fin.val h
+  dsimp only [sqrtRegisters] at this
+  omega
+
+/-- The mathematical side length used by the reduction. -/
+abbrev sideLength (N : ℕ) : ℕ := Nat.sqrt N + 1
+
+/-- Parameters retained throughout the instance loop. -/
+structure Parameters (N U : ℕ) (x : Data 64) : Prop where
+  /-- Input length. -/
+  len : x.regs len = N
+  /-- Magnitude bound. -/
+  upper : x.regs upper = U
+  /-- Input starts after the length header. -/
+  base : x.regs base = 1
+  /-- AB follows the input. -/
+  ab : x.regs matAB = N + 1
+  /-- BC follows AB. -/
+  bc : x.regs matBC = N + 1 + sideLength N * sideLength N
+  /-- AC follows BC. -/
+  ac : x.regs matAC = N + 1 + 2 * (sideLength N * sideLength N)
+  /-- Solver scratch follows AC. -/
+  free : x.regs free = N + 1 + 3 * (sideLength N * sideLength N)
+  /-- Side length. -/
+  side : x.regs side = sideLength N
+  /-- Two instances per possible low-index sum. -/
+  stop : x.regs stop = 2 * sideLength N
+  /-- Positive invalid-index filler. -/
+  filler : x.regs filler = 2 * U + 1
+  /-- Sign-and-magnitude representation of that filler. -/
+  encodedFiller : x.regs encodedFiller = 4 * U + 2
+  /-- Loop increment. -/
+  one : x.regs one = 1
+
+/-- Input-length output of the parameter bank. -/
+abbrev parameterLen : Fin 64 := 0
+/-- Magnitude output of the parameter bank. -/
+abbrev parameterUpper : Fin 64 := 1
+
+/-- Copy the two needed parameter outputs and initialize constants. -/
+def setup : Code .standard 64 := ram[
+  len ← parameterLen; upper ← parameterUpper;
+  base ← #1; one ← #1; sqrtArg ← len ]
+
+/-- Consecutive output blocks and the two loop counters. -/
+def layout : Code .standard 64 := ram[
+  side ← sqrtRoot + one; area ← side * side; stop ← side + side;
+  matAB ← base + len; matBC ← matAB + area; matAC ← matBC + area; free ← matAC + area;
+  filler ← upper + upper; filler ← filler + one; encodedFiller ← filler + filler;
+  inst ← #0; found ← #0 ]
+
+/-- All initialization consists of actual native subprograms and charged register operations. -/
+def prepare (κ : ℕ) : Code .standard 64 :=
+  .seq ((ChanHe.Parameters.program κ).rename parameterRegisters)
+    (.seq setup (.seq (NatSqrt.program.rename sqrtRegisters) layout))
+
+private theorem exec_layout {w N U : ℕ} (x : Data 64)
+    (hN : x.regs len = N) (hU : x.regs upper = U) (hb : x.regs base = 1)
+    (ho : x.regs one = 1)
+    (hr : x.regs sqrtRoot = Nat.sqrt N)
+    (hsize : Fits w (N + 1 + 3 * (sideLength N * sideLength N)))
+    (hfill : Fits w (4 * U + 2)) :
+    ∃ y, ExecWithin w layout x y 12 ∧ Parameters N U y ∧
+      y.regs inst = 0 ∧ y.regs found = 0 ∧ y.mem = x.mem := by
+  let t := sideLength N
+  have ht : Fits w t := hsize.of_le (by have := Nat.le_mul_self t; dsimp [t] at *; omega)
+  have ha : Fits w (t * t) := hsize.of_le (by dsimp [t] at *; omega)
+  have hs : Fits w (t + t) := hsize.of_le (by have := Nat.le_mul_self t; dsimp [t] at *; omega)
+  have hab : Fits w (1 + N) := hsize.of_le (by omega)
+  have hbc : Fits w (1 + N + t * t) := hsize.of_le (by dsimp [t] at *; omega)
+  have hac : Fits w (1 + N + t * t + t * t) := hsize.of_le (by dsimp [t] at *; omega)
+  have hfree : Fits w (1 + N + t * t + t * t + t * t) :=
+    hsize.of_le (by dsimp [t] at *; omega)
+  have hu2 : Fits w (U + U) := hfill.of_le (by omega)
+  have hu1 : Fits w (U + U + 1) := hfill.of_le (by omega)
+  have hu4 : Fits w (U + U + 1 + (U + U + 1)) := hfill.of_le (by omega)
+  refine ⟨?y, ?run, ?parameters, ?counter, ?found, ?memory⟩
+  case run =>
+    ram_eval [layout, hr, ho, hN, hU, hb, ht, ha, hs, hab, hbc, hac, hfree,
+      hu2, hu1, hu4, t, sideLength, len, upper, base, matAB, matBC, matAC,
+      free, side, inst, stop, found, one, filler, encodedFiller, area, sqrtRoot, Fin.mk.injEq]
+  case parameters =>
+    constructor <;>
+      simp +decide [Data.set_regs, len, upper, base, matAB,
+        matBC, matAC, free, side, stop, filler, encodedFiller, one,
+        hN, hU, hb, ho, sideLength] <;> omega
+  case counter => simp [inst]
+  case found => simp
+  case memory => rfl
+
+/-- Exact initialization from the ordinary length header. The existing parameter program
+computes `U = (N+2)^κ`; its entire execution is charged, including the unused extra parameters.
+The additional fit premises cover matrix addresses and the encoded filler, and are independent
+of any solver execution contract. -/
+theorem exec_prepare {w : ℕ} (κ : ℕ) (x : Data 64)
+    (hbudget : Fits w (ChanHe.Parameters.Math.budget (x.mem 0) ((x.mem 0 + 2) ^ κ)))
+    (hsize : Fits w (x.mem 0 + 1 + 3 * (sideLength (x.mem 0) * sideLength (x.mem 0))))
+    (hfill : Fits w (4 * ((x.mem 0 + 2) ^ κ) + 2)) :
+    ∃ y, ExecWithin w (prepare κ) x y
+        (ChanHe.Parameters.time κ (x.mem 0) ((x.mem 0 + 2) ^ κ) +
+          5 * Nat.sqrt (x.mem 0) + 24) ∧
+      Parameters (x.mem 0) ((x.mem 0 + 2) ^ κ) y ∧
+      y.regs inst = 0 ∧ y.regs found = 0 ∧ y.mem = x.mem := by
+  let N := x.mem 0
+  let U := (N + 2) ^ κ
+  obtain ⟨p, hp, hout, hm⟩ := ChanHe.Parameters.exec κ (x.comap parameterRegisters) hbudget
+  let a := p.extend parameterRegisters x
+  have ha := hp.rename parameter_injective
+  have han : a.regs parameterLen = N :=
+    (parameter_injective.extend_apply _ _ ChanHe.Parameters.len).trans hout.len
+  have hau : a.regs parameterUpper = U :=
+    (parameter_injective.extend_apply _ _ ChanHe.Parameters.magnitude).trans hout.magnitude
+  have ham : a.mem = x.mem := hm
+  have h1 : Fits w 1 := hfill.of_le (by omega)
+  let b := a.set len N |>.set upper U |>.set base 1 |>.set one 1
+    |>.set sqrtArg N
+  have hb : ExecWithin w setup a b 5 := by
+    ram_eval [setup, b, han, hau, h1, parameterLen, parameterUpper, len, upper, base,
+      one, sqrtArg, Fin.mk.injEq]
+  have hbn : b.regs sqrtArg = N := by simp [b]
+  have hsqrt : Fits w (4 * b.regs sqrtArg + 4) := hbudget.of_le (by
+    rw [hbn]
+    change 4 * N + 4 ≤ ChanHe.Parameters.Math.budget N U
+    dsimp [ChanHe.Parameters.Math.budget]
+    omega)
+  obtain ⟨c, hc, hcr, -, hcm, -⟩ := NatSqrt.exec_rename sqrtRegisters sqrt_injective b hsqrt
+  have hpres (i : Fin 64) (hi : 34 ≤ i.val) : c.regs i = b.regs i := by
+    apply hc.regs_eq
+    apply Code.preserves_rename_of_forall_ne
+    intro j he
+    have hv := congrArg Fin.val he
+    dsimp only [sqrtRegisters] at hv
+    have := j.isLt
+    omega
+  have hcr' : c.regs sqrtRoot = Nat.sqrt N := by
+    change c.regs sqrtRoot = Nat.sqrt (b.regs sqrtArg) at hcr
+    simpa only [hbn] using hcr
+  have hc' : ExecWithin w (NatSqrt.program.rename sqrtRegisters) b c
+      (5 * Nat.sqrt N + 7) := by
+    change ExecWithin w _ b c (5 * Nat.sqrt (b.regs sqrtArg) + 7) at hc
+    simpa only [hbn] using hc
+  obtain ⟨y, hy, hparams, hi, hf, hym⟩ := exec_layout (N := N) (U := U) c
+    ((hpres len (by decide)).trans (by
+      simp +decide [b, N, U, len, sqrtArg, one, base, upper]))
+    ((hpres upper (by decide)).trans (by
+      simp +decide [b, N, U, upper, sqrtArg, one, base]))
+    ((hpres base (by decide)).trans (by simp +decide [b, base, sqrtArg, one]))
+    ((hpres one (by decide)).trans (by simp +decide [b, one, sqrtArg]))
+    hcr' hsize hfill
+  refine ⟨y, ?_, hparams, hi, hf, hym.trans (hcm.trans ham)⟩
+  convert ha.seq (hb.seq (hc'.seq hy)) using 1
+  · rfl
+  · simp only [Data.comap_mem, N]
+    omega
+
+end Cslib.Algorithms.WordRAM.ThreeSum.Host
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/Host/Program.lean b/Complexity/Algorithms/WordRAM/ThreeSum/Host/Program.lean
new file mode 100644
index 0000000000..c712759ac9
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/Host/Program.lean
@@ -0,0 +1,158 @@
+/-
+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.ThreeSum.Host.Loop
+public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Width
+public import Complexity.Computability.WordRAM.Compile
+
+/-!
+# The complete native Convolution-3SUM host
+
+The host computes its parameters from the ordinary input header, constructs every instance,
+executes the supplied finite solver program in a disjoint register bank, accumulates its answer,
+and halts. The source word width is logarithmic for polynomially bounded integer inputs.
+
+This is a conditional native reduction: the caller must prove execution, correctness and input
+preservation of the actual solver code at the stated width and charged budget. The host does not
+supply a fast Exact Triangle solver or finish the subquadratic 3SUM endpoint.
+
+The construction directly adapts Anthropic's pinned
+[`c3Body`](https://github.com/anthropics/formal-math/blob/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem21a/Convolution/Host.lean).
+
+## Main definitions
+
+* `Host.body`: initialization and the complete native instance loop.
+* `Host.time`: charged time, including the final halt.
+
+## Main results
+
+* `Host.runs_input`: actual initialized native execution, output and input preservation.
+
+## References
+
+* [V. Vassilevska Williams and R. Williams, *Finding, minimizing, and counting weighted
+  subgraphs*][VassilevskaWilliamsWilliams2013]
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.Host
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.ThreeSum
+
+/-- The code depends only on the fixed magnitude exponent and the supplied finite solver. -/
+def body {r : ℕ} (κ : ℕ) (solver : Code .standard (r + 7)) :
+    Code .standard (64 + (r + 7)) :=
+  .seq ((prepare κ).rename hostRegisters) (loop solver)
+
+/-- Complete charged instruction budget, including the halt and every solver invocation. -/
+def time (κ N T : ℕ) : ℕ :=
+  ChanHe.Parameters.time κ N ((N + 2) ^ κ) + 5 * Nat.sqrt N + 27 +
+    2 * sideLength N * (131 * (sideLength N * sideLength N) + T + 25)
+
+/-- Solver time is multiplied by `2t`; all host work is `Oκ((N+1)t + log(N+2))`. -/
+theorem time_bound (κ N T : ℕ) : time κ N T ≤
+    2 * sideLength N * T + 1000 * (N + 1) * sideLength N +
+      (400 * κ + 3000) * Nat.clog 2 (N + 2) := by
+  have hp := ChanHe.Parameters.time_bound κ N
+  have ha := area_le N
+  have ht : 1 ≤ sideLength N := by dsimp [sideLength]; omega
+  have hmul := Nat.mul_le_mul_left (262 * sideLength N) ha
+  dsimp only [time]
+  dsimp only [sideLength] at *
+  nlinarith
+
+/-- Native initialized execution at target width `w+2`. The execution witness identifies the
+actual pre-halt state containing the output. The sole solver premise is an execution theorem
+for the concrete `solver` argument, on the matrices the host actually constructs. -/
+theorem runs_input {κ w r T : ℕ} (input : List ℤ) (solver : Code .standard (r + 7))
+    (hw : width κ input.length ≤ w)
+    (hvalues : ∀ z ∈ input, |z| ≤ ((input.length + 2) ^ κ : ℕ))
+    (hsolver : let N := input.length; let U := (N + 2) ^ κ;
+      let μ : ℕ → ℤ := fun i => input.getD i 0;
+      ∀ s < 2 * sideLength N, ∀ (a : Data (r + 7)) (mem : ℕ → ℕ),
+      a.regs (solverArg 0) = sideLength N → a.regs (solverArg 1) = 2 * U + 1 →
+      a.regs (solverArg 2) = N + 1 →
+      a.regs (solverArg 3) = N + 1 + sideLength N * sideLength N →
+      a.regs (solverArg 4) = N + 1 + 2 * (sideLength N * sideLength N) →
+      a.regs (solverArg 5) = N + 1 + 3 * (sideLength N * sideLength N) →
+      a.mem = (instanceArgs N U s μ).filled mem (sideLength N * sideLength N) →
+      ∃ b, ExecWithin (w + 2) solver a b T ∧ b.regs (solverArg 6) ≤ 1 ∧
+        (b.regs (solverArg 6) = 1 ↔ hit N U s μ) ∧
+        (∀ a < N + 1, b.mem a = mem a)) :
+    ∃ y t, t ≤ time κ input.length T ∧
+      Runs (w + 2) ((body κ solver).program (hostRegisters found))
+        (State.init (input.map encode)) ⟨(body κ solver).size, y⟩ (t - 1) ∧
+      Executes (w + 2) ((body κ solver).program (hostRegisters found))
+        (State.init (input.map encode)) (y.regs (hostRegisters found)) t ∧
+      y.regs (hostRegisters found) ≤ 1 ∧
+      (y.regs (hostRegisters found) = 1 ↔
+        Convolution input.length (fun i => input.getD i 0)) ∧
+      (∀ a < input.length + 1,
+        y.mem a = (Data.init (input.map encode) : Data (64 + (r + 7))).mem a) ∧
+      y.Bounded (w + 2) := by
+  let N := input.length
+  let U := (N + 2) ^ κ
+  let μ : ℕ → ℤ := fun i => input.getD i 0
+  let x : Data (64 + (r + 7)) := Data.init (input.map encode)
+  have hmem : ∀ i < N, x.mem (1 + i) = encode (μ i) := by
+    intro i hi
+    have hm : i < (input.map encode).length := by simpa only [List.length_map] using hi
+    simp only [x, μ, Nat.add_comm 1, Data.init_mem_succ, List.getD_eq_getElem?_getD,
+      List.getElem?_eq_getElem hm,
+      List.getElem?_eq_getElem hi, List.getElem_map, Option.getD_some]
+  have hμ : ∀ i < N, |μ i| ≤ (U : ℤ) := by
+    intro i hi
+    simpa only [μ, U, N, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hi,
+      Option.getD_some] using hvalues input[i] (List.getElem_mem hi)
+  have hpw : ChanHe.Parameters.width κ N ≤ w + 2 :=
+    (Nat.le_add_right _ 4).trans ((parameters_width_le κ N).trans (hw.trans (by omega)))
+  have hf := layout_fits hw
+  have hbudget : Fits (w + 2) (ChanHe.Parameters.Math.budget N U) :=
+    ChanHe.Parameters.budget_fits hpw
+  obtain ⟨p, hp, hpp, hpi, hpf, hpm⟩ := exec_prepare κ (x.comap hostRegisters)
+    (by simpa only [x, Data.comap_mem, Data.init_mem_zero, List.length_map] using hbudget)
+    (by simpa only [x, Data.comap_mem, Data.init_mem_zero, List.length_map] using
+      hf.1.mono (show w ≤ w + 2 by omega))
+    (by simpa only [x, Data.comap_mem, Data.init_mem_zero, List.length_map] using
+      hf.2.mono (show w ≤ w + 2 by omega))
+  simp only [Data.comap_mem, x, Data.init_mem_zero, List.length_map] at hp hpp
+  let a := p.extend hostRegisters x
+  have ha := hp.rename (hostRegisters_injective (r := r + 7))
+  have hac : a.comap hostRegisters = p := Data.comap_extend hostRegisters_injective _ _
+  have hap : Parameters N U (a.comap hostRegisters) := by rw [hac]; exact hpp
+  have hai : a.regs (hostRegisters inst) = 0 :=
+    hostRegisters_injective.extend_apply _ _ _ |>.trans hpi
+  have haf : a.regs (hostRegisters found) = 0 :=
+    hostRegisters_injective.extend_apply _ _ _ |>.trans hpf
+  have ham : a.mem = x.mem := hpm
+  have hinput : ∀ i < N, a.mem (1 + i) = encode (μ i) := by
+    intro i hi
+    rw [ham]
+    exact hmem i hi
+  obtain ⟨y, hy, -, -, hyf, hyans, hym⟩ := exec_loop μ solver a hap hai haf hinput
+    (fun s hs => index_fits hw hs) (filler_fits hw).1 (filler_fits hw).2
+    (fun i hi => value_fits hw (hμ i hi))
+    (hf.1.mono (show w ≤ w + 2 by omega)) hsolver
+  have hans : y.regs (hostRegisters found) = 1 ↔ Convolution N μ :=
+    hyans.trans (convolution_iff_sqrt (U := (U : ℤ)) (by positivity) hμ).symm
+  obtain ⟨n, hn, he⟩ := ha.seq hy
+  have hr := he.runs (pc := 0) (p := (body κ solver).program (hostRegisters found))
+    (Program.Contains.self _).append_left
+  have hi := ChanHe.Parameters.inputFits input hpw hvalues
+  refine ⟨y, n + 1, ?_, ?_, he.executes (hostRegisters found), hyf, hans, ?_, ?_⟩
+  · dsimp only [time, N] at hn ⊢
+    omega
+  · simpa only [Nat.add_sub_cancel, Nat.zero_add, body, State.init] using hr
+  · intro a ha
+    exact (hym a ha).trans (congrFun ham a)
+  · exact hr.bounded_init hi
+
+end Cslib.Algorithms.WordRAM.ThreeSum.Host
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/Host/Width.lean b/Complexity/Algorithms/WordRAM/ThreeSum/Host/Width.lean
new file mode 100644
index 0000000000..6a9a537552
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/Host/Width.lean
@@ -0,0 +1,123 @@
+/-
+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.ThreeSum.Host.Prepare
+
+/-!
+# A logarithmic word width for the Convolution-3SUM host
+
+The existing parameter program's polynomial budget also bounds the host's matrix addresses,
+signed indices and filler. Four extra source bits suffice. These bounds cover the host;
+the concrete solver must separately prove its own execution at the target width.
+
+## Main definitions
+
+* `Host.width`: a positive logarithmic source-width threshold.
+
+## Main results
+
+* `Host.layout_fits`: all matrix addresses and the encoded filler fit.
+* `Host.index_fits`, `Host.filler_fits`: the signed matrix-builder premises.
+* `Host.value_fits`: polynomially bounded input values fit the signed source width.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.Host
+
+open Cslib.WordRAM
+
+/-- Source width; the signed arithmetic kernels use unsigned target words of width `w+2`. -/
+def width (κ N : ℕ) : ℕ := (20 * κ + 125) * Nat.clog 2 (N + 2)
+
+/-- The threshold includes the empty input and magnitude exponent zero. -/
+theorem width_pos (κ N : ℕ) : 0 < width κ N := by
+  have := Nat.clog_pos (b := 2) (by decide) (show 1 < N + 2 by omega)
+  dsimp [width]
+  positivity
+
+/-- The host has at least four more source bits than the parameter routine requires. -/
+theorem parameters_width_le (κ N : ℕ) : ChanHe.Parameters.width κ N + 4 ≤ width κ N := by
+  have := Nat.clog_pos (b := 2) (by decide) (show 1 < N + 2 by omega)
+  dsimp [width, ChanHe.Parameters.width]
+  nlinarith
+
+private theorem margin_fits {κ N w : ℕ} (hw : width κ N ≤ w) :
+    Fits (w - 1) (8 * ChanHe.Parameters.Math.budget N ((N + 2) ^ κ)) := by
+  have hf := ChanHe.Parameters.budget_fits (κ := κ) (n := N) (w := ChanHe.Parameters.width κ N)
+    (Nat.le_refl _)
+  have hwidth := (parameters_width_le κ N).trans hw
+  have hmul : 8 * ChanHe.Parameters.Math.budget N ((N + 2) ^ κ) <
+      8 * 2 ^ ChanHe.Parameters.width κ N := Nat.mul_lt_mul_of_pos_left hf (by decide)
+  apply hmul.trans_le
+  calc
+    _ = 2 ^ (ChanHe.Parameters.width κ N + 3) := by rw [pow_add]; norm_num; omega
+    _ ≤ 2 ^ (w - 1) := Nat.pow_le_pow_right (by decide) (by omega)
+
+private theorem signed_fits {κ N w : ℕ} (hw : width κ N ≤ w) (z : ℤ)
+    (hz : |z| ≤ (8 * ChanHe.Parameters.Math.budget N ((N + 2) ^ κ) : ℕ)) :
+    GenericRAM.Signed.Fits w z := by
+  have hf := margin_fits hw
+  have hwpos := width_pos κ N
+  have hpow : (8 * ChanHe.Parameters.Math.budget N ((N + 2) ^ κ) : ℤ) <
+      2 ^ (w - 1) := by exact_mod_cast hf
+  obtain ⟨hlo, hhi⟩ := abs_le.mp hz
+  exact ⟨by omega, by omega, by omega⟩
+
+/-- A linear bound for the number of entries per generated matrix. -/
+theorem area_le (N : ℕ) : sideLength N * sideLength N ≤ 3 * N + 1 := by
+  have := Nat.sqrt_le N
+  have := Nat.sqrt_le_self N
+  dsimp [sideLength]
+  nlinarith
+
+/-- All three matrix blocks and their one-past-end addresses fit at the source width. -/
+theorem layout_fits {κ N w : ℕ} (hw : width κ N ≤ w) :
+    Fits w (N + 1 + 3 * (sideLength N * sideLength N)) ∧
+      Fits w (4 * (N + 2) ^ κ + 2) := by
+  have hf := (margin_fits hw).mono (show w - 1 ≤ w by omega)
+  have ha := area_le N
+  constructor <;> apply hf.of_le <;> dsimp [ChanHe.Parameters.Math.budget] <;> omega
+
+/-- The builder's positive and negative filler fit the signed source range. -/
+theorem filler_fits {κ N w : ℕ} (hw : width κ N ≤ w) :
+    GenericRAM.Signed.Fits w (2 * ((N + 2) ^ κ : ℕ) + 1) ∧
+      GenericRAM.Signed.Fits w (-(2 * ((N + 2) ^ κ : ℕ) + 1)) := by
+  have hbound : |(2 * ((N + 2) ^ κ : ℕ) + 1 : ℤ)| ≤
+      (8 * ChanHe.Parameters.Math.budget N ((N + 2) ^ κ) : ℕ) := by
+    rw [abs_of_nonneg (by positivity)]
+    exact_mod_cast (show 2 * (N + 2) ^ κ + 1 ≤
+      8 * ChanHe.Parameters.Math.budget N ((N + 2) ^ κ) from by
+        dsimp [ChanHe.Parameters.Math.budget]
+        omega)
+  exact ⟨signed_fits hw _ hbound, signed_fits hw _ (by simpa only [abs_neg] using hbound)⟩
+
+/-- Every signed input index computed in a generated instance fits. -/
+theorem index_fits {κ N w s : ℕ} (hw : width κ N ≤ w) (hs : s < 2 * sideLength N) :
+    GenericRAM.Signed.Fits w ((2 * (sideLength N * sideLength N) + s + 1 : ℕ) : ℤ) := by
+  apply signed_fits hw
+  rw [abs_of_nonneg (by positivity)]
+  have ha := area_le N
+  have ht := Nat.sqrt_le_self N
+  dsimp only [sideLength] at hs
+  exact_mod_cast (show 2 * (sideLength N * sideLength N) + s + 1 ≤
+    8 * ChanHe.Parameters.Math.budget N ((N + 2) ^ κ) from by
+      dsimp [ChanHe.Parameters.Math.budget]
+      omega)
+
+/-- A polynomial magnitude bound implies the signed source fit premise. -/
+theorem value_fits {κ N w : ℕ} (hw : width κ N ≤ w) {z : ℤ}
+    (hz : |z| ≤ ((N + 2) ^ κ : ℕ)) : GenericRAM.Signed.Fits w z := by
+  apply signed_fits hw z
+  have hb : (N + 2) ^ κ ≤ 8 * ChanHe.Parameters.Math.budget N ((N + 2) ^ κ) := by
+    dsimp [ChanHe.Parameters.Math.budget]
+    omega
+  exact hz.trans (by exact_mod_cast hb)
+
+end Cslib.Algorithms.WordRAM.ThreeSum.Host
diff --git a/Complexity/Computability/WordRAM/RegisterFrame.lean b/Complexity/Computability/WordRAM/RegisterFrame.lean
new file mode 100644
index 0000000000..54de876e2d
--- /dev/null
+++ b/Complexity/Computability/WordRAM/RegisterFrame.lean
@@ -0,0 +1,39 @@
+/-
+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.Computability.WordRAM.Structured
+
+/-!
+# Register frames for renamed native programs
+
+## Main results
+
+* `Code.preserves_rename_of_forall_ne`: registers outside an embedded register bank are
+  preserved without unfolding the subroutine's instruction graph.
+-/
+
+public section
+
+namespace Cslib.WordRAM
+
+/-- A renamed subroutine cannot write a register outside the image of its register embedding.
+This generalizes the former private framing rule of the fusion-node register banks. -/
+theorem Code.preserves_rename_of_forall_ne {B : Basis} {r r' : ℕ}
+    (c : Code B r) (f : Fin r → Fin r') (i : Fin r') (hi : ∀ j, f j ≠ i) :
+    (c.rename f).Preserves i := by
+  induction c with
+  | op o =>
+    cases o <;> simp only [Code.rename, Code.Preserves, Op.rename, Op.dest,
+      ne_eq, Option.some.injEq, reduceCtorEq, not_false_eq_true] <;> apply hi
+  | seq a b iha ihb => exact ⟨iha, ihb⟩
+  | branch cond pos neg ihp ihn => exact ⟨ihp, ihn⟩
+  | loop cond body ih => exact ih
+  | rand dst src => simpa only [Code.rename, Code.Preserves] using hi dst
+
+end Cslib.WordRAM
diff --git a/ComplexityTests/ThreeSumHost.lean b/ComplexityTests/ThreeSumHost.lean
new file mode 100644
index 0000000000..8d782fdeaa
--- /dev/null
+++ b/ComplexityTests/ThreeSumHost.lean
@@ -0,0 +1,141 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Algorithms.WordRAM.ThreeSum.Host.Program
+import Mathlib.Tactic.IntervalCases
+
+/-! # Initialized native Convolution-3SUM host clients
+
+The small test solver inspects only the first cell of each matrix. Its correctness is certified
+below only for the empty input and the listed singleton inputs. It is not a general Exact
+Triangle solver. These clients check that the host's conditional execution theorem is usable.
+-/
+
+namespace ComplexityTests.ThreeSumHost
+
+open Cslib WordRAM WordRAM.Signed
+open Algorithms.WordRAM.ThreeSum
+open Algorithms.ThreeSum
+
+private abbrev ab : Fin 7 := 2
+private abbrev bc : Fin 7 := 3
+private abbrev ac : Fin 7 := 4
+private abbrev zero : Fin 7 := 5
+private abbrev out : Fin 7 := 6
+
+private def probe : Code .standard 7 := ram[
+  ab ← *ab; bc ← *bc; ac ← *ac; zero ← #0;
+  if ab = zero then [
+    if bc = zero then [
+      if ac = zero then [ out ← #1 ] else [ out ← #0 ]
+    ] else [ out ← #0 ]
+  ] else [ out ← #0 ] ]
+
+private theorem probe_exec {w : ℕ} (x : Data 7) (h1 : Fits w 1) :
+    ∃ y, ExecWithin w probe x y 9 ∧
+      y.regs out = (if x.mem (x.regs ab) = 0 ∧ x.mem (x.regs bc) = 0 ∧
+        x.mem (x.regs ac) = 0 then 1 else 0) ∧ y.mem = x.mem := by
+  let b := if x.mem (x.regs ab) = 0 ∧ x.mem (x.regs bc) = 0 ∧
+    x.mem (x.regs ac) = 0 then 1 else 0
+  let y := x.set ab (x.mem (x.regs ab)) |>.set bc (x.mem (x.regs bc))
+    |>.set ac (x.mem (x.regs ac)) |>.set zero 0 |>.set out b
+  refine ⟨y, ?_, by simp [y, b], rfl⟩
+  by_cases hab : x.mem (x.regs ab) = 0 <;>
+    by_cases hbc : x.mem (x.regs bc) = 0 <;>
+    by_cases hac : x.mem (x.regs ac) = 0 <;>
+    ram_eval [probe, y, b, hab, hbc, hac, h1, ab, bc, ac, zero, out,
+      true_and, false_and, and_true, and_false, Fin.mk.injEq]
+
+/-- Every supplied first-cell answer is charged, and the probe writes no memory. -/
+example {w : ℕ} (x : Data 7) (h1 : Fits w 1) :
+    ∃ y, ExecWithin w probe x y 9 ∧ y.regs out ≤ 1 ∧ y.mem = x.mem := by
+  obtain ⟨y, he, ho, hm⟩ := probe_exec x h1
+  refine ⟨y, he, ?_, hm⟩
+  rw [ho]
+  split_ifs <;> decide
+
+private theorem probe_spec (input : List ℤ)
+    (hinput : input = [] ∨ input = [-1] ∨ input = [0] ∨ input = [1])
+    (w : ℕ) (h1 : Fits (w + 2) 1) :
+    let N := input.length; let U := (N + 2) ^ 0;
+      let μ : ℕ → ℤ := fun i => input.getD i 0;
+      ∀ s < 2 * Host.sideLength N, ∀ (a : Data 7) (mem : ℕ → ℕ),
+      a.regs (Host.solverArg 0) = Host.sideLength N → a.regs (Host.solverArg 1) = 2 * U + 1 →
+      a.regs (Host.solverArg 2) = N + 1 →
+      a.regs (Host.solverArg 3) = N + 1 + Host.sideLength N * Host.sideLength N →
+      a.regs (Host.solverArg 4) = N + 1 + 2 * (Host.sideLength N * Host.sideLength N) →
+      a.regs (Host.solverArg 5) = N + 1 + 3 * (Host.sideLength N * Host.sideLength N) →
+      a.mem = (Host.instanceArgs N U s μ).filled mem (Host.sideLength N * Host.sideLength N) →
+      ∃ b, ExecWithin (w + 2) probe a b 9 ∧ b.regs (Host.solverArg 6) ≤ 1 ∧
+        (b.regs (Host.solverArg 6) = 1 ↔ Host.hit N U s μ) ∧
+        (∀ a < N + 1, b.mem a = mem a) := by
+  dsimp only [Nat.pow_zero]
+  intro s hs a mem ht hF hab hbc hac hfree hm
+  change a.regs ab = _ at hab
+  change a.regs bc = _ at hbc
+  change a.regs ac = _ at hac
+  obtain ⟨y, he, ho, hym⟩ := probe_exec a h1
+  refine ⟨y, he, ?_, ?_, ?_⟩
+  · change y.regs out ≤ 1
+    rw [ho]
+    split_ifs <;> decide
+  · change y.regs out = 1 ↔ _
+    rw [ho, hab, hbc, hac, hm]
+    rcases hinput with rfl | rfl | rfl | rfl
+    all_goals norm_num [Host.sideLength] at hs
+    all_goals interval_cases s <;>
+      norm_num [Host.instanceArgs, Fill.Args.filled, Fill.Args.valueAB, Fill.Args.valueBC,
+        Fill.Args.valueAC, pick, encode, Host.hit, Algorithms.ExactTriangle.HasZeroTriangle,
+        weightAB, weightBC, weightAC] <;> decide
+  · intro k hk
+    rw [hym, hm]
+    apply Fill.Args.outside_filled
+    all_goals dsimp [Host.instanceArgs]; omega
+
+/-- The full quantitative theorem is inhabited for empty, positive and negative singleton
+inputs, and the output witness is the actual native pre-halt state. -/
+example (input : List ℤ)
+    (hinput : input = [] ∨ input = [-1] ∨ input = [0] ∨ input = [1]) :
+    ∃ y t, t ≤ Host.time 0 input.length 9 ∧
+      Runs 252 ((Host.body 0 probe).program (Host.hostRegisters Host.found))
+        (State.init (input.map encode)) ⟨(Host.body 0 probe).size, y⟩ (t - 1) ∧
+      Executes 252 ((Host.body 0 probe).program (Host.hostRegisters Host.found))
+        (State.init (input.map encode)) (y.regs (Host.hostRegisters Host.found)) t ∧
+      (y.regs (Host.hostRegisters Host.found) = 1 ↔
+        Convolution input.length (fun i => input.getD i 0)) ∧ y.mem 0 = input.length := by
+  have hw : Host.width 0 input.length ≤ 250 := by
+    rcases hinput with rfl | rfl | rfl | rfl <;> decide
+  have hv : ∀ z ∈ input, |z| ≤ ((input.length + 2) ^ 0 : ℕ) := by
+    rcases hinput with rfl | rfl | rfl | rfl <;> simp
+  obtain ⟨y, t, ht, hr, he, -, ha, hm, -⟩ :=
+    Host.runs_input input probe hw hv (probe_spec input hinput 250 (by decide))
+  exact ⟨y, t, ht, hr, he, ha,
+    (hm 0 (by omega)).trans (by simp only [Data.init_mem_zero, List.length_map])⟩
+
+section Interpreter
+
+-- Kernel reduction traverses the parameter routine and sixteen fully expanded cell computations.
+set_option maxRecDepth 16384
+
+/-- Actual host execution sees the zero singleton solution. -/
+example : ((Host.body 0 probe).eval 252 10 (.init [encode 0])).map
+    (fun yn => yn.1.regs (Host.hostRegisters Host.found)) = some 1 := by decide
+
+/-- Actual host execution rejects a positive singleton. -/
+example : ((Host.body 0 probe).eval 252 10 (.init [encode 1])).map
+    (fun yn => yn.1.regs (Host.hostRegisters Host.found)) = some 0 := by decide
+
+/-- Actual host execution rejects a negative singleton. -/
+example : ((Host.body 0 probe).eval 252 10 (.init [encode (-1)])).map
+    (fun yn => yn.1.regs (Host.hostRegisters Host.found)) = some 0 := by decide
+
+/-- Empty input constructs only filler matrices and returns false. -/
+example : ((Host.body 0 probe).eval 127 10 (.init [])).map
+    (fun yn => yn.1.regs (Host.hostRegisters Host.found)) = some 0 := by decide
+
+end Interpreter
+
+end ComplexityTests.ThreeSumHost
diff --git a/ComplexityTests/WordRAMChanHeParameters.lean b/ComplexityTests/WordRAMChanHeParameters.lean
new file mode 100644
index 0000000000..f76dec9c15
--- /dev/null
+++ b/ComplexityTests/WordRAMChanHeParameters.lean
@@ -0,0 +1,64 @@
+/-
+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
+
+import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
+
+/-!
+# Executed boundary cases for native Chan–He parameters
+
+The observations include all nine outputs, the instruction count, and input memory cells.
+The generic run clients below discharge the actual input magnitude and width hypotheses.
+-/
+
+-- This module contains only private execution checks.
+set_option linter.privateModule false
+
+open Cslib.WordRAM
+open Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
+
+private def observe (κ : ℕ) (input : List ℤ) : Option (List ℕ × ℕ × List ℕ) :=
+  ((program κ).eval 64 32 (Data.init (input.map Signed.encode))).map fun (x, t) =>
+    ([x.regs len, x.regs magnitude, x.regs digits, x.regs height, x.regs fuel,
+      x.regs want, x.regs primeBound, x.regs packedLen, x.regs padding], t,
+      [x.mem 0, x.mem 1, x.mem 2])
+
+-- Empty input, including the fixed exponent zero.
+example : observe 0 [] = some ([0, 1, 3, 1, 1, 15, 192, 294912, 5], 83, [0, 0, 0]) := by
+  decide
+
+-- One position; the signed encoding of -1 remains in memory.
+example : observe 0 [-1] = some ([1, 1, 3, 1, 1, 30, 372, 1107072, 5], 88, [1, 3, 0]) := by
+  decide
+
+-- Two positions at exponent zero: the ceiling logarithm and fuel increase.
+example : observe 0 [-1, 1] =
+    some ([2, 1, 3, 2, 4, 30, 372, 1107072, 5], 97, [2, 3, 2]) := by
+  decide
+
+-- Nonconstant polynomial magnitude, with both signed boundary values.
+example : observe 1 [-4, 4] =
+    some ([2, 4, 5, 2, 4, 50, 714, 4078368, 17], 110, [2, 9, 8]) := by
+  decide
+
+-- A native contract client, including all width/magnitude hypotheses and all memory framing.
+example : ∃ y t, t ≤ 5 * Nat.sqrt 2 + 3400 * Nat.clog 2 4 ∧
+    Runs 512 ((program 1).program packedLen) (State.init ([(-4 : ℤ), 4].map Signed.encode))
+      ⟨(program 1).size, y⟩ t ∧ Output 2 4 y ∧
+    y.mem = (Data.init ([(-4 : ℤ), 4].map Signed.encode) : Data 24).mem ∧ y.Bounded 512 := by
+  apply runs_input (κ := 1) [(-4 : ℤ), 4] (by decide)
+  intro z hz
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hz
+  rcases hz with rfl | rfl <;> decide
+
+-- The empty-input width remains positive and the final input-init theorem is satisfiable.
+example : 0 < width 0 0 ∧ InputFits 512 (([] : List ℤ).map Signed.encode) := by
+  constructor
+  · decide
+  · apply inputFits (κ := 0) [] (by decide)
+    simp
diff --git a/ROADMAP.md b/ROADMAP.md
index 787b92c9a0..93afea6258 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -443,6 +443,11 @@ each statement against the numbered result. Organize modules by subject, not cha
   almost-surely terminating structured loops; random-tape equivalence and BPP/RP/ZPP simulation
   bridges for the randomized word RAM ([#1124]); transfer of cell-probe lower bounds; and the
   Horn-SAT, 2SAT, matching and domino-tiling clients.
+- **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
+  concrete fast Exact Triangle solver and the full input/time/width/asymptotic reduction remains
+  open under [#1394].
 - **Stateful algorithms and data structures:** Word-RAM controllers for larger adaptive and
   iterative clients, including the two-stack queue and timeline-editing controllers; reusable
   allocation and deallocation, shrinking, and live and peak space accounting; ownership and
@@ -584,4 +589,5 @@ not planned, not as proved.
 [#1442]: https://github.com/cslib-community/complexitylib/issues/1442
 [#1447]: https://github.com/cslib-community/complexitylib/issues/1447
 [#1449]: https://github.com/cslib-community/complexitylib/issues/1449
+[#1524]: https://github.com/cslib-community/complexitylib/issues/1524
 [#1572]: https://github.com/cslib-community/complexitylib/issues/1572
diff --git a/UPSTREAM.md b/UPSTREAM.md
index 153abe289b..a85c0c8843 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -159,7 +159,13 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   at width `w + 2`, excluding the halt; its theorem identifies the three encoded matrices and
   preserves the input. Layout, signed index/filler bounds and target address bounds are explicit.
   The existing signed and unsigned APIs were reused; no source machine or separate run semantics
-  were copied. The full reduction host, native Chan–He preprocessing, fast Exact Triangle and full
+  were copied. `Algorithms/WordRAM/ThreeSum/Host/` adds the complete charged native host: ordinary
+  header initialization, polynomial magnitude computation, square root, consecutive matrix layout,
+  all `2t` instances and a finite solver program in a disjoint register bank. Its initialized run
+  theorem connects the actual pre-halt state to the Convolution-3SUM answer and preserves the input.
+  The host's source-width threshold is `(20κ+125)clog₂(N+2)`; signed kernels use target width `w+2`.
+  This remains conditional on the supplied solver's native execution/correctness/frame theorem;
+  it does not establish a fast solver. Native Chan–He preprocessing, fast Exact Triangle and full
   input/time/width/asymptotic composition remain in
   [#1394](https://github.com/cslib-community/complexitylib/issues/1394), including the improved
   Section 4 route needed for the published exponent 1.9992. Anthropic's copyright and attribution
diff --git a/scripts/heartbeat_allowlist.txt b/scripts/heartbeat_allowlist.txt
index 21b07a202c..d085bb35dc 100644
--- a/scripts/heartbeat_allowlist.txt
+++ b/scripts/heartbeat_allowlist.txt
@@ -3,3 +3,6 @@
 # rejects any budget above the default in a file not listed here, or above its cap, and reports
 # entries that are no longer needed, so this list only shrinks. Add an entry only with review,
 # and link the issue tracking its reduction.
+
+# #1583: split native parameter segment/frame proofs to reach the default budget.
+Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Parameters.lean 300000