diff --git a/Complexity.lean b/Complexity.lean
index 4d8216846c..d0f5e12191 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -152,6 +152,7 @@ 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.Modulus
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Query
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Residues
diff --git a/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Modulus.lean b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Modulus.lean
new file mode 100644
index 0000000000..cce0b1404f
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Modulus.lean
@@ -0,0 +1,536 @@
+/-
+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.Search
+
+/-!
+# Native setup of the two Chan–He prime searches
+
+The first search uses thresholds `3Λ|Sⱼ|²`. After saving its selected prime, native counting
+at that prime provides the second thresholds `3Λ coll Sⱼ p`. Both searches use the complete
+prime scan and collision queries, including explicit positive signed-modulus encoding.
+
+## Main definitions
+
+* `Modulus.firstSetup`: compute the first search's three thresholds.
+* `Modulus.secondSetup`: compute the second thresholds from native counts.
+* `Modulus.program`: compute the existing Chan–He modulus using two native minimum searches.
+
+## Main results
+
+* `Modulus.exec`: exact modulus, input frame and charged cost from explicit local fits.
+* `Modulus.not_readsWidth`: the program does not inspect the physical word width.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.ThreeSum.ChanHe
+
+/-- Collision divisor bound `Λ`. -/
+abbrev digits : Fin 64 := 59
+/-- First selected candidate, or one if none qualifies. -/
+abbrev first : Fin 64 := 60
+/-- Three times the collision divisor bound. -/
+abbrev multiplier : Fin 64 := 61
+/-- Unsigned product of the two selections, each defaulting to one. -/
+abbrev output : Fin 64 := 62
+
+/-- Charge all six square/threshold multiplications and the three scalar setup instructions. -/
+def firstSetup : Code .standard 64 := ram[
+  Search.rawModulus ← #3; multiplier ← digits * Search.rawModulus; Search.factor ← #1;
+  ⟪.op (.bin .mul (CollisionTest.threshold 0) (CountCall.length 0) (CountCall.length 0))⟫;
+  ⟪.op (.bin .mul (CollisionTest.threshold 0) multiplier (CollisionTest.threshold 0))⟫;
+  ⟪.op (.bin .mul (CollisionTest.threshold 1) (CountCall.length 1) (CountCall.length 1))⟫;
+  ⟪.op (.bin .mul (CollisionTest.threshold 1) multiplier (CollisionTest.threshold 1))⟫;
+  ⟪.op (.bin .mul (CollisionTest.threshold 2) (CountCall.length 2) (CountCall.length 2))⟫;
+  ⟪.op (.bin .mul (CollisionTest.threshold 2) multiplier (CollisionTest.threshold 2))⟫ ]
+
+/-- Charge all three second-threshold multiplications and their scalar setup. -/
+def secondSetup : Code .standard 64 := ram[
+  Search.rawModulus ← #3; multiplier ← digits * Search.rawModulus;
+  ⟪.op (.bin .mul (CollisionTest.threshold 0) multiplier (CountCall.result 0))⟫;
+  ⟪.op (.bin .mul (CollisionTest.threshold 1) multiplier (CountCall.result 1))⟫;
+  ⟪.op (.bin .mul (CollisionTest.threshold 2) multiplier (CountCall.result 2))⟫;
+  Search.factor ← first ]
+
+/-- Run both concrete searches and compute their product. The prime table and its count are
+shared by all nodes and are supplied in the search ABI. -/
+def program : Code .standard 64 :=
+  .seq firstSetup (.seq Search.program
+    (.seq (ram[ first ← Search.answer; Search.two ← #2; CountCall.modulus ← first * Search.two ])
+      (.seq CountTriple.program (.seq secondSetup
+        (.seq Search.program (ram[ output ← first * Search.answer ]))))))
+
+/-- The exact data after the first setup; memory is unchanged. -/
+def firstState (x : Data 64) : Data 64 :=
+  ((((((((x.set Search.rawModulus 3).set multiplier (3 * x.regs digits)).set
+    Search.factor 1).set (CollisionTest.threshold 0) (x.regs (CountCall.length 0) ^ 2)).set
+    (CollisionTest.threshold 0) (3 * x.regs digits * x.regs (CountCall.length 0) ^ 2)).set
+    (CollisionTest.threshold 1) (x.regs (CountCall.length 1) ^ 2)).set
+    (CollisionTest.threshold 1) (3 * x.regs digits * x.regs (CountCall.length 1) ^ 2)).set
+    (CollisionTest.threshold 2) (x.regs (CountCall.length 2) ^ 2)).set
+    (CollisionTest.threshold 2) (3 * x.regs digits * x.regs (CountCall.length 2) ^ 2)
+
+/-- First-search thresholds are computed by nine actual native instructions. -/
+theorem exec_firstSetup {w : ℕ} (x : Data 64) (h3 : Fits w 3)
+    (htriple : Fits w (3 * x.regs digits))
+    (hsq : ∀ j, Fits w (x.regs (CountCall.length j) ^ 2))
+    (hcut : ∀ j, Fits w (3 * x.regs digits * x.regs (CountCall.length j) ^ 2)) :
+    ExecWithin w firstSetup x (firstState x) 9 := by
+  have h1 : Fits w 1 := h3.of_le (by omega)
+  simp only [digits] at htriple
+  simp only [CountCall.length, pow_two] at hsq hcut
+  ram_eval [firstSetup, firstState, h3, h1, htriple, hsq 0, hsq 1, hsq 2,
+    hcut 0, hcut 1, hcut 2, digits, multiplier, Search.rawModulus, Search.factor,
+    CountCall.length, CollisionTest.threshold, Fin.mk.injEq, pow_two, Nat.mul_comm]
+
+/-- The exact data after the second setup; memory is unchanged. -/
+def secondState (x : Data 64) : Data 64 :=
+  (((((x.set Search.rawModulus 3).set multiplier (3 * x.regs digits)).set
+    (CollisionTest.threshold 0) (3 * x.regs digits * x.regs (CountCall.result 0))).set
+    (CollisionTest.threshold 1) (3 * x.regs digits * x.regs (CountCall.result 1))).set
+    (CollisionTest.threshold 2) (3 * x.regs digits * x.regs (CountCall.result 2))).set
+    Search.factor (x.regs first)
+
+/-- Second-search thresholds are computed by six actual native instructions. -/
+theorem exec_secondSetup {w : ℕ} (x : Data 64) (h3 : Fits w 3)
+    (htriple : Fits w (3 * x.regs digits))
+    (hcut : ∀ j, Fits w (3 * x.regs digits * x.regs (CountCall.result j))) :
+    ExecWithin w secondSetup x (secondState x) 6 := by
+  simp only [digits] at htriple
+  simp only [CountCall.result] at hcut
+  ram_eval [secondSetup, secondState, h3, htriple, hcut, digits, multiplier, first,
+    Search.rawModulus, Search.factor, CountCall.result, CollisionTest.threshold,
+    Fin.mk.injEq, Nat.mul_comm]
+
+private theorem selector_bounds {m : ℕ} (hm : 1 ≤ m) (A : ℕ → Prop) [DecidablePred A] :
+    1 ≤ minOrOne {q ∈ Nat.primesLE m | A q} ∧
+      minOrOne {q ∈ Nat.primesLE m | A q} ≤ m := by
+  let S := {q ∈ Nat.primesLE m | A q}
+  by_cases h : S.Nonempty
+  · have hmem : S.min' h ∈ S := Finset.min'_mem _ _
+    have hprime : (S.min' h).Prime ∧ S.min' h < m + 1 := by
+      have hh := (Finset.mem_filter.mp hmem).1
+      rw [Nat.primesLE_eq_filter_range, Finset.mem_filter, Finset.mem_range] at hh
+      exact ⟨hh.2, hh.1⟩
+    change 1 ≤ minOrOne S ∧ minOrOne S ≤ m
+    rw [minOrOne, dite_eq_left h]
+    exact ⟨by have := hprime.1.two_le; omega, by omega⟩
+  · change 1 ≤ minOrOne S ∧ minOrOne S ≤ m
+    rw [minOrOne, dite_eq_right h]
+    exact ⟨le_refl _, hm⟩
+
+private theorem forall_three {P : Fin 3 → Prop} : (∀ j, P j) ↔ P 0 ∧ P 1 ∧ P 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
+
+private theorem first_selector (x : Data 64) (values : Fin 3 → ℕ → ℤ)
+    (hinj : ∀ j, Set.InjOn (values j)
+      (↑(Finset.range (x.regs (CountCall.length j))) : Set ℕ)) :
+    minOrOne {q ∈ Nat.primesLE (x.regs Search.limit) | ∀ j : Fin 3,
+      coll ((Finset.range (x.regs (CountCall.length j))).image (values j)) q *
+        (Nat.primesLE (x.regs Search.limit)).card ≤
+          3 * x.regs digits * x.regs (CountCall.length j) ^ 2} =
+      firstP (Nat.primesLE (x.regs Search.limit)) (x.regs digits)
+        ((Finset.range (x.regs (CountCall.length 0))).image (values 0))
+        ((Finset.range (x.regs (CountCall.length 1))).image (values 1))
+        ((Finset.range (x.regs (CountCall.length 2))).image (values 2)) := by
+  have hcard (j : Fin 3) : ((Finset.range (x.regs (CountCall.length j))).image (values j)).card =
+      x.regs (CountCall.length j) := (Finset.card_image_of_injOn (hinj j)).trans
+        (Finset.card_range _)
+  simp only [firstP, hcard, forall_three]
+
+private abbrev Parameter (i : Fin 64) : Prop :=
+  (28 ≤ i.val ∧ i.val ≤ 35) ∨ (40 ≤ i.val ∧ i.val ≤ 42) ∨ i = digits
+
+private def Same (x y : Data 64) : Prop :=
+  (∀ i, Parameter i → y.regs i = x.regs i) ∧
+    ∀ a < x.regs CountCall.scratch, y.mem a = x.mem a
+
+/-- One polynomial bound for selector counters, thresholds and memory addresses. -/
+def budget (x : Data 64) : ℕ :=
+  let n := x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+    x.regs (CountCall.length 2)
+  x.regs CountCall.histogram + x.regs CountCall.scratch + x.regs Search.primes +
+    x.regs (CountCall.source 0) + x.regs (CountCall.source 1) + x.regs (CountCall.source 2) +
+    (n + 1) ^ 2 * (3 * x.regs digits + x.regs CollisionTest.card + 1) +
+    x.regs Search.limit ^ 2 + x.regs Search.limit + 100
+
+private theorem length_le_sum (x : Data 64) (j : Fin 3) : x.regs (CountCall.length j) ≤
+    x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+      x.regs (CountCall.length 2) := by
+  fin_cases j <;> dsimp [CountCall.length] <;> omega
+
+private theorem source_le_sum (x : Data 64) (j : Fin 3) : x.regs (CountCall.source j) ≤
+    x.regs (CountCall.source 0) + x.regs (CountCall.source 1) +
+      x.regs (CountCall.source 2) := by
+  fin_cases j <;> dsimp [CountCall.source] <;> omega
+
+private theorem budget_bounds (x : Data 64) (j : Fin 3) :
+    x.regs (CountCall.source j) + x.regs (CountCall.length j) ≤ budget x ∧
+    x.regs CountCall.scratch + x.regs (CountCall.length j) ≤ budget x ∧
+    x.regs CountCall.histogram + x.regs Search.limit ^ 2 ≤ budget x ∧
+    x.regs Search.primes + (x.regs Search.limit + 1) ≤ budget x ∧
+    x.regs Search.limit + 3 ≤ budget x ∧
+    x.regs (CountCall.length j) ^ 2 + x.regs (CountCall.length j) + 1 ≤ budget x ∧
+    x.regs (CountCall.length j) ^ 2 * x.regs CollisionTest.card ≤ budget x ∧
+    3 * x.regs digits * x.regs (CountCall.length j) ^ 2 ≤ budget x ∧
+    3 * x.regs digits ≤ budget x ∧ 3 ≤ budget x := by
+  let n := x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+    x.regs (CountCall.length 2)
+  let poly := (n + 1) ^ 2 * (3 * x.regs digits + x.regs CollisionTest.card + 1)
+  have hn : x.regs (CountCall.length j) ≤ n := length_le_sum x j
+  have hs := source_le_sum x j
+  have hpoly : (n + 1) ^ 2 ≤ poly := by
+    simpa only [Nat.mul_one] using Nat.mul_le_mul_left ((n + 1) ^ 2)
+      (show 1 ≤ 3 * x.regs digits + x.regs CollisionTest.card + 1 by omega)
+  have hsquare : x.regs (CountCall.length j) ^ 2 ≤ (n + 1) ^ 2 := by nlinarith
+  have hcard : x.regs (CountCall.length j) ^ 2 * x.regs CollisionTest.card ≤ poly := by
+    exact (Nat.mul_le_mul_right _ hsquare).trans
+      (Nat.mul_le_mul_left _ (by omega))
+  have hcut : 3 * x.regs digits * x.regs (CountCall.length j) ^ 2 ≤ poly := by
+    rw [Nat.mul_comm (3 * x.regs digits)]
+    exact (Nat.mul_le_mul_right _ hsquare).trans
+      (Nat.mul_le_mul_left _ (by omega))
+  have htriple : 3 * x.regs digits ≤ poly := by
+    have hbase : 1 ≤ (n + 1) ^ 2 := by nlinarith
+    exact (show 3 * x.regs digits ≤ 3 * x.regs digits * (n + 1) ^ 2 by
+      nlinarith).trans (by
+        rw [Nat.mul_comm]
+        exact Nat.mul_le_mul_left _ (by omega))
+  have hb : budget x = x.regs CountCall.histogram + x.regs CountCall.scratch +
+      x.regs Search.primes + x.regs (CountCall.source 0) + x.regs (CountCall.source 1) +
+      x.regs (CountCall.source 2) + poly + x.regs Search.limit ^ 2 +
+        x.regs Search.limit + 100 := rfl
+  rw [hb]
+  have hsize : x.regs (CountCall.length j) ^ 2 + x.regs (CountCall.length j) + 1 ≤ poly := by
+    nlinarith
+  omega
+
+private theorem same_length {x y : Data 64} (h : Same x y) (j : Fin 3) :
+    y.regs (CountCall.length j) = x.regs (CountCall.length j) :=
+  h.1 _ (by dsimp [Parameter, CountCall.length]; omega)
+
+private theorem same_source {x y : Data 64} (h : Same x y) (j : Fin 3) :
+    y.regs (CountCall.source j) = x.regs (CountCall.source j) :=
+  h.1 _ (by dsimp [Parameter, CountCall.source]; omega)
+
+private theorem signed_nat_mono {w a b : ℕ} (h : GenericRAM.Signed.Fits w (b : ℤ))
+    (hab : a ≤ b) : GenericRAM.Signed.Fits w (a : ℤ) := by
+  refine ⟨h.1, ?_, lt_of_le_of_lt (by exact_mod_cast hab) h.2.2⟩
+  have hnonneg : (0 : ℤ) ≤ a := Nat.cast_nonneg _
+  have hpower : (0 : ℤ) ≤ 2 ^ (w - 1) := by positivity
+  omega
+
+private structure LocalFits (w : ℕ) (x : Data 64) : Prop where
+  source : ∀ j, Fits (w + 2) (x.regs (CountCall.source j) + x.regs (CountCall.length j))
+  scratch : ∀ j, Fits (w + 2) (x.regs CountCall.scratch + x.regs (CountCall.length j))
+  histogram : Fits (w + 2) (x.regs CountCall.histogram + x.regs Search.limit ^ 2)
+  bitmap : Fits (w + 2) (x.regs Search.primes + (x.regs Search.limit + 1))
+  limit : Fits (w + 2) (x.regs Search.limit + 3)
+  total : ∀ j, Fits (w + 2)
+    (x.regs (CountCall.length j) ^ 2 + x.regs (CountCall.length j) + 1)
+  product : ∀ j, Fits (w + 2) (x.regs (CountCall.length j) ^ 2 * x.regs CollisionTest.card)
+  cutoff : ∀ j, Fits (w + 2) (3 * x.regs digits * x.regs (CountCall.length j) ^ 2)
+  triple : Fits (w + 2) (3 * x.regs digits)
+  three : Fits (w + 2) 3
+
+private theorem localFits_of_budget {w : ℕ} (x : Data 64) (h : Fits (w + 2) (budget x)) :
+    LocalFits w x := by
+  have hb := budget_bounds x 0
+  refine ⟨fun j => h.of_le (budget_bounds x j).1,
+    fun j => h.of_le (budget_bounds x j).2.1, h.of_le hb.2.2.1,
+    h.of_le hb.2.2.2.1, h.of_le hb.2.2.2.2.1, ?_, ?_, ?_,
+    h.of_le hb.2.2.2.2.2.2.2.2.1, h.of_le hb.2.2.2.2.2.2.2.2.2⟩
+  · exact fun j => h.of_le (budget_bounds x j).2.2.2.2.2.1
+  · exact fun j => h.of_le (budget_bounds x j).2.2.2.2.2.2.1
+  · exact fun j => h.of_le (budget_bounds x j).2.2.2.2.2.2.2.1
+
+/-- One search with its factor bounded by the largest candidate. -/
+def searchTime (x : Data 64) : ℕ :=
+  (x.regs Search.limit + 1) * (34 * (x.regs (CountCall.length 0) +
+    x.regs (CountCall.length 1) + x.regs (CountCall.length 2)) +
+    15 * x.regs Search.limit ^ 2 + 102) + 9
+
+private theorem exec_search {w : ℕ} (x y : Data 64) (values : Fin 3 → ℕ → ℤ)
+    (hmod : GenericRAM.Signed.Fits w ((x.regs Search.limit ^ 2 : ℕ) : ℤ))
+    (hfits : LocalFits w x) (hy : Same x y)
+    (hfactor : 0 < y.regs Search.factor) (hfactorle : y.regs Search.factor ≤ x.regs Search.limit)
+    (hbefore : x.regs Search.primes + (x.regs Search.limit + 1) ≤ x.regs CountCall.scratch)
+    (hbitmap : ∀ q ≤ x.regs Search.limit,
+      x.mem (x.regs Search.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))
+    (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 ℕ)) :
+    ∃ z, ExecWithin (w + 2) Search.program y z (searchTime x) ∧ Same x z ∧
+      z.regs Search.answer = minOrOne {q ∈ Nat.primesLE (x.regs Search.limit) | ∀ j : Fin 3,
+        coll ((Finset.range (x.regs (CountCall.length j))).image (values j))
+          (y.regs Search.factor * q) * x.regs CollisionTest.card ≤
+            y.regs (CollisionTest.threshold j)} := by
+  have hl := same_length hy
+  have hs := same_source hy
+  have hk : y.regs CountCall.scratch = x.regs CountCall.scratch := hy.1 _ (by decide)
+  have hd : y.regs CountCall.histogram = x.regs CountCall.histogram := hy.1 _ (by decide)
+  have hm : y.regs Search.limit = x.regs Search.limit := hy.1 _ (by decide)
+  have hp : y.regs Search.primes = x.regs Search.primes := hy.1 _ (by decide)
+  have hc : y.regs CollisionTest.card = x.regs CollisionTest.card := hy.1 _ (by decide)
+  have hM : y.regs Search.factor * x.regs Search.limit ≤ x.regs Search.limit ^ 2 := by
+    simpa only [pow_two] using Nat.mul_le_mul_right (x.regs Search.limit) hfactorle
+  have hyinput : ∀ j i, i < y.regs (CountCall.length j) →
+      y.mem (y.regs (CountCall.source j) + i) = encode (values j i) := by
+    intro j i hi
+    rw [hl] at hi
+    rw [hs, hy.2 _ (by have := hsk j; omega)]
+    exact hinput j i hi
+  have hybitmap : ∀ q ≤ y.regs Search.limit,
+      y.mem (y.regs Search.primes + q) = if q.Prime then 1 else 0 := by
+    intro q hq
+    have hq' : q ≤ x.regs Search.limit := by simpa only [hm] using hq
+    rw [hp, hy.2 _ (by omega)]
+    exact hbitmap q hq'
+  obtain ⟨z, he, hr, hmem, ha⟩ := Search.exec y values hfactor
+    (by rw [hm]; exact signed_nat_mono hmod hM)
+    (by simpa only [hm] using hfits.limit) (by simpa only [hp, hm] using hfits.bitmap)
+    (by simpa only [hp, hm, hk] using hbefore)
+    hybitmap
+    (by simpa only [hl] using hvalues) (by simpa only [hs, hl] using hfits.source)
+    (by simpa only [hk, hl] using hfits.scratch)
+    (by rw [hd, hm]; exact hfits.histogram.of_le (Nat.add_le_add_left hM _))
+    (by simpa only [hl, pow_two] using hfits.total)
+    (by simpa only [hl, hc, pow_two] using hfits.product)
+    (by simpa only [hs, hl, hk] using hsk) (by simpa only [hk, hl, hd] using hkd)
+    hyinput (by simpa only [hl] using hinj)
+  refine ⟨z, he.mono ?_, ?_, ?_⟩
+  · simp only [hm, hl, searchTime]
+    exact Nat.add_le_add_right (Nat.mul_le_mul_left _
+      (Nat.add_le_add_right (Nat.add_le_add_left (Nat.mul_le_mul_left 15 hM) _) _)) _
+  · refine ⟨?_, fun a ha => (hmem a (by simpa only [hk] using ha)).trans (hy.2 a ha)⟩
+    intro i hi
+    by_cases hid : i = digits
+    · subst i
+      exact (he.regs_eq (Search.preserves_caller _ (by decide))).trans (hy.1 _ hi)
+    · exact (hr i (by dsimp only [Parameter] at hi; omega)).trans (hy.1 i hi)
+  · simpa only [hm, hl, hc] using ha
+
+private theorem same_set {x y : Data 64} (h : Same x y) (i : Fin 64)
+    (hi : ¬Parameter i) (v : ℕ) : Same x (y.set i v) := by
+  refine ⟨fun j hj => ?_, h.2⟩
+  have hji : j ≠ i := fun e => hi (e ▸ hj)
+  simpa only [Data.set_regs, Function.update_of_ne hji] using h.1 j hj
+
+private theorem firstSetup_preserves (i : Fin 64) (hi : Parameter i) :
+    firstSetup.Preserves i := by
+  fin_cases i <;> norm_num [Parameter, digits] at hi <;> decide
+
+private theorem secondSetup_preserves (i : Fin 64) (hi : Parameter i) :
+    secondSetup.Preserves i := by
+  fin_cases i <;> norm_num [Parameter, digits] at hi <;> decide
+
+private theorem exec_counts {w M : ℕ} (x y : Data 64) (values : Fin 3 → ℕ → ℤ)
+    (hM : 0 < M) (hMle : M ≤ x.regs Search.limit ^ 2)
+    (hmod : GenericRAM.Signed.Fits w ((x.regs Search.limit ^ 2 : ℕ) : ℤ))
+    (hfits : LocalFits w x) (hy : Same x y)
+    (hmodreg : y.regs CountCall.modulus = encode (M : ℤ))
+    (hvalues : ∀ j i, i < x.regs (CountCall.length j) → GenericRAM.Signed.Fits w (values j i))
+    (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 ℕ)) :
+    ∃ z, ExecWithin (w + 2) CountTriple.program y z
+        (34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+          x.regs (CountCall.length 2)) + 15 * M + 72) ∧ Same x z ∧
+      (∀ j, z.regs (CountCall.result j) = coll
+        ((Finset.range (x.regs (CountCall.length j))).image (values j)) M) ∧
+      ∀ i, ((28 ≤ i.val ∧ i.val < 37) ∨ 40 ≤ i.val) → z.regs i = y.regs i := by
+  have hl := same_length hy
+  have hs := same_source hy
+  have hk : y.regs CountCall.scratch = x.regs CountCall.scratch := hy.1 _ (by decide)
+  have hd : y.regs CountCall.histogram = x.regs CountCall.histogram := hy.1 _ (by decide)
+  have hyinput : ∀ j i, i < y.regs (CountCall.length j) →
+      y.mem (y.regs (CountCall.source j) + i) = encode (values j i) := by
+    intro j i hi
+    rw [hl] at hi
+    rw [hs, hy.2 _ (by have := hsk j; omega)]
+    exact hinput j i hi
+  obtain ⟨z, he, hv, hr, hmem⟩ := CountTriple.exec y values hM
+    (signed_nat_mono hmod hMle) hmodreg (by simpa only [hl] using hvalues)
+    (by simpa only [hs, hl] using hfits.source)
+    (by simpa only [hk, hl] using hfits.scratch)
+    (by rw [hd]; exact hfits.histogram.of_le (Nat.add_le_add_left hMle _))
+    (by simpa only [hl, pow_two] using hfits.total)
+    (by simpa only [hs, hl, hk] using hsk) (by simpa only [hk, hl, hd] using hkd)
+    hyinput (by simpa only [hl] using hinj)
+  refine ⟨z, ?_, ?_, ?_, hr⟩
+  · simpa only [hl] using he
+  · refine ⟨fun i hi => (hr i ?_).trans (hy.1 i hi), ?_⟩
+    · dsimp only [Parameter] at hi
+      rcases hi with hi | hi | rfl
+      · omega
+      · omega
+      · decide
+    · intro a ha
+      exact (hmem a (by simpa only [hk] using ha)).trans (hy.2 a ha)
+  · simpa only [hl] using hv
+
+/-- Both searches, a baseline collision count, scalar setup and the final product. -/
+def cost (x : Data 64) : ℕ :=
+  2 * searchTime x + 34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) +
+    x.regs (CountCall.length 2)) + 15 * x.regs Search.limit + 91
+
+/-- Compute exactly the existing Chan–He modulus with two complete native prime searches.
+The prime bitmap/count is a shared input built by `PrimeTable.program`. A single polynomial
+budget bounds selector counters, thresholds and addresses; input values and the maximum modulus
+fit the source width. The final halt is excluded.
+
+The interface requires `m ≥ 2` for a nonempty candidate-prime window. The intended preprocessing
+caller uses `mPar n U = (wPar n U + 1) * (2 * log₂(wPar n U + 1) + 4) ≥ 4`.
+The default-only window `m = 1` is outside this interface, although the selector bounds extend
+to it; `m = 0` fails the default-selector upper bound. -/
+theorem exec {w : ℕ} (x : Data 64) (values : Fin 3 → ℕ → ℤ)
+    (hm : 2 ≤ x.regs Search.limit)
+    (hmod : GenericRAM.Signed.Fits w ((x.regs Search.limit ^ 2 : ℕ) : ℤ))
+    (hbudget : Fits (w + 2) (budget x))
+    (hcard : x.regs CollisionTest.card = (Nat.primesLE (x.regs Search.limit)).card)
+    (hbefore : x.regs Search.primes + (x.regs Search.limit + 1) ≤ x.regs CountCall.scratch)
+    (hbitmap : ∀ q ≤ x.regs Search.limit,
+      x.mem (x.regs Search.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))
+    (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 (cost x) ∧
+      (∀ i, ((28 ≤ i.val ∧ i.val ≤ 35) ∨ (40 ≤ i.val ∧ i.val ≤ 42) ∨ i = digits) →
+        y.regs i = x.regs i) ∧
+      (∀ a < x.regs CountCall.scratch, y.mem a = x.mem a) ∧
+      y.regs first = firstP (Nat.primesLE (x.regs Search.limit)) (x.regs digits)
+        ((Finset.range (x.regs (CountCall.length 0))).image (values 0))
+        ((Finset.range (x.regs (CountCall.length 1))).image (values 1))
+        ((Finset.range (x.regs (CountCall.length 2))).image (values 2)) ∧
+      y.regs output = modulus (Nat.primesLE (x.regs Search.limit)) (x.regs digits)
+        ((Finset.range (x.regs (CountCall.length 0))).image (values 0))
+        ((Finset.range (x.regs (CountCall.length 1))).image (values 1))
+        ((Finset.range (x.regs (CountCall.length 2))).image (values 2)) := by
+  let S (j : Fin 3) := (Finset.range (x.regs (CountCall.length j))).image (values j)
+  let Q := Nat.primesLE (x.regs Search.limit)
+  let p := firstP Q (x.regs digits) (S 0) (S 1) (S 2)
+  let q := secondP Q (x.regs digits) (S 0) (S 1) (S 2) p
+  have hp : 1 ≤ p ∧ p ≤ x.regs Search.limit := by
+    dsimp only [p, firstP, Q]
+    exact selector_bounds (by omega) _
+  have hq : 1 ≤ q ∧ q ≤ x.regs Search.limit := by
+    dsimp only [q, secondP, Q]
+    exact selector_bounds (by omega) _
+  have hfits := localFits_of_budget x hbudget
+  let a := firstState x
+  have ha : ExecWithin (w + 2) firstSetup x a 9 := exec_firstSetup x hfits.three hfits.triple
+    (fun j => (hfits.total j).of_le (by omega)) hfits.cutoff
+  have has : Same x a := ⟨fun i hi => ha.regs_eq (firstSetup_preserves i hi), fun _ _ => rfl⟩
+  have haf : a.regs Search.factor = 1 := by rfl
+  have hacut (j : Fin 3) : a.regs (CollisionTest.threshold j) =
+      3 * x.regs digits * x.regs (CountCall.length j) ^ 2 := by fin_cases j <;> rfl
+  obtain ⟨b, hb, hbs, hbp⟩ := exec_search x a values hmod hfits has
+    (by rw [haf]; omega) (by rw [haf]; omega) hbefore hbitmap hvalues hsk hkd hinput hinj
+  have hbanswer : b.regs Search.answer = p := by
+    rw [haf] at hbp
+    simp only [Nat.one_mul, hacut, hcard] at hbp
+    exact hbp.trans (first_selector x values hinj)
+  let c := ((b.set first p).set Search.two 2).set CountCall.modulus (2 * p)
+  have hpf : GenericRAM.Signed.Fits w (p : ℤ) := signed_nat_mono hmod
+    (hp.2.trans (Nat.le_self_pow two_ne_zero _))
+  have henc : encode (p : ℤ) = 2 * p := by simp [encode]
+  have hencoded : Fits (w + 2) (2 * p) := by
+    rw [← henc]
+    exact (encode_fits hpf).mono (by omega)
+  have htwo : Fits (w + 2) 2 := hfits.three.of_le (by omega)
+  have hc : ExecWithin (w + 2)
+      (ram[ first ← Search.answer; Search.two ← #2; CountCall.modulus ← first * Search.two ])
+      b c 3 := by
+    ram_eval [c, hbanswer, htwo, hencoded, first, Search.answer, Search.two,
+      CountCall.modulus, Fin.mk.injEq, Nat.mul_comm]
+  have hcs : Same x c := same_set (same_set (same_set hbs first (by decide) _)
+    Search.two (by decide) _) CountCall.modulus (by decide) _
+  have hcm : c.regs CountCall.modulus = encode (p : ℤ) := by simpa only [henc] using
+    (show c.regs CountCall.modulus = 2 * p from rfl)
+  obtain ⟨d, hd, hds, hdcounts, hdr⟩ := exec_counts x c values (by omega)
+    (hp.2.trans (Nat.le_self_pow two_ne_zero _)) hmod hfits hcs hcm hvalues hsk hkd hinput hinj
+  have hdvalue : d.regs first = p := (hdr first (by decide)).trans (by rfl)
+  have hddigits : d.regs digits = x.regs digits := hds.1 _ (by decide)
+  have hcoll (j : Fin 3) : coll (S j) p ≤ x.regs (CountCall.length j) ^ 2 := by
+    have hsize : (S j).card ≤ x.regs (CountCall.length j) :=
+      Finset.card_image_le.trans_eq (Finset.card_range _)
+    exact (coll_le_sq _ _).trans (Nat.pow_le_pow_left hsize 2)
+  let e := secondState d
+  have he : ExecWithin (w + 2) secondSetup d e 6 := exec_secondSetup d hfits.three
+    (by simpa only [hddigits] using hfits.triple)
+    (fun j => by
+      rw [hddigits, hdcounts]
+      exact (hfits.cutoff j).of_le (Nat.mul_le_mul_left _ (hcoll j)))
+  have hes : Same x e := ⟨fun i hi => (he.regs_eq (secondSetup_preserves i hi)).trans
+    (hds.1 i hi), hds.2⟩
+  have hef : e.regs Search.factor = p := by
+    change d.regs first = p
+    exact hdvalue
+  have hecut (j : Fin 3) : e.regs (CollisionTest.threshold j) =
+      3 * x.regs digits * coll (S j) p := by
+    have hr : e.regs (CollisionTest.threshold j) =
+        3 * d.regs digits * d.regs (CountCall.result j) := by fin_cases j <;> rfl
+    rw [hr, hddigits, hdcounts]
+  obtain ⟨f, hf, hfs, hfq⟩ := exec_search x e values hmod hfits hes
+    (by rw [hef]; omega) (by rw [hef]; exact hp.2)
+    hbefore hbitmap hvalues hsk hkd hinput hinj
+  have hfanswer : f.regs Search.answer = q := by
+    simpa only [hef, hecut, hcard, forall_three, q, secondP] using hfq
+  have hfvalue : f.regs first = p := by
+    rw [hf.regs_eq (Search.preserves_caller first (by decide))]
+    change d.regs first = p
+    exact hdvalue
+  have hprod : Fits (w + 2) (f.regs first * f.regs Search.answer) := by
+    rw [hfvalue, hfanswer]
+    apply hfits.histogram.of_le
+    have hle := Nat.mul_le_mul hp.2 hq.2
+    simpa only [pow_two] using hle.trans (Nat.le_add_left _ _)
+  have hfinish : ExecWithin (w + 2) (ram[ output ← first * Search.answer ]) f
+      (f.set output (p * q)) 1 := by
+    simpa only [BinOp.eval, hfvalue, hfanswer] using
+      (ExecWithin.bin (f := .mul) (d := output) (i := first) (j := Search.answer) hprod)
+  have hsame : Same x (f.set output (p * q)) := same_set hfs output (by decide) _
+  refine ⟨f.set output (p * q), ?_, hsame.1, hsame.2, ?_, ?_⟩
+  · exact (ha.seq (hb.seq (hc.seq (hd.seq (he.seq (hf.seq hfinish)))))).mono
+      (by dsimp only [cost]; omega)
+  · simpa +decide [output, first] using hfvalue
+  · change p * q = modulus Q (x.regs digits) (S 0) (S 1) (S 2)
+    rfl
+
+/-- The finite selector program never reads the word width. -/
+theorem not_readsWidth : ¬program.ReadsWidth := by decide
+
+end Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus
diff --git a/ComplexityTests/WordRAMChanHeModulus.lean b/ComplexityTests/WordRAMChanHeModulus.lean
new file mode 100644
index 0000000000..655224e245
--- /dev/null
+++ b/ComplexityTests/WordRAMChanHeModulus.lean
@@ -0,0 +1,107 @@
+/-
+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.Modulus
+
+/-! # Complete native two-prime modulus computations -/
+
+namespace ComplexityTests.WordRAMChanHeModulus
+
+open Cslib.WordRAM Cslib.WordRAM.Signed
+open Cslib.Algorithms.WordRAM.ThreeSum.ChanHe
+
+private def input (n digits : ℕ) (values : ℕ → ℤ) : Data 64 :=
+  ⟨fun i => if i.val = 28 ∨ i.val = 30 ∨ i.val = 32 then n
+    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 2 else if i.val = 41 then 10
+    else if i.val = 42 ∨ i.val = 59 then (if i.val = 42 then 1 else digits) else 71,
+    fun a => if 1 ≤ a ∧ a < 1 + n then encode (values (a - 1))
+      else if 10 ≤ a ∧ a ≤ 12 then (if a = 12 then 1 else 0) else 79⟩
+
+-- Each execution includes two complete prime scans and three baseline counting calls.
+set_option maxRecDepth 8192 in
+/-- Empty sets still compute the exact minimum/default specification, returning `2*2`. -/
+example : (Code.eval 8 6 Modulus.program (input 0 1 (fun i => i))).map
+    (fun yn => [yn.1.regs Modulus.first, yn.1.regs Modulus.output,
+      yn.1.regs Modulus.digits, yn.1.mem 12]) = some [2, 4, 1, 1] := by decide
+
+/-- A target word too small for the very first scalar setup is rejected. -/
+example : (Code.eval 1 1 Modulus.program (input 0 1 (fun i => i))).map
+    (fun yn => yn.1.regs Modulus.output) = none := by decide
+
+/-- The native execution contract is admissible at every small array length, including all
+fits, the complete bitmap, preserved input and injective enumeration. -/
+example (n : Fin 3) : ∃ y,
+    ExecWithin 10 Modulus.program (input n 1 (fun i => i)) y (714 * (n : ℕ) + 1111) ∧
+      y.regs Modulus.output = 4 := by
+  let x := input n 1 (fun i => i)
+  have hn (j : Fin 3) : x.regs (CountCall.length j) = n := by fin_cases j <;> rfl
+  have hs (j : Fin 3) : x.regs (CountCall.source j) = 1 := by fin_cases j <;> rfl
+  have hN : (n : ℕ) ≤ 2 := by omega
+  have hlimit : x.regs Search.limit = 2 := rfl
+  obtain ⟨y, he, hr, hm, hp, hv⟩ := Modulus.exec (w := 8) x (fun _ i => (i : ℤ))
+    (by change 2 ≤ 2; decide)
+    (by change Cslib.GenericRAM.Signed.Fits 8 (4 : ℤ); decide)
+    (by fin_cases n <;> decide) (by change 1 = (Nat.primesLE 2).card; decide)
+    (by change 10 + (2 + 1) ≤ 20; decide)
+    (by intro q hq; change q ≤ 2 at hq; fin_cases n <;> interval_cases q <;> decide)
+    (by intro j i hi; rw [hn] at hi; have hi1 : i ≤ 1 := by omega
+        interval_cases i <;> decide)
+    (by intro j; rw [hs, hn]; change 1 + (n : ℕ) ≤ 20; omega)
+    (by intro j; rw [hn]; change 20 + (n : ℕ) ≤ 30; omega)
+    (by
+      intro j i hi
+      rw [hn] at hi
+      rw [hs]
+      change (if 1 ≤ 1 + i ∧ 1 + i < 1 + (n : ℕ) then encode ((1 + i - 1 : ℕ) : ℤ)
+        else if 10 ≤ 1 + i ∧ 1 + i ≤ 12 then (if 1 + i = 12 then 1 else 0) else 79) = _
+      simp only [show 1 ≤ 1 + i ∧ 1 + i < 1 + (n : ℕ) by omega,
+        and_self, ↓reduceIte, show 1 + i - 1 = i by omega])
+    (by intro j a _ b _ hab; change (a : ℤ) = (b : ℤ) at hab; exact_mod_cast hab)
+  have hcost : Modulus.cost x = 714 * (n : ℕ) + 1111 := by
+    simp only [Modulus.cost, Modulus.searchTime, hn, hlimit]
+    omega
+  refine ⟨y, by simpa only [hcost] using he, ?_⟩
+  have hvalue : Cslib.Algorithms.ThreeSum.ChanHe.modulus (Nat.primesLE 2) 1
+      ((Finset.range (n : ℕ)).image fun i : ℕ => (i : ℤ))
+      ((Finset.range (n : ℕ)).image fun i : ℕ => (i : ℤ))
+      ((Finset.range (n : ℕ)).image fun i : ℕ => (i : ℤ)) = 4 := by fin_cases n <;> decide
+  simp only [hn] at hv
+  exact hv.trans hvalue
+
+/-- A zero divisor bound and negative colliding values reject the only prime twice. The full
+native theorem returns the exact default product one, with admissible input and resource bounds. -/
+example : ∃ y, ExecWithin 10 Modulus.program
+      (input 2 0 (fun i => if i = 0 then -2 else 0)) y
+      (Modulus.cost (input 2 0 (fun i => if i = 0 then -2 else 0))) ∧
+    y.regs Modulus.first = 1 ∧ y.regs Modulus.output = 1 := by
+  let values (i : ℕ) : ℤ := if i = 0 then -2 else 0
+  let x := input 2 0 values
+  have hn (j : Fin 3) : x.regs (CountCall.length j) = 2 := by fin_cases j <;> rfl
+  obtain ⟨y, he, hr, hm, hp, hv⟩ := Modulus.exec (w := 8) x (fun _ => values)
+    (by decide) (by decide) (by decide) (by decide) (by decide)
+    (by intro q hq; change q ≤ 2 at hq; interval_cases q <;> decide)
+    (by intro j i hi; rw [hn] at hi; interval_cases i <;> decide)
+    (by intro j; fin_cases j <;> decide) (by intro j; fin_cases j <;> decide)
+    (by intro j i hi; rw [hn] at hi; fin_cases j <;> interval_cases i <;> decide)
+    (by
+      intro j a ha b hb hab
+      simp only [Finset.mem_coe, Finset.mem_range, hn] at ha hb
+      interval_cases a <;> interval_cases b <;> norm_num [values] at *)
+  refine ⟨y, he, ?_, ?_⟩
+  · have hvalue : Cslib.Algorithms.ThreeSum.ChanHe.firstP (Nat.primesLE 2) 0
+        ((Finset.range 2).image values) ((Finset.range 2).image values)
+        ((Finset.range 2).image values) = 1 := by decide
+    simp only [hn] at hp
+    exact hp.trans hvalue
+  · have hvalue : Cslib.Algorithms.ThreeSum.ChanHe.modulus (Nat.primesLE 2) 0
+        ((Finset.range 2).image values) ((Finset.range 2).image values)
+        ((Finset.range 2).image values) = 1 := by decide
+    simp only [hn] at hv
+    exact hv.trans hvalue
+
+end ComplexityTests.WordRAMChanHeModulus
diff --git a/ROADMAP.md b/ROADMAP.md
index 96a86aba23..29f7bb4fde 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -433,6 +433,9 @@ each statement against the numbered result. Organize modules by subject, not cha
   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.
+- **Native Chan–He modulus** ([#1501](https://github.com/cslib-community/complexitylib/issues/1501)):
+  complete two-prime modulus selection has explicit local fit/frame/cost contracts. The full
+  preprocessing and global width/time composition objective remains under [#1446].
 - **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
diff --git a/UPSTREAM.md b/UPSTREAM.md
index 3e4d44738d..e60a23a35d 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -183,6 +183,10 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   preprocessing from input through frontend, heavy sets, recursion and packed output; the global
   logarithmic width and subquadratic preprocessing bound remain in #1446.
 
+  Complete native two-prime modulus selection uses the same `WordRAM.Code`/`ExecWithin` APIs,
+  with explicit local fit, frame and charged-cost contracts. This component does not complete
+  the preprocessing objective 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
   reduction: minimum-prime searches, collision/heavy-element bounds, light-element arrays, bounded