feat(wordram): compute Chan–He parameters from native input

Complexity.lean

@@ -98,6 +98,9 @@ public import Complexity.Algorithms.WordRAM.Karger.FastCut
 public import Complexity.Algorithms.WordRAM.Karger.Graph
 public import Complexity.Algorithms.WordRAM.KargerMinCut
 public import Complexity.Algorithms.WordRAM.KargerStein
+public import Complexity.Algorithms.WordRAM.NatClog
+public import Complexity.Algorithms.WordRAM.NatLog
+public import Complexity.Algorithms.WordRAM.NatSqrt
 public import Complexity.Algorithms.WordRAM.PrefixSums.Dynamic
 public import Complexity.Algorithms.WordRAM.PrefixSums.Query
 public import Complexity.Algorithms.WordRAM.PrefixSums.Tree
@@ -130,6 +133,7 @@ public import Complexity.Algorithms.WordRAM.Stack.Controller
 public import Complexity.Algorithms.WordRAM.ThreeSum.Cell
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Collisions
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Count
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Residues
 public import Complexity.Algorithms.WordRAM.ThreeSum.Fill
 public import Complexity.Algorithms.WordRAM.ThreeSum.Memory

Complexity/Algorithms/WordRAM/NatClog.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.WordRAM.Notation
+public import Mathlib.Data.Nat.Log
+
+/-!
+# A charged native ceiling binary logarithm
+
+## Main definitions
+
+* `NatClog.program`: successive ceiling division by two.
+
+## Main results
+
+* `NatClog.exec`: the ceiling logarithm with a logarithmic charged instruction bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.NatClog
+
+open Cslib.WordRAM
+
+/-- Quotient, initially the input. -/
+abbrev arg : Fin 4 := 0
+/-- Ceiling logarithm output. -/
+abbrev result : Fin 4 := 1
+/-- Constant one. -/
+abbrev one : Fin 4 := 2
+/-- Constant two. -/
+abbrev two : Fin 4 := 3
+
+/-- Divide the quotient by two and increment the answer. -/
+def body : Code .standard 4 := ram[ arg ← arg + one; arg ← arg / two; result ← result + one ]
+
+/-- Fixed code for `Nat.clog 2`, including its value zero at input zero. -/
+def program : Code .standard 4 :=
+  .seq (ram[ result ← #0; one ← #1; two ← #2 ]) (.loop (.lt one arg) body)
+
+/-- Compute the ceiling binary logarithm in at most `5 ⌈log₂ n⌉ + 5` instructions.
+Memory is untouched and the input quotient is consumed. -/
+theorem exec {w : ℕ} (x : Data 4) (h2 : Fits w 2) (hn : Fits w (x.regs arg + 1))
+    (hout : Fits w (Nat.clog 2 (x.regs arg) + 1)) :
+    ∃ y, ExecWithin w program x y (5 * Nat.clog 2 (x.regs arg) + 5) ∧
+      y.regs result = Nat.clog 2 (x.regs arg) ∧ y.mem = x.mem ∧
+      y.regs one = 1 ∧ y.regs two = 2 := by
+  let I (y : Data 4) : Prop := y.regs one = 1 ∧ y.regs two = 2 ∧
+    y.regs arg ≤ x.regs arg ∧
+    y.regs result + Nat.clog 2 (y.regs arg) = Nat.clog 2 (x.regs arg) ∧ y.mem = x.mem
+  have hbody (y : Data 4) (hy : I y) (hc : (Cond.lt one arg).Holds y) :
+      ∃ z, ExecWithin w body y z 3 ∧ I z ∧
+        Nat.clog 2 (z.regs arg) < Nat.clog 2 (y.regs arg) := by
+    obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+    have hgt : 1 < y.regs arg := by simpa only [Cond.holds_lt, ho] using hc
+    have hpos : 0 < Nat.clog 2 (y.regs arg) := Nat.clog_pos (by decide) (by omega)
+    have hadd : Fits w (y.regs arg + 1) := hn.of_le (by omega)
+    have hdiv : Fits w ((y.regs arg + 1) / 2) :=
+      hn.of_le ((Nat.div_le_self _ _).trans (by omega))
+    have hinc : Fits w (y.regs result + 1) := hout.of_le (by omega)
+    refine ⟨?z, ?run, ?inv, ?decrease⟩
+    case run => ram_eval [body, ho, ht, hadd, hdiv, hinc, arg, result, one, two, Fin.mk.injEq]
+    case inv =>
+      refine ⟨?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [Function.update_apply] using ho
+      · simpa +decide [Function.update_apply] using ht
+      · simpa +decide [Function.update_apply] using
+          (show (y.regs arg + 1) / 2 ≤ x.regs arg from by omega)
+      · change y.regs result + 1 + Nat.clog 2 ((y.regs arg + 1) / 2) = Nat.clog 2 (x.regs arg)
+        have h := Nat.clog_of_two_le (b := 2) (by decide) (by omega : 2 ≤ y.regs arg)
+        simp only [show y.regs arg + 2 - 1 = y.regs arg + 1 by omega] at h
+        omega
+      · exact hm
+    case decrease =>
+      change Nat.clog 2 ((y.regs arg + 1) / 2) < Nat.clog 2 (y.regs arg)
+      have h := Nat.clog_of_two_le (b := 2) (by decide) (by omega : 2 ≤ y.regs arg)
+      simp only [show y.regs arg + 2 - 1 = y.regs arg + 1 by omega] at h
+      omega
+  let x₀ := ((x.set result 0).set one 1).set two 2
+  have hx₀ : I x₀ := by simp +decide [I, x₀, arg, result, one, two]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => Nat.clog 2 (y.regs arg)) hbody hx₀
+  obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+  have hzero : Nat.clog 2 (y.regs arg) = 0 := by
+    have hle : y.regs arg ≤ 1 := by simpa only [Cond.holds_lt, ho, not_lt] using hc
+    exact Nat.clog_of_right_le_one hle 2
+  refine ⟨y, ?_, by omega, hm, ho, ht⟩
+  have h1 : Fits w 1 := h2.of_le (by decide)
+  have hinit : ExecWithin (B := .standard) w (ram[ result ← #0; one ← #1; two ← #2 ]) x x₀ 3 := by
+    ram_eval [x₀, h1, h2]
+  convert hinit.seq he using 1
+  · rfl
+  · simp +decide only [x₀, Data.set_regs, Function.update_apply, arg, result, one, two,
+      ↓reduceIte]
+    omega
+
+/-- Run the routine on any injectively chosen registers. -/
+theorem exec_rename {r w : ℕ} (f : Fin 4 → Fin r) (hf : f.Injective) (x : Data r)
+    (h2 : Fits w 2) (hn : Fits w (x.regs (f arg) + 1))
+    (hout : Fits w (Nat.clog 2 (x.regs (f arg)) + 1)) :
+    ∃ y, ExecWithin w (program.rename f) x y (5 * Nat.clog 2 (x.regs (f arg)) + 5) ∧
+      y.regs (f result) = Nat.clog 2 (x.regs (f arg)) ∧ y.mem = x.mem ∧
+      y.regs (f one) = 1 ∧ y.regs (f two) = 2 := by
+  obtain ⟨a, ha, hr, hm, ho, ht⟩ := exec (x.comap f) h2 hn hout
+  refine ⟨a.extend f x, ha.rename hf, ?_, hm, ?_, ?_⟩
+  · exact (hf.extend_apply _ _ result).trans hr
+  · exact (hf.extend_apply _ _ one).trans ho
+  · exact (hf.extend_apply _ _ two).trans ht
+
+end Cslib.Algorithms.WordRAM.NatClog

Complexity/Algorithms/WordRAM/NatLog.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.WordRAM.Notation
+public import Mathlib.Data.Nat.Log
+
+/-!
+# A charged native binary logarithm
+
+## Main definitions
+
+* `NatLog.program`: successive division by two.
+
+## Main results
+
+* `NatLog.exec`: the floor logarithm with a logarithmic charged instruction bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.NatLog
+
+open Cslib.WordRAM
+
+/-- Quotient, initially the input. -/
+abbrev arg : Fin 4 := 0
+/-- Floor logarithm output. -/
+abbrev result : Fin 4 := 1
+/-- Constant one. -/
+abbrev one : Fin 4 := 2
+/-- Constant two. -/
+abbrev two : Fin 4 := 3
+
+/-- Divide the quotient by two and increment the answer. -/
+def body : Code .standard 4 := ram[ arg ← arg / two; result ← result + one ]
+
+/-- Fixed code for `Nat.log 2`, including its value zero at input zero. -/
+def program : Code .standard 4 :=
+  .seq (ram[ result ← #0; one ← #1; two ← #2 ]) (.loop (.lt one arg) body)
+
+/-- Compute the floor binary logarithm in at most `4 log₂ n + 5` instructions.
+Memory is untouched and the input quotient is consumed. -/
+theorem exec {w : ℕ} (x : Data 4) (h2 : Fits w 2) (hn : Fits w (x.regs arg))
+    (hout : Fits w (Nat.log 2 (x.regs arg) + 1)) :
+    ∃ y, ExecWithin w program x y (4 * Nat.log 2 (x.regs arg) + 5) ∧
+      y.regs result = Nat.log 2 (x.regs arg) ∧ y.mem = x.mem ∧
+      y.regs one = 1 ∧ y.regs two = 2 := by
+  let I (y : Data 4) : Prop := y.regs one = 1 ∧ y.regs two = 2 ∧
+    y.regs arg ≤ x.regs arg ∧
+    y.regs result + Nat.log 2 (y.regs arg) = Nat.log 2 (x.regs arg) ∧ y.mem = x.mem
+  have hbody (y : Data 4) (hy : I y) (hc : (Cond.lt one arg).Holds y) :
+      ∃ z, ExecWithin w body y z 2 ∧ I z ∧
+        Nat.log 2 (z.regs arg) < Nat.log 2 (y.regs arg) := by
+    obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+    have hgt : 1 < y.regs arg := by simpa only [Cond.holds_lt, ho] using hc
+    have hpos : 0 < Nat.log 2 (y.regs arg) := Nat.log_pos (by decide) (by omega)
+    have hdiv : Fits w (y.regs arg / 2) := hn.of_le ((Nat.div_le_self _ _).trans harg)
+    have hinc : Fits w (y.regs result + 1) := hout.of_le (by omega)
+    refine ⟨?z, ?run, ?inv, ?decrease⟩
+    case run => ram_eval [body, ho, ht, hdiv, hinc, arg, result, one, two, Fin.mk.injEq]
+    case inv =>
+      refine ⟨?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [Function.update_apply] using ho
+      · simpa +decide [Function.update_apply] using ht
+      · simpa +decide [Function.update_apply] using (Nat.div_le_self (y.regs arg) 2).trans harg
+      · change y.regs result + 1 + Nat.log 2 (y.regs arg / 2) = Nat.log 2 (x.regs arg)
+        rw [Nat.log_div_base]
+        omega
+      · exact hm
+    case decrease =>
+      change Nat.log 2 (y.regs arg / 2) < Nat.log 2 (y.regs arg)
+      rw [Nat.log_div_base]
+      omega
+  let x₀ := ((x.set result 0).set one 1).set two 2
+  have hx₀ : I x₀ := by simp +decide [I, x₀, arg, result, one, two]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => Nat.log 2 (y.regs arg)) hbody hx₀
+  obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+  have hzero : Nat.log 2 (y.regs arg) = 0 := by
+    have hle : y.regs arg ≤ 1 := by simpa only [Cond.holds_lt, ho, not_lt] using hc
+    exact Nat.log_eq_zero_iff.mpr (Or.inl (by omega))
+  refine ⟨y, ?_, by omega, hm, ho, ht⟩
+  have h1 : Fits w 1 := h2.of_le (by decide)
+  have hinit : ExecWithin (B := .standard) w (ram[ result ← #0; one ← #1; two ← #2 ]) x x₀ 3 := by
+    ram_eval [x₀, h1, h2]
+  convert hinit.seq he using 1
+  · rfl
+  · simp +decide only [x₀, Data.set_regs, Function.update_apply, arg, result, one, two,
+      ↓reduceIte]
+    omega
+
+/-- Run the routine on any injectively chosen registers. -/
+theorem exec_rename {r w : ℕ} (f : Fin 4 → Fin r) (hf : f.Injective) (x : Data r)
+    (h2 : Fits w 2) (hn : Fits w (x.regs (f arg)))
+    (hout : Fits w (Nat.log 2 (x.regs (f arg)) + 1)) :
+    ∃ y, ExecWithin w (program.rename f) x y (4 * Nat.log 2 (x.regs (f arg)) + 5) ∧
+      y.regs (f result) = Nat.log 2 (x.regs (f arg)) ∧ y.mem = x.mem ∧
+      y.regs (f one) = 1 ∧ y.regs (f two) = 2 := by
+  obtain ⟨a, ha, hr, hm, ho, ht⟩ := exec (x.comap f) h2 hn hout
+  refine ⟨a.extend f x, ha.rename hf, ?_, hm, ?_, ?_⟩
+  · exact (hf.extend_apply _ _ result).trans hr
+  · exact (hf.extend_apply _ _ one).trans ho
+  · exact (hf.extend_apply _ _ two).trans ht
+
+end Cslib.Algorithms.WordRAM.NatLog

Complexity/Algorithms/WordRAM/NatSqrt.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.WordRAM.Notation
+public import Mathlib.Data.Nat.Sqrt
+import Mathlib.Tactic.Linarith
+
+/-!
+# A charged native integer square root
+
+## Main definitions
+
+* `NatSqrt.program`: successive squares.
+
+## Main results
+
+* `NatSqrt.exec`: integer square root in a square-root number of native instructions.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.NatSqrt
+
+open Cslib.WordRAM
+
+/-- Input integer, preserved. -/
+abbrev arg : Fin 6 := 0
+/-- Current root and output. -/
+abbrev root : Fin 6 := 1
+/-- Successor of the current root. -/
+abbrev next : Fin 6 := 2
+/-- Square of the successor. -/
+abbrev square : Fin 6 := 3
+/-- Constant one. -/
+abbrev one : Fin 6 := 4
+/-- Input plus one. -/
+abbrev bound : Fin 6 := 5
+
+/-- Advance the root and compute the next square. -/
+def body : Code .standard 6 := ram[
+  root ← next; next ← next + one; square ← next * next ]
+
+/-- A fixed program for the integer square root, with all square computations charged. -/
+def program : Code .standard 6 :=
+  .seq (ram[ root ← #0; next ← #1; square ← #1; one ← #1; bound ← arg + one ])
+    (.loop (.lt square bound) body)
+
+/-- Compute `Nat.sqrt n` in at most `5 sqrt(n) + 7` instructions, preserving input and memory.
+The linear bound `4n + 4` covers the final unsuccessful square as well as all counters. -/
+theorem exec {w : ℕ} (x : Data 6) (hfit : Fits w (4 * x.regs arg + 4)) :
+    ∃ y, ExecWithin w program x y (5 * Nat.sqrt (x.regs arg) + 7) ∧
+      y.regs root = Nat.sqrt (x.regs arg) ∧ y.regs arg = x.regs arg ∧ y.mem = x.mem ∧
+      y.regs one = 1 := by
+  let n := x.regs arg
+  let I (y : Data 6) : Prop := y.regs arg = n ∧ y.regs one = 1 ∧
+    y.regs bound = n + 1 ∧ y.regs next = y.regs root + 1 ∧
+    y.regs square = y.regs next * y.regs next ∧
+    y.regs root ≤ Nat.sqrt n ∧ y.mem = x.mem
+  have hbody (y : Data 6) (hy : I y) (hc : (Cond.lt square bound).Holds y) :
+      ∃ z, ExecWithin w body y z 3 ∧ I z ∧
+        Nat.sqrt n - z.regs root < Nat.sqrt n - y.regs root := by
+    obtain ⟨ha, ho, hb, hn, hsq, hr, hm⟩ := hy
+    have hsmall : y.regs next * y.regs next ≤ n := by
+      simp only [Cond.holds_lt, hsq, hb] at hc
+      omega
+    have hnext : y.regs next ≤ Nat.sqrt n := Nat.le_sqrt.mpr hsmall
+    have hsl := Nat.sqrt_le n
+    have hsle := Nat.sqrt_le_self n
+    have hstep : Fits w (y.regs next + 1) := hfit.of_le (by dsimp [n] at *; omega)
+    have hsquare : Fits w ((y.regs next + 1) * (y.regs next + 1)) := hfit.of_le (by
+      change (y.regs next + 1) * (y.regs next + 1) ≤ 4 * n + 4
+      have hnn : y.regs next ≤ n := hnext.trans hsle
+      nlinarith)
+    refine ⟨?z, ?run, ?inv, ?decrease⟩
+    case run => ram_eval [body, ho, hstep, hsquare, root, next, square, one, Fin.mk.injEq]
+    case inv =>
+      refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [Function.update_apply] using ha
+      · simpa +decide [Function.update_apply] using ho
+      · simpa +decide [Function.update_apply] using hb
+      · rfl
+      · rfl
+      · exact hnext
+      · exact hm
+    case decrease =>
+      change Nat.sqrt n - y.regs next < Nat.sqrt n - y.regs root
+      omega
+  let x₀ := ((((x.set root 0).set next 1).set square 1).set one 1).set bound (n + 1)
+  have hx₀ : I x₀ := by simp +decide [I, x₀, n, root, next, square, one, bound, arg]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => Nat.sqrt n - y.regs root) hbody hx₀
+  obtain ⟨ha, ho, hb, hn, hsq, hr, hm⟩ := hy
+  have hlarge : n < (y.regs root + 1) * (y.regs root + 1) := by
+    simp only [Cond.holds_lt, hsq, hn, hb] at hc
+    omega
+  have hout : y.regs root = Nat.sqrt n := by
+    have h := Nat.sqrt_lt.mpr hlarge
+    omega
+  have h1 : Fits w 1 := hfit.of_le (by omega)
+  have hbfit : Fits w (x.regs arg + 1) := hfit.of_le (by omega)
+  have hinit : ExecWithin (B := .standard) w
+      (ram[ root ← #0; next ← #1; square ← #1; one ← #1; bound ← arg + one ]) x x₀ 5 := by
+    ram_eval [x₀, n, h1, hbfit, root, next, square, one, bound, arg, Fin.mk.injEq]
+  refine ⟨y, ?_, hout, ha, hm, ho⟩
+  convert hinit.seq he using 1
+  · rfl
+  · simp +decide only [x₀, Data.set_regs, Function.update_apply, root, next, square, one,
+      bound, arg, n, ↓reduceIte, Nat.sub_zero]
+    omega
+
+/-- Run successive squares on any injectively chosen registers. -/
+theorem exec_rename {r w : ℕ} (f : Fin 6 → Fin r) (hf : f.Injective) (x : Data r)
+    (hfit : Fits w (4 * x.regs (f arg) + 4)) :
+    ∃ y, ExecWithin w (program.rename f) x y (5 * Nat.sqrt (x.regs (f arg)) + 7) ∧
+      y.regs (f root) = Nat.sqrt (x.regs (f arg)) ∧
+      y.regs (f arg) = x.regs (f arg) ∧ y.mem = x.mem ∧ y.regs (f one) = 1 := by
+  obtain ⟨a, ha, hr, hn, hm, ho⟩ := exec (x.comap f) hfit
+  refine ⟨a.extend f x, ha.rename hf, ?_, ?_, hm, ?_⟩
+  · exact (hf.extend_apply _ _ root).trans hr
+  · exact (hf.extend_apply _ _ arg).trans hn
+  · exact (hf.extend_apply _ _ one).trans ho
+
+end Cslib.Algorithms.WordRAM.NatSqrt