diff --git a/Complexity.lean b/Complexity.lean
index cfa5796f19..4d8216846c 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -118,6 +118,8 @@ public import Complexity.Algorithms.WordRAM.PrefixSums.Dynamic
 public import Complexity.Algorithms.WordRAM.PrefixSums.Query
 public import Complexity.Algorithms.WordRAM.PrefixSums.Tree
 public import Complexity.Algorithms.WordRAM.PrefixSums.Update
+public import Complexity.Algorithms.WordRAM.PrimeTable
+public import Complexity.Algorithms.WordRAM.PrimeTrial
 public import Complexity.Algorithms.WordRAM.PriorityQueue.Basic
 public import Complexity.Algorithms.WordRAM.PriorityQueue.BinaryHeap
 public import Complexity.Algorithms.WordRAM.PriorityQueue.BinaryHeap.Model
@@ -144,10 +146,16 @@ public import Complexity.Algorithms.WordRAM.RadixSort.Scan
 public import Complexity.Algorithms.WordRAM.Stack
 public import Complexity.Algorithms.WordRAM.Stack.Controller
 public import Complexity.Algorithms.WordRAM.ThreeSum.Cell
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Collisions
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Count
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.CountFrame
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.CountTriple
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Query
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Residues
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Search
 public import Complexity.Algorithms.WordRAM.ThreeSum.Fill
 public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Loop
 public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Prepare
diff --git a/Complexity/Algorithms/WordRAM/PrimeTable.lean b/Complexity/Algorithms/WordRAM/PrimeTable.lean
new file mode 100644
index 0000000000..52ed1ba938
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/PrimeTable.lean
@@ -0,0 +1,224 @@
+/-
+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.PrimeTrial
+public import Mathlib.NumberTheory.PrimeCounting
+
+/-!
+# Native prime tables
+
+This fixed program tests every candidate through the supplied bound, writes its primality
+bit, and counts the primes. Trial division, table addresses, writes and loops are charged.
+There is no primality oracle or assumed sieve.
+
+## Main definitions
+
+* `PrimeTable.program`: the complete native table builder.
+* `PrimeTable.memory`: its output bitmap and memory frame.
+
+## Main results
+
+* `PrimeTable.exec`: exact bitmap and prime count in an explicit quadratic instruction bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.PrimeTable
+
+open Cslib.WordRAM
+open Finset
+
+/-- Registers of the trial-division subroutine. -/
+def trialRegisters (i : Fin 6) : Fin 15 := ⟨i.val, by omega⟩
+
+private theorem trial_injective : Function.Injective trialRegisters := by
+  intro i j h
+  apply Fin.ext
+  exact congrArg (fun i : Fin 15 => i.val) h
+
+/-- Current trial-division candidate. -/
+abbrev arg : Fin 15 := 0
+/-- Current candidate's primality bit. -/
+abbrev flag : Fin 15 := 2
+/-- Largest candidate. -/
+abbrev limit : Fin 15 := 6
+/-- Output bitmap base. -/
+abbrev base : Fin 15 := 7
+/-- First candidate not yet written. -/
+abbrev cursor : Fin 15 := 8
+/-- Address scratch. -/
+abbrev addr : Fin 15 := 9
+/-- Number of primes written. -/
+abbrev count : Fin 15 := 10
+/-- One past the largest candidate. -/
+abbrev stop : Fin 15 := 11
+/-- Constant one. -/
+abbrev one : Fin 15 := 12
+/-- Constant zero. -/
+abbrev zero : Fin 15 := 13
+/-- Constant two. -/
+abbrev two : Fin 15 := 14
+
+/-- Handle zero and one directly; test all larger candidates by charged native trial division. -/
+def test : Code .standard 15 :=
+  .branch (.lt cursor two) (ram[ flag ← #0 ])
+    (.seq (ram[ arg ← cursor ]) (PrimeTrial.program.rename trialRegisters))
+
+/-- Test, write the bit, update the count, and advance the candidate. -/
+def body : Code .standard 15 :=
+  .seq test (ram[ addr ← base + cursor; *addr ← flag;
+    count ← count + flag; cursor ← cursor + one ])
+
+/-- A finite native prime-table program with its bound and base supplied in registers. -/
+def program : Code .standard 15 :=
+  .seq (ram[ one ← #1; zero ← #0; two ← #2; cursor ← #0; count ← #0;
+    stop ← limit + one ]) (.loop (.lt cursor stop) body)
+
+/-- The first `k` primality bits, preserving all other memory cells. -/
+def memory (mem : ℕ → ℕ) (base k : ℕ) : ℕ → ℕ :=
+  fun a => if base ≤ a ∧ a < base + k then if (a - base).Prime then 1 else 0 else mem a
+
+private theorem memory_zero (mem : ℕ → ℕ) (base : ℕ) : memory mem base 0 = mem := by
+  funext a
+  simp [memory]
+
+private theorem memory_succ (mem : ℕ → ℕ) (base k : ℕ) :
+    memory mem base (k + 1) = Function.update (memory mem base k)
+      (base + k) (if k.Prime then 1 else 0) := by
+  funext a
+  by_cases ha : a = base + k
+  · subst a
+    simp [memory]
+  · rw [Function.update_of_ne ha]
+    have h : (base ≤ a ∧ a < base + (k + 1)) ↔ (base ≤ a ∧ a < base + k) := by omega
+    simp only [memory, h]
+
+private theorem exec_test {w m : ℕ} (x : Data 15) (htwo : x.regs two = 2)
+    (hbound : x.regs cursor ≤ m) (hfit : Fits w (m + 3)) :
+    ∃ y, ExecWithin w test x y (7 * m + 9) ∧
+      y.regs flag = (if (x.regs cursor).Prime then 1 else 0) ∧ y.mem = x.mem ∧
+      ∀ i, 6 ≤ i.val → y.regs i = x.regs i := by
+  by_cases hp : x.regs cursor < 2
+  · have hnp : ¬(x.regs cursor).Prime := fun h => by have := h.two_le; omega
+    refine ⟨x.set flag 0, ?_, by simp [hnp], rfl, ?_⟩
+    · exact (ExecWithin.branch_pos (by simpa only [Cond.holds_lt, htwo] using hp)
+        (ExecWithin.const (fits_zero w))).mono (by omega)
+    · intro i hi
+      have hne : i ≠ flag := by intro h; subst i; change 6 ≤ 2 at hi; omega
+      simp only [Data.set_regs, Function.update_of_ne hne]
+  · let p := x.set arg (x.regs cursor)
+    have hcopy : ExecWithin (B := .standard) w (ram[ arg ← cursor ]) x p 1 :=
+      ExecWithin.copy
+    obtain ⟨a, ha, haf, haa, ham⟩ := PrimeTrial.exec (p.comap trialRegisters)
+      (by change 2 ≤ x.regs cursor; omega)
+      (hfit.of_le (by change x.regs cursor + 2 ≤ m + 3; omega))
+    let y := a.extend trialRegisters p
+    have hf : y.regs flag = a.regs PrimeTrial.flag := by
+      change Function.extend trialRegisters a.regs p.regs (trialRegisters PrimeTrial.flag) = _
+      exact trial_injective.extend_apply _ _ _
+    refine ⟨y, ?_, hf.trans haf, ham, ?_⟩
+    · exact (ExecWithin.branch_neg (by simpa only [Cond.holds_lt, htwo] using hp)
+        (hcopy.seq (ha.rename trial_injective))).mono (by
+          change 1 + (7 * (x.regs cursor - 2) + 6) + 2 ≤ 7 * m + 9
+          omega)
+    · intro i hi
+      change Function.extend trialRegisters a.regs p.regs i = x.regs i
+      rw [Function.extend_apply']
+      · have hne : i ≠ arg := by intro h; subst i; change 6 ≤ 0 at hi; omega
+        exact Function.update_of_ne hne _ _
+      · rintro ⟨j, hj⟩
+        have := congrArg Fin.val hj
+        dsimp [trialRegisters] at this
+        omega
+
+
+/-- Write every primality bit through `m`, count exactly `Nat.primesLE m`, and preserve
+all cells outside the bitmap. Trial division gives the explicit quadratic bound
+`(m+1)(7m+15)+8`; the final halt is excluded. -/
+theorem exec {w : ℕ} (x : Data 15)
+    (hfit : Fits w (x.regs limit + 3))
+    (haddr : Fits w (x.regs base + (x.regs limit + 1))) :
+    ∃ y, ExecWithin w program x y ((x.regs limit + 1) * (7 * x.regs limit + 15) + 8) ∧
+      y.mem = memory x.mem (x.regs base) (x.regs limit + 1) ∧
+      y.regs count = #(Nat.primesLE (x.regs limit)) ∧
+      y.regs limit = x.regs limit ∧ y.regs base = x.regs base := by
+  let m := x.regs limit
+  let I (y : Data 15) : Prop := y.regs limit = m ∧ y.regs base = x.regs base ∧
+    y.regs stop = m + 1 ∧ y.regs one = 1 ∧ y.regs zero = 0 ∧ y.regs two = 2 ∧
+    y.regs cursor ≤ m + 1 ∧ y.regs count = Nat.primeCounting' (y.regs cursor) ∧
+    y.mem = memory x.mem (x.regs base) (y.regs cursor)
+  have hbody (y : Data 15) (hy : I y) (hc : (Cond.lt cursor stop).Holds y) :
+      ∃ q, ExecWithin w body y q (7 * m + 13) ∧ I q ∧
+        m + 1 - q.regs cursor < m + 1 - y.regs cursor := by
+    obtain ⟨hl, hb, hs, ho, hz, ht, hi, hcount, hm⟩ := hy
+    have hlt : y.regs cursor < m + 1 := by simpa only [Cond.holds_lt, hs] using hc
+    obtain ⟨z, he, hzf, hzm, hzr⟩ := exec_test y ht (show y.regs cursor ≤ m by omega) hfit
+    have hzb : z.regs base = x.regs base := (hzr base (by decide)).trans hb
+    have hzi : z.regs cursor = y.regs cursor := hzr cursor (by decide)
+    have hzc : z.regs count = Nat.primeCounting' (y.regs cursor) :=
+      (hzr count (by decide)).trans hcount
+    have hzo : z.regs one = 1 := (hzr one (by decide)).trans ho
+    have hzf_le : z.regs flag ≤ 1 := by rw [hzf]; split_ifs <;> omega
+    have ha : Fits w (z.regs base + z.regs cursor) := haddr.of_le (by rw [hzb, hzi]; omega)
+    have hn : Fits w (z.regs cursor + 1) := hfit.of_le (by rw [hzi]; change _ ≤ m + 3; omega)
+    have hct : Fits w (z.regs count + z.regs flag) := hfit.of_le (by
+      rw [hzc]
+      have hle : Nat.primeCounting' (y.regs cursor) ≤ y.regs cursor :=
+        Nat.count_le Nat.Prime
+      change _ ≤ m + 3
+      omega)
+    refine ⟨?q, ?run, ?inv, ?decrease⟩
+    case run =>
+      have htail : ExecWithin w (ram[ addr ← base + cursor; *addr ← flag;
+          count ← count + flag; cursor ← cursor + one ]) z ?q 4 := by
+        ram_eval [ha, hn, hct, hzo]
+      exact (he.seq htail).mono (by omega)
+    case inv =>
+      refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [Function.update_apply] using (hzr limit (by decide)).trans hl
+      · simpa +decide [Function.update_apply] using hzb
+      · simpa +decide [Function.update_apply] using (hzr stop (by decide)).trans hs
+      · simpa +decide [Function.update_apply] using hzo
+      · simpa +decide [Function.update_apply] using (hzr zero (by decide)).trans hz
+      · simpa +decide [Function.update_apply] using (hzr two (by decide)).trans ht
+      · simpa +decide [Function.update_apply, hzi] using Nat.succ_le_of_lt hlt
+      · change z.regs count + z.regs flag = Nat.primeCounting' (z.regs cursor + 1)
+        rw [hzc, hzf, hzi]
+        simp only [Nat.primeCounting', Nat.count_succ]
+      · change Function.update z.mem (z.regs base + z.regs cursor) (z.regs flag) =
+          memory x.mem (x.regs base) (z.regs cursor + 1)
+        rw [hzm, hm, hzb, hzi, hzf, ← memory_succ]
+    case decrease =>
+      change m + 1 - (z.regs cursor + 1) < m + 1 - y.regs cursor
+      rw [hzi]
+      omega
+  let x₀ := (((((x.set one 1).set zero 0).set two 2).set cursor 0).set count 0).set stop (m + 1)
+  have hx₀ : I x₀ := by
+    simp +decide [I, x₀, m, limit, base, stop, one, zero, two, cursor, count,
+      Nat.primeCounting', Nat.count_zero, memory_zero]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => m + 1 - y.regs cursor) hbody hx₀
+  obtain ⟨hl, hb, hs, ho, hz, ht, hi, hcount, hm⟩ := hy
+  have hend : y.regs cursor = m + 1 := by
+    simp only [Cond.holds_lt, hs] at hc
+    omega
+  have h1 : Fits w 1 := hfit.of_le (by omega)
+  have h2 : Fits w 2 := hfit.of_le (by omega)
+  have hstop : Fits w (x.regs limit + 1) := hfit.of_le (by omega)
+  have hinit : ExecWithin (B := .standard) w
+      (ram[ one ← #1; zero ← #0; two ← #2; cursor ← #0; count ← #0;
+        stop ← limit + one ]) x x₀ 6 := by
+    ram_eval [x₀, m, h1, h2, hstop, limit, base, stop, one, zero, two, cursor, count, Fin.mk.injEq]
+  refine ⟨y, ?_, by simpa only [hend] using hm, ?_, hl, hb⟩
+  · have hi₀ : x₀.regs cursor = 0 := rfl
+    have hcost : 7 * m + 13 + 2 = 7 * m + 15 := by omega
+    exact (hinit.seq he).mono (by rw [hi₀, Nat.sub_zero, hcost]; dsimp only [m]; omega)
+  · rw [hcount, hend, Nat.primesLE_card_eq_primeCounting, Nat.primeCounting]
+
+end Cslib.Algorithms.WordRAM.PrimeTable
diff --git a/Complexity/Algorithms/WordRAM/PrimeTrial.lean b/Complexity/Algorithms/WordRAM/PrimeTrial.lean
new file mode 100644
index 0000000000..ec29efe117
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/PrimeTrial.lean
@@ -0,0 +1,142 @@
+/-
+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.Prime.Defs
+
+/-!
+# Charged native trial division
+
+This is a finite instruction program, not an invocation of Lean's primality decision procedure.
+The Chan–He prime table will call it only on candidates at least two.
+
+## Main definitions
+
+* `PrimeTrial.program`: trial divisors from two up to the candidate.
+
+## Main results
+
+* `PrimeTrial.exec`: native trial division with an explicit linear instruction bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.PrimeTrial
+
+open Cslib.WordRAM
+
+/-- Candidate, preserved. -/
+abbrev arg : Fin 6 := 0
+/-- Current trial divisor. -/
+abbrev divisor : Fin 6 := 1
+/-- Primality flag. -/
+abbrev flag : Fin 6 := 2
+/-- Remainder scratch. -/
+abbrev remainder : Fin 6 := 3
+/-- Constant one. -/
+abbrev one : Fin 6 := 4
+/-- Constant zero. -/
+abbrev zero : Fin 6 := 5
+
+/-- Test one trial divisor and advance. The conditional also charges its control instructions. -/
+def body : Code .standard 6 := ram[
+  remainder ← arg % divisor;
+  if remainder = zero then [ flag ← zero ] else [ flag ← flag ];
+  divisor ← divisor + one ]
+
+/-- Initialize and test every divisor strictly between one and the candidate. -/
+def program : Code .standard 6 :=
+  .seq (ram[ divisor ← #2; flag ← #1; one ← #1; zero ← #0 ])
+    (.loop (.lt divisor arg) body)
+
+private def Good (p k : ℕ) : Prop := ∀ d, 2 ≤ d → d < k → p % d ≠ 0
+
+private theorem good_succ (p k : ℕ) (hk : 2 ≤ k) :
+    Good p (k + 1) ↔ Good p k ∧ p % k ≠ 0 := by
+  constructor
+  · intro h
+    exact ⟨fun d hd hdk => h d hd (by omega), h k hk (by omega)⟩
+  · rintro ⟨h, hmod⟩ d hd hdk
+    by_cases hdk' : d = k
+    · simpa only [hdk'] using hmod
+    · exact h d hd (by omega)
+
+/-- Test a candidate at least two in at most `7(p-2)+6` native instructions.
+All divisors are actual register values; the native remainder instruction is charged. -/
+theorem exec {w : ℕ} (x : Data 6) (hp : 2 ≤ x.regs arg)
+    (hfit : Fits w (x.regs arg + 2)) :
+    ∃ y, ExecWithin w program x y (7 * (x.regs arg - 2) + 6) ∧
+      y.regs flag = (if (x.regs arg).Prime then 1 else 0) ∧
+      y.regs arg = x.regs arg ∧ y.mem = x.mem := by
+  classical
+  let p := x.regs arg
+  let I (y : Data 6) : Prop := y.regs arg = p ∧ y.regs one = 1 ∧ y.regs zero = 0 ∧
+    2 ≤ y.regs divisor ∧ y.regs divisor ≤ p ∧
+    y.regs flag = (if Good p (y.regs divisor) then 1 else 0) ∧ y.mem = x.mem
+  have hbody (y : Data 6) (hy : I y) (hc : (Cond.lt divisor arg).Holds y) :
+      ∃ z, ExecWithin w body y z 5 ∧ I z ∧ p - z.regs divisor < p - y.regs divisor := by
+    obtain ⟨ha, ho, hz, hd, hdp, hf, hm⟩ := hy
+    have hlt : y.regs divisor < p := by simpa only [Cond.holds_lt, ha] using hc
+    have hmod : Fits w (p % y.regs divisor) := hfit.of_le (by
+      have := Nat.mod_le p (y.regs divisor)
+      change p % y.regs divisor ≤ p + 2
+      omega)
+    have hinc : Fits w (y.regs divisor + 1) := hfit.of_le (by change _ ≤ p + 2; omega)
+    let z := ((y.set remainder (p % y.regs divisor)).set flag
+      (if p % y.regs divisor = 0 then 0 else y.regs flag)).set divisor (y.regs divisor + 1)
+    have he : ExecWithin w body y z 5 := by
+      by_cases hrem : p % y.regs divisor = 0 <;>
+        ram_eval [body, z, ha, ho, hz, hmod, hinc, hrem, arg, divisor, flag,
+          remainder, one, zero, Fin.mk.injEq]
+    have hflag : (if p % y.regs divisor = 0 then 0 else y.regs flag) =
+        if Good p (y.regs divisor + 1) then 1 else 0 := by
+      rw [hf]
+      have hg := good_succ p (y.regs divisor) hd
+      by_cases hrem : p % y.regs divisor = 0
+      · have hg' : ¬Good p (y.regs divisor + 1) := fun h => (hg.mp h).2 hrem
+        simp only [hrem, hg', ↓reduceIte]
+      · have hg' : Good p (y.regs divisor + 1) ↔ Good p (y.regs divisor) := by tauto
+        simp only [hrem, hg', ↓reduceIte]
+    refine ⟨z, he, ?_, ?_⟩
+    · refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [z, Function.update_apply, arg, divisor, flag, remainder] using ha
+      · simpa +decide [z, Function.update_apply, one, divisor, flag, remainder] using ho
+      · simpa +decide [z, Function.update_apply, zero, divisor, flag, remainder] using hz
+      · simpa +decide [z, Function.update_apply, divisor] using
+          (show 2 ≤ y.regs divisor + 1 by omega)
+      · simpa +decide [z, Function.update_apply, divisor] using Nat.succ_le_of_lt hlt
+      · simpa +decide [z, Function.update_apply, divisor, flag, remainder] using hflag
+      · exact hm
+    · change p - (y.regs divisor + 1) < p - y.regs divisor
+      omega
+  let x₀ := (((x.set divisor 2).set flag 1).set one 1).set zero 0
+  have hx₀ : I x₀ := by
+    have hgood : Good p 2 := by intro d hd hlt; omega
+    simp +decide [I, x₀, p, arg, divisor, flag, one, zero, hgood, hp]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I (fun y => p - y.regs divisor) hbody hx₀
+  obtain ⟨ha, ho, hz, hd, hdp, hf, hm⟩ := hy
+  have hend : y.regs divisor = p := by simp only [Cond.holds_lt, ha] at hc; omega
+  have hprime : Good p p ↔ p.Prime := by
+    rw [Nat.prime_def_lt']
+    constructor
+    · intro h
+      refine ⟨hp, fun d hd hdp hdiv => ?_⟩
+      exact h d hd hdp (Nat.mod_eq_zero_of_dvd hdiv)
+    · rintro ⟨_, h⟩ d hd hdp hzero
+      exact h d hd hdp (Nat.dvd_of_mod_eq_zero hzero)
+  have h1 : Fits w 1 := hfit.of_le (by omega)
+  have h2 : Fits w 2 := hfit.of_le (by omega)
+  have hinit : ExecWithin (B := .standard) w
+      (ram[ divisor ← #2; flag ← #1; one ← #1; zero ← #0 ]) x x₀ 4 := by
+    ram_eval [x₀, h1, h2]
+  refine ⟨y, ?_, by simpa only [hend, hprime] using hf, ha, hm⟩
+  have hd₀ : x₀.regs divisor = 2 := rfl
+  exact (hinit.seq he).mono (by rw [hd₀]; dsimp only [p]; omega)
+
+end Cslib.Algorithms.WordRAM.PrimeTrial
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CollisionTest.lean b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CollisionTest.lean
new file mode 100644
index 0000000000..37545bd9a0
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CollisionTest.lean
@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall
+import Mathlib.Tactic.FinCases
+
+/-!
+# Native tests of the three Chan–He collision inequalities
+
+Each inequality multiplies a computed collision count by the number of candidate primes,
+then compares it with its supplied threshold. All multiplications, branches and flag updates
+are ordinary charged instructions. No predicate is executed by an oracle.
+
+## Main definitions
+
+* `CollisionTest.program`: test all three inequalities.
+
+## Main results
+
+* `CollisionTest.exec`: the exact acceptance flag in at most thirteen instructions.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest
+
+open Cslib.WordRAM
+
+/-- Number of candidate primes. -/
+abbrev card : Fin 64 := 42
+/-- Threshold for one of the three sets. -/
+def threshold (j : Fin 3) : Fin 64 := ⟨44 + j.val, by omega⟩
+/-- Constant zero. -/
+abbrev zero : Fin 64 := 52
+/-- Collision count times the number of candidate primes. -/
+abbrev scaled : Fin 64 := 57
+/-- Acceptance flag. -/
+abbrev good : Fin 64 := 58
+
+/-- One charged multiplication and comparison, retaining a previously false flag. -/
+def compare (j : Fin 3) : Code .standard 64 :=
+  let value := CountCall.result j
+  let cutoff := threshold j
+  ram[ scaled ← value * card;
+    if cutoff < scaled then [ good ← zero ] else [ good ← good ] ]
+
+/-- Initialize a true flag and test all three supplied collision counts. -/
+def program : Code .standard 64 :=
+  .seq (ram[ good ← #1 ]) (.seq (compare 0) (.seq (compare 1) (compare 2)))
+
+private theorem exec_compare {w : ℕ} (j : Fin 3) (x : Data 64)
+    (hz : x.regs zero = 0)
+    (hfit : Fits w (x.regs (CountCall.result j) * x.regs card)) :
+    ∃ y, ExecWithin w (compare j) x y 4 ∧
+      y.regs good = (if x.regs (CountCall.result j) * x.regs card ≤ x.regs (threshold j)
+        then x.regs good else 0) ∧ y.mem = x.mem ∧
+      ∀ i, i ≠ scaled → i ≠ good → y.regs i = x.regs i := by
+  let product := x.regs (CountCall.result j) * x.regs card
+  let y := (x.set scaled product).set good
+    (if x.regs (threshold j) < product then 0 else x.regs good)
+  have hm : ExecWithin w
+      (.op (.bin .mul scaled (CountCall.result j) card)) x (x.set scaled product) 1 :=
+    ExecWithin.bin hfit
+  have hcut : (x.set scaled product).regs (threshold j) = x.regs (threshold j) := by
+    fin_cases j <;> rfl
+  have hz' : (x.set scaled product).regs zero = 0 := by
+    simpa +decide [zero, scaled] using hz
+  have hg' : (x.set scaled product).regs good = x.regs good := rfl
+  have hscaled : (x.set scaled product).regs scaled = product := rfl
+  have he : ExecWithin w (compare j) x y 4 := by
+    by_cases hlt : x.regs (threshold j) < product
+    · have hc : (Cond.lt (threshold j) scaled).Holds (x.set scaled product) := by
+        simpa only [Cond.holds_lt, hcut, hscaled] using hlt
+      have hb := ExecWithin.branch_pos (B := .standard) (w := w) (pos := ram[ good ← zero ])
+        (neg := ram[ good ← good ]) hc
+        (ExecWithin.copy (x := x.set scaled product) (d := good) (s := zero))
+      have hb' : ExecWithin (B := .standard) w
+          (.branch (.lt (threshold j) scaled) (ram[ good ← zero ]) (ram[ good ← good ]))
+          (x.set scaled product) y 2 := by
+        simpa only [y, hlt, ↓reduceIte, hz'] using hb
+      exact (hm.seq hb').mono (by decide)
+    · have hc : ¬(Cond.lt (threshold j) scaled).Holds (x.set scaled product) := by
+        simpa only [Cond.holds_lt, hcut, hscaled] using hlt
+      have hb := ExecWithin.branch_neg (B := .standard) (w := w) (pos := ram[ good ← zero ])
+        (neg := ram[ good ← good ]) hc
+        (ExecWithin.copy (x := x.set scaled product) (d := good) (s := good))
+      have hb' : ExecWithin (B := .standard) w
+          (.branch (.lt (threshold j) scaled) (ram[ good ← zero ]) (ram[ good ← good ]))
+          (x.set scaled product) y 3 := by
+        simpa only [y, hlt, ↓reduceIte, hg'] using hb
+      exact hm.seq hb'
+  refine ⟨y, he, ?_, rfl, ?_⟩
+  · change (if x.regs (threshold j) < product then 0 else x.regs good) =
+      if product ≤ x.regs (threshold j) then x.regs good else 0
+    by_cases hlt : x.regs (threshold j) < product
+    · have hnot : ¬product ≤ x.regs (threshold j) := by omega
+      simp only [hlt, hnot, ↓reduceIte]
+    · have hle : product ≤ x.regs (threshold j) := by omega
+      simp only [hlt, hle, ↓reduceIte]
+  · intro i hs hg
+    simp only [y, Data.set_regs, Function.update_of_ne hg, Function.update_of_ne hs]
+
+/-- Test all three inequalities with a shared acceptance flag. The only written registers
+are `scaled` and `good`; memory and every other caller register are unchanged. -/
+theorem exec {w : ℕ} (x : Data 64) (h1 : Fits w 1) (hz : x.regs zero = 0)
+    (hfit : ∀ j, Fits w (x.regs (CountCall.result j) * x.regs card)) :
+    ∃ y, ExecWithin w program x y 13 ∧
+      y.regs good = (if
+        x.regs (CountCall.result 0) * x.regs card ≤ x.regs (threshold 0) ∧
+        x.regs (CountCall.result 1) * x.regs card ≤ x.regs (threshold 1) ∧
+        x.regs (CountCall.result 2) * x.regs card ≤ x.regs (threshold 2) then 1 else 0) ∧
+      y.mem = x.mem ∧ ∀ i, i ≠ scaled → i ≠ good → y.regs i = x.regs i := by
+  let R (y : Data 64) : Prop := y.mem = x.mem ∧
+    ∀ i, i ≠ scaled → i ≠ good → y.regs i = x.regs i
+  have hcall (j : Fin 3) (y : Data 64) (hy : R y) :
+      ∃ z, ExecWithin w (compare j) y z 4 ∧ R z ∧
+        z.regs good = (if x.regs (CountCall.result j) * x.regs card ≤ x.regs (threshold j)
+          then y.regs good else 0) := by
+    obtain ⟨hm, hr⟩ := hy
+    have hvalue : y.regs (CountCall.result j) = x.regs (CountCall.result j) :=
+      hr _ (by fin_cases j <;> decide) (by fin_cases j <;> decide)
+    have hcard : y.regs card = x.regs card := hr _ (by decide) (by decide)
+    have hcut : y.regs (threshold j) = x.regs (threshold j) :=
+      hr _ (by fin_cases j <;> decide) (by fin_cases j <;> decide)
+    obtain ⟨z, he, hf, hzm, hzr⟩ := exec_compare j y
+      ((hr _ (by decide) (by decide)).trans hz)
+      (by simpa only [hvalue, hcard] using hfit j)
+    exact ⟨z, he, ⟨hzm.trans hm, fun i hs hg => (hzr i hs hg).trans (hr i hs hg)⟩,
+      by simpa only [hvalue, hcard, hcut] using hf⟩
+  let x₀ := x.set good 1
+  have hx₀ : R x₀ := ⟨rfl, fun i _ hg => Function.update_of_ne hg _ _⟩
+  obtain ⟨a, ha, hRa, hfa⟩ := hcall 0 x₀ hx₀
+  obtain ⟨b, hb, hRb, hfb⟩ := hcall 1 a hRa
+  obtain ⟨c, hc, hRc, hfc⟩ := hcall 2 b hRb
+  refine ⟨c, ?_, ?_, hRc⟩
+  · exact (ExecWithin.const h1).seq (ha.seq (hb.seq hc))
+  · rw [hfc, hfb, hfa]
+    change (if _ then (if _ then (if _ then 1 else 0) else 0) else 0) = _
+    split_ifs <;> omega
+
+end Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CountCall.lean b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CountCall.lean
new file mode 100644
index 0000000000..de574e2935
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CountCall.lean
@@ -0,0 +1,172 @@
+/-
+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.ChanHe.CountFrame
+import Mathlib.Tactic.FinCases
+
+/-!
+# Charged calls to Chan–He collision counting
+
+The prime searches keep their parameters outside the counting workspace. Each of the three
+set arrays has a fixed pair of base/length registers and its own result register. This module
+charges argument setup and result delivery as well as the complete native counting routine.
+
+## Main definitions
+
+* `CountCall.program`: a counting call on one of the three input arrays.
+
+## Main results
+
+* `CountCall.exec`: exact collision count, memory frame and preserved caller registers.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+
+/-- Counting workspace in a larger, fixed register file. -/
+def registers (i : Fin 28) : Fin 64 := ⟨i.val, by omega⟩
+
+private theorem registers_injective : Function.Injective registers := by
+  intro i j h
+  apply Fin.ext
+  exact congrArg (fun i : Fin 64 => i.val) h
+
+/-- Length register for the selected set. -/
+def length (j : Fin 3) : Fin 64 := ⟨28 + 2 * j.val, by omega⟩
+/-- Base register for the selected set. -/
+def source (j : Fin 3) : Fin 64 := ⟨29 + 2 * j.val, by omega⟩
+/-- Residue scratch base. -/
+abbrev scratch : Fin 64 := 34
+/-- Histogram base. -/
+abbrev histogram : Fin 64 := 35
+/-- Encoded positive modulus. -/
+abbrev modulus : Fin 64 := 36
+/-- Collision-count output register for the selected set. -/
+def result (j : Fin 3) : Fin 64 := ⟨37 + j.val, by omega⟩
+
+/-- Counting input base register. -/
+abbrev countSource : Fin 64 := registers Count.src
+/-- Counting scratch base register. -/
+abbrev countScratch : Fin 64 := registers Count.scratch
+/-- Counting input length register. -/
+abbrev countLength : Fin 64 := registers Count.len
+/-- Counting encoded-modulus register. -/
+abbrev countModulus : Fin 64 := registers Count.modulus
+/-- Counting histogram base register. -/
+abbrev countHistogram : Fin 64 := registers Count.dst
+/-- Counting result register. -/
+abbrev countTotal : Fin 64 := registers Count.total
+
+/-- Five runtime register copies deliver the counting arguments. -/
+def prepare (j : Fin 3) : Code .standard 64 :=
+  let input := source j
+  let n := length j
+  ram[ countSource ← input; countScratch ← scratch; countLength ← n;
+    countModulus ← modulus; countHistogram ← histogram ]
+
+/-- A complete native count call, including argument and result copies. -/
+def program (j : Fin 3) : Code .standard 64 :=
+  .seq (prepare j) (.seq (Count.program.rename registers) (.op (.copy (result j) countTotal)))
+
+private theorem extend_outside (a : Data 28) (x : Data 64) (i : Fin 64) (hi : 28 ≤ i.val) :
+    (a.extend registers x).regs i = x.regs i := by
+  change Function.extend registers a.regs x.regs i = x.regs i
+  apply Function.extend_apply'
+  rintro ⟨j, hj⟩
+  have := congrArg Fin.val hj
+  dsimp [registers] at this
+  omega
+
+/-- A native count call costs `34n+5M+24`, including five argument copies and one result copy.
+The mathematical input is an injective array enumeration, as required by the existing set-based
+Chan–He collision count. All registers outside the workspace, except its chosen result, survive. -/
+theorem exec {w M : ℕ} (j : Fin 3) (x : Data 64) (values : ℕ → ℤ) (hM : 0 < M)
+    (hmod : GenericRAM.Signed.Fits w (M : ℤ))
+    (hmodreg : x.regs modulus = encode (M : ℤ))
+    (hfit : ∀ i < x.regs (length j), GenericRAM.Signed.Fits w (values i))
+    (hs : Fits (w + 2) (x.regs (source j) + x.regs (length j)))
+    (hk : Fits (w + 2) (x.regs scratch + x.regs (length j)))
+    (hd : Fits (w + 2) (x.regs histogram + M))
+    (ht : Fits (w + 2) (x.regs (length j) * x.regs (length j) + x.regs (length j) + 1))
+    (hsk : x.regs (source j) + x.regs (length j) ≤ x.regs scratch)
+    (hkd : x.regs scratch + x.regs (length j) ≤ x.regs histogram)
+    (hinput : ∀ i < x.regs (length j),
+      x.mem (x.regs (source j) + i) = encode (values i))
+    (hinj : Set.InjOn values (↑(Finset.range (x.regs (length j))) : Set ℕ)) :
+    ∃ y, ExecWithin (w + 2) (program j) x y (34 * x.regs (length j) + 5 * M + 24) ∧
+      y.mem = Count.memory x.mem values (x.regs (length j)) M
+        (x.regs scratch) (x.regs histogram) ∧
+      y.regs (result j) = Cslib.Algorithms.ThreeSum.ChanHe.coll
+        ((Finset.range (x.regs (length j))).image values) M ∧
+      ∀ i, 28 ≤ i.val → i ≠ result j → y.regs i = x.regs i := by
+  let q := ((((x.set countSource (x.regs (source j))).set countScratch (x.regs scratch)).set
+    countLength (x.regs (length j))).set countModulus (x.regs modulus)).set
+    countHistogram (x.regs histogram)
+  have hprep : ExecWithin (w + 2) (prepare j) x q 5 := by
+    fin_cases j <;>
+      ram_eval [prepare, q, source, length, registers, countSource, countScratch,
+        countLength, countModulus, countHistogram, scratch, histogram, modulus,
+        Count.src, Count.scratch, Count.len, Count.modulus, Count.dst, Fin.mk.injEq]
+  have hq (i : Fin 64) (hi : 28 ≤ i.val) : q.regs i = x.regs i := by
+    have hne (k : Fin 64) (hk : k.val < 28) : i ≠ k := by
+      intro h
+      have := congrArg Fin.val h
+      omega
+    simp only [q, Data.set_regs, Function.update_of_ne (hne countSource (by decide)),
+      Function.update_of_ne (hne countScratch (by decide)),
+      Function.update_of_ne (hne countLength (by decide)),
+      Function.update_of_ne (hne countModulus (by decide)),
+      Function.update_of_ne (hne countHistogram (by decide))]
+  have hqs : (q.comap registers).regs Count.src = x.regs (source j) := by
+    simp +decide [q, registers, countSource, countScratch, countLength, countModulus,
+      countHistogram, Count.src, Count.scratch, Count.len, Count.modulus, Count.dst]
+  have hqn : (q.comap registers).regs Count.len = x.regs (length j) := by
+    simp +decide [q, registers, countSource, countScratch, countLength, countModulus,
+      countHistogram, Count.src, Count.scratch, Count.len, Count.modulus, Count.dst]
+  have hqk : (q.comap registers).regs Count.scratch = x.regs scratch := by
+    simp +decide [q, registers, countSource, countScratch, countLength, countModulus,
+      countHistogram, Count.src, Count.scratch, Count.len, Count.modulus, Count.dst]
+  have hqd : (q.comap registers).regs Count.dst = x.regs histogram := by
+    simp +decide [q, registers, countSource, countScratch, countLength, countModulus,
+      countHistogram, Count.src, Count.scratch, Count.len, Count.modulus, Count.dst]
+  have hqm : (q.comap registers).regs Count.modulus = x.regs modulus := by
+    simp +decide [q, registers, countSource, countScratch, countLength, countModulus,
+      countHistogram, Count.src, Count.scratch, Count.len, Count.modulus, Count.dst]
+  obtain ⟨a, ha, ham, hav, _⟩ := Count.exec_coll (q.comap registers) values hM hmod
+    (hqm.trans hmodreg) (by simpa only [hqn] using hfit)
+    (by simpa only [hqs, hqn] using hs) (by simpa only [hqk, hqn] using hk)
+    (by simpa only [hqd] using hd) (by simpa only [hqn] using ht)
+    (by simpa only [hqs, hqn, hqk] using hsk)
+    (by simpa only [hqk, hqn, hqd] using hkd)
+    (by
+      change ∀ i < (q.comap registers).regs Count.len,
+        x.mem ((q.comap registers).regs Count.src + i) = encode (values i)
+      simpa only [hqn, hqs] using hinput)
+    (by simpa only [hqn] using hinj)
+  let y := a.extend registers q
+  have hy : ExecWithin (w + 2) (Count.program.rename registers) q y
+      (34 * x.regs (length j) + 5 * M + 18) := by
+    simpa only [hqn] using ha.rename registers_injective
+  have hyt : y.regs countTotal = a.regs Count.total := by
+    change Function.extend registers a.regs q.regs (registers Count.total) = _
+    exact registers_injective.extend_apply _ _ _
+  refine ⟨y.set (result j) (y.regs countTotal), ?_, ?_, ?_, ?_⟩
+  · exact (hprep.seq (hy.seq ExecWithin.copy)).mono (by omega)
+  · change a.mem = _
+    have hqmem : q.mem = x.mem := rfl
+    simpa only [Data.comap_mem, hqmem, hqn, hqk, hqd] using ham
+  · simp only [Data.set_regs, Function.update_self, hyt]
+    simpa only [hqn] using hav
+  · intro i hi hne
+    rw [Data.set_regs, Function.update_of_ne hne, extend_outside a q i hi, hq i hi]
+
+end Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CountFrame.lean b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CountFrame.lean
new file mode 100644
index 0000000000..ba7f1a1e05
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CountFrame.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Count
+
+/-!
+# Collision-counting register and memory frames
+
+Prime-search clients reuse the same fixed counting program on successive candidates.
+Its input parameters and all memory below its scratch blocks are preserved.
+
+## Main results
+
+* `Count.memory_before`: cells below the two workspace blocks retain their contents.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count
+
+open Cslib.WordRAM
+
+/-- Neither the residue array nor the histogram modifies an earlier memory cell. -/
+theorem memory_before (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M scratch dst a : ℕ)
+    (hs : a < scratch) (hd : a < dst) : memory mem values n M scratch dst a = mem a := by
+  simp [memory, Histogram.memory, Residues.memory, show ¬(dst ≤ a ∧ a < dst + M) by omega,
+    show ¬(scratch ≤ a ∧ a < scratch + n) by omega]
+
+end Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CountTriple.lean b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CountTriple.lean
new file mode 100644
index 0000000000..09ea12f05a
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/CountTriple.lean
@@ -0,0 +1,122 @@
+/-
+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.ChanHe.CountCall
+import Mathlib.Tactic.FinCases
+
+/-!
+# Native collision counts for the three Chan–He sets
+
+All three calls are actual native counting programs, with charged argument and result copies.
+The prime-search control registers and every input cell below the workspace are preserved.
+
+## Main definitions
+
+* `CountTriple.program`: three complete native collision-count calls.
+
+## Main results
+
+* `CountTriple.exec`: exact counts for all three sets and charged total time.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountTriple
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+
+/-- Run one full count call on each of the three arrays. -/
+def program : Code .standard 64 :=
+  .seq (CountCall.program 0) (.seq (CountCall.program 1) (CountCall.program 2))
+
+/-- Count collisions in all three injectively enumerated sets in at most
+`34(n₀+n₁+n₂)+15M+72` instructions, excluding halt. All caller registers except the
+three results are preserved, as is all memory before the counting workspace. -/
+theorem exec {w M : ℕ} (x : Data 64) (values : Fin 3 → ℕ → ℤ) (hM : 0 < M)
+    (hmod : GenericRAM.Signed.Fits w (M : ℤ))
+    (hmodreg : x.regs CountCall.modulus = encode (M : ℤ))
+    (hfit : ∀ j i, i < x.regs (CountCall.length j) → GenericRAM.Signed.Fits w (values j i))
+    (hs : ∀ j, Fits (w + 2) (x.regs (CountCall.source j) + x.regs (CountCall.length j)))
+    (hk : ∀ j, Fits (w + 2) (x.regs CountCall.scratch + x.regs (CountCall.length j)))
+    (hd : Fits (w + 2) (x.regs CountCall.histogram + M))
+    (ht : ∀ j, Fits (w + 2) (x.regs (CountCall.length j) * x.regs (CountCall.length j) +
+      x.regs (CountCall.length j) + 1))
+    (hsk : ∀ j, x.regs (CountCall.source j) + x.regs (CountCall.length j) ≤
+      x.regs CountCall.scratch)
+    (hkd : ∀ j, x.regs CountCall.scratch + x.regs (CountCall.length j) ≤
+      x.regs CountCall.histogram)
+    (hinput : ∀ j i, i < x.regs (CountCall.length j) →
+      x.mem (x.regs (CountCall.source j) + i) = encode (values j i))
+    (hinj : ∀ j, Set.InjOn (values j)
+      (↑(Finset.range (x.regs (CountCall.length j))) : Set ℕ)) :
+    ∃ y, ExecWithin (w + 2) program x y
+        (34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+          x.regs (CountCall.length 2)) + 15 * M + 72) ∧
+      (∀ j, y.regs (CountCall.result j) = Cslib.Algorithms.ThreeSum.ChanHe.coll
+        ((Finset.range (x.regs (CountCall.length j))).image (values j)) M) ∧
+      (∀ i, (28 ≤ i.val ∧ i.val < 37) ∨ 40 ≤ i.val → y.regs i = x.regs i) ∧
+      ∀ a < x.regs CountCall.scratch, y.mem a = x.mem a := by
+  let P (i : Fin 64) : Prop := (28 ≤ i.val ∧ i.val < 37) ∨ 40 ≤ i.val
+  let R (y : Data 64) : Prop := (∀ i, P i → y.regs i = x.regs i) ∧
+    ∀ a < x.regs CountCall.scratch, y.mem a = x.mem a
+  have hcall (j : Fin 3) (y : Data 64) (hy : R y) :
+      ∃ z, ExecWithin (w + 2) (CountCall.program j) y z
+          (34 * x.regs (CountCall.length j) + 5 * M + 24) ∧ R z ∧
+        z.regs (CountCall.result j) = Cslib.Algorithms.ThreeSum.ChanHe.coll
+          ((Finset.range (x.regs (CountCall.length j))).image (values j)) M ∧
+        ∀ i, 28 ≤ i.val → i ≠ CountCall.result j → z.regs i = y.regs i := by
+    obtain ⟨hr, hm⟩ := hy
+    have hl : y.regs (CountCall.length j) = x.regs (CountCall.length j) :=
+      hr _ (by dsimp [P, CountCall.length]; omega)
+    have hb : y.regs (CountCall.source j) = x.regs (CountCall.source j) :=
+      hr _ (by dsimp [P, CountCall.source]; omega)
+    have hws : y.regs CountCall.scratch = x.regs CountCall.scratch := hr _ (by decide)
+    have hwh : y.regs CountCall.histogram = x.regs CountCall.histogram := hr _ (by decide)
+    have hwm : y.regs CountCall.modulus = encode (M : ℤ) := (hr _ (by decide)).trans hmodreg
+    obtain ⟨z, he, hzm, hzv, hzr⟩ := CountCall.exec j y (values j) hM hmod hwm
+      (by simpa only [hl] using hfit j) (by simpa only [hb, hl] using hs j)
+      (by simpa only [hws, hl] using hk j) (by simpa only [hwh] using hd)
+      (by simpa only [hl] using ht j) (by simpa only [hb, hl, hws] using hsk j)
+      (by simpa only [hws, hl, hwh] using hkd j)
+      (by
+        intro i hi
+        have hi' : i < x.regs (CountCall.length j) := by simpa only [hl] using hi
+        rw [hb, hm (x.regs (CountCall.source j) + i) (by have := hsk j; omega)]
+        exact hinput j i hi')
+      (by simpa only [hl] using hinj j)
+    refine ⟨z, by simpa only [hl] using he, ?_, by simpa only [hl] using hzv, hzr⟩
+    refine ⟨?_, ?_⟩
+    · intro i hi
+      have hlow : 28 ≤ i.val := by dsimp [P] at hi; omega
+      have hne : i ≠ CountCall.result j := by
+        intro heq
+        have := congrArg Fin.val heq
+        dsimp [P, CountCall.result] at *
+        omega
+      exact (hzr i hlow hne).trans (hr i hi)
+    · intro a ha
+      rw [hzm, Count.memory_before]
+      · exact hm a ha
+      · simpa only [hws] using ha
+      · have := hkd j
+        rw [hwh]
+        omega
+  have hx : R x := ⟨fun _ _ => rfl, fun _ _ => rfl⟩
+  obtain ⟨a, ha, hRa, hva, hfa⟩ := hcall 0 x hx
+  obtain ⟨b, hb, hRb, hvb, hfb⟩ := hcall 1 a hRa
+  obtain ⟨c, hc, hRc, hvc, hfc⟩ := hcall 2 b hRb
+  refine ⟨c, (ha.seq (hb.seq hc)).mono (by omega), ?_, hRc⟩
+  intro j
+  fin_cases j
+  · exact (hfc (CountCall.result 0) (by decide) (by decide)).trans
+      ((hfb (CountCall.result 0) (by decide) (by decide)).trans hva)
+  · exact (hfc (CountCall.result 1) (by decide) (by decide)).trans hvb
+  · exact hvc
+
+end Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountTriple
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Query.lean b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Query.lean
new file mode 100644
index 0000000000..9e61f1a50a
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Query.lean
@@ -0,0 +1,99 @@
+/-
+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.ChanHe.CountTriple
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest
+
+/-!
+# Complete native collision queries for Chan–He prime searches
+
+A query computes all three collision counts and tests their scaled thresholds. No count or
+acceptance test is supplied as advice: all counting and comparison instructions are charged.
+
+## Main definitions
+
+* `Query.program`: the complete native collision-count and threshold query.
+
+## Main results
+
+* `Query.exec`: exact three-inequality acceptance, input frame and instruction bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Query
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.ThreeSum.ChanHe
+
+/-- Count collisions and test all three inequalities. -/
+def program : Code .standard 64 := .seq CountTriple.program CollisionTest.program
+
+/-- Execute a complete three-set collision query within
+`34(n₀+n₁+n₂)+15M+85` instructions. Multiplication fits are bounded by `nⱼ²·card`,
+independently of the actual input collision count. The final halt is excluded. -/
+theorem exec {w M : ℕ} (x : Data 64) (values : Fin 3 → ℕ → ℤ) (hM : 0 < M)
+    (hmod : GenericRAM.Signed.Fits w (M : ℤ))
+    (hmodreg : x.regs CountCall.modulus = encode (M : ℤ))
+    (hfit : ∀ j i, i < x.regs (CountCall.length j) → GenericRAM.Signed.Fits w (values j i))
+    (hs : ∀ j, Fits (w + 2) (x.regs (CountCall.source j) + x.regs (CountCall.length j)))
+    (hk : ∀ j, Fits (w + 2) (x.regs CountCall.scratch + x.regs (CountCall.length j)))
+    (hd : Fits (w + 2) (x.regs CountCall.histogram + M))
+    (ht : ∀ j, Fits (w + 2) (x.regs (CountCall.length j) * x.regs (CountCall.length j) +
+      x.regs (CountCall.length j) + 1))
+    (hproduct : ∀ j, Fits (w + 2) (x.regs (CountCall.length j) * x.regs (CountCall.length j) *
+      x.regs CollisionTest.card))
+    (hz : x.regs CollisionTest.zero = 0)
+    (hsk : ∀ j, x.regs (CountCall.source j) + x.regs (CountCall.length j) ≤
+      x.regs CountCall.scratch)
+    (hkd : ∀ j, x.regs CountCall.scratch + x.regs (CountCall.length j) ≤
+      x.regs CountCall.histogram)
+    (hinput : ∀ j i, i < x.regs (CountCall.length j) →
+      x.mem (x.regs (CountCall.source j) + i) = encode (values j i))
+    (hinj : ∀ j, Set.InjOn (values j)
+      (↑(Finset.range (x.regs (CountCall.length j))) : Set ℕ)) :
+    ∃ y, ExecWithin (w + 2) program x y
+        (34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+          x.regs (CountCall.length 2)) + 15 * M + 85) ∧
+      y.regs CollisionTest.good = (if
+        coll ((Finset.range (x.regs (CountCall.length 0))).image (values 0)) M *
+          x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold 0) ∧
+        coll ((Finset.range (x.regs (CountCall.length 1))).image (values 1)) M *
+          x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold 1) ∧
+        coll ((Finset.range (x.regs (CountCall.length 2))).image (values 2)) M *
+          x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold 2) then 1 else 0) ∧
+      (∀ i, ((28 ≤ i.val ∧ i.val < 37) ∨ 40 ≤ i.val) →
+        i ≠ CollisionTest.scaled → i ≠ CollisionTest.good → y.regs i = x.regs i) ∧
+      ∀ a < x.regs CountCall.scratch, y.mem a = x.mem a := by
+  obtain ⟨a, ha, hav, har, ham⟩ := CountTriple.exec x values hM hmod hmodreg
+    hfit hs hk hd ht hsk hkd hinput hinj
+  have hac : a.regs CollisionTest.card = x.regs CollisionTest.card := har _ (by decide)
+  have hat (j : Fin 3) : a.regs (CollisionTest.threshold j) =
+      x.regs (CollisionTest.threshold j) := har _ (by dsimp [CollisionTest.threshold]; omega)
+  have h1 : Fits (w + 2) 1 := (show Fits 2 1 from by decide).mono (by omega)
+  have hprod (j : Fin 3) :
+      Fits (w + 2) (a.regs (CountCall.result j) * a.regs CollisionTest.card) := by
+    rw [hav j, hac]
+    apply (hproduct j).of_le
+    apply Nat.mul_le_mul_right
+    have hcard : ((Finset.range (x.regs (CountCall.length j))).image (values j)).card ≤
+        x.regs (CountCall.length j) :=
+      Finset.card_image_le.trans_eq (Finset.card_range _)
+    exact (coll_le_sq _ _).trans (by simpa only [pow_two] using Nat.mul_self_le_mul_self hcard)
+  obtain ⟨b, hb, hbg, hbm, hbr⟩ := CollisionTest.exec a h1
+    ((har _ (by decide)).trans hz) hprod
+  refine ⟨b, (ha.seq hb).mono (by omega), ?_, ?_, ?_⟩
+  · simpa only [hav, hac, hat] using hbg
+  · intro i hi hs hg
+    exact (hbr i hs hg).trans (har i hi)
+  · intro i hi
+    rw [hbm]
+    exact ham i hi
+
+end Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Query
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Search.lean b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Search.lean
new file mode 100644
index 0000000000..eef9c8d51e
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Search.lean
@@ -0,0 +1,507 @@
+/-
+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.PrimeTable
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Query
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum
+
+/-!
+# Native least-prime collision searches
+
+The search scans the prime bitmap in increasing order. A candidate runs the complete native
+three-set collision query. Its first acceptance is retained while the remaining candidates
+are visited without further bitmap reads. If no candidate is accepted, the answer is one, matching
+`ChanHe.minOrOne`.
+
+## Main definitions
+
+* `Search.program`: a fixed native prime search using charged collision queries.
+
+## Main results
+
+* `Search.exec`: exact minimum/default selection with native fits, frames and charged cost.
+* `Search.preserves_caller`: the upper five caller registers are preserved.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.ThreeSum.ChanHe
+
+/-- Largest candidate prime. -/
+abbrev limit : Fin 64 := 40
+/-- Prime bitmap base. -/
+abbrev primes : Fin 64 := 41
+/-- Factor multiplied by the candidate prime. -/
+abbrev factor : Fin 64 := 43
+/-- Current candidate. -/
+abbrev cursor : Fin 64 := 47
+/-- One past the largest candidate. -/
+abbrev stop : Fin 64 := 48
+/-- Selected prime, or the default one. -/
+abbrev answer : Fin 64 := 49
+/-- Whether an acceptance has already occurred. -/
+abbrev found : Fin 64 := 50
+/-- Constant one. -/
+abbrev one : Fin 64 := 51
+/-- Constant zero. -/
+abbrev zero : Fin 64 := 52
+/-- Constant two, for positive signed encoding. -/
+abbrev two : Fin 64 := 53
+/-- Unencoded candidate modulus. -/
+abbrev rawModulus : Fin 64 := 54
+/-- Bitmap address scratch. -/
+abbrev addr : Fin 64 := 55
+/-- Loaded primality bit. -/
+abbrev bit : Fin 64 := 56
+/-- Encoded candidate modulus. -/
+abbrev modulus : Fin 64 := CountCall.modulus
+/-- Acceptance flag returned by the collision query. -/
+abbrev good : Fin 64 := CollisionTest.good
+
+/-- Compute and encode the candidate modulus, then run the full collision query. -/
+def query : Code .standard 64 :=
+  .seq (ram[ rawModulus ← factor * cursor; modulus ← rawModulus * two ]) Query.program
+
+/-- Record an accepted candidate, or retain the previous answer. -/
+def pick : Code .standard 64 := ram[
+  if good = one then [ answer ← cursor; found ← one ] else [ answer ← answer ] ]
+
+/-- A charged instruction that retains the answer. -/
+def nop : Code .standard 64 := ram[ answer ← answer ]
+
+/-- Load a bitmap entry. -/
+def load : Code .standard 64 := ram[ addr ← primes + cursor; bit ← *addr ]
+
+/-- Before the first acceptance, run the query exactly on prime candidates. -/
+def inner : Code .standard 64 :=
+  .branch (.eq found zero)
+    (.seq load (.branch (.eq bit one) (.seq query pick) nop)) nop
+
+/-- One candidate and its charged cursor increment. -/
+def body : Code .standard 64 := .seq inner (ram[ cursor ← cursor + one ])
+
+/-- Initialize the selector and scan the entire bounded candidate range. -/
+def program : Code .standard 64 :=
+  .seq (ram[ one ← #1; zero ← #0; two ← #2; cursor ← #0;
+    stop ← limit + one; answer ← one; found ← zero ]) (.loop (.lt cursor stop) body)
+
+/-- The five upper caller registers survive the complete native search. -/
+theorem preserves_caller (i : Fin 64) (hi : 59 ≤ i.val) : program.Preserves i := by
+  fin_cases i <;> norm_num at hi <;> decide
+
+private abbrev Fixed (i : Fin 64) : Prop := (28 ≤ i.val ∧ i.val ≤ 35) ∨ (40 ≤ i.val ∧ i.val ≤ 46)
+
+private abbrev Control (i : Fin 64) : Prop :=
+  (28 ≤ i.val ∧ i.val ≤ 35) ∨ (40 ≤ i.val ∧ i.val ≤ 53)
+
+private def Stable (x y : Data 64) : Prop :=
+  (∀ i, Fixed i → y.regs i = x.regs i) ∧
+    ∀ a < x.regs CountCall.scratch, y.mem a = x.mem a
+
+private def Status (A : ℕ → Prop) (k : ℕ) (y : Data 64) : Prop :=
+  (y.regs found = 0 ∧ y.regs answer = 1 ∧ ∀ q < k, ¬(q.Prime ∧ A q)) ∨
+  (y.regs found = 1 ∧ y.regs answer < k ∧ (y.regs answer).Prime ∧ A (y.regs answer) ∧
+    ∀ q < y.regs answer, ¬(q.Prime ∧ A q))
+
+private theorem exec_nop {w : ℕ} (x : Data 64) : ExecWithin w nop x x 1 := by
+  have hx : x.set answer (x.regs answer) = x := Data.ext (Function.update_eq_self _ _) rfl
+  simpa only [nop, hx] using (ExecWithin.copy (B := .standard) (w := w)
+    (x := x) (d := answer) (s := answer))
+
+private theorem exec_pick {w : ℕ} (x : Data 64) (A : Prop) [Decidable A]
+    (ho : x.regs one = 1) (hg : x.regs good = if A then 1 else 0) :
+    ∃ y, ExecWithin w pick x y 3 ∧ y.mem = x.mem ∧
+      y.regs answer = (if A then x.regs cursor else x.regs answer) ∧
+      y.regs found = (if A then 1 else x.regs found) ∧
+      ∀ i, i ≠ answer → i ≠ found → y.regs i = x.regs i := by
+  by_cases hA : A
+  · let y := (x.set answer (x.regs cursor)).set found 1
+    refine ⟨y, ?_, rfl, ?_, ?_, ?_⟩
+    · ram_eval [pick, y, ho, hg, hA, good, one, cursor, answer, found, Fin.mk.injEq]
+    · simp +decide [y, hA, answer, found]
+    · simp [y, hA]
+    · intro i ha hf
+      simp only [y, Data.set_regs, Function.update_of_ne ha, Function.update_of_ne hf]
+  · refine ⟨x, ?_, rfl, by simp [hA], by simp [hA], fun _ _ _ => rfl⟩
+    have hc : ¬(Cond.eq good one).Holds x := by simp [hg, hA, ho]
+    exact ExecWithin.branch_neg hc (exec_nop x)
+
+private theorem status_min {A : ℕ → Prop} [DecidablePred A] {m : ℕ} {y : Data 64}
+    (h : Status A (m + 1) y) :
+    y.regs answer = minOrOne {q ∈ Nat.primesLE m | A q} := by
+  let S := {q ∈ Nat.primesLE m | A q}
+  rcases h with ⟨hf, ha, hn⟩ | ⟨hf, hk, hp, hA, hn⟩
+  · have hs : S = ∅ := by
+      apply Finset.eq_empty_iff_forall_notMem.mpr
+      intro q hq
+      have hq' := Finset.mem_filter.mp hq
+      have hmem := Finset.mem_filter.mp (by
+        simpa only [Nat.primesLE_eq_filter_range] using hq'.1)
+      exact hn q (Finset.mem_range.mp hmem.1) ⟨hmem.2, hq'.2⟩
+    rw [ha]
+    change 1 = minOrOne S
+    simp [hs, minOrOne]
+  · have hmem : y.regs answer ∈ S := by
+      simp only [S, Finset.mem_filter, Nat.primesLE_eq_filter_range, Finset.mem_range]
+      exact ⟨⟨hk, hp⟩, hA⟩
+    have hs : S.Nonempty := ⟨_, hmem⟩
+    have hmin : S.min' hs = y.regs answer := by
+      apply le_antisymm (Finset.min'_le _ _ hmem)
+      apply Finset.le_min'
+      intro q hq
+      by_contra hnot
+      have hq' := Finset.mem_filter.mp hq
+      have hpq := (Finset.mem_filter.mp (by
+        simpa only [Nat.primesLE_eq_filter_range] using hq'.1)).2
+      exact hn q (by omega) ⟨hpq, hq'.2⟩
+    change y.regs answer = minOrOne S
+    simp only [minOrOne, dite_eq_left hs, hmin]
+
+
+private theorem fixed_ne_high {i j : Fin 64} (hi : Fixed i) (hj : 47 ≤ j.val) : i ≠ j := by
+  intro h
+  have := congrArg Fin.val h
+  dsimp [Fixed] at hi
+  omega
+
+private theorem stable_set_high {x y : Data 64} (h : Stable x y) (i : Fin 64)
+    (hi : 47 ≤ i.val) (v : ℕ) : Stable x (y.set i v) := by
+  exact ⟨fun j hj => by
+    simpa only [Data.set_regs, Function.update_of_ne (fixed_ne_high hj hi)] using h.1 j hj,
+    h.2⟩
+
+private theorem status_of_regs {A : ℕ → Prop} {k : ℕ} {x y : Data 64}
+    (hf : y.regs found = x.regs found) (ha : y.regs answer = x.regs answer)
+    (h : Status A k x) : Status A k y := by
+  simpa only [Status, hf, ha] using h
+
+private theorem status_extend {A : ℕ → Prop} {k : ℕ} {y : Data 64}
+    (h : Status A k y) (hnew : y.regs found = 0 → ¬(k.Prime ∧ A k)) :
+    Status A (k + 1) y := by
+  rcases h with ⟨hf, ha, hn⟩ | ⟨hf, hk, hp, hA, hn⟩
+  · exact Or.inl ⟨hf, ha, fun q hq => by
+      by_cases hqk : q < k
+      · exact hn q hqk
+      · have : q = k := by omega
+        subst q
+        exact hnew hf⟩
+  · exact Or.inr ⟨hf, by omega, hp, hA, hn⟩
+
+private theorem exec_driver {w T : ℕ} (x : Data 64) (A : ℕ → Prop) [DecidablePred A]
+    (hfit : Fits w (x.regs limit + 3))
+    (haddr : Fits w (x.regs primes + (x.regs limit + 1)))
+    (hbefore : x.regs primes + (x.regs limit + 1) ≤ x.regs CountCall.scratch)
+    (hbitmap : ∀ q ≤ x.regs limit, x.mem (x.regs primes + q) = if q.Prime then 1 else 0)
+    (hquery : ∀ y, Stable x y → y.regs cursor ≤ x.regs limit →
+      y.regs one = 1 → y.regs zero = 0 → y.regs two = 2 → (y.regs cursor).Prime →
+      ∃ z, ExecWithin w query y z T ∧ Stable x z ∧
+        z.regs good = (if A (y.regs cursor) then 1 else 0) ∧
+        ∀ i, Control i → z.regs i = y.regs i) :
+    ∃ y, ExecWithin w program x y ((x.regs limit + 1) * (T + 15) + 9) ∧
+      Stable x y ∧ y.regs answer = minOrOne {q ∈ Nat.primesLE (x.regs limit) | A q} := by
+  let m := x.regs limit
+  let I (y : Data 64) : Prop := Stable x y ∧ y.regs stop = m + 1 ∧
+    y.regs one = 1 ∧ y.regs zero = 0 ∧ y.regs two = 2 ∧ y.regs cursor ≤ m + 1 ∧
+    Status A (y.regs cursor) y
+  have hbody (y : Data 64) (hy : I y) (hc : (Cond.lt cursor stop).Holds y) :
+      ∃ z, ExecWithin w body y z (T + 13) ∧ I z ∧
+        m + 1 - z.regs cursor < m + 1 - y.regs cursor := by
+    obtain ⟨hstable, hstop, ho, hz, ht, hi, hstatus⟩ := hy
+    have hlt : y.regs cursor < m + 1 := by simpa only [Cond.holds_lt, hstop] using hc
+    have hinner : ∃ z, ExecWithin w inner y z (T + 12) ∧ Stable x z ∧
+        z.regs stop = m + 1 ∧ z.regs one = 1 ∧ z.regs zero = 0 ∧ z.regs two = 2 ∧
+        z.regs cursor = y.regs cursor ∧ Status A (y.regs cursor + 1) z := by
+      rcases hstatus with hnone | hsome
+      · obtain ⟨hf, ha, hn⟩ := hnone
+        have hfound : (Cond.eq found zero).Holds y := by simp [hf, hz]
+        have hpr : y.regs primes = x.regs primes := hstable.1 _ (by decide)
+        have hread : y.mem (y.regs primes + y.regs cursor) =
+            if (y.regs cursor).Prime then 1 else 0 := by
+          rw [hpr, hstable.2 (x.regs primes + y.regs cursor) (by omega)]
+          exact hbitmap _ (by change y.regs cursor ≤ m; omega)
+        have had : Fits w (y.regs primes + y.regs cursor) := haddr.of_le (by rw [hpr]; omega)
+        let u := (y.set addr (y.regs primes + y.regs cursor)).set bit
+          (if (y.regs cursor).Prime then 1 else 0)
+        have hload : ExecWithin w load y u 2 := by
+          ram_eval [load, u, had, hread, addr, bit, primes, cursor, Fin.mk.injEq]
+        have hu (i : Fin 64) (hC : Control i) : u.regs i = y.regs i := by
+          have hia : i ≠ addr := by intro h; subst i; norm_num [Control, addr] at hC
+          have hib : i ≠ bit := by intro h; subst i; norm_num [Control, bit] at hC
+          simp only [u, Data.set_regs, Function.update_of_ne hia, Function.update_of_ne hib]
+        have hus : Stable x u := stable_set_high
+          (stable_set_high hstable addr (by decide) _) bit (by decide) _
+        have huo : u.regs one = 1 := (hu one (by decide)).trans ho
+        have huz : u.regs zero = 0 := (hu zero (by decide)).trans hz
+        have hut : u.regs two = 2 := (hu two (by decide)).trans ht
+        have hui : u.regs cursor = y.regs cursor := hu cursor (by decide)
+        have husp : u.regs stop = m + 1 := (hu stop (by decide)).trans hstop
+        have huf : u.regs found = 0 := (hu found (by decide)).trans hf
+        have hua : u.regs answer = 1 := (hu answer (by decide)).trans ha
+        by_cases hp : (y.regs cursor).Prime
+        · have hbit : (Cond.eq bit one).Holds u := by
+            simp only [Cond.holds_eq, huo]
+            simp +decide [u, bit, addr, hp]
+          obtain ⟨v, hv, hvs, hvg, hvr⟩ := hquery u hus (by rw [hui]; change _ ≤ m; omega)
+            huo huz hut (by simpa only [hui] using hp)
+          have hvo : v.regs one = 1 := (hvr one (by decide)).trans huo
+          obtain ⟨z, hpick, hzm, hza, hzf, hzr⟩ := exec_pick v (A (y.regs cursor)) hvo
+            (by simpa only [hui] using hvg)
+          have hzctrl (i : Fin 64) (hC : Control i) (hia : i ≠ answer) (hif : i ≠ found) :
+              z.regs i = y.regs i :=
+            (hzr i hia hif).trans ((hvr i hC).trans (hu i hC))
+          have hzs : Stable x z := ⟨fun i hF =>
+            (hzr i (fixed_ne_high hF (by decide)) (fixed_ne_high hF (by decide))).trans
+              (hvs.1 i hF), fun a ha => by rw [hzm]; exact hvs.2 a ha⟩
+          have hvi : v.regs cursor = y.regs cursor := (hvr cursor (by decide)).trans hui
+          have hvf : v.regs found = 0 := (hvr found (by decide)).trans huf
+          have hva : v.regs answer = 1 := (hvr answer (by decide)).trans hua
+          refine ⟨z, ?_, hzs, ?_, ?_, ?_, ?_, hzctrl cursor (by decide) (by decide) (by decide), ?_⟩
+          · exact (ExecWithin.branch_pos hfound
+              (hload.seq (ExecWithin.branch_pos hbit (hv.seq hpick)))).mono (by omega)
+          · exact (hzctrl stop (by decide) (by decide) (by decide)).trans hstop
+          · exact (hzctrl one (by decide) (by decide) (by decide)).trans ho
+          · exact (hzctrl zero (by decide) (by decide) (by decide)).trans hz
+          · exact (hzctrl two (by decide) (by decide) (by decide)).trans ht
+          · by_cases hA : A (y.regs cursor)
+            · have hanswer : z.regs answer = y.regs cursor := by
+                simpa only [hA, ↓reduceIte, hvi] using hza
+              refine Or.inr ⟨by simpa only [hA, ↓reduceIte] using hzf, ?_, ?_, ?_, ?_⟩
+              · rw [hanswer]; omega
+              · simpa only [hanswer] using hp
+              · simpa only [hanswer] using hA
+              · simpa only [hanswer] using hn
+            · have hanswer : z.regs answer = 1 := by simpa only [hA, ↓reduceIte, hva] using hza
+              refine Or.inl ⟨by simpa only [hA, ↓reduceIte, hvf] using hzf, hanswer, ?_⟩
+              intro q hq hqA
+              by_cases hqk : q < y.regs cursor
+              · exact hn q hqk hqA
+              · have hqeq : q = y.regs cursor := by omega
+                subst q
+                exact hA hqA.2
+        · have hbit : ¬(Cond.eq bit one).Holds u := by
+            simp only [Cond.holds_eq, huo]
+            simp +decide [u, bit, addr, hp]
+          have hnop := exec_nop (w := w) u
+          refine ⟨u, ?_, hus, husp, huo, huz, hut, hui, Or.inl ⟨huf, hua, ?_⟩⟩
+          · exact (ExecWithin.branch_pos hfound
+              (hload.seq (ExecWithin.branch_neg hbit hnop))).mono (by omega)
+          · intro q hq hqA
+            by_cases hqk : q < y.regs cursor
+            · exact hn q hqk hqA
+            · have hqeq : q = y.regs cursor := by omega
+              subst q
+              exact hp hqA.1
+      · have hfound : ¬(Cond.eq found zero).Holds y := by
+          simp only [Cond.holds_eq, hsome.1, hz]; omega
+        refine ⟨y, (ExecWithin.branch_neg hfound (exec_nop y)).mono (by omega),
+          hstable, hstop, ho, hz, ht, rfl, ?_⟩
+        exact status_extend (Or.inr hsome) (fun h0 => by rw [hsome.1] at h0; omega)
+    obtain ⟨z, he, hs, hsp, hzo, hzz, hzt, hzi, hstat⟩ := hinner
+    have hinc : Fits w (z.regs cursor + z.regs one) :=
+      hfit.of_le (by rw [hzi, hzo]; change _ ≤ m + 3; omega)
+    have hstep : ExecWithin w (Code.op (.bin .add cursor cursor one)) z
+        (z.set cursor (z.regs cursor + 1)) 1 := by
+      simpa only [BinOp.eval, hzo] using (ExecWithin.bin (f := .add) (d := cursor) (i := cursor)
+        (j := one) hinc)
+    refine ⟨z.set cursor (z.regs cursor + 1), he.seq hstep, ?_, ?_⟩
+    · refine ⟨stable_set_high hs cursor (by decide) _, ?_, ?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [stop, cursor] using hsp
+      · simpa +decide [one, cursor] using hzo
+      · simpa +decide [zero, cursor] using hzz
+      · simpa +decide [two, cursor] using hzt
+      · simpa only [Data.set_regs, Function.update_self, hzi] using Nat.succ_le_of_lt hlt
+      · simpa only [Data.set_regs, Function.update_self] using
+          status_of_regs (x := z) (y := z.set cursor (z.regs cursor + 1))
+            (by simp +decide [found, cursor])
+            (by simp +decide [answer, cursor]) (by simpa only [hzi] using hstat)
+    · simp only [Data.set_regs, Function.update_self, hzi]
+      omega
+  let x₀ := ((((((x.set one 1).set zero 0).set two 2).set cursor 0).set stop (m + 1)).set
+    answer 1).set found 0
+  have hinit : ExecWithin w (ram[
+      one ← #1; zero ← #0; two ← #2; cursor ← #0; stop ← limit + one;
+      answer ← one; found ← zero]) x x₀ 7 := by
+    have h1 : Fits w 1 := hfit.of_le (by omega)
+    have h2 : Fits w 2 := hfit.of_le (by omega)
+    have h0 : Fits w 0 := hfit.of_le (by omega)
+    have hm : Fits w (m + 1) := hfit.of_le (by change m + 1 ≤ m + 3; omega)
+    ram_eval [x₀, m, one, zero, two, cursor, stop, limit, answer, found,
+      h1, h2, h0, hm, Fin.mk.injEq]
+  have hi : I x₀ := by
+    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, Or.inl ⟨?_, ?_, ?_⟩⟩
+    · exact stable_set_high (stable_set_high (stable_set_high (stable_set_high
+        (stable_set_high (stable_set_high (stable_set_high ⟨fun _ _ => rfl,
+          fun _ _ => rfl⟩ one (by decide) _) zero (by decide) _) two (by decide) _)
+            cursor (by decide) _) stop (by decide) _) answer (by decide) _) found (by decide) _
+    all_goals simp +decide [x₀, stop, one, zero, two, cursor, answer, found]
+  obtain ⟨y, he, hy, hexit⟩ := ExecWithin.loop_invariant I
+    (fun y => m + 1 - y.regs cursor) hbody hi
+  obtain ⟨hs, hsp, hyo, hyz, hyt, hyi, hstat⟩ := hy
+  have hcur : y.regs cursor = m + 1 := by
+    simp only [Cond.holds_lt, hsp] at hexit
+    omega
+  refine ⟨y, (hinit.seq he).mono ?_, hs, ?_⟩
+  · have hcur₀ : x₀.regs cursor = 0 := by
+      simp +decide [x₀, cursor, found, answer, stop]
+    rw [hcur₀]
+    simp only [Nat.sub_zero]
+    change 7 + ((m + 1) * (T + 13 + 2) + 2) ≤ (m + 1) * (T + 15) + 9
+    have hcost : T + 13 + 2 = T + 15 := by omega
+    rw [hcost]
+    omega
+  · exact status_min (by simpa only [hcur] using hstat)
+
+/-- The least prime whose three actual collision counts satisfy the supplied thresholds.
+Every candidate query is executed by `Query.program`; the hypotheses only constrain native
+input values, layout and word fits. All instructions, including the scan after acceptance,
+are charged. The final halt is excluded. -/
+theorem exec {w : ℕ} (x : Data 64) (values : Fin 3 → ℕ → ℤ)
+    (hfactor : 0 < x.regs factor)
+    (hmod : GenericRAM.Signed.Fits w ((x.regs factor * x.regs limit : ℕ) : ℤ))
+    (hfit : Fits (w + 2) (x.regs limit + 3))
+    (haddr : Fits (w + 2) (x.regs primes + (x.regs limit + 1)))
+    (hbefore : x.regs primes + (x.regs limit + 1) ≤ x.regs CountCall.scratch)
+    (hbitmap : ∀ q ≤ x.regs limit, x.mem (x.regs primes + q) = if q.Prime then 1 else 0)
+    (hvalues : ∀ j i, i < x.regs (CountCall.length j) → GenericRAM.Signed.Fits w (values j i))
+    (hs : ∀ j, Fits (w + 2) (x.regs (CountCall.source j) + x.regs (CountCall.length j)))
+    (hk : ∀ j, Fits (w + 2) (x.regs CountCall.scratch + x.regs (CountCall.length j)))
+    (hd : Fits (w + 2) (x.regs CountCall.histogram + x.regs factor * x.regs limit))
+    (ht : ∀ j, Fits (w + 2) (x.regs (CountCall.length j) * x.regs (CountCall.length j) +
+      x.regs (CountCall.length j) + 1))
+    (hproduct : ∀ j, Fits (w + 2) (x.regs (CountCall.length j) * x.regs (CountCall.length j) *
+      x.regs CollisionTest.card))
+    (hsk : ∀ j, x.regs (CountCall.source j) + x.regs (CountCall.length j) ≤
+      x.regs CountCall.scratch)
+    (hkd : ∀ j, x.regs CountCall.scratch + x.regs (CountCall.length j) ≤
+      x.regs CountCall.histogram)
+    (hinput : ∀ j i, i < x.regs (CountCall.length j) →
+      x.mem (x.regs (CountCall.source j) + i) = encode (values j i))
+    (hinj : ∀ j, Set.InjOn (values j)
+      (↑(Finset.range (x.regs (CountCall.length j))) : Set ℕ)) :
+    ∃ y, ExecWithin (w + 2) program x y
+        ((x.regs limit + 1) * (34 * (x.regs (CountCall.length 0) +
+          x.regs (CountCall.length 1) + x.regs (CountCall.length 2)) +
+          15 * (x.regs factor * x.regs limit) + 102) + 9) ∧
+      (∀ i, ((28 ≤ i.val ∧ i.val ≤ 35) ∨ (40 ≤ i.val ∧ i.val ≤ 46)) →
+        y.regs i = x.regs i) ∧
+      (∀ a < x.regs CountCall.scratch, y.mem a = x.mem a) ∧
+      y.regs answer = minOrOne {q ∈ Nat.primesLE (x.regs limit) | ∀ j : Fin 3,
+        coll ((Finset.range (x.regs (CountCall.length j))).image (values j))
+          (x.regs factor * q) * x.regs CollisionTest.card ≤
+            x.regs (CollisionTest.threshold j)} := by
+  let A (q : ℕ) : Prop := ∀ j : Fin 3,
+    coll ((Finset.range (x.regs (CountCall.length j))).image (values j))
+      (x.regs factor * q) * x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold j)
+  let T := 34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+    x.regs (CountCall.length 2)) + 15 * (x.regs factor * x.regs limit) + 87
+  have hquery (y : Data 64) (hy : Stable x y) (hiq : y.regs cursor ≤ x.regs limit)
+      (ho : y.regs one = 1) (hz : y.regs zero = 0) (htwo : y.regs two = 2)
+      (hp : (y.regs cursor).Prime) :
+      ∃ z, ExecWithin (w + 2) query y z T ∧ Stable x z ∧
+        z.regs good = (if A (y.regs cursor) then 1 else 0) ∧
+        ∀ i, Control i → z.regs i = y.regs i := by
+    let M := x.regs factor * y.regs cursor
+    have hM : 0 < M := Nat.mul_pos hfactor hp.pos
+    have hMle : M ≤ x.regs factor * x.regs limit := Nat.mul_le_mul_left _ hiq
+    have hMf : GenericRAM.Signed.Fits w (M : ℤ) := by
+      refine ⟨hmod.1, ?_, lt_of_le_of_lt (by exact_mod_cast hMle) hmod.2.2⟩
+      have hnonneg : (0 : ℤ) ≤ M := Nat.cast_nonneg _
+      have hpower : (0 : ℤ) ≤ 2 ^ (w - 1) := by positivity
+      omega
+    have henc : encode (M : ℤ) = 2 * M := by simp [encode]
+    have hencoded : Fits (w + 2) (2 * M) := by
+      rw [← henc]
+      exact (encode_fits hMf).mono (by omega)
+    have hraw : Fits (w + 2) M := hencoded.of_le (by omega)
+    have hyf : y.regs factor = x.regs factor := hy.1 _ (by decide)
+    let u := (y.set rawModulus M).set modulus (2 * M)
+    have hprep : ExecWithin (w + 2)
+        (ram[ rawModulus ← factor * cursor; modulus ← rawModulus * two ]) y u 2 := by
+      ram_eval [u, M, hyf, htwo, hraw, hencoded, rawModulus, modulus, factor, cursor, two,
+        CountCall.modulus, Fin.mk.injEq, Nat.mul_comm]
+    have huc (i : Fin 64) (hi : Control i) : u.regs i = y.regs i := by
+      have hr : i ≠ rawModulus := by intro h; subst i; norm_num [Control, rawModulus] at hi
+      have hm : i ≠ modulus := by
+        intro h; subst i; norm_num [Control, modulus, CountCall.modulus] at hi
+      simp only [u, Data.set_regs, Function.update_of_ne hr, Function.update_of_ne hm]
+    have huf (i : Fin 64) (hi : Fixed i) : u.regs i = x.regs i :=
+      (huc i (by unfold Control Fixed at *; omega)).trans (hy.1 i hi)
+    have hlen (j : Fin 3) : u.regs (CountCall.length j) = x.regs (CountCall.length j) :=
+      huf _ (by dsimp [CountCall.length, Fixed]; omega)
+    have hsrc (j : Fin 3) : u.regs (CountCall.source j) = x.regs (CountCall.source j) :=
+      huf _ (by dsimp [CountCall.source, Fixed]; omega)
+    have hscratch : u.regs CountCall.scratch = x.regs CountCall.scratch := huf _ (by decide)
+    have hhist : u.regs CountCall.histogram = x.regs CountCall.histogram := huf _ (by decide)
+    have hcard : u.regs CollisionTest.card = x.regs CollisionTest.card := huf _ (by decide)
+    have hcut (j : Fin 3) : u.regs (CollisionTest.threshold j) =
+        x.regs (CollisionTest.threshold j) :=
+      huf _ (by dsimp [Fixed, CollisionTest.threshold]; omega)
+    have hmodreg : u.regs CountCall.modulus = encode (M : ℤ) := by
+      simpa only [henc] using (show u.regs modulus = 2 * M from by simp [u])
+    have huinput : ∀ j i, i < u.regs (CountCall.length j) →
+        u.mem (u.regs (CountCall.source j) + i) = encode (values j i) := by
+      intro j i hi
+      rw [hlen] at hi
+      change y.mem (u.regs (CountCall.source j) + i) = _
+      rw [hsrc, hy.2 _ (by have := hsk j; omega)]
+      exact hinput j i hi
+    obtain ⟨z, he, hgood, hreg, hmem⟩ := Query.exec u values hM hMf hmodreg
+      (by simpa only [hlen] using hvalues) (by simpa only [hsrc, hlen] using hs)
+      (by simpa only [hscratch, hlen] using hk)
+      (by rw [hhist]; exact hd.of_le (Nat.add_le_add_left hMle _))
+      (by simpa only [hlen] using ht) (by simpa only [hlen, hcard] using hproduct)
+      ((huc zero (by decide)).trans hz)
+      (by simpa only [hsrc, hlen, hscratch] using hsk)
+      (by simpa only [hscratch, hlen, hhist] using hkd) huinput
+      (by simpa only [hlen] using hinj)
+    have hcontrol (i : Fin 64) (hi : Control i) : z.regs i = y.regs i := by
+      have hscl : i ≠ CollisionTest.scaled := by
+        intro h; subst i; norm_num [Control, CollisionTest.scaled] at hi
+      have hg : i ≠ CollisionTest.good := by
+        intro h; subst i; norm_num [Control, CollisionTest.good] at hi
+      exact (hreg i (by unfold Control at hi; omega) hscl hg).trans (huc i hi)
+    refine ⟨z, (hprep.seq he).mono ?_, ?_, ?_, hcontrol⟩
+    · dsimp only [T]
+      rw [hlen 0, hlen 1, hlen 2]
+      have := Nat.mul_le_mul_left 15 hMle
+      omega
+    · refine ⟨fun i hi => (hcontrol i (by unfold Fixed Control at *; omega)).trans
+          (hy.1 i hi), ?_⟩
+      intro a ha
+      rw [hmem a (by simpa only [hscratch] using ha)]
+      exact hy.2 a ha
+    · have hA : A (y.regs cursor) ↔
+          coll ((Finset.range (x.regs (CountCall.length 0))).image (values 0)) M *
+            x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold 0) ∧
+          coll ((Finset.range (x.regs (CountCall.length 1))).image (values 1)) M *
+            x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold 1) ∧
+          coll ((Finset.range (x.regs (CountCall.length 2))).image (values 2)) M *
+            x.regs CollisionTest.card ≤ x.regs (CollisionTest.threshold 2) := by
+        constructor
+        · intro h; exact ⟨h 0, h 1, h 2⟩
+        · intro h j
+          fin_cases j
+          · exact h.1
+          · exact h.2.1
+          · exact h.2.2
+      simpa only [hlen, hcard, hcut, ← hA] using hgood
+  obtain ⟨y, he, hs, ha⟩ := exec_driver x A hfit haddr hbefore hbitmap hquery
+  refine ⟨y, he.mono ?_, hs.1, hs.2, ha⟩
+  dsimp only [T]
+  have hcost : 34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+      x.regs (CountCall.length 2)) + 15 * (x.regs factor * x.regs limit) + 87 + 15 =
+      34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+        x.regs (CountCall.length 2)) + 15 * (x.regs factor * x.regs limit) + 102 := by omega
+  rw [hcost]
+
+end Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Search
diff --git a/ComplexityTests/WordRAMChanHeQuery.lean b/ComplexityTests/WordRAMChanHeQuery.lean
new file mode 100644
index 0000000000..dc16eb04c9
--- /dev/null
+++ b/ComplexityTests/WordRAMChanHeQuery.lean
@@ -0,0 +1,55 @@
+/-
+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.ChanHe.Query
+
+/-! # Executed native three-set collision queries -/
+
+namespace ComplexityTests.WordRAMChanHeQuery
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.WordRAM.ThreeSum.ChanHe
+
+private def input : Data 64 :=
+  ⟨fun i => if i.val = 28 then 1 else if i.val = 29 then 1
+    else if i.val = 30 then 2 else if i.val = 31 then 5
+    else if i.val = 32 then 0 else if i.val = 33 then 10
+    else if i.val = 34 then 20 else if i.val = 35 then 30
+    else if i.val = 36 then encode 3 else if i.val = 42 then 3
+    else if i.val = 44 then 0 else if i.val = 45 then 6
+    else if i.val = 46 then 0 else if i.val = 52 then 0 else 71,
+    fun a => if a = 1 then encode (-1) else if a = 2 then encode 0
+      else if a = 3 then encode 1 else if a = 5 then encode (-5)
+      else if a = 6 then encode (-2) else if a = 7 then encode 1
+      else if a = 8 then encode 4 else if a = 10 then encode 0
+      else if a = 11 then encode 3 else 79⟩
+
+-- The three complete counting calls unfold all renamed loops and their register maps.
+set_option maxRecDepth 8192 in
+-- Reduce the complete interpreter run directly in the kernel, avoiding elaborator normalization.
+/-- Arrays of lengths one, two and zero test setup/result copies and empty-array counting. -/
+example : (Code.eval 8 3 CountTriple.program input).map
+    (fun yn => [yn.1.regs (CountCall.result 0), yn.1.regs (CountCall.result 1),
+      yn.1.regs (CountCall.result 2), yn.1.regs (40 : Fin 64), yn.1.mem 5]) =
+        some [0, 2, 0, 71, encode (-5)] := by decide +kernel
+
+-- The full query additionally reduces three scaled inequalities after the counting loops.
+set_option maxRecDepth 8192 in
+-- Reduce the complete interpreter run directly in the kernel, avoiding elaborator normalization.
+/-- Equality at the scaled threshold is accepted, and caller controls and input are framed. -/
+example : (Code.eval 8 3 Query.program input).map
+    (fun yn => [yn.1.regs CollisionTest.good, yn.1.regs (40 : Fin 64), yn.1.mem 5]) =
+      some [1, 71, encode (-5)] := by decide +kernel
+
+-- This negative case executes the same complete native query with one smaller threshold.
+set_option maxRecDepth 8192 in
+-- Reduce the complete interpreter run directly in the kernel, avoiding elaborator normalization.
+/-- A strict failure of one threshold rejects the three-set candidate. -/
+example : (Code.eval 8 3 Query.program
+    (input.set (CollisionTest.threshold 1) 5)).map (fun yn => yn.1.regs CollisionTest.good) =
+      some 0 := by decide +kernel
+
+end ComplexityTests.WordRAMChanHeQuery
diff --git a/ComplexityTests/WordRAMChanHeSearch.lean b/ComplexityTests/WordRAMChanHeSearch.lean
new file mode 100644
index 0000000000..cbdd66497f
--- /dev/null
+++ b/ComplexityTests/WordRAMChanHeSearch.lean
@@ -0,0 +1,131 @@
+/-
+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.ChanHe.Search
+
+/-! # Executed least-prime collision searches -/
+
+namespace ComplexityTests.WordRAMChanHeSearch
+
+open Cslib.WordRAM
+open Cslib.Algorithms.ThreeSum.ChanHe
+open Cslib.Algorithms.WordRAM.ThreeSum.ChanHe
+
+private def emptyInput (m : ℕ) : Data 64 :=
+  ⟨fun i => if i.val = 28 ∨ i.val = 30 ∨ i.val = 32 then 0
+    else if i.val = 29 ∨ i.val = 31 ∨ i.val = 33 then 1
+    else if i.val = 34 then 20 else if i.val = 35 then 30
+    else if i.val = 40 then m else if i.val = 41 then 10
+    else if i.val = 42 then 1 else if i.val = 43 then 1
+    else if i.val = 44 ∨ i.val = 45 ∨ i.val = 46 then 0 else 71,
+    fun a => if a = 12 ∨ a = 13 then 1 else 0⟩
+
+/-- Zero candidates return the specified default, without running a collision query. -/
+example : (Code.eval 8 2 Search.program (emptyInput 0)).map
+    (fun yn => yn.1.regs Search.answer) = some 1 := by decide
+
+/-- The nonprime boundary one still returns the default. -/
+example : (Code.eval 8 3 Search.program (emptyInput 1)).map
+    (fun yn => yn.1.regs Search.answer) = some 1 := by decide
+
+-- The positive case reduces the full renamed three-set query inside the search loop.
+set_option maxRecDepth 8192 in
+/-- The first prime is accepted at three zero thresholds for three empty sets. -/
+example : (Code.eval 8 4 Search.program (emptyInput 2)).map
+    (fun yn => [yn.1.regs Search.answer, yn.1.regs Search.found, yn.1.mem 12]) =
+      some [2, 1, 1] := by decide
+
+-- After accepting two, the search executes only the charged skip branch for three.
+set_option maxRecDepth 8192 in
+/-- Later accepted primes cannot overwrite the minimum or rerun the collision query. -/
+example : (Code.eval 8 5 Search.program (emptyInput 3)).map
+    (fun yn => [yn.1.regs Search.answer, yn.1.regs CountCall.modulus]) =
+      some [2, 4] := by decide
+
+-- The rejected prime still runs all three native collision-counting calls.
+set_option maxRecDepth 8192 in
+/-- The only prime fails because zero and two collide, so the answer is the default one. -/
+example : (Code.eval 8 4 Search.program
+    ⟨Function.update (emptyInput 2).regs (CountCall.length 0) 2,
+      Function.update (emptyInput 2).mem 2 4⟩).map
+    (fun yn => [yn.1.regs Search.answer, yn.1.regs Search.found]) =
+      some [1, 0] := by decide
+
+/-- The full execution contract has an admissible initialized instance, including every fit,
+bitmap cell and input frame. -/
+example : ∃ y, ExecWithin 8 Search.program (emptyInput 2) y (3 * 132 + 9) ∧
+    y.regs Search.answer = 2 := by
+  have hlen (j : Fin 3) : (emptyInput 2).regs (CountCall.length j) = 0 := by
+    fin_cases j <;> decide
+  have hcut (j : Fin 3) : (emptyInput 2).regs (CollisionTest.threshold j) = 0 := by
+    fin_cases j <;> decide
+  obtain ⟨y, he, hregs, hmem, ha⟩ := Search.exec (w := 6) (emptyInput 2) (fun _ _ => 0)
+    (by decide) (by decide) (by decide) (by decide) (by decide)
+    (by intro q hq; change q ≤ 2 at hq; interval_cases q <;> decide)
+    (by intros; decide)
+    (by intro j; fin_cases j <;> decide) (by intro j; fin_cases j <;> decide)
+    (by decide) (by intro j; fin_cases j <;> decide) (by intro j; fin_cases j <;> decide)
+    (by intro j; fin_cases j <;> decide) (by intro j; fin_cases j <;> decide)
+    (by intro j i hi; rw [hlen] at hi; omega)
+    (by
+      intro j a ha
+      simp only [hlen, Finset.range_zero, Finset.coe_empty, Set.mem_empty_iff_false] at ha)
+  refine ⟨y, he, ?_⟩
+  simp only [hlen, hcut, Finset.range_zero, Finset.image_empty, coll, Finset.offDiag_empty,
+    Finset.filter_empty, Finset.card_empty, Nat.zero_mul, Nat.le_refl, implies_true,
+    Finset.filter_true] at ha
+  have hselect : minOrOne (Nat.primesLE 2) = 2 := by decide
+  change y.regs Search.answer = minOrOne (Nat.primesLE 2) at ha
+  exact ha.trans hselect
+
+private def laterInput : Data 64 :=
+  ⟨Function.update (Function.update (emptyInput 3).regs (CountCall.length 0) 2) Search.factor 2,
+    Function.update (emptyInput 3).mem 2 8⟩
+
+private def laterValues (j : Fin 3) (i : ℕ) : ℤ := if j = 0 then if i = 0 then 0 else 4 else 0
+
+-- Factor two queries moduli four and six. The first collides on {0,4}; the second does not.
+-- The actual answer, accepted flag, encoded modulus and charged bound are all observed.
+/-- info: true -/
+#guard_msgs in
+#eval decide ((Code.eval 8 8 Search.program laterInput).map (fun yn =>
+  ([yn.1.regs Search.answer, yn.1.regs Search.found, yn.1.regs CountCall.modulus],
+    decide (yn.2 ≤ 1049))) = some ([3, 1, 12], true))
+
+-- The same nonempty factor-two case discharges every fit, array and bitmap premise of the
+-- complete native execution theorem; its output witness is the actual executed state.
+example : ∃ y, ExecWithin 8 Search.program laterInput y 1049 ∧ y.regs Search.answer = 3 := by
+  obtain ⟨y, he, _, _, ha⟩ := Search.exec (w := 6) laterInput laterValues
+    (by decide) (by decide) (by decide) (by decide) (by decide)
+    (by intro q hq; change q ≤ 3 at hq; interval_cases q <;> decide)
+    (by intro j i _; unfold laterValues; split; split <;> decide; decide)
+    (by intro j; fin_cases j <;> decide) (by intro j; fin_cases j <;> decide)
+    (by decide) (by intro j; fin_cases j <;> decide) (by intro j; fin_cases j <;> decide)
+    (by intro j; fin_cases j <;> decide) (by intro j; fin_cases j <;> decide)
+    (by
+      intro j i hi
+      fin_cases j
+      · have hi' : i < 2 := hi
+        interval_cases i <;> decide
+      · have hi' : i < 0 := hi
+        omega
+      · have hi' : i < 0 := hi
+        omega)
+    (by
+      intro j i hi k hk he
+      fin_cases j
+      · have hi' : i < 2 := Finset.mem_range.mp hi
+        have hk' : k < 2 := Finset.mem_range.mp hk
+        interval_cases i <;> interval_cases k <;> simp [laterValues] at he ⊢
+      · have hi' : i < 0 := Finset.mem_range.mp hi
+        omega
+      · have hi' : i < 0 := Finset.mem_range.mp hi
+        omega)
+  refine ⟨y, ?_, ha.trans (by decide)⟩
+  convert he using 1
+  decide
+
+end ComplexityTests.WordRAMChanHeSearch
diff --git a/ComplexityTests/WordRAMPrimeTable.lean b/ComplexityTests/WordRAMPrimeTable.lean
new file mode 100644
index 0000000000..43c6cb6a40
--- /dev/null
+++ b/ComplexityTests/WordRAMPrimeTable.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Algorithms.WordRAM.PrimeTable
+
+/-! # Native trial division and prime bitmap regressions -/
+
+namespace ComplexityTests.WordRAMPrimeTable
+
+open Cslib.WordRAM
+open Cslib.Algorithms.WordRAM
+
+private def trialInput (n : ℕ) : Data 6 := (Data.init []).set PrimeTrial.arg n
+
+/-- The smallest candidate is prime; the first composite and a larger prime are distinguished. -/
+example : (Code.eval 8 8 PrimeTrial.program (trialInput 2)).map
+      (fun yn => yn.1.regs PrimeTrial.flag) = some 1 ∧
+    (Code.eval 8 8 PrimeTrial.program (trialInput 4)).map
+      (fun yn => yn.1.regs PrimeTrial.flag) = some 0 ∧
+    (Code.eval 8 8 PrimeTrial.program (trialInput 7)).map
+      (fun yn => yn.1.regs PrimeTrial.flag) = some 1 := by decide
+
+/-- The generic trial-division theorem is admissible on a composite candidate. -/
+example : ∃ y, ExecWithin 8 PrimeTrial.program (trialInput 4) y 20 ∧
+    y.regs PrimeTrial.flag = 0 ∧ y.regs PrimeTrial.arg = 4 ∧ y.mem 0 = 0 := by
+  obtain ⟨y, hy, hf, ha, hm⟩ := PrimeTrial.exec (w := 8) (trialInput 4)
+    (by decide) (by decide)
+  exact ⟨y, hy, hf.trans (by decide), ha, by rw [hm]; rfl⟩
+
+private def tableInput (n : ℕ) : Data 15 :=
+  ⟨fun i => if i = PrimeTable.limit then n else if i = PrimeTable.base then 20 else 0,
+    fun _ => 79⟩
+
+private def observe (n : ℕ) : Option (List ℕ × ℕ) :=
+  (Code.eval 8 (n + 1) PrimeTable.program (tableInput n)).map fun yn =>
+    ((List.range (n + 1)).map (fun i => yn.1.mem (20 + i)), yn.1.regs PrimeTable.count)
+
+/-- Zero and one are not prime; the length-two boundary adds the first prime bit. -/
+example : observe 0 = some ([0], 0) ∧ observe 1 = some ([0, 0], 0) ∧
+    observe 2 = some ([0, 0, 1], 1) := by decide
+
+-- This concrete interpreter traverses all trial divisions up to ten and their register maps.
+set_option maxRecDepth 4096 in
+/-- The complete bitmap overwrites nonzero memory and counts all four primes up to ten. -/
+example : observe 10 = some ([0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0], 4) := by decide
+
+/-- The quantitative complete-table contract has a satisfiable frame and fit instance. -/
+example : ∃ y, ExecWithin 8 PrimeTable.program (tableInput 10) y 943 ∧
+    y.regs PrimeTable.count = 4 ∧ y.mem 22 = 1 ∧ y.mem 24 = 0 ∧
+    y.mem 19 = 79 ∧ y.mem 31 = 79 := by
+  obtain ⟨y, hy, hm, hc, _⟩ := PrimeTable.exec (w := 8) (tableInput 10)
+    (by decide) (by decide)
+  refine ⟨y, hy, hc.trans (by decide), ?_, ?_, ?_, ?_⟩ <;> rw [hm] <;> decide
+
+/-- A fitting base can still have a nonfitting bitmap endpoint, and then execution faults. -/
+example : (Code.eval 8 6 PrimeTable.program
+    ((tableInput 5).set PrimeTable.base 253)).map (fun yn => yn.1.regs PrimeTable.count) =
+      none := by decide
+
+end ComplexityTests.WordRAMPrimeTable
diff --git a/ROADMAP.md b/ROADMAP.md
index 5fc6cb5a6f..96a86aba23 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -429,6 +429,10 @@ each statement against the numbered result. Organize modules by subject, not cha
   kept separate; and develop general open-program composition. Use Cook–Levin and GGM as
   regression clients. Improve configuration views, tape partitions and handoff identities only
   where several clients benefit, keeping machine transitions out of global simp.
+- **Native Chan–He components** ([#1446]): native parameter, collision-counting, prime-table and
+  collision-tested minimum-search programs have explicit local fit/frame/cost contracts.
+  Frontend enumeration, heavy extraction, recursive traversal, packed output and global
+  preprocessing width/time composition remain.
 - **Mathlib TM2:** sublinear work-space comparisons and a linear-space forward simulation.
 - **Generic RAM:** uniform arbitrary-program dispatch and general width-selection and input-fit
   theorems; simulating operations by programs over smaller bases; structured programs and time
@@ -444,7 +448,7 @@ each statement against the numbered result. Organize modules by subject, not cha
   witness recovery ([#1447]) are proved mathematically. The tensor identity, full recursion,
   shared encodings and pruned-evaluation core ([#1459]) include exact visited-leaf and passed-set
   bounds, with the empty zero-depth root handled explicitly. The finite thin-product component
-  ([#1463]) proves valid layouts, arbitrary-size padding/tiling, exact queried signed products and
+  ([#1463](https://github.com/cslib-community/complexitylib/issues/1463)) proves valid layouts, arbitrary-size padding/tiling, exact queried signed products and
   sparse encoding/leaf/passed-set totals. These counts are not native instruction costs. It still
   needs native tensor/sparse-query programs, native Chan–He preprocessing, the reduction
   host, the fast Exact Triangle solver and full
@@ -598,7 +602,9 @@ not planned, not as proved.
 [#1435]: https://github.com/cslib-community/complexitylib/issues/1435
 [#1438]: https://github.com/cslib-community/complexitylib/issues/1438
 [#1442]: https://github.com/cslib-community/complexitylib/issues/1442
+[#1446]: https://github.com/cslib-community/complexitylib/issues/1446
 [#1447]: https://github.com/cslib-community/complexitylib/issues/1447
 [#1449]: https://github.com/cslib-community/complexitylib/issues/1449
+[#1459]: https://github.com/cslib-community/complexitylib/issues/1459
 [#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 b009e0bce4..3e4d44738d 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -177,6 +177,11 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   [#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
   are retained; the native proofs and representation choices are local.
+  Native numeric parameter computation, signed-residue/histogram counting, trial-division prime
+  tables and collision-tested least-prime scans also use the existing `WordRAM.Code`/`ExecWithin`
+  APIs. Their explicit local fit, frame and charged-cost contracts do not yet compose the complete
+  preprocessing from input through frontend, heavy sets, recursion and packed output; the global
+  logarithmic width and subquadratic preprocessing bound remain in #1446.
 
   `Algorithms/ThreeSum/ThreeSets.lean` and `ArrayPacking.lean` provide the generic distinct-position
   frontend and three-array packing. `Algorithms/ThreeSum/ChanHe/` now adapts the core mathematical