edemaine · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026
diff --git a/Complexity.lean b/Complexity.lean
@@ -61,6 +61,7 @@ public import Complexity.Algorithms.ThreeSum.ChanHe.Collisions
 public import Complexity.Algorithms.ThreeSum.ChanHe.Defs
 public import Complexity.Algorithms.ThreeSum.ChanHe.FromNumbers
 public import Complexity.Algorithms.ThreeSum.ChanHe.Recursion
+public import Complexity.Algorithms.ThreeSum.ChanHe.SelectorBounds
 public import Complexity.Algorithms.ThreeSum.ChanHe.Sizes
 public import Complexity.Algorithms.ThreeSum.Convolution
 public import Complexity.Algorithms.ThreeSum.Defs
@@ -118,6 +119,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,11 +147,67 @@ 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.BucketCounts
+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.CountPlace
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlaceMemory
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.CountTriple
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Modulus
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.NodeExec
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.NodeInitialize
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.NodeLayout
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.NodeMemory
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.NodeProgram
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.NodeRound
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.NodeSetup
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.NodeSpec
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Padding
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Place
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PlaceExec
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PlaceMemory
+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.ChanHe.TraversalAdmitted
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalCall
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalChildren
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalCost
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalDeliver
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalEmission
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalEmissionFrame
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalExec
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalFrames
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalInvariant
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalLive
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalLoop
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalModel
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalOutput
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalPending
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalProgram
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalResources
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalRoot
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalSkip
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalStack
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalStep
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalTime
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalVisit
 public import Complexity.Algorithms.WordRAM.ThreeSum.Fill
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Arrays
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Bounds
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Execute
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Input
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Layout
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Model
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Program
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Scan
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Select
+public import Complexity.Algorithms.WordRAM.ThreeSum.Frontend.Time
 public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Loop
 public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Prepare
 public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Program
@@ -1717,6 +1776,7 @@ public import Complexity.Computability.WordRAM.Dynamic
 public import Complexity.Computability.WordRAM.ExactNotation
 public import Complexity.Computability.WordRAM.Function
 public import Complexity.Computability.WordRAM.Generic
+public import Complexity.Computability.WordRAM.GhostLoop
 public import Complexity.Computability.WordRAM.Heap
 public import Complexity.Computability.WordRAM.ListArray
 public import Complexity.Computability.WordRAM.MapOp

diff --git a/Complexity/Algorithms/ThreeSum/ChanHe/SelectorBounds.lean b/Complexity/Algorithms/ThreeSum/ChanHe/SelectorBounds.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.ThreeSum.ChanHe.Defs
+
+/-!
+# Size bounds for the Chan–He selectors, including their default
+
+Bounding the modulus does not require either filter to succeed: a failed filter returns one.
+These bounds therefore apply to native execution with arbitrary nonnegative collision thresholds,
+including empty input sets. They do not assert the collision-shrinking property of a successful
+search.
+
+## Main results
+
+* `minOrOne_filter_bounds`: a positive bounded candidate set keeps its filtered selector bounded.
+* `modulus_bounds_of_candidates`: both selections, including defaults, have product in `[1,m²]`.
+
+The bounds are original elementary consequences of the existing finite selectors.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.ThreeSum.ChanHe
+
+open Finset
+
+/-- Filtering positive candidates bounded by `m` keeps the default-one selector in `[1,m]`.
+The candidate set and the filtered set may both be empty. -/
+theorem minOrOne_filter_bounds {Q : Finset ℕ} {m : ℕ} (hm : 1 ≤ m)
+    (hpos : ∀ q ∈ Q, 1 ≤ q) (hle : ∀ q ∈ Q, q ≤ m)
+    (A : ℕ → Prop) [DecidablePred A] :
+    1 ≤ minOrOne {q ∈ Q | A q} ∧ minOrOne {q ∈ Q | A q} ≤ m := by
+  let S := {q ∈ Q | A q}
+  by_cases h : S.Nonempty
+  · have hmem : S.min' h ∈ Q := (mem_filter.mp (min'_mem S h)).1
+    change 1 ≤ minOrOne S ∧ minOrOne S ≤ m
+    rw [minOrOne, dite_eq_left h]
+    exact ⟨hpos _ hmem, hle _ hmem⟩
+  · change 1 ≤ minOrOne S ∧ minOrOne S ≤ m
+    rw [minOrOne, dite_eq_right h]
+    exact ⟨le_rfl, hm⟩
+
+/-- Positive bounded candidates bound the modulus regardless of whether either filter succeeds.
+This is a size bound only; no magnitude or successful-search premise is needed. -/
+theorem modulus_bounds_of_candidates {Q : Finset ℕ} {m : ℕ} (hm : 1 ≤ m)
+    (hpos : ∀ q ∈ Q, 1 ≤ q) (hle : ∀ q ∈ Q, q ≤ m)
+    (Λ : ℕ) (S₁ S₂ S₃ : Finset ℤ) :
+    1 ≤ modulus Q Λ S₁ S₂ S₃ ∧ modulus Q Λ S₁ S₂ S₃ ≤ m ^ 2 := by
+  have hp : 1 ≤ firstP Q Λ S₁ S₂ S₃ ∧ firstP Q Λ S₁ S₂ S₃ ≤ m :=
+    minOrOne_filter_bounds hm hpos hle _
+  have hq : 1 ≤ secondP Q Λ S₁ S₂ S₃ (firstP Q Λ S₁ S₂ S₃) ∧
+      secondP Q Λ S₁ S₂ S₃ (firstP Q Λ S₁ S₂ S₃) ≤ m :=
+    minOrOne_filter_bounds hm hpos hle _
+  exact ⟨Nat.mul_le_mul hp.1 hq.1,
+    (Nat.mul_le_mul hp.2 hq.2).trans_eq (pow_two m).symm⟩
+
+end Cslib.Algorithms.ThreeSum.ChanHe
diff --git a/Complexity/Algorithms/WordRAM/PrimeTable.lean 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