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,8 @@ 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.ShiftedSizes
 public import Complexity.Algorithms.ThreeSum.ChanHe.Sizes
 public import Complexity.Algorithms.ThreeSum.Convolution
 public import Complexity.Algorithms.ThreeSum.Defs
@@ -146,17 +148,87 @@ 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.Preprocessing
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingBounds
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingEntries
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingExecute
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingFinish
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingInput
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingIntermediates
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingInvariant
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingLayout
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingLoad
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingLoop
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingPrimes
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingProgram
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingReserve
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingSetup
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingSnapshot
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingStep
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingTime
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.PreprocessingWidth
 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.Frame
+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
@@ -1725,6 +1797,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
@@ -1765,6 +1838,7 @@ public import Complexity.Computability.WordRAM.Structured
 public import Complexity.Computability.WordRAM.Subroutine
 public import Complexity.Computability.WordRAM.Time
 public import Complexity.Computability.WordRAM.Trace
+public import Complexity.Computability.WordRAM.Width
 public import Complexity.Crypto.Computational.Basic
 public import Complexity.Crypto.Computational.CollisionResistant
 public import Complexity.Crypto.Computational.Commitment

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/ThreeSum/ChanHe/ShiftedSizes.lean b/Complexity/Algorithms/ThreeSum/ChanHe/ShiftedSizes.lean
@@ -0,0 +1,74 @@
+/-
+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.Sizes
+
+/-!
+# Size bounds for the initialized-input magnitude convention
+
+Native parameter computation uses `(n+2)^κ`, including at lengths zero and one. The existing
+finite instances retain their actual input-length parameter `n`; only their quantitative upper
+bounds are compared with the existing estimates at `n+2`.
+
+## Main results
+
+* `mPar_mono_input`: candidate bounds are monotone in input length.
+* `mPar_shifted_pow_le`: square-root times squared-logarithm bound for the actual native modulus.
+* `length_instances_shifted_pow_le`: degree-seven logarithmic instance count at every length.
+* `packed_length_shifted_pow_le`: linear times fourth-logarithm common packed length.
+
+These elementary parameter bridges are original and reuse the existing finite Chan–He bounds.
+They do not change the finite instances or replace the actual input length by a padded input.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.ThreeSum.ChanHe
+
+/-- Increasing the length parameter increases the candidate window without changing magnitude. -/
+theorem mPar_mono_input {n n' : ℕ} (hn : n ≤ n') (U : ℕ) : mPar n U ≤ mPar n' U := by
+  have hs := Nat.sqrt_le_sqrt hn
+  unfold mPar wPar
+  gcongr
+
+/-- The actual native parameter keeps length `n` and uses shifted polynomial magnitude. -/
+theorem mPar_shifted_pow_le (n κ : ℕ) :
+    mPar n (2 * (n + 2) ^ κ) ≤
+      (5 * κ + 16) * (10 * κ + 40) * (Nat.sqrt (n + 2) + 1) *
+        (Nat.log 2 (n + 2) + 1) ^ 2 :=
+  (mPar_mono_input (show n ≤ n + 2 by omega) _).trans (mPar_pow_le (n + 2) κ)
+
+/-- The unchanged actual finite instance list has a logarithmic count even at lengths zero/one. -/
+theorem length_instances_shifted_pow_le (n κ : ℕ) (x : Fin n → ℤ) :
+    (instances n ((n + 2) ^ κ) x).length ≤ numBound κ (n + 2) := by
+  have hlog : 1 ≤ Nat.log 2 (n + 2) := Nat.log_pos (by decide) (by omega)
+  have hΛ : labelBits (2 * (n + 2) ^ κ) ≤ (κ + 2) * (Nat.log 2 (n + 2) + 1) :=
+    (labelBits_pow_le (n + 2) κ).trans (by rw [add_mul]; omega)
+  have hone : 1 ≤ ((κ + 2) * (Nat.log 2 (n + 2) + 1)) ^ 2 :=
+    Nat.one_le_pow _ _ (by positivity)
+  have hn : Nat.log 2 n ≤ Nat.log 2 (n + 2) := Nat.log_mono_right (by omega)
+  calc (instances n ((n + 2) ^ κ) x).length
+      ≤ (2 * labelBits (2 * (n + 2) ^ κ) ^ 2 + 2) * (2 * Nat.log 2 n + 2) ^ 5 :=
+        length_instances_le ..
+    _ ≤ (2 * ((κ + 2) * (Nat.log 2 (n + 2) + 1)) ^ 2 +
+        2 * ((κ + 2) * (Nat.log 2 (n + 2) + 1)) ^ 2) *
+          (2 * Nat.log 2 (n + 2) + 2) ^ 5 := by gcongr; omega
+    _ = numBound κ (n + 2) := by unfold numBound; ring
+
+/-- The unchanged common packed length is bounded by the old estimate evaluated at `n+2`. -/
+theorem packed_length_shifted_pow_le (κ n : ℕ) :
+    8 * mPar n (2 * (n + 2) ^ κ) ^ 2 ≤
+      32 * ((5 * κ + 16) * (10 * κ + 40)) ^ 2 * (n + 2) *
+        (Nat.log 2 (n + 2) + 1) ^ 4 := by
+  calc 8 * mPar n (2 * (n + 2) ^ κ) ^ 2 ≤ lenOf κ (n + 2) :=
+      Nat.mul_le_mul_left 8 (Nat.pow_le_pow_left
+        (mPar_mono_input (show n ≤ n + 2 by omega) _) 2)
+    _ ≤ _ := lenOf_le κ (n + 2) (by omega)
+
+end Cslib.Algorithms.ThreeSum.ChanHe