diff --git a/Complexity.lean b/Complexity.lean
index 3b94e48ab..c6f04557f 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -29,6 +29,7 @@ public import Complexity.Algorithms.Lean.Sort.Bitonic.Basic
 public import Complexity.Algorithms.Lean.Sort.Bitonic.Correctness
 public import Complexity.Algorithms.Lean.Sort.Bitonic.Trace
 public import Complexity.Algorithms.Lean.Sort.Bitonic.ZeroOne
+public import Complexity.Algorithms.Lean.UniformProbing
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Basic
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Elements
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Insert
@@ -86,6 +87,7 @@ public import Complexity.Algorithms.WordRAM.Dictionary.CuckooHashing
 public import Complexity.Algorithms.WordRAM.Dictionary.CuckooHashing.HashFamily
 public import Complexity.Algorithms.WordRAM.Dictionary.LinearProbing
 public import Complexity.Algorithms.WordRAM.Dictionary.LinearProbing.FiveWise
+public import Complexity.Algorithms.WordRAM.Dictionary.UniformProbing
 public import Complexity.Algorithms.WordRAM.Dijkstra.Fibonacci
 public import Complexity.Algorithms.WordRAM.Dijkstra.FibonacciStatement
 public import Complexity.Algorithms.WordRAM.Dijkstra.GenericPQ
diff --git a/Complexity/Algorithms/Lean/UniformProbing.lean b/Complexity/Algorithms/Lean/UniformProbing.lean
new file mode 100644
index 000000000..123f675b7
--- /dev/null
+++ b/Complexity/Algorithms/Lean/UniformProbing.lean
@@ -0,0 +1,1436 @@
+/-
+Copyright (c) 2026 Renfei Zhou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Renfei Zhou
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.Lean.Dictionary
+public import Complexity.Languages.Probabilistic.RandomOracle
+public import Complexity.Probability.PMF.Expect
+public import Complexity.Probability.PMF.Uniform
+public import Complexity.Probability.Product
+import Mathlib.Data.Fintype.Perm
+import Mathlib.Topology.Instances.ENNReal.Lemmas
+
+/-!
+# Uniform Probing in Open-Addressed Hash Tables
+
+This file formalizes the classical uniform-probing model of open-addressed hashing from
+[Cormen, Leiserson, Rivest, and Stein, *Introduction to Algorithms*, third edition (MIT Press,
+2009), Section 11.4 ("Open addressing", pp. 270–277)][CLRS2009], realizing the bounded-capacity
+insert-only dictionary specification `Cslib.Algorithms.Lean.Dictionary.spec` over `m` table slots
+(`2 * n_max ≤ m`).
+
+In the textbook uniform-probing ("uniform hashing") model, each key `u : Fin U` is assigned an
+independent uniform random permutation `π u : Equiv.Perm (Fin m)`
+(`PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m))`), which may equivalently be sampled lazily on
+demand via `Cslib.RandomOracle.uniform_interpret_eq_lazy`
+(`Complexity/Languages/Probabilistic/RandomOracle.lean`).
+
+## Source statements and notation mapping
+
+In [CLRS2009], third edition, Section 11.4:
+* An open-address table has `m` slots (`Fin m`) and holds `n` stored elements (`O.card` or
+  `(Dictionary.dom s).card`, bounded by `n_max` with `2 * n_max ≤ m`), giving load factor
+  `α = n / m < 1` (`α ≤ 1 / 2` when `2 * n ≤ m`).
+* Under uniform hashing (p. 271), each key's probe sequence `h(k, 0), h(k, 1), …, h(k, m - 1)` is
+  equally likely to be any of the `m!` permutations of `{0, 1, …, m - 1}` (`Equiv.Perm (Fin m)`).
+  Every search or insertion counts all inspected slots along the probe sequence up to and including
+  the stopping slot (`unsuccessfulProbes O σ = missedProbes O σ + 1` and
+  `probeCount T u σ = unsuccessfulProbes (otherOccupiedSlots T u) σ`).
+* **Theorem 11.6 (pp. 274–275)** states that in an open-address hash table with load factor
+  `α = n / m < 1`, the expected number of probes in an unsuccessful search is at most
+  `1 / (1 - α) = m / (m - n)` under uniform hashing; its proof establishes the exact occupancy tail
+  product `Pr{X ≥ i} = ∏_{j = 0}^{i - 2} ((n - j) / (m - j)) ≤ α ^ (i - 1)`.
+* **Corollary 11.7 (p. 276)** states that inserting an element into an open-address hash table with
+  load factor `α < 1` requires at most `1 / (1 - α) = m / (m - n)` probes on average.
+* **Theorem 11.8 (p. 276)** states that when each key in the table is equally likely to be searched
+  for, the expected number of probes in a successful search is at most `(1 / α) ln(1 / (1 - α))`.
+  Its proof first establishes for a fixed stored key `u` that searching for `u` follows the exact
+  same probe sequence as when `u` was inserted (`probeCount_runTable_eq_firstInsert`), so if `u` was
+  first inserted after a prefix `ops₁` reaching state `s₁` with `i = (Dictionary.dom s₁).card` keys,
+  the expected number of probes for `u` is at most `1 / (1 - i / m) = m / (m - i)`
+  (`expect_probeCount_of_mem_dom_le`, and `≤ 2` when `2 * n_max ≤ m` via
+  `expect_probeCount_of_mem_dom_le_two`). The uniform-key-averaged logarithmic endpoint
+  `(1 / α) ln(1 / (1 - α))` is not formalized here.
+
+## Main definitions
+
+* `Cslib.Algorithms.Lean.UniformProbing.allOccupied`,
+  `Cslib.Algorithms.Lean.UniformProbing.missedProbesFrom`,
+  `Cslib.Algorithms.Lean.UniformProbing.missedProbes`,
+  `Cslib.Algorithms.Lean.UniformProbing.unsuccessfulProbes`,
+  `Cslib.Algorithms.Lean.UniformProbing.probeSlotIndex`: slot-probe predicates, probe counts, and
+  first-available slot index along a probe permutation `σ : Equiv.Perm (Fin m)`.
+* `Cslib.Algorithms.Lean.UniformProbing.Table`,
+  `Cslib.Algorithms.Lean.UniformProbing.emptyTable`,
+  `Cslib.Algorithms.Lean.UniformProbing.occupiedSlots`,
+  `Cslib.Algorithms.Lean.UniformProbing.otherOccupiedSlots`,
+  `Cslib.Algorithms.Lean.UniformProbing.probeCount`: pure open-addressed table of `m` slots and
+  per-key probe count.
+* `Cslib.Algorithms.Lean.UniformProbing.tableGet`,
+  `Cslib.Algorithms.Lean.UniformProbing.tableInsert`,
+  `Cslib.Algorithms.Lean.UniformProbing.tableStep`,
+  `Cslib.Algorithms.Lean.UniformProbing.runTable`,
+  `Cslib.Algorithms.Lean.UniformProbing.TableRep`: open-addressed `get`/`insert` operations and
+  representation invariant linking `Table U m` to `Dictionary.State U`.
+
+## Main results
+
+* `Cslib.Algorithms.Lean.UniformProbing.toOuterMeasure_allOccupied_eq_prod`,
+  `Cslib.Algorithms.Lean.UniformProbing.toOuterMeasure_allOccupied_le_pow`: on a table with
+  `n = O.card ≤ m` occupied slots, the probability over
+  `σ ← PMF.uniformOfFintype (Equiv.Perm (Fin m))`
+  that the first `k ≤ m` probes all hit `O` (`k < unsuccessfulProbes O σ`) is
+  `∏ i ∈ Finset.range k, ((n - i : ℝ≥0∞) / (m - i : ℝ≥0∞)) ≤ ((n : ℝ≥0∞) / (m : ℝ≥0∞)) ^ k`
+  ([CLRS2009], third edition, proof of Theorem 11.6, pp. 274–275).
+* `Cslib.Algorithms.Lean.UniformProbing.expect_unsuccessfulProbes_le`,
+  `Cslib.Algorithms.Lean.UniformProbing.expect_unsuccessfulProbes_le_two`,
+  `Cslib.Algorithms.Lean.UniformProbing.expect_probeCount_of_eq_none_le`,
+  `Cslib.Algorithms.Lean.UniformProbing.expect_probeCount_of_eq_none_le_two`: Theorem 11.6
+  (pp. 274–275) and Corollary 11.7 (p. 276) of [CLRS2009], third edition — an unsuccessful lookup or
+  fresh-key insertion into a table holding `n < m` keys makes at most `m / (m - n)` probes in
+  expectation (`≤ 2` when `2 * n ≤ m`).
+* `Cslib.Algorithms.Lean.UniformProbing.TableRep.probeCount_tableInsert_of_isSome`,
+  `Cslib.Algorithms.Lean.UniformProbing.probeCount_runTable_eq_firstInsert`,
+  `Cslib.Algorithms.Lean.UniformProbing.expect_probeCount_of_mem_dom_le`,
+  `Cslib.Algorithms.Lean.UniformProbing.expect_probeCount_of_mem_dom_le_two`: pathwise
+  insertion-cost identity and per-key intermediate bound from the proof of Theorem 11.8 (p. 276) of
+  [CLRS2009], third edition — a successful lookup of a fixed present key `u ∈ dom s` makes the
+  exact same number of probes as the operation that first inserted `u` after prefix `ops₁`
+  (reaching state `s₁`), which is at most `m / (m - (Dictionary.dom s₁).card) ≤ 2` in expectation
+  when `2 * n_max ≤ m` (the uniform-key-averaged `(1 / α) ln(1 / (1 - α))` endpoint of Theorem 11.8
+  is not formalized here).
+* `Cslib.Algorithms.Lean.UniformProbing.uniform_interpret_eq_lazy_perm`: eager sampling of the
+  independent permutation family `Fin U → Equiv.Perm (Fin m)` agrees in distribution with lazy
+  on-demand oracle evaluation (`RandomOracle.uniform_interpret_eq_lazy`).
+
+## Representation space note
+
+Storing an explicit table of independent permutations in `(Equiv.Perm (Fin m)) ^ U` requires
+`U * log₂ (m!)` bits (`Ω(U)` machine words when `U = poly(n_max) ≫ n_max`). To achieve an
+`O(n_max)`-word self-contained Word-RAM dictionary,
+`Complexity/Algorithms/WordRAM/Dictionary/UniformProbing.lean` pairs a 2-universal multiply-shift
+primary hash `h₁(u) ∈ Fin (2 ^ M)` with a tabulated odd stride `h₂(u) ∈ Fin (2 ^ M)`
+([CLRS2009], third edition, Section 11.4, "Double hashing", pp. 272–274), reusing the
+open-addressed table invariants proved here.
+
+## References
+
+* [T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein,
+  *Introduction to Algorithms*, third edition (MIT Press, 2009), Section 11.4,
+  pp. 270–277][CLRS2009]
+* [M. Mitzenmacher and E. Upfal, *Probability and Computing*][MitzenmacherUpfal2017]
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.Lean.UniformProbing
+
+open Cslib.Algorithms.Lean
+open Cslib.Probability
+open scoped BigOperators ENNReal
+
+/-! ## Section 1: Permutation probe counts and stopping indices -/
+
+/-- Event that the first `k` slots `σ ⟨0, _⟩, ..., σ ⟨k - 1, _⟩` of permutation `σ` all belong to
+the occupied slot set `O`. -/
+def allOccupied {m : ℕ} (O : Finset (Fin m)) (k : ℕ) (σ : Equiv.Perm (Fin m)) : Prop :=
+  ∀ i : Fin m, i.val < k → σ i ∈ O
+
+instance instDecidableAllOccupied {m : ℕ} (O : Finset (Fin m)) (k : ℕ)
+    (σ : Equiv.Perm (Fin m)) : Decidable (allOccupied O k σ) := by
+  unfold allOccupied
+  infer_instance
+
+@[simp]
+theorem allOccupied_zero {m : ℕ} (O : Finset (Fin m)) (σ : Equiv.Perm (Fin m)) :
+    allOccupied O 0 σ := by
+  intro i hi
+  omega
+
+theorem allOccupied_succ_iff {m : ℕ} {O : Finset (Fin m)} {k : ℕ} (hk : k < m)
+    (σ : Equiv.Perm (Fin m)) :
+    allOccupied O (k + 1) σ ↔ allOccupied O k σ ∧ σ ⟨k, hk⟩ ∈ O := by
+  constructor
+  · intro h
+    refine ⟨fun i hi => h i (by omega), h ⟨k, hk⟩ (by simp)⟩
+  · rintro ⟨h, hk_mem⟩ i hi
+    rcases Nat.lt_succ_iff_lt_or_eq.mp hi with hlt | heq
+    · exact h i hlt
+    · have : i = ⟨k, hk⟩ := Fin.ext heq
+      rwa [this]
+
+theorem allOccupied_mono {m : ℕ} {O : Finset (Fin m)} {j k : ℕ} (hjk : j ≤ k)
+    {σ : Equiv.Perm (Fin m)} (h : allOccupied O k σ) : allOccupied O j σ :=
+  fun i hi => h i (lt_of_lt_of_le hi hjk)
+
+/-- Count how many consecutive slots `σ ⟨idx, _⟩, σ ⟨idx + 1, _⟩, ...` belong to `O`, for up to
+`rem` steps starting at `idx`. -/
+def missedProbesFrom {m : ℕ} (O : Finset (Fin m)) (σ : Equiv.Perm (Fin m)) :
+    ℕ → ℕ → ℕ
+  | 0, _ => 0
+  | rem + 1, idx =>
+    if h : idx < m then
+      if σ ⟨idx, h⟩ ∈ O then 1 + missedProbesFrom O σ rem (idx + 1) else 0
+    else 0
+
+/-- Number of consecutive probes `σ 0, σ 1, ...` that hit `O` before the first slot outside `O`. -/
+def missedProbes {m : ℕ} (O : Finset (Fin m)) (σ : Equiv.Perm (Fin m)) : ℕ :=
+  missedProbesFrom O σ m 0
+
+/-- Total number of slot probes `1 + missedProbes O σ` made by an unsuccessful search (or fresh-key
+insertion) against occupied slot set `O` along permutation `σ`. -/
+def unsuccessfulProbes {m : ℕ} (O : Finset (Fin m)) (σ : Equiv.Perm (Fin m)) : ℕ :=
+  1 + missedProbes O σ
+
+theorem missedProbesFrom_le {m : ℕ} (O : Finset (Fin m)) (σ : Equiv.Perm (Fin m))
+    (rem idx : ℕ) : missedProbesFrom O σ rem idx ≤ rem := by
+  induction rem generalizing idx with
+  | zero => simp [missedProbesFrom]
+  | succ rem ih =>
+    simp only [missedProbesFrom]
+    split_ifs
+    · have := ih (idx + 1)
+      omega
+    · omega
+    · omega
+
+theorem missedProbes_le {m : ℕ} (O : Finset (Fin m)) (σ : Equiv.Perm (Fin m)) :
+    missedProbes O σ ≤ m :=
+  missedProbesFrom_le O σ m 0
+
+theorem mem_of_lt_missedProbesFrom {m : ℕ} {O : Finset (Fin m)} {σ : Equiv.Perm (Fin m)}
+    {rem idx t : ℕ} (hrem : idx + rem ≤ m) (ht : t < missedProbesFrom O σ rem idx) :
+    ∃ h : idx + t < m, σ ⟨idx + t, h⟩ ∈ O := by
+  induction rem generalizing idx t with
+  | zero =>
+    simp [missedProbesFrom] at ht
+  | succ rem ih =>
+    have hidx : idx < m := by omega
+    simp only [missedProbesFrom, hidx, ↓reduceDIte] at ht
+    split_ifs at ht with hmem
+    · cases t with
+      | zero =>
+        exact ⟨hidx, by simpa using hmem⟩
+      | succ t =>
+        have ht' : t < missedProbesFrom O σ rem (idx + 1) := by omega
+        obtain ⟨h', hmem'⟩ := ih (idx := idx + 1) (by omega) ht'
+        refine ⟨by omega, ?_⟩
+        have heq : (⟨idx + (t + 1), by omega⟩ : Fin m) = ⟨idx + 1 + t, h'⟩ :=
+          Fin.ext (show idx + (t + 1) = idx + 1 + t by omega)
+        rwa [heq]
+    · omega
+
+theorem notMem_at_missedProbesFrom {m : ℕ} {O : Finset (Fin m)} {σ : Equiv.Perm (Fin m)}
+    {rem idx : ℕ} (hrem : idx + rem ≤ m) (hlt : missedProbesFrom O σ rem idx < rem) :
+    ∃ h : idx + missedProbesFrom O σ rem idx < m,
+      σ ⟨idx + missedProbesFrom O σ rem idx, h⟩ ∉ O := by
+  induction rem generalizing idx with
+  | zero => omega
+  | succ rem ih =>
+    have hidx : idx < m := by omega
+    simp only [missedProbesFrom, hidx, ↓reduceDIte] at hlt ⊢
+    split_ifs with hmem
+    · simp only [hmem, ↓reduceIte] at hlt
+      have hlt' : missedProbesFrom O σ rem (idx + 1) < rem := by omega
+      obtain ⟨h', hnot⟩ := ih (idx := idx + 1) (by omega) hlt'
+      refine ⟨by omega, ?_⟩
+      have heq :
+          (⟨idx + (1 + missedProbesFrom O σ rem (idx + 1)), by omega⟩ : Fin m) =
+            ⟨idx + 1 + missedProbesFrom O σ rem (idx + 1), h'⟩ :=
+        Fin.ext (show idx + (1 + missedProbesFrom O σ rem (idx + 1)) =
+          idx + 1 + missedProbesFrom O σ rem (idx + 1) by omega)
+      rwa [heq]
+    · exact ⟨hidx, by simpa using hmem⟩
+
+/-- For any `k ≤ m`, at least `k` probes miss (`k ≤ missedProbes O σ`) if and only if the first `k`
+slots of `σ` all belong to `O`. -/
+theorem le_missedProbes_iff_allOccupied {m : ℕ} {O : Finset (Fin m)} {k : ℕ} (hk : k ≤ m)
+    (σ : Equiv.Perm (Fin m)) :
+    k ≤ missedProbes O σ ↔ allOccupied O k σ := by
+  constructor
+  · intro hle i hi
+    have hit : i.val < missedProbesFrom O σ m 0 := lt_of_lt_of_le hi hle
+    obtain ⟨_, hmem⟩ := mem_of_lt_missedProbesFrom (by omega) hit
+    simpa using hmem
+  · intro hall
+    by_contra hnot
+    have hlt : missedProbesFrom O σ m 0 < k := not_le.mp hnot
+    obtain ⟨hidx, hnotMem⟩ := notMem_at_missedProbesFrom (by omega) (lt_of_lt_of_le hlt hk)
+    have hidx' : missedProbesFrom O σ m 0 < m := by omega
+    have hnotMem' : σ ⟨missedProbesFrom O σ m 0, hidx'⟩ ∉ O := by
+      convert hnotMem using 2
+      ext
+      simp
+    exact hnotMem' (hall ⟨missedProbesFrom O σ m 0, hidx'⟩ hlt)
+
+/-- For any `k ≤ m`, an unsuccessful search inspects more than `k` slots
+(`k < unsuccessfulProbes O σ`) if and only if the first `k` slots of `σ` all belong to `O`. -/
+theorem lt_unsuccessfulProbes_iff_allOccupied {m : ℕ} {O : Finset (Fin m)} {k : ℕ} (hk : k ≤ m)
+    (σ : Equiv.Perm (Fin m)) :
+    k < unsuccessfulProbes O σ ↔ allOccupied O k σ := by
+  rw [unsuccessfulProbes, ← le_missedProbes_iff_allOccupied hk]
+  omega
+
+/-- When `O.card < m`, not all `m` slots of `σ` can belong to `O`. -/
+theorem not_allOccupied_self_of_card_lt {m : ℕ} {O : Finset (Fin m)} (hO : O.card < m)
+    (σ : Equiv.Perm (Fin m)) : ¬ allOccupied O m σ := by
+  intro hall
+  have hsub : Finset.univ.map σ.toEmbedding ⊆ O := by
+    intro x hx
+    rcases Finset.mem_map.mp hx with ⟨i, -, rfl⟩
+    exact hall i i.isLt
+  have hcard := Finset.card_le_card hsub
+  simp only [Finset.card_map, Finset.card_univ, Fintype.card_fin] at hcard
+  omega
+
+/-- When `O.card < m`, `missedProbes O σ < m` for every permutation `σ`. -/
+theorem missedProbes_lt_of_card_lt {m : ℕ} {O : Finset (Fin m)} (hO : O.card < m)
+    (σ : Equiv.Perm (Fin m)) : missedProbes O σ < m := by
+  have hle := missedProbes_le O σ
+  have hne : missedProbes O σ ≠ m := by
+    intro heq
+    exact not_allOccupied_self_of_card_lt hO σ
+      ((le_missedProbes_iff_allOccupied le_rfl σ).mp (by omega))
+  omega
+
+/-- The probe index `⟨missedProbes O σ, _⟩ : Fin m` of the first slot along `σ` outside `O` when
+`O.card < m`. -/
+def probeSlotIndex {m : ℕ} (O : Finset (Fin m)) (σ : Equiv.Perm (Fin m))
+    (hO : O.card < m) : Fin m :=
+  ⟨missedProbes O σ, missedProbes_lt_of_card_lt hO σ⟩
+
+@[simp]
+theorem val_probeSlotIndex {m : ℕ} (O : Finset (Fin m)) (σ : Equiv.Perm (Fin m))
+    (hO : O.card < m) : (probeSlotIndex O σ hO).val = missedProbes O σ :=
+  rfl
+
+theorem mem_of_lt_probeSlotIndex {m : ℕ} {O : Finset (Fin m)} {σ : Equiv.Perm (Fin m)}
+    (hO : O.card < m) {i : Fin m} (hi : i.val < (probeSlotIndex O σ hO).val) :
+    σ i ∈ O :=
+  (le_missedProbes_iff_allOccupied (le_of_lt (missedProbes_lt_of_card_lt hO σ)) σ).mp le_rfl i hi
+
+theorem notMem_apply_probeSlotIndex {m : ℕ} {O : Finset (Fin m)} {σ : Equiv.Perm (Fin m)}
+    (hO : O.card < m) : σ (probeSlotIndex O σ hO) ∉ O := by
+  obtain ⟨_, hnot⟩ := notMem_at_missedProbesFrom (O := O) (σ := σ) (by omega)
+    (missedProbes_lt_of_card_lt hO σ)
+  simpa [probeSlotIndex, missedProbes] using hnot
+
+/-- Exact characterization of `missedProbes O σ`: for any `i₀ : Fin m`, `missedProbes O σ = i₀.val`
+if and only if all earlier probes `i < i₀` lie in `O` and `σ i₀ ∉ O`. -/
+theorem missedProbes_eq_iff {m : ℕ} {O : Finset (Fin m)} {σ : Equiv.Perm (Fin m)} (i₀ : Fin m) :
+    missedProbes O σ = i₀.val ↔ allOccupied O i₀.val σ ∧ σ i₀ ∉ O := by
+  constructor
+  · intro heq
+    have hlt : missedProbes O σ < m := heq ▸ i₀.isLt
+    have hall : allOccupied O i₀.val σ :=
+      (le_missedProbes_iff_allOccupied (le_of_lt i₀.isLt) σ).mp (by omega)
+    obtain ⟨hidx, hnot⟩ := notMem_at_missedProbesFrom (O := O) (σ := σ) (by omega) hlt
+    have hi₀ : (⟨0 + missedProbesFrom O σ m 0, hidx⟩ : Fin m) = i₀ := by
+      ext
+      simpa [missedProbes] using heq
+    rw [hi₀] at hnot
+    exact ⟨hall, hnot⟩
+  · rintro ⟨hall, hnot⟩
+    have hge : i₀.val ≤ missedProbes O σ :=
+      (le_missedProbes_iff_allOccupied (le_of_lt i₀.isLt) σ).mpr hall
+    have hnot_succ : ¬ (i₀.val + 1 ≤ missedProbes O σ) := by
+      intro hle
+      have hall' := (le_missedProbes_iff_allOccupied i₀.isLt σ).mp hle
+      exact hnot (hall' i₀ (by omega))
+    omega
+
+theorem probeSlotIndex_eq_iff {m : ℕ} {O : Finset (Fin m)} {σ : Equiv.Perm (Fin m)}
+    (hO : O.card < m) (i₀ : Fin m) :
+    probeSlotIndex O σ hO = i₀ ↔ allOccupied O i₀.val σ ∧ σ i₀ ∉ O := by
+  rw [Fin.ext_iff, val_probeSlotIndex, missedProbes_eq_iff]
+
+/-- Tail-sum identity on `Fin m`: when `O.card < m`, the total number of probes
+`unsuccessfulProbes O σ` equals the number of `k ∈ Finset.range m` for which `allOccupied O k σ`
+holds. -/
+theorem unsuccessfulProbes_eq_sum_boole {m : ℕ} {O : Finset (Fin m)} (hO : O.card < m)
+    (σ : Equiv.Perm (Fin m)) :
+    unsuccessfulProbes O σ =
+      ∑ k ∈ Finset.range m, if allOccupied O k σ then 1 else 0 := by
+  have hlt : missedProbes O σ < m := missedProbes_lt_of_card_lt hO σ
+  have hcongr : ∀ k ∈ Finset.range m,
+      (if allOccupied O k σ then 1 else 0) =
+        (if k ∈ Finset.range (missedProbes O σ + 1) then 1 else 0) := by
+    intro k hk
+    have hk_le : k ≤ m := le_of_lt (Finset.mem_range.mp hk)
+    simp only [Finset.mem_range, Nat.lt_succ_iff, le_missedProbes_iff_allOccupied hk_le]
+  rw [Finset.sum_congr rfl hcongr, ← Finset.sum_filter,
+    Finset.filter_mem_eq_inter, Finset.inter_eq_right.mpr (by
+      intro k hk
+      rw [Finset.mem_range] at hk ⊢
+      omega),
+    Finset.sum_const, smul_eq_mul, mul_one, Finset.card_range, unsuccessfulProbes, Nat.add_comm]
+
+/-! ## Section 2: Textbook Uniform-Probing Expected-Probe Bounds ([CLRS2009], Theorem 11.6) -/
+
+/-- Set of permutations `σ : Equiv.Perm (Fin m)` whose first `k` probes all belong to `O`. -/
+def occPermSet {m : ℕ} (O : Finset (Fin m)) (k : ℕ) : Finset (Equiv.Perm (Fin m)) :=
+  Finset.univ.filter fun σ => allOccupied O k σ
+
+@[simp]
+theorem mem_occPermSet {m : ℕ} {O : Finset (Fin m)} {k : ℕ} {σ : Equiv.Perm (Fin m)} :
+    σ ∈ occPermSet O k ↔ allOccupied O k σ := by
+  simp [occPermSet]
+
+@[simp]
+theorem occPermSet_zero {m : ℕ} (O : Finset (Fin m)) :
+    occPermSet O 0 = Finset.univ := by
+  ext σ
+  simp [occPermSet]
+
+/-- Right-multiplying `σ` by `Equiv.swap ⟨k, hk⟩ j` (for `k ≤ j.val`) preserves `allOccupied O k`.
+-/
+private theorem allOccupied_mul_swap_iff {m : ℕ} {O : Finset (Fin m)} {k : ℕ} (hk : k < m)
+    {j : Fin m} (hj : k ≤ j.val) (σ : Equiv.Perm (Fin m)) :
+    allOccupied O k (σ * Equiv.swap ⟨k, hk⟩ j) ↔ allOccupied O k σ := by
+  have hfix : ∀ i : Fin m, i.val < k → (Equiv.swap ⟨k, hk⟩ j) i = i := by
+    intro i hi
+    apply Equiv.swap_apply_of_ne_of_ne
+    · intro h
+      have : i.val = k := congrArg Fin.val h
+      omega
+    · intro h
+      have : i.val = j.val := congrArg Fin.val h
+      omega
+  refine ⟨fun h i hi => ?_, fun h i hi => ?_⟩
+  · have := h i hi
+    rwa [Equiv.Perm.mul_apply, hfix i hi] at this
+  · rw [Equiv.Perm.mul_apply, hfix i hi]
+    exact h i hi
+
+/-- By transposition symmetry `σ ↦ σ * Equiv.swap ⟨k, hk⟩ j`, for every `j : Fin m` with
+`k ≤ j.val`, the number of permutations in `occPermSet O k` with `σ j ∈ O` equals
+`(occPermSet O (k + 1)).card`. -/
+private theorem card_filter_occPermSet_eq_succ {m : ℕ} (O : Finset (Fin m)) {k : ℕ} (hk : k < m)
+    {j : Fin m} (hj : k ≤ j.val) :
+    ((occPermSet O k).filter fun σ => σ j ∈ O).card = (occPermSet O (k + 1)).card := by
+  classical
+  let τ : Equiv.Perm (Fin m) := Equiv.swap ⟨k, hk⟩ j
+  refine Finset.card_bij (fun σ _ => σ * τ) ?_ ?_ ?_
+  · intro σ hσ
+    rcases Finset.mem_filter.mp hσ with ⟨hσ_occ, hσj⟩
+    rw [mem_occPermSet] at hσ_occ ⊢
+    rw [allOccupied_succ_iff hk]
+    refine ⟨(allOccupied_mul_swap_iff hk hj σ).mpr hσ_occ, ?_⟩
+    simpa [τ] using hσj
+  · intro σ₁ _ σ₂ _ heq
+    exact mul_right_cancel heq
+  · intro σ hσ
+    rw [mem_occPermSet, allOccupied_succ_iff hk] at hσ
+    refine ⟨σ * τ, ?_, ?_⟩
+    · rw [Finset.mem_filter, mem_occPermSet]
+      refine ⟨(allOccupied_mul_swap_iff hk hj σ).mpr hσ.1, ?_⟩
+      simpa [τ] using hσ.2
+    · ext x
+      simp [τ]
+
+/-- For any permutation `σ : Equiv.Perm (Fin m)`, the number of indices `i : Fin m` with `σ i ∈ O`
+equals `O.card`. -/
+private theorem card_filter_apply_mem_eq {m : ℕ} (O : Finset (Fin m)) (σ : Equiv.Perm (Fin m)) :
+    (Finset.univ.filter fun i : Fin m => σ i ∈ O).card = O.card := by
+  refine Finset.card_bij (fun i _ => σ i) ?_ ?_ ?_
+  · intro i hi
+    exact (Finset.mem_filter.mp hi).2
+  · intro i₁ _ i₂ _ h
+    exact σ.injective h
+  · intro y hy
+    exact ⟨σ.symm y, Finset.mem_filter.mpr ⟨Finset.mem_univ _, by simp [hy]⟩, by simp⟩
+
+/-- Partition of a `Finset` into elements satisfying `p` and `¬ p`. -/
+private theorem card_filter_add_card_filter_neg {α : Type*} (s : Finset α)
+    (p : α → Prop) [DecidablePred p] :
+    (s.filter p).card + (s.filter fun x => ¬ p x).card = s.card := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | @insert a s ha ih =>
+    by_cases hp : p a <;> simp [Finset.filter_insert, hp, ha] <;> omega
+
+/-- Cardinality of `{i : Fin m | i.val < k}` when `k ≤ m`. -/
+private theorem card_filter_val_lt {m k : ℕ} (hk : k ≤ m) :
+    (Finset.univ.filter fun i : Fin m => i.val < k).card = k := by
+  refine (Finset.card_bij (fun i _ => i.val) ?_ ?_ ?_).trans (Finset.card_range k)
+  · intro i hi
+    exact Finset.mem_range.mpr (Finset.mem_filter.mp hi).2
+  · intro i₁ _ i₂ _ h
+    exact Fin.ext h
+  · intro j hj
+    have hj_lt : j < k := Finset.mem_range.mp hj
+    exact ⟨⟨j, lt_of_lt_of_le hj_lt hk⟩,
+      Finset.mem_filter.mpr ⟨Finset.mem_univ _, hj_lt⟩, rfl⟩
+
+/-- Cardinality of `{i : Fin m | k ≤ i.val}` when `k ≤ m`. -/
+private theorem card_filter_val_ge {m k : ℕ} (hk : k ≤ m) :
+    (Finset.univ.filter fun i : Fin m => k ≤ i.val).card = m - k := by
+  have hpart := card_filter_add_card_filter_neg
+    (Finset.univ : Finset (Fin m)) (fun i : Fin m => i.val < k)
+  have hneg : (Finset.univ.filter fun i : Fin m => ¬ i.val < k) =
+      Finset.univ.filter fun i : Fin m => k ≤ i.val := by
+    ext i
+    simp
+  rw [hneg, card_filter_val_lt hk, Finset.card_univ, Fintype.card_fin] at hpart
+  omega
+
+/-- For any `σ ∈ occPermSet O k` with `k ≤ m`, the number of remaining indices `j ≥ k` satisfying
+`σ j ∈ O` is `O.card - k` (and `k ≤ O.card`). -/
+private theorem card_filter_ge_and_mem {m : ℕ} {O : Finset (Fin m)} {k : ℕ} (hk : k ≤ m)
+    {σ : Equiv.Perm (Fin m)} (hσ : σ ∈ occPermSet O k) :
+    ((Finset.univ.filter fun j : Fin m => k ≤ j.val).filter fun j => σ j ∈ O).card =
+      O.card - k := by
+  rw [mem_occPermSet] at hσ
+  set S := Finset.univ.filter fun j : Fin m => σ j ∈ O
+  have hpart := card_filter_add_card_filter_neg S (fun j : Fin m => j.val < k)
+  have hlt_eq : S.filter (fun j : Fin m => j.val < k) =
+      Finset.univ.filter fun j : Fin m => j.val < k := by
+    ext j
+    simp only [S, Finset.mem_filter, Finset.mem_univ, true_and]
+    exact ⟨fun h => h.2, fun h => ⟨hσ j h, h⟩⟩
+  have hge_eq : S.filter (fun j : Fin m => ¬ j.val < k) =
+      (Finset.univ.filter fun j : Fin m => k ≤ j.val).filter fun j => σ j ∈ O := by
+    ext j
+    simp only [S, Finset.mem_filter, Finset.mem_univ, true_and, not_lt]
+    exact and_comm
+  rw [hlt_eq, hge_eq, card_filter_val_lt hk, card_filter_apply_mem_eq O σ] at hpart
+  omega
+
+/-- **Exact step recurrence for `occPermSet`**: for any `k < m`,
+`(m - k) * (occPermSet O (k + 1)).card = (O.card - k) * (occPermSet O k).card`. -/
+theorem mul_card_occPermSet_succ {m : ℕ} (O : Finset (Fin m)) {k : ℕ} (hk : k < m) :
+    (m - k) * (occPermSet O (k + 1)).card = (O.card - k) * (occPermSet O k).card := by
+  classical
+  set J_ge := Finset.univ.filter fun j : Fin m => k ≤ j.val
+  have hsum_j :
+      ∑ j ∈ J_ge, ((occPermSet O k).filter fun σ => σ j ∈ O).card =
+        (m - k) * (occPermSet O (k + 1)).card := by
+    have hcongr : ∀ j ∈ J_ge,
+        ((occPermSet O k).filter fun σ => σ j ∈ O).card = (occPermSet O (k + 1)).card := by
+      intro j hj
+      exact card_filter_occPermSet_eq_succ O hk (Finset.mem_filter.mp hj).2
+    rw [Finset.sum_congr rfl hcongr, Finset.sum_const, smul_eq_mul,
+      card_filter_val_ge (le_of_lt hk)]
+  have hsum_σ :
+      ∑ j ∈ J_ge, ((occPermSet O k).filter fun σ => σ j ∈ O).card =
+        (O.card - k) * (occPermSet O k).card := by
+    simp only [Finset.card_filter]
+    rw [Finset.sum_comm]
+    have hcongr : ∀ σ ∈ occPermSet O k,
+        (∑ j ∈ J_ge, if σ j ∈ O then 1 else 0) = O.card - k := by
+      intro σ hσ
+      rw [← Finset.card_filter]
+      exact card_filter_ge_and_mem (le_of_lt hk) hσ
+    rw [Finset.sum_congr rfl hcongr, Finset.sum_const, smul_eq_mul, Nat.mul_comm]
+  omega
+
+/-- **Exact textbook product formula ([CLRS2009], Proof of Theorem 11.6)**:
+for any occupied slot set `O : Finset (Fin m)` and `k ≤ m`, the probability over a uniform random
+permutation `σ ← PMF.uniformOfFintype (Equiv.Perm (Fin m))` that the first `k` probes all hit `O`
+(`k < unsuccessfulProbes O σ`) is `∏ i ∈ Finset.range k, ((O.card - i : ℝ≥0∞) / (m - i : ℝ≥0∞))`.
+-/
+theorem toOuterMeasure_allOccupied_eq_prod {m : ℕ} (O : Finset (Fin m)) {k : ℕ} (hk : k ≤ m) :
+    (PMF.uniformOfFintype (Equiv.Perm (Fin m))).toOuterMeasure {σ | allOccupied O k σ} =
+      ∏ i ∈ Finset.range k, (((O.card - i : ℕ) : ℝ≥0∞) / ((m - i : ℕ) : ℝ≥0∞)) := by
+  induction k with
+  | zero =>
+    rw [PMF.toOuterMeasure_uniformOfFintype]
+    change ((occPermSet O 0).card : ℝ≥0∞) * (Fintype.card (Equiv.Perm (Fin m)) : ℝ≥0∞)⁻¹ = _
+    rw [occPermSet_zero, Finset.card_univ, Finset.prod_range_zero]
+    have hcard_pos : 0 < Fintype.card (Equiv.Perm (Fin m)) := Fintype.card_pos_iff.mpr ⟨1⟩
+    exact ENNReal.mul_inv_cancel (by exact_mod_cast hcard_pos.ne') (ENNReal.natCast_ne_top _)
+  | succ k ih =>
+    have hk_lt : k < m := hk
+    rw [Finset.prod_range_succ, ← ih (le_of_lt hk_lt)]
+    rw [PMF.toOuterMeasure_uniformOfFintype, PMF.toOuterMeasure_uniformOfFintype]
+    change ((occPermSet O (k + 1)).card : ℝ≥0∞) * (Fintype.card (Equiv.Perm (Fin m)) : ℝ≥0∞)⁻¹ =
+      ((occPermSet O k).card : ℝ≥0∞) * (Fintype.card (Equiv.Perm (Fin m)) : ℝ≥0∞)⁻¹ *
+        (((O.card - k : ℕ) : ℝ≥0∞) / ((m - k : ℕ) : ℝ≥0∞))
+    have hrec : (((m - k : ℕ) : ℝ≥0∞) * ((occPermSet O (k + 1)).card : ℝ≥0∞)) =
+        ((O.card - k : ℕ) : ℝ≥0∞) * ((occPermSet O k).card : ℝ≥0∞) := by
+      exact_mod_cast mul_card_occPermSet_succ O hk_lt
+    have hmk_ne0 : ((m - k : ℕ) : ℝ≥0∞) ≠ 0 := by
+      exact_mod_cast (by omega : m - k ≠ 0)
+    have hmk_top : ((m - k : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _
+    have hcard_eq : ((occPermSet O (k + 1)).card : ℝ≥0∞) =
+        ((occPermSet O k).card : ℝ≥0∞) * (((O.card - k : ℕ) : ℝ≥0∞) / ((m - k : ℕ) : ℝ≥0∞)) := by
+      rw [div_eq_mul_inv, ← mul_assoc, mul_comm ((occPermSet O k).card : ℝ≥0∞), ← hrec,
+        mul_comm ((m - k : ℕ) : ℝ≥0∞), mul_assoc, ENNReal.mul_inv_cancel hmk_ne0 hmk_top, mul_one]
+    rw [hcard_eq]
+    ring
+
+/-- Each factor `(n - i) / (m - i)` for `i < m` and `n ≤ m` is at most `n / m`. -/
+theorem sub_div_sub_le_div {n m i : ℕ} (hnm : n ≤ m) (hi : i < m) :
+    (((n - i : ℕ) : ℝ≥0∞) / ((m - i : ℕ) : ℝ≥0∞)) ≤ (n : ℝ≥0∞) / (m : ℝ≥0∞) := by
+  have hm_ne0 : (m : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : m ≠ 0)
+  have hm_top : (m : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top m
+  have hmi_ne0 : ((m - i : ℕ) : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : m - i ≠ 0)
+  have hmi_top : ((m - i : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top (m - i)
+  have hnat : (n - i) * m ≤ n * (m - i) := by
+    rw [Nat.sub_mul, Nat.mul_sub, Nat.mul_comm n i]
+    exact Nat.sub_le_sub_left (Nat.mul_le_mul_left i hnm) (n * m)
+  have hcast : ((n - i : ℕ) : ℝ≥0∞) * (m : ℝ≥0∞) ≤ (n : ℝ≥0∞) * ((m - i : ℕ) : ℝ≥0∞) := by
+    exact_mod_cast hnat
+  calc
+    (((n - i : ℕ) : ℝ≥0∞) / ((m - i : ℕ) : ℝ≥0∞))
+      = (((n - i : ℕ) : ℝ≥0∞) * (m : ℝ≥0∞)) * ((m : ℝ≥0∞)⁻¹ * ((m - i : ℕ) : ℝ≥0∞)⁻¹) := by
+          rw [div_eq_mul_inv, mul_assoc, ← mul_assoc (m : ℝ≥0∞),
+            ENNReal.mul_inv_cancel hm_ne0 hm_top, one_mul]
+    _ ≤ ((n : ℝ≥0∞) * ((m - i : ℕ) : ℝ≥0∞)) * ((m : ℝ≥0∞)⁻¹ * ((m - i : ℕ) : ℝ≥0∞)⁻¹) := by
+          gcongr
+    _ = (n : ℝ≥0∞) / (m : ℝ≥0∞) := by
+          rw [div_eq_mul_inv, mul_assoc, mul_left_comm ((m - i : ℕ) : ℝ≥0∞),
+            ENNReal.mul_inv_cancel hmi_ne0 hmi_top, mul_one]
+
+/-- **Upper bound `(n / m) ^ k` on the `k`-probe tail probability ([CLRS2009], Proof of Theorem
+11.6)**: for any occupied slot set `O : Finset (Fin m)` and `k ≤ m`, the probability over a uniform
+random permutation `σ` that the first `k` probes all hit `O` is at most
+`((O.card : ℝ≥0∞) / (m : ℝ≥0∞)) ^ k`. -/
+theorem toOuterMeasure_allOccupied_le_pow {m : ℕ} (O : Finset (Fin m)) {k : ℕ} (hk : k ≤ m) :
+    (PMF.uniformOfFintype (Equiv.Perm (Fin m))).toOuterMeasure {σ | allOccupied O k σ} ≤
+      ((O.card : ℝ≥0∞) / (m : ℝ≥0∞)) ^ k := by
+  have hO_le : O.card ≤ m := by
+    simpa using Finset.card_le_univ O
+  rw [toOuterMeasure_allOccupied_eq_prod O hk]
+  calc
+    (∏ i ∈ Finset.range k, (((O.card - i : ℕ) : ℝ≥0∞) / ((m - i : ℕ) : ℝ≥0∞)))
+      ≤ ∏ _i ∈ Finset.range k, ((O.card : ℝ≥0∞) / (m : ℝ≥0∞)) :=
+        Finset.prod_le_prod fun i hi =>
+          sub_div_sub_le_div hO_le (lt_of_lt_of_le (Finset.mem_range.mp hi) hk)
+    _ = ((O.card : ℝ≥0∞) / (m : ℝ≥0∞)) ^ k := by
+        simp [Finset.prod_const]
+
+/-- Finite geometric sum identity in `ℝ≥0∞` without subtraction: for `n < m`,
+`∑ k ∈ Finset.range j, (n / m) ^ k + (m / (m - n)) * (n / m) ^ j = m / (m - n)`. -/
+theorem sum_div_pow_add_tail {n m : ℕ} (hnm : n < m) (j : ℕ) :
+    (∑ k ∈ Finset.range j, ((n : ℝ≥0∞) / (m : ℝ≥0∞)) ^ k) +
+      ((m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞)) * ((n : ℝ≥0∞) / (m : ℝ≥0∞)) ^ j =
+        (m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞) := by
+  have hm_ne0 : (m : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : m ≠ 0)
+  have hm_top : (m : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top m
+  have hmn_ne0 : ((m - n : ℕ) : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : m - n ≠ 0)
+  have hmn_top : ((m - n : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top (m - n)
+  have hstep : 1 + ((m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞)) * ((n : ℝ≥0∞) / (m : ℝ≥0∞)) =
+      (m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞) := by
+    have hmul : ((m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞)) * ((n : ℝ≥0∞) / (m : ℝ≥0∞)) =
+        (n : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞) := by
+      rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv,
+        mul_comm (n : ℝ≥0∞), ← mul_assoc, mul_right_comm (m : ℝ≥0∞),
+        ENNReal.mul_inv_cancel hm_ne0 hm_top, one_mul, mul_comm]
+    rw [hmul, ← ENNReal.div_self hmn_ne0 hmn_top, ← ENNReal.add_div]
+    congr 1
+    exact_mod_cast Nat.sub_add_cancel (le_of_lt hnm)
+  induction j with
+  | zero => simp
+  | succ j ih =>
+    have htail : ((n : ℝ≥0∞) / (m : ℝ≥0∞)) ^ j +
+        ((m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞)) * ((n : ℝ≥0∞) / (m : ℝ≥0∞)) ^ (j + 1) =
+          ((m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞)) * ((n : ℝ≥0∞) / (m : ℝ≥0∞)) ^ j := by
+      rw [pow_succ, ← mul_assoc,
+        mul_comm ((m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞)) (((n : ℝ≥0∞) / (m : ℝ≥0∞)) ^ j),
+        mul_assoc]
+      nth_rw 1 [← mul_one (((n : ℝ≥0∞) / (m : ℝ≥0∞)) ^ j)]
+      rw [← mul_add, hstep, mul_comm]
+    rw [Finset.sum_range_succ, add_assoc, htail, ih]
+
+/-- For `n < m`, any partial geometric sum `∑ k ∈ Finset.range j, (n / m) ^ k` is at most
+`m / (m - n)`. -/
+theorem sum_div_pow_le {n m : ℕ} (hnm : n < m) (j : ℕ) :
+    (∑ k ∈ Finset.range j, ((n : ℝ≥0∞) / (m : ℝ≥0∞)) ^ k) ≤
+      (m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞) := by
+  rw [← sum_div_pow_add_tail hnm j]
+  exact le_self_add
+
+/-- When `2 * n ≤ m` and `0 < m`, `m / (m - n) ≤ 2` (`1 / (1 - α) ≤ 2` for load factor `α ≤ 1 / 2`).
+-/
+theorem div_sub_le_two {n m : ℕ} (hm : 0 < m) (h2n : 2 * n ≤ m) :
+    (m : ℝ≥0∞) / ((m - n : ℕ) : ℝ≥0∞) ≤ 2 := by
+  have hmn_ne0 : ((m - n : ℕ) : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : m - n ≠ 0)
+  have hmn_top : ((m - n : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top (m - n)
+  rw [ENNReal.div_le_iff_le_mul (Or.inl hmn_ne0) (Or.inl hmn_top)]
+  exact_mod_cast (by omega : m ≤ 2 * (m - n))
+
+/-- **Theorem 11.6 of [CLRS2009] (Expected probes in an unsuccessful search)**:
+for any occupied slot set `O : Finset (Fin m)` with `O.card < m`, the expected number of probes
+`unsuccessfulProbes O σ` over a uniform random permutation
+`σ ← PMF.uniformOfFintype (Equiv.Perm (Fin m))` is at most `m / (m - O.card)`. -/
+theorem expect_unsuccessfulProbes_le {m : ℕ} {O : Finset (Fin m)} (hO : O.card < m) :
+    (∑' σ : Equiv.Perm (Fin m),
+      PMF.uniformOfFintype (Equiv.Perm (Fin m)) σ * (unsuccessfulProbes O σ : ℝ≥0∞)) ≤
+        (m : ℝ≥0∞) / ((m - O.card : ℕ) : ℝ≥0∞) := by
+  classical
+  let μ := PMF.uniformOfFintype (Equiv.Perm (Fin m))
+  have hdecomp : ∀ σ : Equiv.Perm (Fin m),
+      μ σ * (unsuccessfulProbes O σ : ℝ≥0∞) =
+        ∑ k ∈ Finset.range m, μ σ * (if allOccupied O k σ then 1 else 0) := by
+    intro σ
+    rw [← Finset.mul_sum]
+    congr 1
+    exact_mod_cast unsuccessfulProbes_eq_sum_boole hO σ
+  change (∑' σ : Equiv.Perm (Fin m), μ σ * (unsuccessfulProbes O σ : ℝ≥0∞)) ≤ _
+  simp_rw [hdecomp]
+  rw [tsum_fintype, Finset.sum_comm]
+  have hterm : ∀ k ∈ Finset.range m,
+      (∑ σ : Equiv.Perm (Fin m), μ σ * (if allOccupied O k σ then (1 : ℝ≥0∞) else 0)) =
+        μ.toOuterMeasure {σ | allOccupied O k σ} := by
+    intro k _
+    rw [PMF.toOuterMeasure_apply, tsum_fintype]
+    refine Finset.sum_congr rfl fun σ _ => ?_
+    unfold Set.indicator
+    by_cases h : allOccupied O k σ
+    · have hmem : σ ∈ {σ | allOccupied O k σ} := h
+      simp [h, hmem]
+    · have hmem : σ ∉ {σ | allOccupied O k σ} := h
+      simp [h, hmem]
+  rw [Finset.sum_congr rfl hterm]
+  calc
+    (∑ k ∈ Finset.range m, μ.toOuterMeasure {σ | allOccupied O k σ})
+      ≤ ∑ k ∈ Finset.range m, ((O.card : ℝ≥0∞) / (m : ℝ≥0∞)) ^ k :=
+        Finset.sum_le_sum fun k hk =>
+          toOuterMeasure_allOccupied_le_pow O (le_of_lt (Finset.mem_range.mp hk))
+    _ ≤ (m : ℝ≥0∞) / ((m - O.card : ℕ) : ℝ≥0∞) := sum_div_pow_le hO m
+
+/-- **Half-load corollary of Theorem 11.6 ([CLRS2009], Section 11.4)**:
+when `0 < m` and `2 * O.card ≤ m` (load factor `α = O.card / m ≤ 1 / 2`), the expected number of
+probes in an unsuccessful search is at most `2`. -/
+theorem expect_unsuccessfulProbes_le_two {m : ℕ} {O : Finset (Fin m)}
+    (hm : 0 < m) (h2n : 2 * O.card ≤ m) :
+    (∑' σ : Equiv.Perm (Fin m),
+      PMF.uniformOfFintype (Equiv.Perm (Fin m)) σ * (unsuccessfulProbes O σ : ℝ≥0∞)) ≤ 2 :=
+  (expect_unsuccessfulProbes_le (by omega)).trans (div_sub_le_two hm h2n)
+
+
+/-! ## Section 3: Open-Addressed Table Model ([CLRS2009], Section 11.4, pp. 270–276) -/
+
+/-- Pure open-addressed hash table of `m` slots over key universe `Fin U`, where each slot holds
+`none` (empty) or `some (u, v)` (occupied by key `u` with value `v`). -/
+abbrev Table (U m : ℕ) := Fin m → Option (Fin U × ℕ)
+
+/-- The initially empty table of `m` slots. -/
+def emptyTable (U m : ℕ) : Table U m := fun _ => none
+
+/-- The finite set of currently occupied slot indices in table `T`. -/
+def occupiedSlots {U m : ℕ} (T : Table U m) : Finset (Fin m) :=
+  Finset.univ.filter fun j => (T j).isSome
+
+/-- The finite set of slot indices in `T` occupied by keys distinct from `u`. -/
+def otherOccupiedSlots {U m : ℕ} (T : Table U m) (u : Fin U) : Finset (Fin m) :=
+  Finset.univ.filter fun j => (T j).isSome ∧ (T j).map Prod.fst ≠ some u
+
+/-- Total number of slot probes `1 + missedProbes (otherOccupiedSlots T u) σ` made when probing
+table `T` for key `u` along permutation `σ`. -/
+def probeCount {U m : ℕ} (T : Table U m) (u : Fin U) (σ : Equiv.Perm (Fin m)) : ℕ :=
+  unsuccessfulProbes (otherOccupiedSlots T u) σ
+
+@[simp]
+theorem occupiedSlots_emptyTable (U m : ℕ) :
+    occupiedSlots (emptyTable U m) = ∅ := by
+  ext j
+  simp [occupiedSlots, emptyTable]
+
+@[simp]
+theorem otherOccupiedSlots_emptyTable (U m : ℕ) (u : Fin U) :
+    otherOccupiedSlots (emptyTable U m) u = ∅ := by
+  ext j
+  simp [otherOccupiedSlots, emptyTable]
+
+theorem mem_otherOccupiedSlots_iff {U m : ℕ} {T : Table U m} {u : Fin U} {j : Fin m} :
+    j ∈ otherOccupiedSlots T u ↔ ∃ u' v', T j = some (u', v') ∧ u' ≠ u := by
+  simp only [otherOccupiedSlots, Finset.mem_filter, Finset.mem_univ, true_and]
+  cases h : T j with
+  | none => simp
+  | some p =>
+    rcases p with ⟨u', v'⟩
+    simp
+
+theorem otherOccupiedSlots_subset_occupiedSlots {U m : ℕ} (T : Table U m) (u : Fin U) :
+    otherOccupiedSlots T u ⊆ occupiedSlots T := by
+  intro j hj
+  rcases mem_otherOccupiedSlots_iff.mp hj with ⟨u', v', hTj, -⟩
+  simp [occupiedSlots, hTj]
+
+/-- Open-addressed table representation invariant linking concrete slot array `T : Table U m` to
+abstract dictionary state `s : Dictionary.State U` under permutation family
+`π : Fin U → Equiv.Perm (Fin m)`. -/
+structure TableRep {U m : ℕ} (π : Fin U → Equiv.Perm (Fin m)) (s : Dictionary.State U)
+    (T : Table U m) : Prop where
+  /-- Every occupied slot `j` holds `(u, v)` with `s u = some v` at key `u`'s stopping probe index.
+  -/
+  slot_spec : ∀ j u v, T j = some (u, v) →
+    s u = some v ∧ ∃ h : missedProbes (otherOccupiedSlots T u) (π u) < m,
+      j = π u ⟨missedProbes (otherOccupiedSlots T u) (π u), h⟩
+  /-- Every present key `u` with `s u = some v` is stored at its stopping probe index. -/
+  key_spec : ∀ u v, s u = some v →
+    ∃ h : missedProbes (otherOccupiedSlots T u) (π u) < m,
+      T (π u ⟨missedProbes (otherOccupiedSlots T u) (π u), h⟩) = some (u, v)
+
+/-- The empty table represents `Dictionary.empty U` under any permutation family `π`. -/
+theorem tableRep_empty {U m : ℕ} (π : Fin U → Equiv.Perm (Fin m)) :
+    TableRep π (Dictionary.empty U) (emptyTable U m) where
+  slot_spec j _ _ h := by simp [emptyTable] at h
+  key_spec u _ h := by simp [Dictionary.empty] at h
+
+/-- Under `TableRep π s T`, each key `u` occupies at most one slot in `T`. -/
+theorem TableRep.slot_eq_of_same_key {U m : ℕ} {π : Fin U → Equiv.Perm (Fin m)}
+    {s : Dictionary.State U} {T : Table U m} (hrep : TableRep π s T)
+    {j₁ j₂ : Fin m} {u : Fin U} {v₁ v₂ : ℕ}
+    (h₁ : T j₁ = some (u, v₁)) (h₂ : T j₂ = some (u, v₂)) : j₁ = j₂ := by
+  obtain ⟨-, hlt₁, rfl⟩ := hrep.slot_spec j₁ u v₁ h₁
+  obtain ⟨-, _, rfl⟩ := hrep.slot_spec j₂ u v₂ h₂
+  rfl
+
+/-- Under `TableRep π s T`, the number of occupied slots in `T` equals `(Dictionary.dom s).card`. -/
+theorem TableRep.card_occupiedSlots {U m : ℕ} {π : Fin U → Equiv.Perm (Fin m)}
+    {s : Dictionary.State U} {T : Table U m} (hrep : TableRep π s T) :
+    (occupiedSlots T).card = (Dictionary.dom s).card := by
+  refine Finset.card_bij
+    (fun j hj => ((T j).get (by simpa [occupiedSlots] using hj)).1) ?_ ?_ ?_
+  · intro j hj
+    have his : (T j).isSome := by simpa [occupiedSlots] using hj
+    obtain ⟨⟨u, v⟩, hTj⟩ := Option.isSome_iff_exists.mp his
+    have hsu := (hrep.slot_spec j u v hTj).1
+    simp [Dictionary.dom, hTj, hsu]
+  · intro j₁ hj₁ j₂ hj₂ heq
+    obtain ⟨⟨u₁, v₁⟩, h₁⟩ := Option.isSome_iff_exists.mp (by simpa [occupiedSlots] using hj₁)
+    obtain ⟨⟨u₂, v₂⟩, h₂⟩ := Option.isSome_iff_exists.mp (by simpa [occupiedSlots] using hj₂)
+    have hu : u₁ = u₂ := by simpa [h₁, h₂] using heq
+    subst hu
+    exact hrep.slot_eq_of_same_key h₁ h₂
+  · intro u hu
+    obtain ⟨v, hsu⟩ := Dictionary.mem_dom_iff.mp hu
+    obtain ⟨hlt, hTj⟩ := hrep.key_spec u v hsu
+    refine ⟨π u ⟨missedProbes (otherOccupiedSlots T u) (π u), hlt⟩, ?_, ?_⟩
+    · simp [occupiedSlots, hTj]
+    · simp [hTj]
+
+/-- Under `TableRep π s T`, `(otherOccupiedSlots T u).card = ((Dictionary.dom s).erase u).card`. -/
+theorem TableRep.card_otherOccupiedSlots {U m : ℕ} {π : Fin U → Equiv.Perm (Fin m)}
+    {s : Dictionary.State U} {T : Table U m} (hrep : TableRep π s T) (u : Fin U) :
+    (otherOccupiedSlots T u).card = ((Dictionary.dom s).erase u).card := by
+  refine Finset.card_bij
+    (fun j hj => ((T j).get (by
+      exact (Finset.mem_filter.mp hj).2.1)).1) ?_ ?_ ?_
+  · intro j hj
+    rcases mem_otherOccupiedSlots_iff.mp hj with ⟨u', v', hTj, hne⟩
+    have hsu' := (hrep.slot_spec j u' v' hTj).1
+    simp [Dictionary.dom, hTj, hsu', hne]
+  · intro j₁ hj₁ j₂ hj₂ heq
+    rcases mem_otherOccupiedSlots_iff.mp hj₁ with ⟨u₁, v₁, h₁, -⟩
+    rcases mem_otherOccupiedSlots_iff.mp hj₂ with ⟨u₂, v₂, h₂, -⟩
+    have hu : u₁ = u₂ := by simpa [h₁, h₂] using heq
+    subst hu
+    exact hrep.slot_eq_of_same_key h₁ h₂
+  · intro u' hu'
+    rcases Finset.mem_erase.mp hu' with ⟨hne, hu'_dom⟩
+    obtain ⟨v', hsu'⟩ := Dictionary.mem_dom_iff.mp hu'_dom
+    obtain ⟨hlt, hTj⟩ := hrep.key_spec u' v' hsu'
+    refine ⟨π u' ⟨missedProbes (otherOccupiedSlots T u') (π u'), hlt⟩, ?_, ?_⟩
+    · exact mem_otherOccupiedSlots_iff.mpr ⟨u', v', hTj, hne⟩
+    · simp [hTj]
+
+/-- Under `TableRep π s T`, `(otherOccupiedSlots T u).card ≤ (Dictionary.dom s).card`. -/
+theorem TableRep.card_otherOccupiedSlots_le {U m : ℕ} {π : Fin U → Equiv.Perm (Fin m)}
+    {s : Dictionary.State U} {T : Table U m} (hrep : TableRep π s T) (u : Fin U) :
+    (otherOccupiedSlots T u).card ≤ (Dictionary.dom s).card := by
+  rw [hrep.card_otherOccupiedSlots u]
+  exact Finset.card_erase_le
+
+/-- When `s u = none`, no slot in `T` holds key `u`, so `otherOccupiedSlots T u = occupiedSlots T`.
+-/
+theorem TableRep.otherOccupiedSlots_eq_occupiedSlots_of_eq_none {U m : ℕ}
+    {π : Fin U → Equiv.Perm (Fin m)} {s : Dictionary.State U} {T : Table U m}
+    (hrep : TableRep π s T) {u : Fin U} (hu : s u = none) :
+    otherOccupiedSlots T u = occupiedSlots T := by
+  ext j
+  refine ⟨fun hj => otherOccupiedSlots_subset_occupiedSlots T u hj, fun hj => ?_⟩
+  simp only [occupiedSlots, Finset.mem_filter, Finset.mem_univ, true_and] at hj
+  obtain ⟨⟨u', v'⟩, hTj⟩ := Option.isSome_iff_exists.mp hj
+  have hsu' := (hrep.slot_spec j u' v' hTj).1
+  have hne : u' ≠ u := by
+    rintro rfl
+    rw [hu] at hsu'
+    cases hsu'
+  exact mem_otherOccupiedSlots_iff.mpr ⟨u', v', hTj, hne⟩
+
+/-- When `TableRep π s T` and `(Dictionary.dom s).card < m`, the stopping index for any key `u`
+satisfies `missedProbes (otherOccupiedSlots T u) (π u) < m`. -/
+theorem TableRep.missedProbes_lt {U m : ℕ} {π : Fin U → Equiv.Perm (Fin m)}
+    {s : Dictionary.State U} {T : Table U m} (hrep : TableRep π s T)
+    (hcard : (Dictionary.dom s).card < m) (u : Fin U) :
+    missedProbes (otherOccupiedSlots T u) (π u) < m :=
+  missedProbes_lt_of_card_lt (lt_of_le_of_lt (hrep.card_otherOccupiedSlots_le u) hcard) (π u)
+
+/-- Target slot `π u ⟨missedProbes (otherOccupiedSlots T u) (π u), _⟩` where key `u` is found or
+inserted when `(otherOccupiedSlots T u).card < m`. -/
+def targetSlot {U m : ℕ} (π : Fin U → Equiv.Perm (Fin m)) (T : Table U m) (u : Fin U)
+    (hO : (otherOccupiedSlots T u).card < m) : Fin m :=
+  π u (probeSlotIndex (otherOccupiedSlots T u) (π u) hO)
+
+/-- Under `TableRep π s T` and `hO : (otherOccupiedSlots T u).card < m`, `T (targetSlot π T u hO)`
+equals `(s u).map (fun v => (u, v))`. -/
+theorem TableRep.apply_targetSlot {U m : ℕ} {π : Fin U → Equiv.Perm (Fin m)}
+    {s : Dictionary.State U} {T : Table U m} (hrep : TableRep π s T) (u : Fin U)
+    (hO : (otherOccupiedSlots T u).card < m) :
+    T (targetSlot π T u hO) = (s u).map (fun v => (u, v)) := by
+  cases hsu : s u with
+  | none =>
+    simp only [Option.map_none]
+    have hnot : targetSlot π T u hO ∉ otherOccupiedSlots T u :=
+      notMem_apply_probeSlotIndex hO
+    cases hTj : T (targetSlot π T u hO) with
+    | none => rfl
+    | some p =>
+      rcases p with ⟨u', v'⟩
+      by_cases hne : u' = u
+      · subst hne
+        have hsu' := (hrep.slot_spec _ u' v' hTj).1
+        rw [hsu] at hsu'
+        cases hsu'
+      · exact False.elim (hnot (mem_otherOccupiedSlots_iff.mpr ⟨u', v', hTj, hne⟩))
+  | some v =>
+    simp only [Option.map_some]
+    obtain ⟨_, hTj⟩ := hrep.key_spec u v hsu
+    exact hTj
+
+/-- Pure open-addressed lookup `tableGet hm π T u` when `0 < m`: inspects slot
+`π u ⟨min (missedProbes (otherOccupiedSlots T u) (π u)) (m - 1), _⟩` and returns `some v` if it
+contains `(u, v)`, else `none`. -/
+def tableGet {U m : ℕ} (hm : 0 < m) (π : Fin U → Equiv.Perm (Fin m)) (T : Table U m)
+    (u : Fin U) : Option ℕ :=
+  let idx := min (missedProbes (otherOccupiedSlots T u) (π u)) (m - 1)
+  match T (π u ⟨idx, by omega⟩) with
+  | some (u', v) => if u' = u then some v else none
+  | none => none
+
+/-- Pure open-addressed insertion `tableInsert hm π T u v`: writes `some (u, v)` at slot
+`π u ⟨min (missedProbes (otherOccupiedSlots T u) (π u)) (m - 1), _⟩`. -/
+def tableInsert {U m : ℕ} (hm : 0 < m) (π : Fin U → Equiv.Perm (Fin m)) (T : Table U m)
+    (u : Fin U) (v : ℕ) : Table U m :=
+  let idx := min (missedProbes (otherOccupiedSlots T u) (π u)) (m - 1)
+  Function.update T (π u ⟨idx, by omega⟩) (some (u, v))
+
+theorem tableInsert_eq_update_targetSlot {U m : ℕ} (hm : 0 < m) (π : Fin U → Equiv.Perm (Fin m))
+    (T : Table U m) (u : Fin U) (v : ℕ) (hO : (otherOccupiedSlots T u).card < m) :
+    tableInsert hm π T u v = Function.update T (targetSlot π T u hO) (some (u, v)) := by
+  have hlt : missedProbes (otherOccupiedSlots T u) (π u) < m :=
+    missedProbes_lt_of_card_lt hO (π u)
+  have hmin : min (missedProbes (otherOccupiedSlots T u) (π u)) (m - 1) =
+      missedProbes (otherOccupiedSlots T u) (π u) := Nat.min_eq_left (by omega)
+  have hslot : (⟨min (missedProbes (otherOccupiedSlots T u) (π u)) (m - 1), by omega⟩ : Fin m) =
+      probeSlotIndex (otherOccupiedSlots T u) (π u) hO := Fin.ext hmin
+  dsimp only [tableInsert, targetSlot]
+  rw [hslot]
+
+/-- Under `TableRep π s T` and `(otherOccupiedSlots T u).card < m`, `tableGet hm π T u = s u`. -/
+theorem TableRep.tableGet_eq {U m : ℕ} (hm : 0 < m) {π : Fin U → Equiv.Perm (Fin m)}
+    {s : Dictionary.State U} {T : Table U m} (hrep : TableRep π s T) (u : Fin U)
+    (hO : (otherOccupiedSlots T u).card < m) :
+    tableGet hm π T u = s u := by
+  have hlt : missedProbes (otherOccupiedSlots T u) (π u) < m :=
+    missedProbes_lt_of_card_lt hO (π u)
+  have hmin : min (missedProbes (otherOccupiedSlots T u) (π u)) (m - 1) =
+      missedProbes (otherOccupiedSlots T u) (π u) := Nat.min_eq_left (by omega)
+  dsimp only [tableGet]
+  have hslot : (⟨min (missedProbes (otherOccupiedSlots T u) (π u)) (m - 1), by omega⟩ : Fin m) =
+      probeSlotIndex (otherOccupiedSlots T u) (π u) hO := Fin.ext hmin
+  rw [hslot]
+  have htarget := hrep.apply_targetSlot u hO
+  dsimp only [targetSlot] at htarget
+  rw [htarget]
+  cases s u <;> simp
+
+/-- Inserting `(u, v)` leaves `otherOccupiedSlots` for `u` itself unchanged. -/
+theorem otherOccupiedSlots_tableInsert_self {U m : ℕ} (hm : 0 < m)
+    {π : Fin U → Equiv.Perm (Fin m)} {s : Dictionary.State U} {T : Table U m}
+    (_hrep : TableRep π s T) (u : Fin U) (v : ℕ)
+    (hO : (otherOccupiedSlots T u).card < m) :
+    otherOccupiedSlots (tableInsert hm π T u v) u = otherOccupiedSlots T u := by
+  rw [tableInsert_eq_update_targetSlot hm π T u v hO]
+  ext j
+  by_cases hj : j = targetSlot π T u hO
+  · subst hj
+    have hnot : targetSlot π T u hO ∉ otherOccupiedSlots T u :=
+      notMem_apply_probeSlotIndex hO
+    simp [mem_otherOccupiedSlots_iff, hnot]
+  · simp [mem_otherOccupiedSlots_iff, Function.update_of_ne hj]
+
+/-- Inserting `(u, v)` preserves the stopping index `missedProbes (otherOccupiedSlots · w) (π w)`
+for every key `w` already present in `s` (`(s w).isSome`). -/
+theorem TableRep.missedProbes_tableInsert_of_isSome {U m : ℕ} (hm : 0 < m)
+    {π : Fin U → Equiv.Perm (Fin m)} {s : Dictionary.State U} {T : Table U m}
+    (hrep : TableRep π s T) (u : Fin U) (v : ℕ)
+    (hO : (otherOccupiedSlots T u).card < m)
+    {w : Fin U} (hw : (s w).isSome) :
+    missedProbes (otherOccupiedSlots (tableInsert hm π T u v) w) (π w) =
+      missedProbes (otherOccupiedSlots T w) (π w) := by
+  by_cases hwu : w = u
+  · subst hwu
+    rw [otherOccupiedSlots_tableInsert_self hm hrep w v hO]
+  · obtain ⟨vw, hsw⟩ := Option.isSome_iff_exists.mp hw
+    obtain ⟨hlt_w, hTw⟩ := hrep.key_spec w vw hsw
+    set iw : Fin m := ⟨missedProbes (otherOccupiedSlots T w) (π w), hlt_w⟩
+    have hiw_spec := (missedProbes_eq_iff (O := otherOccupiedSlots T w) (σ := π w) iw).mp rfl
+    have htarget_u := hrep.apply_targetSlot u hO
+    have hne_slot : π w iw ≠ targetSlot π T u hO := by
+      intro heq
+      rw [← heq, hTw] at htarget_u
+      cases hsu : s u with
+      | none => simp [hsu] at htarget_u
+      | some vu =>
+        simp only [hsu, Option.map_some, Option.some.injEq, Prod.mk.injEq] at htarget_u
+        exact hwu htarget_u.1
+    rw [tableInsert_eq_update_targetSlot hm π T u v hO]
+    apply (missedProbes_eq_iff iw).mpr
+    refine ⟨fun i hi => ?_, ?_⟩
+    · have hi_mem : π w i ∈ otherOccupiedSlots T w := hiw_spec.1 i hi
+      rcases mem_otherOccupiedSlots_iff.mp hi_mem with ⟨u', v', hTi, hne'⟩
+      rw [mem_otherOccupiedSlots_iff]
+      by_cases h_eq : π w i = targetSlot π T u hO
+      · refine ⟨u, v, ?_, Ne.symm hwu⟩
+        simp [h_eq]
+      · refine ⟨u', v', ?_, hne'⟩
+        simp [Function.update_of_ne h_eq, hTi]
+    · rw [mem_otherOccupiedSlots_iff]
+      rintro ⟨u', v', hTiw, hne'⟩
+      simp only [Function.update_of_ne hne_slot] at hTiw
+      rw [hTw] at hTiw
+      injection hTiw with hpair
+      injection hpair with hu' _
+      exact hne' hu'.symm
+
+/-- **Preservation of `TableRep` under `tableInsert`**: if `TableRep π s T` and
+`(otherOccupiedSlots T u).card < m`, then `tableInsert hm π T u v` satisfies
+`TableRep π (Function.update s u (some v))`. -/
+theorem TableRep.tableInsert {U m : ℕ} (hm : 0 < m) {π : Fin U → Equiv.Perm (Fin m)}
+    {s : Dictionary.State U} {T : Table U m} (hrep : TableRep π s T) (u : Fin U) (v : ℕ)
+    (hO : (otherOccupiedSlots T u).card < m) :
+    TableRep π (Function.update s u (some v)) (tableInsert hm π T u v) := by
+  have hlt_u : missedProbes (otherOccupiedSlots T u) (π u) < m :=
+    missedProbes_lt_of_card_lt hO (π u)
+  have hself_mp :
+      missedProbes (otherOccupiedSlots (UniformProbing.tableInsert hm π T u v) u) (π u) =
+        missedProbes (otherOccupiedSlots T u) (π u) := by
+    rw [otherOccupiedSlots_tableInsert_self hm hrep u v hO]
+  have hupd := tableInsert_eq_update_targetSlot hm π T u v hO
+  refine ⟨?_, ?_⟩
+  · intro j w vw hj
+    by_cases hju : j = targetSlot π T u hO
+    · subst hju
+      rw [hupd] at hj
+      simp only [Function.update_self, Option.some.injEq, Prod.mk.injEq] at hj
+      rcases hj with ⟨rfl, rfl⟩
+      refine ⟨by simp, ⟨by omega, ?_⟩⟩
+      ext
+      simp [targetSlot, probeSlotIndex, hself_mp]
+    · rw [hupd, Function.update_of_ne hju] at hj
+      obtain ⟨hsw, hlt_w, hj_eq⟩ := hrep.slot_spec j w vw hj
+      have hwu : w ≠ u := by
+        rintro rfl
+        have ⟨_, hTu⟩ := hrep.key_spec w vw hsw
+        have h_same := hrep.slot_eq_of_same_key hj hTu
+        exact hju h_same
+      have hw_mp := hrep.missedProbes_tableInsert_of_isSome hm u v hO (by rw [hsw]; rfl)
+      refine ⟨by simp [Function.update_of_ne hwu, hsw], ⟨by omega, ?_⟩⟩
+      ext
+      simpa [hw_mp] using congrArg Fin.val hj_eq
+  · intro w vw hsw'
+    by_cases hwu : w = u
+    · subst hwu
+      simp only [Function.update_self, Option.some.injEq] at hsw'
+      subst hsw'
+      refine ⟨by omega, ?_⟩
+      have hidx_eq :
+          (⟨missedProbes (otherOccupiedSlots (UniformProbing.tableInsert hm π T w v) w) (π w),
+            by omega⟩ : Fin m) = probeSlotIndex (otherOccupiedSlots T w) (π w) hO := by
+        ext
+        simp [probeSlotIndex, hself_mp]
+      rw [hidx_eq, hupd]
+      simp [targetSlot]
+    · simp only [Function.update_of_ne hwu] at hsw'
+      obtain ⟨hlt_w, hTw⟩ := hrep.key_spec w vw hsw'
+      have hw_mp := hrep.missedProbes_tableInsert_of_isSome hm u v hO (by rw [hsw']; rfl)
+      refine ⟨by omega, ?_⟩
+      have hidx_eq :
+          (⟨missedProbes (otherOccupiedSlots (UniformProbing.tableInsert hm π T u v) w) (π w),
+            by omega⟩ : Fin m) = ⟨missedProbes (otherOccupiedSlots T w) (π w), hlt_w⟩ := by
+        ext
+        exact hw_mp
+      rw [hidx_eq, hupd]
+      have hne_slot :
+          π w ⟨missedProbes (otherOccupiedSlots T w) (π w), hlt_w⟩ ≠ targetSlot π T u hO := by
+        intro heq
+        have htarget_u := hrep.apply_targetSlot u hO
+        rw [← heq, hTw] at htarget_u
+        cases hsu : s u with
+        | none => simp [hsu] at htarget_u
+        | some vu =>
+          simp only [hsu, Option.map_some, Option.some.injEq, Prod.mk.injEq] at htarget_u
+          exact hwu htarget_u.1
+      simp [Function.update_of_ne hne_slot, hTw]
+
+/-- Inserting `(u, v)` leaves `probeCount · u (π u)` unchanged. -/
+theorem TableRep.probeCount_tableInsert_self {U m : ℕ} (hm : 0 < m)
+    {π : Fin U → Equiv.Perm (Fin m)} {s : Dictionary.State U} {T : Table U m}
+    (hrep : TableRep π s T) (u : Fin U) (v : ℕ)
+    (hO : (otherOccupiedSlots T u).card < m) :
+    probeCount (UniformProbing.tableInsert hm π T u v) u (π u) = probeCount T u (π u) := by
+  simp [probeCount, unsuccessfulProbes, otherOccupiedSlots_tableInsert_self hm hrep u v hO]
+
+/-- **Probe invariance for present keys ([CLRS2009], Section 11.4, p. 275)**:
+once a key `w` is present in `s` (`(s w).isSome`), inserting or updating any key `(u, v)` leaves
+the number of probes `probeCount · w (π w)` made when searching for `w` unchanged. -/
+theorem TableRep.probeCount_tableInsert_of_isSome {U m : ℕ} (hm : 0 < m)
+    {π : Fin U → Equiv.Perm (Fin m)} {s : Dictionary.State U} {T : Table U m}
+    (hrep : TableRep π s T) (u : Fin U) (v : ℕ)
+    (hO : (otherOccupiedSlots T u).card < m)
+    {w : Fin U} (hw : (s w).isSome) :
+    probeCount (UniformProbing.tableInsert hm π T u v) w (π w) = probeCount T w (π w) := by
+  simp [probeCount, unsuccessfulProbes, hrep.missedProbes_tableInsert_of_isSome hm u v hO hw]
+
+/-- Execute a single `Dictionary.Op U` on open-addressed table `T`. -/
+def tableStep {U m : ℕ} (hm : 0 < m) (π : Fin U → Equiv.Perm (Fin m)) (T : Table U m)
+    (o : Dictionary.Op U) : Table U m × (Dictionary.spec U 0 0).Result o :=
+  match o with
+  | .get u => (T, tableGet hm π T u)
+  | .insert u v => (tableInsert hm π T u v, ())
+
+/-- Execute a sequence of `Dictionary.Op U` operations on `T` under permutation family `π`. -/
+def runTableFrom {U m : ℕ} (hm : 0 < m) (π : Fin U → Equiv.Perm (Fin m)) :
+    Table U m → List (Dictionary.Op U) → Table U m
+  | T, [] => T
+  | T, o :: os => runTableFrom hm π (tableStep hm π T o).1 os
+
+/-- Table produced by running `ops` starting from `emptyTable U m`. -/
+def runTable {U m : ℕ} (hm : 0 < m) (π : Fin U → Equiv.Perm (Fin m))
+    (ops : List (Dictionary.Op U)) : Table U m :=
+  runTableFrom hm π (emptyTable U m) ops
+
+/-- Under any admissible operation `(Dictionary.spec U V n_max).valid s o` with `n_max ≤ m` and
+`TableRep π s T`, `(otherOccupiedSlots T u).card < m` holds for the operated key `u`. -/
+theorem TableRep.card_otherOccupiedSlots_lt_of_valid {U V n_max m : ℕ} (_hm : 0 < m)
+    (hcap : n_max ≤ m) {π : Fin U → Equiv.Perm (Fin m)} {s : Dictionary.State U} {T : Table U m}
+    (hrep : TableRep π s T) (hs : (Dictionary.dom s).card ≤ n_max)
+    {u : Fin U} {v : ℕ} (hval : (Dictionary.spec U V n_max).valid s (.insert u v)) :
+    (otherOccupiedSlots T u).card < m := by
+  rcases hval.1 with hlt | hisSome
+  · have hle := hrep.card_otherOccupiedSlots_le u
+    omega
+  · rw [hrep.card_otherOccupiedSlots u]
+    have hmem : u ∈ Dictionary.dom s := Dictionary.mem_dom_iff_isSome.mpr hisSome
+    have herase := Finset.card_erase_lt_of_mem hmem
+    omega
+
+/-- Any valid operation history preserves `TableRep`. -/
+theorem tableRep_runTableFrom {U V n_max m : ℕ} (hm : 0 < m) (hcap : n_max ≤ m)
+    (π : Fin U → Equiv.Perm (Fin m)) {s : Dictionary.State U} {T : Table U m}
+    (hrep : TableRep π s T) (hs : (Dictionary.dom s).card ≤ n_max)
+    {ops : List (Dictionary.Op U)} (hvh : (Dictionary.spec U V n_max).ValidHistory s ops) :
+    TableRep π ((Dictionary.spec U V n_max).run s ops).1 (runTableFrom hm π T ops) := by
+  induction ops generalizing s T with
+  | nil => exact hrep
+  | cons o os ih =>
+    have hs' : (Dictionary.dom ((Dictionary.spec U V n_max).step s o).1).card ≤ n_max :=
+      Dictionary.card_dom_step_le_of_valid hs hvh.1
+    cases o with
+    | get u =>
+      exact ih hrep hs' hvh.2
+    | insert u v =>
+      have hO : (otherOccupiedSlots T u).card < m :=
+        hrep.card_otherOccupiedSlots_lt_of_valid hm hcap hs hvh.1
+      exact ih (hrep.tableInsert hm u v hO) hs' hvh.2
+
+/-- Running any valid operation history from `emptyTable U m` produces a table satisfying
+`TableRep`. -/
+theorem tableRep_runTable {U V n_max m : ℕ} (hm : 0 < m) (hcap : n_max ≤ m)
+    (π : Fin U → Equiv.Perm (Fin m)) {ops : List (Dictionary.Op U)}
+    (hvh : (Dictionary.spec U V n_max).ValidHistory (Dictionary.empty U) ops) :
+    TableRep π ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops).1
+      (runTable hm π ops) :=
+  tableRep_runTableFrom hm hcap π (tableRep_empty π) (by simp) hvh
+
+/-- If key `w` is already present in `s`, then running any valid continuation `ops` from `(s, T)`
+preserves `probeCount · w (π w)`. -/
+theorem probeCount_runTableFrom_of_isSome {U V n_max m : ℕ} (hm : 0 < m) (hcap : n_max ≤ m)
+    (π : Fin U → Equiv.Perm (Fin m)) {s : Dictionary.State U} {T : Table U m}
+    (hrep : TableRep π s T) (hs : (Dictionary.dom s).card ≤ n_max)
+    {w : Fin U} (hw : (s w).isSome)
+    {ops : List (Dictionary.Op U)} (hvh : (Dictionary.spec U V n_max).ValidHistory s ops) :
+    probeCount (runTableFrom hm π T ops) w (π w) = probeCount T w (π w) := by
+  induction ops generalizing s T with
+  | nil => rfl
+  | cons o os ih =>
+    have hs' : (Dictionary.dom ((Dictionary.spec U V n_max).step s o).1).card ≤ n_max :=
+      Dictionary.card_dom_step_le_of_valid hs hvh.1
+    cases o with
+    | get u =>
+      exact ih hrep hs' hw hvh.2
+    | insert u v =>
+      have hO : (otherOccupiedSlots T u).card < m :=
+        hrep.card_otherOccupiedSlots_lt_of_valid hm hcap hs hvh.1
+      have hw' : ((Function.update s u (some v)) w).isSome := by
+        by_cases hwu : w = u
+        · subst hwu; simp
+        · simpa [Function.update_of_ne hwu] using hw
+      rw [runTableFrom, tableStep, ih (hrep.tableInsert hm u v hO) hs' hw' hvh.2]
+      exact hrep.probeCount_tableInsert_of_isSome hm u v hO hw
+
+/-- Prefix + suffix decomposition for `ValidHistory` and `runTableFrom`. -/
+theorem validHistory_and_runTableFrom_append {U V n_max m : ℕ} (hm : 0 < m)
+    (π : Fin U → Equiv.Perm (Fin m)) :
+    ∀ {l₁ l₂ : List (Dictionary.Op U)} {s : Dictionary.State U} (T : Table U m),
+      (Dictionary.spec U V n_max).ValidHistory s (l₁ ++ l₂) →
+      (Dictionary.spec U V n_max).ValidHistory s l₁ ∧
+      (Dictionary.spec U V n_max).ValidHistory ((Dictionary.spec U V n_max).run s l₁).1 l₂ ∧
+      runTableFrom hm π T (l₁ ++ l₂) = runTableFrom hm π (runTableFrom hm π T l₁) l₂
+  | [], _, _, _, h => ⟨trivial, h, rfl⟩
+  | o :: l₁, l₂, s, T, h => by
+    obtain ⟨h₁, h₂, hrun⟩ :=
+      validHistory_and_runTableFrom_append hm π
+        (s := ((Dictionary.spec U V n_max).step s o).1) (tableStep hm π T o).1 h.2
+    exact ⟨⟨h.1, h₁⟩, h₂, hrun⟩
+
+/-- **Pathwise insertion-cost identity from the proof of Theorem 11.8 of [CLRS2009], third edition,
+p. 276 (`probeCount_runTable_eq_firstInsert`)**:
+if `ops = ops₁ ++ (.insert u v₀ :: ops₂)` is a valid operation history where `ops₁` is the prefix
+before `u` is inserted (`((Dictionary.spec U V n_max).run (Dictionary.empty U) ops₁).1 u = none`),
+then the number of probes made when searching for `u` after the entire history `ops` equals the
+number of probes made when `u` was first inserted after `ops₁`. -/
+theorem probeCount_runTable_eq_firstInsert {U V n_max m : ℕ} (hm : 0 < m) (hcap : n_max ≤ m)
+    (π : Fin U → Equiv.Perm (Fin m))
+    {ops₁ ops₂ : List (Dictionary.Op U)} {u : Fin U} {v₀ : ℕ}
+    (hvh : (Dictionary.spec U V n_max).ValidHistory (Dictionary.empty U)
+      (ops₁ ++ (.insert u v₀ :: ops₂))) :
+    probeCount (runTable hm π (ops₁ ++ (.insert u v₀ :: ops₂))) u (π u) =
+      probeCount (runTable hm π ops₁) u (π u) := by
+  obtain ⟨hvh₁, hvh_rest, hrun_eq⟩ :=
+    validHistory_and_runTableFrom_append hm π (emptyTable U m) hvh
+  set s₁ : Dictionary.State U := ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops₁).1
+  set T₁ := runTable hm π ops₁
+  have hrep₁ : TableRep π s₁ T₁ := tableRep_runTable hm hcap π hvh₁
+  have hs₁ : (Dictionary.dom s₁).card ≤ n_max := Dictionary.card_dom_run_empty_le hvh₁
+  have hO₁ : (otherOccupiedSlots T₁ u).card < m :=
+    hrep₁.card_otherOccupiedSlots_lt_of_valid hm hcap hs₁ hvh_rest.1
+  have hrep_ins : TableRep π (Function.update s₁ u (some v₀)) (tableInsert hm π T₁ u v₀) :=
+    hrep₁.tableInsert hm u v₀ hO₁
+  have hs_ins : (Dictionary.dom (Function.update s₁ u (some v₀))).card ≤ n_max :=
+    Dictionary.card_dom_step_le_of_valid hs₁ hvh_rest.1
+  change probeCount (runTableFrom hm π (emptyTable U m) (ops₁ ++ (.insert u v₀ :: ops₂))) u (π u) =
+    probeCount T₁ u (π u)
+  rw [hrun_eq]
+  change probeCount (runTableFrom hm π (tableInsert hm π T₁ u v₀) ops₂) u (π u) =
+    probeCount T₁ u (π u)
+  rw [probeCount_runTableFrom_of_isSome hm hcap π hrep_ins hs_ins
+    (by rw [Function.update_self]; rfl) hvh_rest.2]
+  exact hrep₁.probeCount_tableInsert_self hm u v₀ hO₁
+
+/-- If key `u` is never inserted during `ops` (`∀ v, .insert u v ∉ ops`), then `runTableFrom` is
+independent of `π u`: updating `π` at `u` leaves the resulting table unchanged. -/
+theorem runTableFrom_update_eq {U m : ℕ} (hm : 0 < m) (π : Fin U → Equiv.Perm (Fin m))
+    (u : Fin U) (σ : Equiv.Perm (Fin m)) (T : Table U m) :
+    ∀ {ops : List (Dictionary.Op U)},
+      (∀ v, Dictionary.Op.insert u v ∉ ops) →
+      runTableFrom hm (Function.update π u σ) T ops = runTableFrom hm π T ops
+  | [], _ => rfl
+  | .get _ :: _, hno => by
+    dsimp only [runTableFrom, tableStep]
+    exact runTableFrom_update_eq hm π u σ T fun v hv => hno v (List.mem_cons_of_mem _ hv)
+  | .insert w v :: _, hno => by
+    have hwu : w ≠ u := by
+      rintro rfl
+      exact hno v List.mem_cons_self
+    have hins : tableInsert hm (Function.update π u σ) T w v = tableInsert hm π T w v := by
+      simp [tableInsert, Function.update_of_ne hwu]
+    dsimp only [runTableFrom, tableStep]
+    rw [hins]
+    exact runTableFrom_update_eq hm π u σ (tableInsert hm π T w v)
+      fun v' hv' => hno v' (List.mem_cons_of_mem _ hv')
+
+/-- Once `(s₀ u).isSome`, running any list of operations `l` preserves `isSome` at `u`. -/
+private theorem isSome_run_of_isSome {U V n_max : ℕ} {u : Fin U} :
+    ∀ (l : List (Dictionary.Op U)) {s₀ : Dictionary.State U},
+      (s₀ u).isSome → (((Dictionary.spec U V n_max).run s₀ l).1 u).isSome
+  | [], _, h => h
+  | .get _ :: l, _, h => isSome_run_of_isSome l h
+  | .insert w _ :: l, s₀, h => by
+    apply isSome_run_of_isSome l (s₀ := ((Dictionary.spec U V n_max).step s₀ (.insert w _)).1)
+    dsimp only [Dictionary.spec]
+    by_cases hwu : u = w
+    · subst hwu; simp
+    · simpa [Function.update_of_ne hwu] using h
+
+/-- If `((Dictionary.spec U V n_max).run s ops).1 u = none`, then no `.insert u v` appears in `ops`.
+-/
+theorem not_mem_insert_of_run_eq_none {U V n_max : ℕ} {u : Fin U} :
+    ∀ {ops : List (Dictionary.Op U)} {s : Dictionary.State U},
+      ((Dictionary.spec U V n_max).run s ops).1 u = none →
+      ∀ v, Dictionary.Op.insert u v ∉ ops
+  | [], _, _, _ => by simp
+  | o :: os, s, hnone, v => by
+    intro hmem
+    rcases List.mem_cons.mp hmem with rfl | htail
+    · have his :
+          (((Dictionary.spec U V n_max).run
+            (((Dictionary.spec U V n_max).step s (.insert u v)).1) os).1 u).isSome :=
+        isSome_run_of_isSome (V := V) (n_max := n_max) os
+          (by dsimp [Dictionary.spec]; rw [Function.update_self]; rfl)
+      have hnone' :
+          (((Dictionary.spec U V n_max).run
+            (((Dictionary.spec U V n_max).step s (.insert u v)).1) os).1 u) = none := hnone
+      rw [hnone'] at his
+      cases his
+    · exact not_mem_insert_of_run_eq_none
+        (s := ((Dictionary.spec U V n_max).step s o).1) hnone v htail
+
+/-- **Theorem 11.6 (pp. 274–275) & Corollary 11.7 (p. 276) of [CLRS2009], third edition, over
+`PMF.uniformOfFintype`**:
+for any valid operation history `ops` reaching state `s` with `(Dictionary.dom s).card < m` and any
+absent key `u` (`s u = none`), the expected number of probes made by an unsuccessful lookup `get u`
+or fresh-key insertion `insert u v` on `runTable hm π ops` over
+`π ← PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m))` is at most
+`m / (m - (Dictionary.dom s).card)` (`≤ 2` when `2 * (Dictionary.dom s).card ≤ m`). -/
+theorem expect_probeCount_of_eq_none_le {U V n_max m : ℕ} (hm : 0 < m) (hcap : n_max ≤ m)
+    {ops : List (Dictionary.Op U)}
+    (hvh : (Dictionary.spec U V n_max).ValidHistory (Dictionary.empty U) ops)
+    {u : Fin U} (hu : ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops).1 u = none)
+    (hcard :
+      (Dictionary.dom ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops).1).card < m) :
+    let s := ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops).1
+    (∑' π : Fin U → Equiv.Perm (Fin m),
+      PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m)) π *
+        (probeCount (runTable hm π ops) u (π u) : ℝ≥0∞)) ≤
+      (m : ℝ≥0∞) / ((m - (Dictionary.dom s).card : ℕ) : ℝ≥0∞) := by
+  intro s
+  have hcard_s : (Dictionary.dom s).card < m := hcard
+  have : Nonempty (Equiv.Perm (Fin m)) := ⟨1⟩
+  let μ_all := PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m))
+  let μ_one := PMF.uniformOfFintype (Equiv.Perm (Fin m))
+  have hno : ∀ v, Dictionary.Op.insert u v ∉ ops := not_mem_insert_of_run_eq_none hu
+  have hupd : μ_all = μ_one.bind (fun σ => μ_all.map (fun π => Function.update π u σ)) :=
+    (PMF.uniformOfFintype_update (ι := Fin U) (γ := Equiv.Perm (Fin m)) u).symm
+  calc
+    (∑' π, μ_all π * (probeCount (runTable hm π ops) u (π u) : ℝ≥0∞))
+      = ∑' π, (μ_one.bind (fun σ => μ_all.map (fun π₀ => Function.update π₀ u σ))) π *
+          (probeCount (runTable hm π ops) u (π u) : ℝ≥0∞) := by
+          rw [← hupd]
+    _ = ∑' σ, μ_one σ * ∑' π₀, μ_all π₀ *
+          (probeCount (runTable hm (Function.update π₀ u σ) ops) u
+            ((Function.update π₀ u σ) u) : ℝ≥0∞) := by
+          rw [PMF.tsum_bind_mul]
+          refine tsum_congr fun σ => congrArg (μ_one σ * ·) ?_
+          exact PMF.tsum_map_mul μ_all (fun π₀ => Function.update π₀ u σ)
+            (fun π => (probeCount (runTable hm π ops) u (π u) : ℝ≥0∞))
+    _ = ∑' π₀, μ_all π₀ * ∑' σ, μ_one σ *
+          (unsuccessfulProbes (occupiedSlots (runTable hm π₀ ops)) σ : ℝ≥0∞) := by
+          simp_rw [← ENNReal.tsum_mul_left]
+          rw [tsum_comm]
+          refine tsum_congr fun π₀ => tsum_congr fun σ => ?_
+          have hrep : TableRep π₀ s (runTable hm π₀ ops) := tableRep_runTable hm hcap π₀ hvh
+          have htbl : runTable hm (Function.update π₀ u σ) ops = runTable hm π₀ ops :=
+            runTableFrom_update_eq hm π₀ u σ (emptyTable U m) hno
+          rw [htbl, Function.update_self, probeCount,
+            hrep.otherOccupiedSlots_eq_occupiedSlots_of_eq_none hu]
+          ring
+    _ ≤ ∑' π₀, μ_all π₀ * ((m : ℝ≥0∞) / ((m - (Dictionary.dom s).card : ℕ) : ℝ≥0∞)) := by
+          refine tsum_le_tsum fun π₀ => ?_
+          gcongr
+          have hrep : TableRep π₀ s (runTable hm π₀ ops) := tableRep_runTable hm hcap π₀ hvh
+          have hcard_occ : (occupiedSlots (runTable hm π₀ ops)).card = (Dictionary.dom s).card :=
+            hrep.card_occupiedSlots
+          rw [← hcard_occ]
+          exact expect_unsuccessfulProbes_le (by omega)
+    _ = (m : ℝ≥0∞) / ((m - (Dictionary.dom s).card : ℕ) : ℝ≥0∞) := by
+          rw [ENNReal.tsum_mul_right, μ_all.tsum_coe, one_mul]
+
+/-- **Half-load corollary of Theorem 11.6 & Corollary 11.7 ([CLRS2009], third edition, Section 11.4,
+pp. 274–276)**:
+when `2 * n_max ≤ m`, any unsuccessful lookup or fresh-key insertion after a valid history `ops`
+makes at most `2` probes in expectation over
+`π ← PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m))`. -/
+theorem expect_probeCount_of_eq_none_le_two {U V n_max m : ℕ} (hm : 0 < m) (h2cap : 2 * n_max ≤ m)
+    {ops : List (Dictionary.Op U)}
+    (hvh : (Dictionary.spec U V n_max).ValidHistory (Dictionary.empty U) ops)
+    {u : Fin U} (hu : ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops).1 u = none) :
+    (∑' π : Fin U → Equiv.Perm (Fin m),
+      PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m)) π *
+        (probeCount (runTable hm π ops) u (π u) : ℝ≥0∞)) ≤ 2 := by
+  have hdom_le :
+      (Dictionary.dom ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops).1).card ≤ n_max :=
+    Dictionary.card_dom_run_empty_le hvh
+  refine (expect_probeCount_of_eq_none_le hm (by omega) hvh hu (by omega)).trans ?_
+  exact div_sub_le_two hm (by omega)
+
+/-- **Per-key successful-search bound from the proof of Theorem 11.8 of [CLRS2009], third edition,
+p. 276**:
+if `ops = ops₁ ++ (.insert u v₀ :: ops₂)` is a valid operation history where `ops₁` is the prefix
+before `u` is first inserted (`s₁ u = none`), then the expected number of probes made when
+searching for the fixed key `u` after `ops` equals the expected number of probes when `u` was first
+inserted after `ops₁`, and is at most `m / (m - (Dictionary.dom s₁).card)` (this formalizes the
+per-key intermediate bound `1 / (1 - i / m) = m / (m - i)` for `i = (Dictionary.dom s₁).card` from
+the proof of Theorem 11.8; the uniform-key-averaged `(1 / α) ln(1 / (1 - α))` endpoint of Theorem
+11.8 is not formalized here). -/
+theorem expect_probeCount_of_mem_dom_le {U V n_max m : ℕ} (hm : 0 < m) (hcap : n_max ≤ m)
+    {ops₁ ops₂ : List (Dictionary.Op U)} {u : Fin U} {v₀ : ℕ}
+    (hvh : (Dictionary.spec U V n_max).ValidHistory (Dictionary.empty U)
+      (ops₁ ++ (.insert u v₀ :: ops₂)))
+    (hu₁ : ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops₁).1 u = none)
+    (hcard₁ :
+      (Dictionary.dom ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops₁).1).card < m) :
+    let s₁ := ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops₁).1
+    (∑' π : Fin U → Equiv.Perm (Fin m),
+      PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m)) π *
+        (probeCount (runTable hm π (ops₁ ++ (.insert u v₀ :: ops₂))) u (π u) : ℝ≥0∞)) ≤
+      (m : ℝ≥0∞) / ((m - (Dictionary.dom s₁).card : ℕ) : ℝ≥0∞) := by
+  intro s₁
+  have hvh₁ : (Dictionary.spec U V n_max).ValidHistory (Dictionary.empty U) ops₁ :=
+    (validHistory_and_runTableFrom_append hm (fun _ => 1) (emptyTable U m) hvh).1
+  have hcongr : ∀ π : Fin U → Equiv.Perm (Fin m),
+      probeCount (runTable hm π (ops₁ ++ (.insert u v₀ :: ops₂))) u (π u) =
+        probeCount (runTable hm π ops₁) u (π u) :=
+    fun π => probeCount_runTable_eq_firstInsert hm hcap π hvh
+  simp_rw [hcongr]
+  exact expect_probeCount_of_eq_none_le hm hcap hvh₁ hu₁ hcard₁
+
+/-- **Half-load per-key successful-search bound from the proof of Theorem 11.8 ([CLRS2009], third
+edition, Section 11.4, p. 276)**:
+when `2 * n_max ≤ m`, any successful lookup of a fixed present key `u` (first inserted after prefix
+`ops₁`) makes at most `2` probes in expectation over
+`π ← PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m))`. -/
+theorem expect_probeCount_of_mem_dom_le_two {U V n_max m : ℕ} (hm : 0 < m) (h2cap : 2 * n_max ≤ m)
+    {ops₁ ops₂ : List (Dictionary.Op U)} {u : Fin U} {v₀ : ℕ}
+    (hvh : (Dictionary.spec U V n_max).ValidHistory (Dictionary.empty U)
+      (ops₁ ++ (.insert u v₀ :: ops₂)))
+    (hu₁ : ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops₁).1 u = none) :
+    (∑' π : Fin U → Equiv.Perm (Fin m),
+      PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m)) π *
+        (probeCount (runTable hm π (ops₁ ++ (.insert u v₀ :: ops₂))) u (π u) : ℝ≥0∞)) ≤ 2 := by
+  have hvh₁ : (Dictionary.spec U V n_max).ValidHistory (Dictionary.empty U) ops₁ :=
+    (validHistory_and_runTableFrom_append hm (fun _ => 1) (emptyTable U m) hvh).1
+  have hdom₁_le :
+      (Dictionary.dom ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops₁).1).card ≤ n_max :=
+    Dictionary.card_dom_run_empty_le hvh₁
+  refine (expect_probeCount_of_mem_dom_le hm (by omega) hvh hu₁ (by omega)).trans ?_
+  exact div_sub_le_two hm (by omega)
+
+/-! ## Section 4: Lazy Random-Oracle Equivalence (`RandomOracle.uniform_interpret_eq_lazy`) -/
+
+/-- Any adaptive oracle program querying per-key permutations `u ↦ π u : Equiv.Perm (Fin m)` has the
+exact same output distribution whether the permutation table
+`π ← PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m))` is sampled eagerly upfront or lazily on
+first query via `Cslib.RandomOracle.answer`. -/
+theorem uniform_interpret_eq_lazy_perm {U m : ℕ} {α : Type}
+    (program : OracleComp (fun _ : Fin U => Equiv.Perm (Fin m)) α) :
+    (do
+      let π ← PMF.uniformOfFintype (Fin U → Equiv.Perm (Fin m))
+      OracleComp.interpret (fun u => PMF.pure (π u)) program) =
+        ((OracleComp.interpret
+          (Cslib.RandomOracle.answer (fun _ : Fin U => PMF.uniformOfFintype (Equiv.Perm (Fin m))))
+          program).run (fun _ => none)).map Prod.fst :=
+  Cslib.RandomOracle.uniform_interpret_eq_lazy program
+
+end Cslib.Algorithms.Lean.UniformProbing
diff --git a/Complexity/Algorithms/WordRAM/Dictionary/UniformProbing.lean b/Complexity/Algorithms/WordRAM/Dictionary/UniformProbing.lean
new file mode 100644
index 000000000..7a7942fd2
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/Dictionary/UniformProbing.lean
@@ -0,0 +1,2209 @@
+/-
+Copyright (c) 2026 Renfei Zhou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Renfei Zhou
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.Lean.Dictionary
+public import Complexity.Algorithms.Lean.UniformProbing
+public import Complexity.Algorithms.WordRAM.Hashing.MultiplyShift
+public import Complexity.Algorithms.WordRAM.Hashing.Tabulation
+public import Complexity.Computability.WordRAM.ExactNotation
+public import Complexity.Computability.WordRAM.Randomized.Subroutine
+import Complexity.Probability.PMF.Expect
+
+/-!
+# Self-Contained Open-Addressed Permutation-Probing Dictionary on the Word-RAM
+
+This file implements a self-contained open-addressed permutation-probing dictionary realizing
+`Cslib.Algorithms.Lean.Dictionary.spec U V n_max` (`get` and `insert` up to `n_max` distinct keys)
+on the Word-RAM (`Cslib.WordRAM.Basis.exact` and `Cslib.WordRAM.Basis.standard`), following the
+double-hashing construction of
+[Cormen, Leiserson, Rivest, and Stein, *Introduction to Algorithms*, third edition (MIT Press,
+2009), Section 11.4, "Double hashing", pp. 272–274][CLRS2009] with simple tabulation due to
+Zobrist (1970) and Pătraşcu and Thorup (2012).
+
+## Design and reuse of `Cslib.Algorithms.Lean.UniformProbing`
+
+In the ideal uniform-probing model (`Complexity/Algorithms/Lean/UniformProbing.lean`), each key
+`u : Fin U` is assigned an independent random permutation `π u : Equiv.Perm (Fin m)`. Storing an
+explicit table of `U` permutations requires `Ω(U)` words when `U = poly(n_max) ≫ n_max`.
+
+To achieve a self-contained `O(n_max)`-word data structure (when `U = poly(n_max)`), we construct
+for each key `u : Fin U` a full-cycle affine permutation of `m = 2 ^ M` slots
+(`M = Nat.clog 2 (max (4 * n_max) 4)`):
+`probePerm θ u i = (h₁(u) + i * h₂(u)) mod 2 ^ M`, where:
+* `h₁(u) ∈ Fin (2 ^ M)` is a 2-universal multiply-shift hash
+  (`Cslib.Algorithms.WordRAM.Hashing.MultiplyShift`);
+* `h₂(u) ∈ Fin (2 ^ M)` is an odd stride computed by `d`-character simple tabulation
+  (`Cslib.Algorithms.WordRAM.Hashing.Tabulation.TabulatedOddStride`, with character bit-width
+  `b = max 1 (⌊log₂ (max n_max 2)⌋ / 2)` and `d = numChars U n_max`), following Zobrist (1970)
+  and Pătraşcu and Thorup (2012).
+
+Because `h₂(u)` is always odd and therefore coprime to `2 ^ M`, `probePerm θ u` is a bijection on
+`Fin (2 ^ M)` for **every** seed `θ` and key `u` (`TabulatedOddStride.bijective_probeSeq`). We
+therefore instantiate `Cslib.Algorithms.Lean.UniformProbing.TableRep (probePerm θ)` directly on the
+concrete Word-RAM slot arrays. Note that `TabulatedOddStride` proves full-cycle permutation
+bijectivity (`bijective_probeSeq`) rather than full uniform-permutation independence: accordingly,
+`subroutineDS` certifies the concrete deterministic full-cycle body bound
+`charge = opSteps U n_max = 13 * numBuckets n_max + 8 * numChars U n_max + 49`
+(`O(n_max + log U / log n_max)`), while `expect_opPathSteps_le_of_probeBound` and
+`expect_idealProbeSteps_le` connect the exact probe-path body cost
+`13 * probeCount + 8 * numChars U n_max + 49` to `≤ 8 * numChars U n_max + 75` expected
+instructions under an ideal uniform permutation law
+(`Complexity/Algorithms/Lean/UniformProbing.lean`, Theorem 11.6, Corollary 11.7, and the per-key
+bound from the proof of Theorem 11.8 of [CLRS2009], third edition, pp. 274–276).
+
+## Model, specialization, and cost scope
+
+* For fixed universe `U` and capacity bound `n_max` and an admissible external machine word width
+  `w` (`2 * hashBits U n_max ≤ w`, `Fits w (base + space U n_max)`, `Fits w V`),
+  `subroutineCode U n_max` uses precomputed configuration literals (`bucketBits`, `hashBits`,
+  `charBits`, `numChars`, masks, and layout offsets baked as instruction literals, with
+  `initParams = Fin.elim0`).
+* Expected and amortized bounds in `seq_expected_amortized` charge initialization (`initFresh`) and
+  subroutine operation bodies (`C.ExecSteps`) across an operation history `ops` fixed independently
+  of the sampled seed (oblivious adversary), excluding caller argument delivery, caller
+  control/dispatch loops, and code/configuration construction.
+* `Dictionary.spec U V n_max` is insert-only (`get` and `insert` up to `n_max` distinct keys), so
+  open-addressed slots require no tombstones.
+
+## Main definitions
+
+* `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.bucketBits`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.numBuckets`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.hashBits`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.charBits`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.numChars`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.space`: table dimension parameters and memory
+  footprint.
+* `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.Seed`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.seedLaw`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.primaryHash`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.strideHash`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.probePerm`: seed space, uniform seed law,
+  multiply-shift primary hash, tabulated odd stride, and full-cycle probe permutation.
+* `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.extractSlots`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.Rep`: slot-array extractor and Word-RAM
+  representation invariant.
+* `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.allocSpan`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.initSetup`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.opCode`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.subroutineCode`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.subroutineDS`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.subroutineDSStandard`: structured Word-RAM
+  programs and `Randomized.SubroutineDS` certificates over `Basis.exact` and `Basis.standard`.
+
+## Main results
+
+* `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.setup_exec_spec`: randomized seed and table
+  initialization in `setupSteps U n_max = 5 * (numChars U n_max * 2 ^ charBits n_max) + 25`
+  expected instructions.
+* `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.opCode_execWithin`: every `get` or `insert`
+  operation on key `u` executes in at most
+  `opPathSteps U n_max θ T u = 13 * probeCount T u (probePerm θ u) + 8 * numChars U n_max + 49 ≤
+  opSteps U n_max` instructions for every seed `θ`.
+* `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.seq_expected_amortized`: end-to-end expected
+  instruction bound across any admissible sequence `ops : List (Dictionary.Op U)`.
+* `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.isUniversalHash_primaryHash`:
+  `(2 / numBuckets n_max)`-universality of `primaryHash` under `seedLaw U n_max`.
+* `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.expect_opPathSteps_le_of_probeBound`,
+  `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing.expect_idealProbeSteps_le`: parametric
+  expected-step transfer (`13 * B + 8 * numChars U n_max + 49`) from any expected-probe bound `B`,
+  yielding `≤ 8 * numChars U n_max + 75` under the ideal uniform permutation law (`B = 2`).
+
+## References
+
+* [T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein,
+  *Introduction to Algorithms*, third edition (MIT Press, 2009), Section 11.4,
+  pp. 270–277][CLRS2009]
+* [M. Mitzenmacher and E. Upfal, *Probability and Computing*][MitzenmacherUpfal2017]
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.Dictionary.UniformProbing
+
+open Cslib.Algorithms.Lean
+open Cslib.Algorithms.Lean.UniformProbing
+open Cslib.Algorithms.WordRAM.Hashing
+open Cslib.Algorithms.WordRAM.Hashing.Tabulation
+open Cslib.Probability
+open Cslib.WordRAM
+open Cslib.WordRAM.Randomized
+open scoped BigOperators ENNReal
+
+/-! ## Section 1: Table Parameters, Seed Space, and Full-Cycle Probe Permutations -/
+
+/-- Log₂ of the power-of-2 table size: `M = ⌈log₂ (max (4 * n_max) 4)⌉ ≥ 2`. -/
+def bucketBits (n_max : ℕ) : ℕ :=
+  Nat.clog 2 (max (4 * n_max) 4)
+
+/-- Power-of-2 number of open-addressed table slots `m = 2 ^ bucketBits n_max ≥ max (4 * n_max) 4`.
+-/
+def numBuckets (n_max : ℕ) : ℕ :=
+  2 ^ bucketBits n_max
+
+/-- Bit-width `w₀ = max (bucketBits n_max) ⌈log₂ (max U 2)⌉` for the multiply-shift primary hash.
+-/
+def hashBits (U n_max : ℕ) : ℕ :=
+  max (bucketBits n_max) (Nat.clog 2 (max U 2))
+
+/-- Character bit-width `b = max 1 (⌊log₂ (max n_max 2)⌋ / 2)` for the tabulated odd stride. -/
+def charBits (n_max : ℕ) : ℕ :=
+  TabulatedOddStride.charBits n_max
+
+/-- Number of base-`2 ^ b` characters `d = max 1 ⌈⌈log₂ (max U 2)⌉ / b⌉` used by the tabulated odd
+stride. When `U = poly(n_max)`, `numChars U n_max = O(1)`. -/
+def numChars (U n_max : ℕ) : ℕ :=
+  max 1 ((Nat.clog 2 (max U 2) + charBits n_max - 1) / charBits n_max)
+
+/-- Memory footprint `4 + d * 2 ^ b` words of the `TabulatedOddStride` table at `[base, ...)`. -/
+def tabSpace (U n_max : ℕ) : ℕ :=
+  TabulatedOddStride.space n_max (numChars U n_max)
+
+/-- Offset `tabSpace U n_max + 1` of the open-addressed slot arrays relative to `base` (after the
+`TabulatedOddStride` table at `[base, base + tabSpace U n_max)` and the 1-word multiply-shift seed
+at `base + tabSpace U n_max`). -/
+def slotOffset (U n_max : ℕ) : ℕ :=
+  tabSpace U n_max + 1
+
+/-- Total memory footprint `slotOffset U n_max + 3 * numBuckets n_max` words in
+`[base, base + space U n_max)`. -/
+def space (U n_max : ℕ) : ℕ :=
+  slotOffset U n_max + 3 * numBuckets n_max
+
+theorem two_le_bucketBits (n_max : ℕ) : 2 ≤ bucketBits n_max := by
+  dsimp only [bucketBits]
+  calc
+    2 = Nat.clog 2 (2 ^ 2) := (Nat.clog_pow 2 2 (by decide)).symm
+    _ ≤ Nat.clog 2 (max (4 * n_max) 4) := Nat.clog_mono_right 2 (by omega)
+
+theorem bucketBits_pos (n_max : ℕ) : 0 < bucketBits n_max :=
+  lt_of_lt_of_le (by decide : 0 < 2) (two_le_bucketBits n_max)
+
+theorem max_four_mul_le_numBuckets (n_max : ℕ) :
+    max (4 * n_max) 4 ≤ numBuckets n_max :=
+  Nat.le_pow_clog (by decide) (max (4 * n_max) 4)
+
+theorem four_le_numBuckets (n_max : ℕ) : 4 ≤ numBuckets n_max :=
+  le_trans (Nat.le_max_right (4 * n_max) 4) (max_four_mul_le_numBuckets n_max)
+
+theorem four_mul_le_numBuckets (n_max : ℕ) : 4 * n_max ≤ numBuckets n_max :=
+  le_trans (Nat.le_max_left (4 * n_max) 4) (max_four_mul_le_numBuckets n_max)
+
+theorem two_mul_le_numBuckets (n_max : ℕ) : 2 * n_max ≤ numBuckets n_max := by
+  have := four_mul_le_numBuckets n_max
+  omega
+
+theorem lt_numBuckets (n_max : ℕ) : n_max < numBuckets n_max := by
+  have h4 := four_le_numBuckets n_max
+  have h4n := four_mul_le_numBuckets n_max
+  omega
+
+theorem numBuckets_pos (n_max : ℕ) : 0 < numBuckets n_max :=
+  lt_of_lt_of_le (by decide : 0 < 4) (four_le_numBuckets n_max)
+
+instance instNonemptyFinNumBuckets (n_max : ℕ) : Nonempty (Fin (numBuckets n_max)) :=
+  ⟨⟨0, numBuckets_pos n_max⟩⟩
+
+theorem bucketBits_le_hashBits (U n_max : ℕ) : bucketBits n_max ≤ hashBits U n_max :=
+  Nat.le_max_left _ _
+
+theorem hashBits_pos (U n_max : ℕ) : 0 < hashBits U n_max :=
+  lt_of_lt_of_le (bucketBits_pos n_max) (bucketBits_le_hashBits U n_max)
+
+theorem one_le_numChars (U n_max : ℕ) : 1 ≤ numChars U n_max :=
+  Nat.le_max_left 1 _
+
+theorem lt_two_pow_hashBits {U : ℕ} (n_max : ℕ) (u : Fin U) :
+    u.val < 2 ^ hashBits U n_max := by
+  have h1 : u.val < max U 2 := lt_of_lt_of_le u.isLt (Nat.le_max_left U 2)
+  have h2 : max U 2 ≤ 2 ^ Nat.clog 2 (max U 2) := Nat.le_pow_clog (by decide) (max U 2)
+  have h3 : 2 ^ Nat.clog 2 (max U 2) ≤ 2 ^ hashBits U n_max :=
+    Nat.pow_le_pow_right (by decide) (Nat.le_max_right _ _)
+  exact lt_of_lt_of_le h1 (le_trans h2 h3)
+
+/-- Embed key `u : Fin U` into `Fin (2 ^ hashBits U n_max)`. -/
+def encodeKey {U : ℕ} (n_max : ℕ) (u : Fin U) : Fin (2 ^ hashBits U n_max) :=
+  ⟨u.val, lt_two_pow_hashBits n_max u⟩
+
+@[simp]
+theorem val_encodeKey {U : ℕ} (n_max : ℕ) (u : Fin U) :
+    (encodeKey n_max u).val = u.val := rfl
+
+theorem encodeKey_injective {U : ℕ} (n_max : ℕ) :
+    Function.Injective (encodeKey (U := U) n_max) := by
+  intro u₁ u₂ h
+  exact Fin.ext (congrArg (fun x : Fin (2 ^ hashBits U n_max) => x.val) h)
+
+/-- Combined random seed `(b_ms, T)` consisting of the multiply-shift seed
+`b_ms : Fin (2 ^ (hashBits U n_max - 1))` and the character table
+`T : Fin (numChars U n_max * 2 ^ charBits n_max) → Fin (numBuckets n_max)`. -/
+abbrev Seed (U n_max : ℕ) : Type :=
+  Fin (2 ^ (hashBits U n_max - 1)) ×
+    (Fin (numChars U n_max * 2 ^ charBits n_max) → Fin (numBuckets n_max))
+
+instance instNonemptySeed (U n_max : ℕ) : Nonempty (Seed U n_max) :=
+  ⟨(⟨0, Nat.two_pow_pos _⟩, fun _ => ⟨0, numBuckets_pos n_max⟩)⟩
+
+/-- Uniform reference distribution over `Seed U n_max`. -/
+noncomputable def seedLaw (U n_max : ℕ) : PMF (Seed U n_max) :=
+  PMF.uniformOfFintype (Seed U n_max)
+
+theorem multiplyShift_lt_numBuckets {U n_max : ℕ}
+    (b : Fin (2 ^ (hashBits U n_max - 1))) (x : Fin (2 ^ hashBits U n_max)) :
+    multiplyShift (hashBits U n_max) (bucketBits n_max) b x < numBuckets n_max := by
+  dsimp only [multiplyShift, numBuckets]
+  refine Nat.div_lt_of_lt_mul ?_
+  rw [← pow_add, Nat.sub_add_cancel (bucketBits_le_hashBits U n_max)]
+  exact Nat.mod_lt _ (Nat.two_pow_pos _)
+
+/-- Multiply-shift primary slot `h₁(u) ∈ Fin (numBuckets n_max)`. -/
+def primaryHash {U n_max : ℕ} (θ : Seed U n_max) (u : Fin U) : Fin (numBuckets n_max) :=
+  ⟨multiplyShift (hashBits U n_max) (bucketBits n_max) θ.1 (encodeKey n_max u),
+    multiplyShift_lt_numBuckets θ.1 (encodeKey n_max u)⟩
+
+@[simp]
+theorem val_primaryHash {U n_max : ℕ} (θ : Seed U n_max) (u : Fin U) :
+    (primaryHash θ u).val =
+      multiplyShift (hashBits U n_max) (bucketBits n_max) θ.1 (encodeKey n_max u) :=
+  rfl
+
+/-- Raw simple-tabulation character XOR sum `simpleTab b d M θ.2 u.val : Fin (numBuckets n_max)`. -/
+def rawTabHash {U n_max : ℕ} (θ : Seed U n_max) (u : Fin U) : Fin (numBuckets n_max) :=
+  TabulatedOddStride.simpleTab (charBits n_max) (numChars U n_max) (bucketBits n_max) θ.2 u.val
+
+/-- Tabulated odd stride `h₂(u) = (2 * rawTabHash θ u + 1) mod 2 ^ M ∈ Fin (numBuckets n_max)`. -/
+def strideHash {U n_max : ℕ} (θ : Seed U n_max) (u : Fin U) : Fin (numBuckets n_max) :=
+  TabulatedOddStride.tabulatedOddStride (charBits n_max) (numChars U n_max) (bucketBits n_max)
+    θ.2 u.val
+
+/-- Full-cycle double-hashing probe permutation
+`probePerm θ u : Equiv.Perm (Fin (numBuckets n_max))` sending probe index `i` to
+`(h₁(u) + i * h₂(u)) mod 2 ^ M`, certified bijective by `TabulatedOddStride.bijective_probeSeq`. -/
+noncomputable def probePerm {U n_max : ℕ} (θ : Seed U n_max) (u : Fin U) :
+    Equiv.Perm (Fin (numBuckets n_max)) :=
+  Equiv.ofBijective
+    (TabulatedOddStride.probeSeq (bucketBits n_max) (primaryHash θ u).val (rawTabHash θ u).val)
+    (TabulatedOddStride.bijective_probeSeq (bucketBits n_max)
+      (primaryHash θ u).val (rawTabHash θ u).val)
+
+theorem probePerm_apply {U n_max : ℕ} (θ : Seed U n_max) (u : Fin U)
+    (i : Fin (numBuckets n_max)) :
+    probePerm θ u i =
+      TabulatedOddStride.probeSeq (bucketBits n_max) (primaryHash θ u).val (rawTabHash θ u).val i :=
+  rfl
+
+@[simp]
+theorem val_probePerm {U n_max : ℕ} (θ : Seed U n_max) (u : Fin U)
+    (i : Fin (numBuckets n_max)) :
+    (probePerm θ u i).val =
+      ((primaryHash θ u).val + i.val * (strideHash θ u).val) % numBuckets n_max :=
+  rfl
+
+@[simp]
+theorem probePerm_zero {U n_max : ℕ} (θ : Seed U n_max) (u : Fin U) :
+    probePerm θ u ⟨0, numBuckets_pos n_max⟩ = primaryHash θ u := by
+  apply Fin.ext
+  rw [val_probePerm]
+  simpa using Nat.mod_eq_of_lt (primaryHash θ u).isLt
+
+/-- One step of the Word-RAM probe loop `(slot + stride) &&& (2 ^ M - 1)` advances from
+`probePerm θ u ⟨i, _⟩` to `probePerm θ u ⟨i + 1, _⟩`. -/
+theorem val_probePerm_succ {U n_max : ℕ} (θ : Seed U n_max) (u : Fin U)
+    {i : ℕ} (hi : i + 1 < numBuckets n_max) :
+    (probePerm θ u ⟨i + 1, hi⟩).val =
+      ((probePerm θ u ⟨i, by omega⟩).val + (strideHash θ u).val) &&&
+        (numBuckets n_max - 1) := by
+  change (probePerm θ u ⟨i + 1, hi⟩).val =
+    ((probePerm θ u ⟨i, by omega⟩).val + (strideHash θ u).val) &&&
+      (2 ^ bucketBits n_max - 1)
+  rw [Nat.and_two_pow_sub_one_eq_mod, val_probePerm, val_probePerm]
+  simp [numBuckets, Nat.add_mul, one_mul, Nat.add_assoc]
+
+/-! ## Section 2: Concrete Slot Extraction and Representation Invariant -/
+
+/-- Well-formedness of the flat open-addressed slot arrays at
+`[base + slotOffset U n_max, base + slotOffset U n_max + 3 * numBuckets n_max)`:
+each `used[j]` word is `0` or `1`, and whenever `used[j] = 1`, `key[j] < U`. -/
+def SlotArrayWF (base U n_max : ℕ) (mem : ℕ → ℕ) : Prop :=
+  let sBase := base + slotOffset U n_max
+  let m := numBuckets n_max
+  ∀ j : Fin m,
+    (mem (sBase + j.val) = 0 ∨ mem (sBase + j.val) = 1) ∧
+    (mem (sBase + j.val) = 1 → mem (sBase + m + j.val) < U)
+
+/-- Extract the abstract open-addressed table `UniformProbing.Table U (numBuckets n_max)` from
+Word-RAM memory `mem`. -/
+def extractSlots (base U n_max : ℕ) (mem : ℕ → ℕ) :
+    UniformProbing.Table U (numBuckets n_max) :=
+  let sBase := base + slotOffset U n_max
+  let m := numBuckets n_max
+  fun j =>
+    if mem (sBase + j.val) = 0 then none
+    else if h : mem (sBase + m + j.val) < U then
+      some (⟨mem (sBase + m + j.val), h⟩, mem (sBase + 2 * m + j.val))
+    else none
+
+theorem extractSlots_eq_none_iff {base U n_max : ℕ} {mem : ℕ → ℕ}
+    (hwf : SlotArrayWF base U n_max mem) (j : Fin (numBuckets n_max)) :
+    extractSlots base U n_max mem j = none ↔
+      mem (base + slotOffset U n_max + j.val) = 0 := by
+  rcases hwf j with ⟨h0 | h1, hkey⟩
+  · simp [extractSlots, h0]
+  · have hlt : mem (base + slotOffset U n_max + numBuckets n_max + j.val) < U := hkey h1
+    simp [extractSlots, h1, hlt]
+
+theorem extractSlots_eq_some_iff {base U n_max : ℕ} {mem : ℕ → ℕ}
+    (hwf : SlotArrayWF base U n_max mem) (j : Fin (numBuckets n_max))
+    (u : Fin U) (v : ℕ) :
+    extractSlots base U n_max mem j = some (u, v) ↔
+      mem (base + slotOffset U n_max + j.val) = 1 ∧
+      mem (base + slotOffset U n_max + numBuckets n_max + j.val) = u.val ∧
+      mem (base + slotOffset U n_max + 2 * numBuckets n_max + j.val) = v := by
+  rcases hwf j with ⟨h0 | h1, hkey⟩
+  · simp [extractSlots, h0]
+  · have hlt : mem (base + slotOffset U n_max + numBuckets n_max + j.val) < U := hkey h1
+    simp [extractSlots, h1, hlt, Fin.ext_iff]
+
+theorem mem_otherOccupiedSlots_extractSlots_iff {base U n_max : ℕ} {mem : ℕ → ℕ}
+    (hwf : SlotArrayWF base U n_max mem) (u : Fin U) (j : Fin (numBuckets n_max)) :
+    j ∈ otherOccupiedSlots (extractSlots base U n_max mem) u ↔
+      mem (base + slotOffset U n_max + j.val) = 1 ∧
+      mem (base + slotOffset U n_max + numBuckets n_max + j.val) ≠ u.val := by
+  rw [mem_otherOccupiedSlots_iff]
+  constructor
+  · rintro ⟨u', v', hsome, hne⟩
+    rw [extractSlots_eq_some_iff hwf] at hsome
+    refine ⟨hsome.1, ?_⟩
+    rw [hsome.2.1]
+    exact fun h => hne (Fin.ext h)
+  · rintro ⟨h1, hne⟩
+    have hlt : mem (base + slotOffset U n_max + numBuckets n_max + j.val) < U :=
+      (hwf j).2 h1
+    refine ⟨⟨mem (base + slotOffset U n_max + numBuckets n_max + j.val), hlt⟩,
+      mem (base + slotOffset U n_max + 2 * numBuckets n_max + j.val), ?_, ?_⟩
+    · rw [extractSlots_eq_some_iff hwf]
+      exact ⟨h1, rfl, rfl⟩
+    · intro heq
+      exact hne (congrArg Fin.val heq)
+
+/-- Coupled representation invariant `Rep w base U V n_max θ s x` on `Data 12`:
+* `x.Bounded w`;
+* `x.regs 0 = base`;
+* `TabulatedOddStride.Rep` holds for `θ.2` at `[base, base + tabSpace U n_max)`;
+* `x.mem (base + tabSpace U n_max) = θ.1.val` holds the multiply-shift seed;
+* `SlotArrayWF base U n_max x.mem` and `UniformProbing.TableRep (probePerm θ) s (extractSlots ...)`
+  hold on the slot arrays;
+* `(Dictionary.dom s).card ≤ n_max` and `Dictionary.ValuesBounded V s`. -/
+structure Rep (w base U V n_max : ℕ) (θ : Seed U n_max) (s : Dictionary.State U)
+    (x : Data 12) : Prop where
+  bounded : x.Bounded w
+  regs_base : x.regs 0 = base
+  tab_rep : TabulatedOddStride.Rep base (charBits n_max) (numChars U n_max)
+    (bucketBits n_max) θ.2 x.mem
+  ms_seed : x.mem (base + tabSpace U n_max) = θ.1.val
+  slot_wf : SlotArrayWF base U n_max x.mem
+  table_rep : UniformProbing.TableRep (probePerm θ) s (extractSlots base U n_max x.mem)
+  dom_le : (Dictionary.dom s).card ≤ n_max
+  vals_bounded : Dictionary.ValuesBounded V s
+
+theorem Rep.unique {w base U V n_max : ℕ} {θ : Seed U n_max}
+    {s₁ s₂ : Dictionary.State U} {x : Data 12}
+    (h₁ : Rep w base U V n_max θ s₁ x) (h₂ : Rep w base U V n_max θ s₂ x) :
+    s₁ = s₂ := by
+  funext u
+  cases hs₁ : s₁ u with
+  | none =>
+    cases hs₂ : s₂ u with
+    | none => rfl
+    | some v₂ =>
+      obtain ⟨hlt, hT⟩ := h₂.table_rep.key_spec u v₂ hs₂
+      have hs₁' := (h₁.table_rep.slot_spec _ u v₂ hT).1
+      rw [hs₁] at hs₁'
+      cases hs₁'
+  | some v₁ =>
+    obtain ⟨hlt, hT⟩ := h₁.table_rep.key_spec u v₁ hs₁
+    exact (h₂.table_rep.slot_spec _ u v₁ hT).1.symm
+
+theorem mem_footprint_of_lt_space {base U n_max a : ℕ}
+    (hlo : base ≤ a) (hhi : a < base + space U n_max) :
+    a ∈ (Block.mk base (space U n_max)).footprint := by
+  rw [Block.mem_footprint]
+  exact ⟨hlo, hhi⟩
+
+theorem SlotArrayWF.congr_mem {base U n_max : ℕ} {mem mem' : ℕ → ℕ}
+    (hmem : ∀ a ∈ (Block.mk base (space U n_max)).footprint, mem' a = mem a)
+    (hwf : SlotArrayWF base U n_max mem) :
+    SlotArrayWF base U n_max mem' := by
+  intro j
+  have hj := j.isLt
+  have hsp : space U n_max = slotOffset U n_max + 3 * numBuckets n_max := rfl
+  have h0 : mem' (base + slotOffset U n_max + j.val) =
+      mem (base + slotOffset U n_max + j.val) :=
+    hmem _ (mem_footprint_of_lt_space (by omega) (by omega))
+  have h1 : mem' (base + slotOffset U n_max + numBuckets n_max + j.val) =
+      mem (base + slotOffset U n_max + numBuckets n_max + j.val) :=
+    hmem _ (mem_footprint_of_lt_space (by omega) (by omega))
+  dsimp only [SlotArrayWF] at hwf ⊢
+  rw [h0, h1]
+  exact hwf j
+
+theorem extractSlots_congr_mem {base U n_max : ℕ} {mem mem' : ℕ → ℕ}
+    (hmem : ∀ a ∈ (Block.mk base (space U n_max)).footprint, mem' a = mem a) :
+    extractSlots base U n_max mem' = extractSlots base U n_max mem := by
+  funext j
+  have hj := j.isLt
+  have hsp : space U n_max = slotOffset U n_max + 3 * numBuckets n_max := rfl
+  have h0 : mem' (base + slotOffset U n_max + j.val) =
+      mem (base + slotOffset U n_max + j.val) :=
+    hmem _ (mem_footprint_of_lt_space (by omega) (by omega))
+  have h1 : mem' (base + slotOffset U n_max + numBuckets n_max + j.val) =
+      mem (base + slotOffset U n_max + numBuckets n_max + j.val) :=
+    hmem _ (mem_footprint_of_lt_space (by omega) (by omega))
+  have h2 : mem' (base + slotOffset U n_max + 2 * numBuckets n_max + j.val) =
+      mem (base + slotOffset U n_max + 2 * numBuckets n_max + j.val) :=
+    hmem _ (mem_footprint_of_lt_space (by omega) (by omega))
+  dsimp only [extractSlots]
+  rw [h0, h1, h2]
+
+theorem Rep.congr {w base U V n_max : ℕ} {θ : Seed U n_max} {s : Dictionary.State U}
+    {x x' : Data 12}
+    (hbdd : x'.Bounded w) (hbase : x'.regs 0 = x.regs 0)
+    (hmem : ∀ a ∈ (Block.mk base (space U n_max)).footprint, x'.mem a = x.mem a)
+    (hrep : Rep w base U V n_max θ s x) :
+    Rep w base U V n_max θ s x' := by
+  have hsp : space U n_max =
+      (4 + numChars U n_max * 2 ^ charBits n_max) + 1 + 3 * numBuckets n_max := rfl
+  have htab_eq : tabSpace U n_max = 4 + numChars U n_max * 2 ^ charBits n_max := rfl
+  have htab : TabulatedOddStride.Rep base (charBits n_max) (numChars U n_max)
+      (bucketBits n_max) θ.2 x'.mem := by
+    rcases hrep.tab_rep with ⟨hm0, hm1, hm2, hm3, hmt⟩
+    refine ⟨?_, ?_, ?_, ?_, fun i => ?_⟩
+    · rw [hmem base (mem_footprint_of_lt_space (by omega) (by omega)), hm0]
+    · rw [hmem (base + 1) (mem_footprint_of_lt_space (by omega) (by omega)), hm1]
+    · rw [hmem (base + 2) (mem_footprint_of_lt_space (by omega) (by omega)), hm2]
+    · rw [hmem (base + 3) (mem_footprint_of_lt_space (by omega) (by omega)), hm3]
+    · have hi := i.isLt
+      rw [hmem (base + 4 + i.val) (mem_footprint_of_lt_space (by omega) (by omega)), hmt i]
+  have hms : x'.mem (base + tabSpace U n_max) = θ.1.val := by
+    rw [hmem (base + tabSpace U n_max) (mem_footprint_of_lt_space (by omega) (by omega)),
+      hrep.ms_seed]
+  refine ⟨hbdd, hbase.trans hrep.regs_base, htab, hms,
+    hrep.slot_wf.congr_mem hmem, ?_, hrep.dom_le, hrep.vals_bounded⟩
+  rw [extractSlots_congr_mem hmem]
+  exact hrep.table_rep
+
+theorem slotArrayWF_of_zero {base U n_max : ℕ} {mem : ℕ → ℕ}
+    (hz : ∀ j : Fin (numBuckets n_max), mem (base + slotOffset U n_max + j.val) = 0) :
+    SlotArrayWF base U n_max mem := by
+  intro j
+  refine ⟨Or.inl (hz j), ?_⟩
+  rw [hz j]
+  intro h
+  omega
+
+theorem extractSlots_eq_emptyTable_of_zero {base U n_max : ℕ} {mem : ℕ → ℕ}
+    (hz : ∀ j : Fin (numBuckets n_max), mem (base + slotOffset U n_max + j.val) = 0) :
+    extractSlots base U n_max mem = emptyTable U (numBuckets n_max) := by
+  funext j
+  simp [extractSlots, emptyTable, hz j]
+
+/-! ## Section 3: Register Layout, Allocation, and Randomized Initialization -/
+
+/-- Register `0` (`baseReg`, persistent): holds the base memory address `base`. -/
+abbrev regBase : Fin 12 := 0
+
+/-- Register `1` (`curReg`): loop condition / multiply-shift seed / tabulation key scratch. -/
+abbrev regCond : Fin 12 := 1
+
+/-- Register `2` (`zeroReg`): memory address / multiply-shift key / tabulation output scratch. -/
+abbrev regAddr : Fin 12 := 2
+
+/-- Register `3` (`oneReg`): current probe slot `slot ∈ Fin (numBuckets n_max)`. -/
+abbrev regSlot : Fin 12 := 3
+
+/-- Register `4`: slot array base address `base + slotOffset U n_max`. -/
+abbrev regSlotBase : Fin 12 := 4
+
+/-- Register `5`: bucket mask `numBuckets n_max - 1`. -/
+abbrev regMaskM : Fin 12 := 5
+
+/-- Register `6`: odd probe stride `strideHash θ u`. -/
+abbrev regStride : Fin 12 := 6
+
+/-- Register `7`: table size `numBuckets n_max`. -/
+abbrev regM : Fin 12 := 7
+
+/-- Register `8`: constant `0` during probing / general scratch. -/
+abbrev regZero : Fin 12 := 8
+
+/-- Register `9` (`output`): operation tag (`0` for `get`, `1` for `insert`) on input; decoded
+return value (`0` for `none`/`()`, `v + 1` for `some v`) on output. -/
+abbrev regOp : Fin 12 := 9
+
+/-- Register `10`: input key `u.val < U`. -/
+abbrev regU : Fin 12 := 10
+
+/-- Register `11` (`frontierReg`): input value `v < V` for `insert` / allocation frontier. -/
+abbrev regV : Fin 12 := 11
+
+/-- Register injection `Fin 5 → Fin 12` embedding `MultiplyShift` into registers `1..5`
+(preserving `regBase = 0` and `6..11`). -/
+def msMap : Fin 5 → Fin 12 :=
+  fun i => ⟨i.val + 1, by omega⟩
+
+theorem injective_msMap : Function.Injective msMap := by
+  intro i j h
+  ext
+  simpa [msMap] using congrArg Fin.val h
+
+theorem notMem_range_msMap {j : Fin 12} (hj : j.val = 0 ∨ 6 ≤ j.val) :
+    j ∉ Set.range msMap := by
+  rintro ⟨i, rfl⟩
+  have := i.isLt
+  simp only [msMap] at hj
+  omega
+
+/-- Register injection `Fin 9 → Fin 12` embedding `TabulatedOddStride` into registers `0..8`
+(with `tabMap 0 = regBase` and preserving `regOp = 9`, `regU = 10`, `regV = 11`). -/
+def tabMap : Fin 9 → Fin 12 :=
+  fun i => ⟨i.val, by omega⟩
+
+theorem injective_tabMap : Function.Injective tabMap := by
+  intro i j h
+  ext
+  simpa [tabMap] using congrArg Fin.val h
+
+theorem notMem_range_tabMap {j : Fin 12} (hj : 9 ≤ j.val) :
+    j ∉ Set.range tabMap := by
+  rintro ⟨i, rfl⟩
+  have := i.isLt
+  simp only [tabMap] at hj
+  omega
+
+/-- Allocation program `allocSpan U n_max` (3 instructions): copies `frontierReg` (`regV`) to
+`baseReg` (`regBase`) and advances `frontierReg` by `space U n_max`. -/
+def allocSpan (U n_max : ℕ) : Code .exact 12 :=
+  .seq (.op (.copy regBase regV))
+  (.seq (.op (.const regCond (space U n_max)))
+        (.op (.exactBin .add regV regBase regCond)))
+
+theorem allocSpan_execWithin {w base U n_max : ℕ} {x : Data 12}
+    (hS : Fits w (base + space U n_max)) (hfr : x.regs regV = base) :
+    ∃ x₁ : Data 12,
+      ExecWithin w (allocSpan U n_max) x x₁ 3 ∧
+      x₁.mem = x.mem ∧
+      x₁.regs regBase = base ∧
+      x₁.regs regV = base + space U n_max := by
+  have hfit_sp : Fits w (space U n_max) := hS.of_le (by omega)
+  set s1 := x.set regBase base
+  have e1 : Exec w (.op (.copy regBase regV) : Code .exact 12) x s1 1 := by
+    simpa [s1, hfr] using (Exec.copy (B := .exact) (w := w) (d := regBase) (s := regV) (x := x))
+  set s2 := s1.set regCond (space U n_max)
+  have e2 : Exec w (.op (.const regCond (space U n_max)) : Code .exact 12) s1 s2 1 :=
+    Exec.const hfit_sp
+  set s3 := s2.set regV (base + space U n_max)
+  have e3 : Exec w (.op (.exactBin .add regV regBase regCond) : Code .exact 12) s2 s3 1 :=
+    Exec.alu (by simp +decide [StandardOp.evalExact, s2, s1]) hS
+  exact ⟨s3, (e1.seq (e2.seq e3)).within, rfl,
+    by simp +decide [s3, s2, s1], by simp +decide [s3]⟩
+
+/-- Deterministic 5-instruction glue between `MultiplyShift.initCode` and
+`TabulatedOddStride.initFromBCode`: stores the multiply-shift seed `regCond` at
+`base + tabSpace U n_max` and loads `charBits n_max` into `regMaskM` and `bucketBits n_max` into
+`regAddr`. -/
+def initMidCode (U n_max : ℕ) : Code .exact 12 :=
+  .seq (.op (.const regAddr (tabSpace U n_max)))
+  (.seq (.op (.exactBin .add regAddr regBase regAddr))
+  (.seq (.op (.store regAddr regCond))
+  (.seq (.op (.const regMaskM (charBits n_max)))
+        (.op (.const regAddr (bucketBits n_max))))))
+
+/-- Closed-form machine state after `initMidCode U n_max`. -/
+def initMidData (base U n_max : ℕ) (d : Data 12) : Data 12 :=
+  ((((d.set regAddr (tabSpace U n_max)).set regAddr (base + tabSpace U n_max)).write
+    (base + tabSpace U n_max) (d.regs regCond)).set regMaskM (charBits n_max)).set
+    regAddr (bucketBits n_max)
+
+theorem fits_of_space {w base U n_max : ℕ} (hS : Fits w (base + space U n_max)) :
+    Fits w (base + tabSpace U n_max) ∧
+    Fits w (2 ^ charBits n_max) ∧
+    Fits w (2 ^ bucketBits n_max) ∧
+    Fits w (numChars U n_max) ∧
+    Fits w (charBits n_max) ∧
+    Fits w (bucketBits n_max) := by
+  have hd : 1 ≤ numChars U n_max := one_le_numChars U n_max
+  have hpowB_pos : 1 ≤ 2 ^ charBits n_max := Nat.one_le_two_pow
+  have hpowB_le : 2 ^ charBits n_max ≤ numChars U n_max * 2 ^ charBits n_max :=
+    Nat.le_mul_of_pos_left _ hd
+  have hd_le : numChars U n_max ≤ numChars U n_max * 2 ^ charBits n_max :=
+    Nat.le_mul_of_pos_right _ hpowB_pos
+  have htab : tabSpace U n_max = 4 + numChars U n_max * 2 ^ charBits n_max := rfl
+  have hsp : space U n_max = tabSpace U n_max + 1 + 3 * numBuckets n_max := rfl
+  have hcb_lt : charBits n_max < 2 ^ charBits n_max := Nat.lt_two_pow_self
+  have hbb_lt : bucketBits n_max < 2 ^ bucketBits n_max := Nat.lt_two_pow_self
+  have hM : 2 ^ bucketBits n_max = numBuckets n_max := rfl
+  refine ⟨hS.of_le (by omega), hS.of_le (by omega), hS.of_le (by omega),
+    hS.of_le (by omega), hS.of_le (by omega), hS.of_le (by omega)⟩
+
+theorem initMidCode_exec {w base U n_max : ℕ} {d : Data 12}
+    (hbase : d.regs regBase = base) (hS : Fits w (base + space U n_max)) :
+    Exec w (initMidCode U n_max) d (initMidData base U n_max d) 5 := by
+  obtain ⟨hfit_btab, _, _, _, hfit_cb, hfit_bb⟩ := fits_of_space hS
+  have hfit_tab : Fits w (tabSpace U n_max) := hfit_btab.of_le (by omega)
+  set s1 := d.set regAddr (tabSpace U n_max)
+  have e1 : Exec w (.op (.const regAddr (tabSpace U n_max)) : Code .exact 12) d s1 1 :=
+    Exec.const hfit_tab
+  set s2 := s1.set regAddr (base + tabSpace U n_max)
+  have e2 : Exec w (.op (.exactBin .add regAddr regBase regAddr) : Code .exact 12) s1 s2 1 :=
+    Exec.alu (by simp +decide [StandardOp.evalExact, s1, hbase]) hfit_btab
+  set s3 := s2.write (base + tabSpace U n_max) (d.regs regCond)
+  have e3 : Exec w (.op (.store regAddr regCond) : Code .exact 12) s2 s3 1 := by
+    simpa +decide [s3, s2, s1] using
+      (Exec.store (B := .exact) (w := w) (a := regAddr) (s := regCond) (x := s2))
+  set s4 := s3.set regMaskM (charBits n_max)
+  have e4 : Exec w (.op (.const regMaskM (charBits n_max)) : Code .exact 12) s3 s4 1 :=
+    Exec.const hfit_cb
+  set s5 := s4.set regAddr (bucketBits n_max)
+  have e5 : Exec w (.op (.const regAddr (bucketBits n_max)) : Code .exact 12) s4 s5 1 :=
+    Exec.const hfit_bb
+  exact e1.seq (e2.seq (e3.seq (e4.seq e5)))
+
+/-- Complete randomized setup program `initSetup U n_max`: samples the multiply-shift seed,
+stores it at `base + tabSpace U n_max`, and initializes the `TabulatedOddStride` table at
+`[base, base + tabSpace U n_max)`. -/
+def initSetup (U n_max : ℕ) : Code .exact 12 :=
+  .seq ((MultiplyShift.initCode (hashBits U n_max)).rename msMap)
+  (.seq (initMidCode U n_max)
+        ((TabulatedOddStride.initFromBCode (numChars U n_max)).rename tabMap))
+
+/-- Total instruction count `5 * (numChars U n_max * 2 ^ charBits n_max) + 25` of `initSetup`. -/
+def setupSteps (U n_max : ℕ) : ℕ :=
+  5 * (numChars U n_max * 2 ^ charBits n_max) + 25
+
+/-- Extract the multiply-shift seed from `mem (base + tabSpace U n_max)`. -/
+def extractMSSeedFromMem (base U n_max : ℕ) (mem : ℕ → ℕ) : Fin (2 ^ (hashBits U n_max - 1)) :=
+  if h : mem (base + tabSpace U n_max) < 2 ^ (hashBits U n_max - 1) then
+    ⟨mem (base + tabSpace U n_max), h⟩
+  else
+    ⟨0, Nat.two_pow_pos _⟩
+
+/-- Extract the combined seed `Seed U n_max` from machine state `y`. -/
+def extractSeedPair (base U n_max : ℕ) (y : Data 12) : Seed U n_max :=
+  (extractMSSeedFromMem base U n_max y.mem,
+    TabulatedOddStride.extractTable base (charBits n_max) (numChars U n_max) (bucketBits n_max)
+      y.mem)
+
+/-- Stage-1 state distribution produced by
+`(MultiplyShift.initCode (hashBits U n_max)).rename msMap`. -/
+noncomputable def msInitPMF (U n_max : ℕ) (x₁ : Data 12) : PMF (Data 12) :=
+  (Prod.fst <$>
+    ((fun z => (z.1.extend msMap x₁, z.2)) <$>
+      MultiplyShift.initComp (hashBits U n_max) (x₁.comap msMap))).eval
+
+/-- Stage-3 state distribution produced by
+`(TabulatedOddStride.initFromBCode (numChars U n_max)).rename tabMap`. -/
+noncomputable def tabInitPMF (base U n_max : ℕ) (y₂ : Data 12) : PMF (Data 12) :=
+  (Prod.fst <$>
+    ((fun z => (z.1.extend tabMap y₂, z.2)) <$>
+      TabulatedOddStride.initFromBComp base (charBits n_max) (numChars U n_max) (bucketBits n_max)
+        (y₂.comap tabMap))).eval
+
+/-- Output state distribution of `initSetup U n_max`. -/
+noncomputable def initSetupPMF (base U n_max : ℕ) (x₁ : Data 12) : PMF (Data 12) :=
+  (msInitPMF U n_max x₁).bind (fun y₁ => tabInitPMF base U n_max (initMidData base U n_max y₁))
+
+/-- Coupled `(Seed × Data 12)` distribution produced by `initSetup U n_max`. -/
+noncomputable def initSeedStatePMF (base U n_max : ℕ) (x₁ : Data 12) :
+    PMF (Seed U n_max × Data 12) :=
+  (initSetupPMF base U n_max x₁).map (fun y => (extractSeedPair base U n_max y, y))
+
+theorem mem_support_msInitPMF {U n_max : ℕ} {x₁ y₁ : Data 12}
+    (hy₁ : y₁ ∈ (msInitPMF U n_max x₁).support) :
+    y₁.regs regBase = x₁.regs regBase ∧
+    y₁.regs regV = x₁.regs regV ∧
+    y₁.regs regCond < 2 ^ (hashBits U n_max - 1) ∧
+    (y₁.comap msMap).regs MultiplyShift.regB = y₁.regs regCond ∧
+    y₁.mem = x₁.mem := by
+  dsimp only [msInitPMF] at hy₁
+  rw [Functor.map_map, ProbComp.eval_map, PMF.mem_support_map_iff] at hy₁
+  obtain ⟨z, hz, rfl⟩ := hy₁
+  rw [ProbComp.support_eval] at hz
+  dsimp only [MultiplyShift.initComp] at hz
+  obtain ⟨k, -, hk⟩ := OracleComp.mem_supportWith_bind_iff.mp hz
+  cases OracleComp.eq_of_mem_supportWith_pure hk
+  have hlt : k.val < 2 ^ (hashBits U n_max - 1) := by
+    have hpos : 1 ≤ 2 ^ (hashBits U n_max - 1) := Nat.one_le_two_pow
+    have hk_lt := k.isLt
+    omega
+  refine ⟨Data.extend_regs_of_notMem _ _ (notMem_range_msMap (by decide)),
+    Data.extend_regs_of_notMem _ _ (notMem_range_msMap (by decide)), ?_, rfl, rfl⟩
+  change ((MultiplyShift.initData (hashBits U n_max) (x₁.comap msMap) k.val).extend msMap
+    x₁ |>.comap msMap).regs MultiplyShift.regB < 2 ^ (hashBits U n_max - 1)
+  rw [Data.comap_extend injective_msMap]
+  simpa [MultiplyShift.initData] using hlt
+
+theorem map_extractSeed_msInitPMF (U n_max : ℕ) (x₁ : Data 12) :
+    (msInitPMF U n_max x₁).map
+        (fun y₁ => MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap)) =
+      PMF.uniformOfFintype (Fin (2 ^ (hashBits U n_max - 1))) := by
+  dsimp only [msInitPMF]
+  rw [Functor.map_map, ProbComp.eval_map, PMF.map_comp]
+  have hcomp :
+      ((fun y₁ : Data 12 => MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap)) ∘
+        fun x : Data 5 × ℕ => x.1.extend msMap x₁) =
+      fun x : Data 5 × ℕ => MultiplyShift.extractSeed (hashBits U n_max) x.1 := by
+    funext z
+    simp [Data.comap_extend injective_msMap]
+  rw [hcomp]
+  exact MultiplyShift.map_extractSeed_eval_initComp (hashBits U n_max) (x₁.comap msMap)
+
+theorem mem_support_tabInitPMF {base U n_max : ℕ} {y₂ y : Data 12}
+    (hbase : y₂.regs regBase = base)
+    (hy : y ∈ (tabInitPMF base U n_max y₂).support) :
+    TabulatedOddStride.Rep base (charBits n_max) (numChars U n_max) (bucketBits n_max)
+      (TabulatedOddStride.extractTable base (charBits n_max) (numChars U n_max) (bucketBits n_max)
+        y.mem) y.mem ∧
+    y.regs regBase = base ∧
+    y.regs regV = y₂.regs regV ∧
+    (∀ a, (a < base ∨ base + tabSpace U n_max ≤ a) → y.mem a = y₂.mem a) := by
+  dsimp only [tabInitPMF] at hy
+  rw [Functor.map_map, ProbComp.eval_map, PMF.mem_support_map_iff] at hy
+  obtain ⟨z, hz, rfl⟩ := hy
+  rw [ProbComp.support_eval] at hz
+  have hbase_comap : (y₂.comap tabMap).regs TabulatedOddStride.regBase = base := hbase
+  obtain ⟨-, hrep, hbase', hframe⟩ :=
+    TabulatedOddStride.mem_support_initFromBComp hbase_comap hz
+  have hbase_ext : (z.1.extend tabMap y₂).regs regBase = base := by
+    change ((z.1.extend tabMap y₂).comap tabMap).regs TabulatedOddStride.regBase = base
+    rw [Data.comap_extend injective_tabMap]
+    exact hbase'
+  have hv_ext : (z.1.extend tabMap y₂).regs regV = y₂.regs regV :=
+    Data.extend_regs_of_notMem _ _ (notMem_range_tabMap (by decide))
+  exact ⟨hrep, hbase_ext, hv_ext, hframe⟩
+
+theorem map_extractSeedPair_tabInitPMF {base U n_max : ℕ} {y₁ : Data 12}
+    (hbase : y₁.regs regBase = base)
+    (hcond : y₁.regs regCond < 2 ^ (hashBits U n_max - 1)) :
+    (tabInitPMF base U n_max (initMidData base U n_max y₁)).map (extractSeedPair base U n_max) =
+      (PMF.uniformOfFintype
+        (Fin (numChars U n_max * 2 ^ charBits n_max) → Fin (numBuckets n_max))).map
+        (fun T => (MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap), T)) := by
+  set y₂ := initMidData base U n_max y₁
+  have hy₂_base : y₂.regs regBase = base := by
+    simpa [y₂, initMidData, regBase, regAddr, regMaskM] using hbase
+  have hcongr :
+      (tabInitPMF base U n_max y₂).map (extractSeedPair base U n_max) =
+      (tabInitPMF base U n_max y₂).map
+        (fun y =>
+          (MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap),
+            TabulatedOddStride.extractTable base (charBits n_max) (numChars U n_max)
+              (bucketBits n_max) y.mem)) := by
+    apply PMF.map_congr_on_support
+    intro y hy
+    obtain ⟨-, -, -, hframe⟩ := mem_support_tabInitPMF hy₂_base hy
+    have hms_mem : y.mem (base + tabSpace U n_max) = y₁.regs regCond := by
+      rw [hframe (base + tabSpace U n_max) (Or.inr le_rfl)]
+      simp [y₂, initMidData, Data.write]
+    have hms_eq : extractMSSeedFromMem base U n_max y.mem =
+        MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap) := by
+      have hregB : y₁.regs (msMap MultiplyShift.regB) = y₁.regs regCond := rfl
+      apply Fin.ext
+      dsimp only [extractMSSeedFromMem, MultiplyShift.extractSeed, Data.comap]
+      simp [hms_mem, hregB, hcond]
+    exact Prod.ext hms_eq rfl
+  rw [hcongr]
+  dsimp only [tabInitPMF]
+  rw [Functor.map_map, ProbComp.eval_map, PMF.map_comp]
+  have hcomp :
+      ((fun y : Data 12 =>
+          (MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap),
+            TabulatedOddStride.extractTable base (charBits n_max) (numChars U n_max)
+              (bucketBits n_max) y.mem)) ∘
+        fun z : Data 9 × ℕ => z.1.extend tabMap y₂) =
+      ((fun T => (MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap), T)) ∘
+        fun z : Data 9 × ℕ =>
+          TabulatedOddStride.extractTable base (charBits n_max) (numChars U n_max)
+            (bucketBits n_max) z.1.mem) := rfl
+  rw [hcomp, ← PMF.map_comp]
+  change (((TabulatedOddStride.initFromBComp base (charBits n_max) (numChars U n_max)
+      (bucketBits n_max) (y₂.comap tabMap)).eval).map
+      (fun z => TabulatedOddStride.extractTable base (charBits n_max) (numChars U n_max)
+        (bucketBits n_max) z.1.mem)).map
+      (fun T => (MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap), T)) =
+    (PMF.uniformOfFintype
+      (Fin (numChars U n_max * 2 ^ charBits n_max) → Fin (2 ^ bucketBits n_max))).map
+      (fun T => (MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap), T))
+  rw [TabulatedOddStride.map_extractTable_eval_initFromBComp]
+
+/-- **Exact uniformity of the sampled seed pair**: the seed marginal of `initSeedStatePMF` is the
+exact product uniform distribution `seedLaw U n_max`. -/
+theorem map_fst_initSeedStatePMF {base U n_max : ℕ} {x₁ : Data 12}
+    (hbase : x₁.regs regBase = base) :
+    (initSeedStatePMF base U n_max x₁).map Prod.fst = seedLaw U n_max := by
+  dsimp only [initSeedStatePMF, initSetupPMF]
+  rw [PMF.map_comp]
+  have hfst : Prod.fst ∘ (fun y : Data 12 => (extractSeedPair base U n_max y, y)) =
+      extractSeedPair base U n_max := rfl
+  rw [hfst, PMF.map_bind]
+  let μ_tab : PMF (Fin (numChars U n_max * 2 ^ charBits n_max) → Fin (numBuckets n_max)) :=
+    PMF.uniformOfFintype
+      (Fin (numChars U n_max * 2 ^ charBits n_max) → Fin (numBuckets n_max))
+  have hbind :
+      (msInitPMF U n_max x₁).bind
+        (fun y₁ => (tabInitPMF base U n_max (initMidData base U n_max y₁)).map
+          (extractSeedPair base U n_max)) =
+      (msInitPMF U n_max x₁).bind
+        (fun y₁ => μ_tab.map
+          (fun T => (MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap), T))) := by
+    ext θ
+    rw [PMF.bind_apply, PMF.bind_apply]
+    refine tsum_congr fun y₁ => ?_
+    by_cases hy₁ : y₁ ∈ (msInitPMF U n_max x₁).support
+    · obtain ⟨hb₁, -, hcond₁, -, -⟩ := mem_support_msInitPMF hy₁
+      rw [map_extractSeedPair_tabInitPMF (hb₁.trans hbase) hcond₁]
+    · rw [(PMF.apply_eq_zero_iff _ _).mpr hy₁, zero_mul, zero_mul]
+  rw [hbind]
+  have hmap_bind :
+      (msInitPMF U n_max x₁).bind
+        (fun y₁ => μ_tab.map
+          (fun T => (MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap), T))) =
+      ((msInitPMF U n_max x₁).map
+        (fun y₁ => MultiplyShift.extractSeed (hashBits U n_max) (y₁.comap msMap))).bind
+        (fun b => μ_tab.map (fun T => (b, T))) := by
+    rw [PMF.bind_map]
+    rfl
+  rw [hmap_bind, map_extractSeed_msInitPMF]
+  exact Cslib.Probability.PMF.uniformOfFintype_prod _ _
+
+theorem initSetup_execCodeDist {w base U n_max : ℕ} {x₁ : Data 12}
+    (hbase : x₁.regs regBase = base) (hS : Fits w (base + space U n_max))
+    (hw : 2 * hashBits U n_max ≤ w) :
+    ExecCodeDist w (initSetup U n_max) x₁ (initSetupPMF base U n_max x₁) (setupSteps U n_max) := by
+  have hw₀ : hashBits U n_max ≤ w := by omega
+  obtain ⟨hfit_btab, hfit_powB, hfit_powM, hfit_d, -, -⟩ := fits_of_space hS
+  have hms_rand :=
+    (MultiplyShift.initCode_execRand (w := w) hw₀ (x₁.comap msMap)).rename injective_msMap
+  have hms_dist : ExecCodeDist w
+      ((MultiplyShift.initCode (hashBits U n_max)).rename msMap) x₁
+      (msInitPMF U n_max x₁) 2 := by
+    refine (ExecCodeDist.of_execRand hms_rand).congr_dist rfl ?_
+    rw [ProbComp.expect_map]
+    refine (ProbComp.expect_mono_on_support fun z hz => ?_).trans
+      (le_of_eq (ProbComp.expect_const _ 2))
+    dsimp only [MultiplyShift.initComp] at hz
+    obtain ⟨k, -, hk⟩ := OracleComp.mem_supportWith_bind_iff.mp hz
+    cases OracleComp.eq_of_mem_supportWith_pure hk
+    exact le_rfl
+  have hrest : ∀ y₁ ∈ (msInitPMF U n_max x₁).support,
+      ExecCodeDist w
+        (.seq (initMidCode U n_max)
+          ((TabulatedOddStride.initFromBCode (numChars U n_max)).rename tabMap))
+        y₁ (tabInitPMF base U n_max (initMidData base U n_max y₁))
+        (5 + (5 * (numChars U n_max * 2 ^ charBits n_max) + 18 : ℕ)) := by
+    intro y₁ hy₁
+    obtain ⟨hb₁, -, -, -, -⟩ := mem_support_msInitPMF hy₁
+    have hmid := ExecCodeDist.of_exec (initMidCode_exec (hb₁.trans hbase) hS)
+    set y₂ := initMidData base U n_max y₁
+    have hy₂_base : (y₂.comap tabMap).regs TabulatedOddStride.regBase = base := by
+      simpa +decide [y₂, initMidData, tabMap, Data.comap] using hb₁.trans hbase
+    have hy₂_b : (y₂.comap tabMap).regs TabulatedOddStride.regB = charBits n_max := by
+      simp +decide [y₂, initMidData, tabMap, Data.comap]
+    have hy₂_M : (y₂.comap tabMap).regs TabulatedOddStride.regOut = bucketBits n_max := by
+      simp +decide [y₂, initMidData, tabMap, Data.comap]
+    have htab_rand :=
+      (TabulatedOddStride.initFromBCode_execRand (w := w)
+        hy₂_base hy₂_b hy₂_M hfit_btab hfit_powB hfit_powM hfit_d).rename injective_tabMap
+    have htab_dist : ExecCodeDist w
+        ((TabulatedOddStride.initFromBCode (numChars U n_max)).rename tabMap) y₂
+        (tabInitPMF base U n_max y₂)
+        (5 * (numChars U n_max * 2 ^ charBits n_max) + 18 : ℕ) := by
+      refine (ExecCodeDist.of_execRand htab_rand).congr_dist rfl ?_
+      rw [ProbComp.expect_map]
+      refine (ProbComp.expect_mono_on_support fun z hz => ?_).trans
+        (le_of_eq (ProbComp.expect_const _ _))
+      obtain ⟨hsteps, -, -, -⟩ := TabulatedOddStride.mem_support_initFromBComp hy₂_base hz
+      exact_mod_cast hsteps.le
+    exact hmid.seq_pure htab_dist
+  have hseq := hms_dist.seq_const hrest (fun _ _ => le_rfl)
+  refine hseq.congr_dist rfl ?_
+  dsimp only [setupSteps]
+  norm_cast
+  omega
+
+/-- Full `SubroutineDS.setup_exec` certificate for `initSetup U n_max`. -/
+theorem setup_exec_spec {w base U V n_max : ℕ} {x₁ : Data 12}
+    (hS : Fits w (base + space U n_max)) (hw : 2 * hashBits U n_max ≤ w)
+    (hx₁ : x₁.Bounded w) (hbase : x₁.regs regBase = base)
+    (hfr : x₁.regs regV = base + space U n_max)
+    (hz : ∀ a ∈ (Block.mk base (space U n_max)).footprint, x₁.mem a = 0) :
+    ∃ ν₀ : PMF (Seed U n_max × Data 12),
+      ExecCodeDist w (initSetup U n_max) x₁ (ν₀.map Prod.snd) (setupSteps U n_max) ∧
+      (∀ θ, (ν₀.map Prod.fst) θ ≤ 1 * seedLaw U n_max θ) ∧
+      ∀ p ∈ ν₀.support,
+        p.2.regs regV = base + space U n_max ∧
+        Rep w base U V n_max p.1 (Dictionary.empty U) p.2 ∧
+        (0 : ℕ) ≤ 0 ∧
+        Modifies (Block.mk base (space U n_max)).footprint x₁.mem p.2.mem := by
+  refine ⟨initSeedStatePMF base U n_max x₁, ?_, ?_, ?_⟩
+  · have hsnd : (initSeedStatePMF base U n_max x₁).map Prod.snd =
+        initSetupPMF base U n_max x₁ := by
+      dsimp only [initSeedStatePMF]
+      rw [PMF.map_comp]
+      exact PMF.map_id _
+    rw [hsnd]
+    exact initSetup_execCodeDist hbase hS hw
+  · intro θ
+    rw [map_fst_initSeedStatePMF hbase, one_mul]
+  · intro p hp
+    dsimp only [initSeedStatePMF] at hp
+    rw [PMF.mem_support_map_iff] at hp
+    obtain ⟨y, hy, rfl⟩ := hp
+    have hbdd_y : y.Bounded w :=
+      (initSetup_execCodeDist hbase hS hw).bounded hx₁ y hy
+    dsimp only [initSetupPMF] at hy
+    rw [PMF.mem_support_bind_iff] at hy
+    obtain ⟨y₁, hy₁, hy₃⟩ := hy
+    obtain ⟨hb₁, hv₁, hcond₁, -, hmem₁⟩ := mem_support_msInitPMF hy₁
+    set y₂ := initMidData base U n_max y₁
+    have hy₂_base : y₂.regs regBase = base := by
+      simpa +decide [y₂, initMidData] using hb₁.trans hbase
+    obtain ⟨htab_rep, hy_base, hy_v, hframe₃⟩ := mem_support_tabInitPMF hy₂_base hy₃
+    have hy_v_eq : y.regs regV = base + space U n_max := by
+      rw [hy_v]
+      simpa +decide [y₂, initMidData, hv₁] using hfr
+    have hms_mem : y.mem (base + tabSpace U n_max) = y₁.regs regCond := by
+      rw [hframe₃ (base + tabSpace U n_max) (Or.inr le_rfl)]
+      simp [y₂, initMidData, Data.write]
+    have hms_seed : y.mem (base + tabSpace U n_max) = (extractSeedPair base U n_max y).1.val := by
+      dsimp only [extractSeedPair, extractMSSeedFromMem]
+      have hlt_mem : y.mem (base + tabSpace U n_max) < 2 ^ (hashBits U n_max - 1) := by
+        rwa [hms_mem]
+      simp [hlt_mem]
+    have hz_slots : ∀ j : Fin (numBuckets n_max),
+        y.mem (base + slotOffset U n_max + j.val) = 0 := by
+      intro j
+      have hj := j.isLt
+      have hsp : space U n_max = slotOffset U n_max + 3 * numBuckets n_max := rfl
+      have hso : slotOffset U n_max = tabSpace U n_max + 1 := rfl
+      rw [hframe₃ (base + slotOffset U n_max + j.val) (Or.inr (by omega))]
+      have hne : base + slotOffset U n_max + j.val ≠ base + tabSpace U n_max := by omega
+      simpa [y₂, initMidData, Data.write, Function.update_of_ne hne, hmem₁] using
+        hz _ (mem_footprint_of_lt_space (by omega) (by omega))
+    have hwf : SlotArrayWF base U n_max y.mem := slotArrayWF_of_zero hz_slots
+    have hempty : extractSlots base U n_max y.mem = emptyTable U (numBuckets n_max) :=
+      extractSlots_eq_emptyTable_of_zero hz_slots
+    have htrep : TableRep (probePerm (extractSeedPair base U n_max y))
+        (Dictionary.empty U) (extractSlots base U n_max y.mem) := by
+      rw [hempty]
+      exact tableRep_empty _
+    have hmod : Modifies (Block.mk base (space U n_max)).footprint x₁.mem y.mem := by
+      intro a ha
+      have ha_out : a < base ∨ base + space U n_max ≤ a := by
+        by_contra h
+        rw [not_or, not_lt, not_le] at h
+        exact ha (mem_footprint_of_lt_space h.1 h.2)
+      have hsp : space U n_max = tabSpace U n_max + 1 + 3 * numBuckets n_max := rfl
+      have ha₃ : a < base ∨ base + tabSpace U n_max ≤ a := by omega
+      have hne : a ≠ base + tabSpace U n_max := by omega
+      rw [hframe₃ a ha₃]
+      simp [y₂, initMidData, Data.write, Function.update_of_ne hne, hmem₁]
+    refine ⟨hy_v_eq, ⟨hbdd_y, hy_base, htab_rep, hms_seed, hwf, htrep, ?_, ?_⟩, le_rfl, hmod⟩
+    · simp
+    · exact Dictionary.valuesBounded_empty U V
+
+/-! ## Section 4: Lookup and Insertion Operations (`opCode`) -/
+
+/-- Probe inspection snippet `probeCheckCode` (`≤ 9` instructions): checks whether the slot in
+`regSlot` belongs to `otherOccupiedSlots (extractSlots base U n_max d.mem) u` (i.e.,
+`used[slot] = 1` and `key[slot] ≠ u.val`), storing `1` in `regCond` if so and `0` otherwise. -/
+def probeCheckCode : Code .exact 12 :=
+  .seq (.op (.exactBin .add regAddr regSlotBase regSlot))
+  (.seq (.op (.load regCond regAddr))
+        (.branch (.eq regCond regZero)
+          (.op (.const regCond 0))
+          (.seq (.op (.exactBin .add regAddr regAddr regM))
+          (.seq (.op (.load regCond regAddr))
+                (.branch (.eq regCond regU)
+                  (.op (.const regCond 0))
+                  (.op (.const regCond 1)))))))
+
+theorem probeCheckCode_execWithin {w base U n_max : ℕ} {d : Data 12}
+    (hS : Fits w (base + space U n_max))
+    (hwf : SlotArrayWF base U n_max d.mem)
+    (u : Fin U) (slot : Fin (numBuckets n_max))
+    (hsbase : d.regs regSlotBase = base + slotOffset U n_max)
+    (hslot : d.regs regSlot = slot.val)
+    (hm : d.regs regM = numBuckets n_max)
+    (hzero : d.regs regZero = 0)
+    (hu : d.regs regU = u.val) :
+    ∃ d' : Data 12,
+      ExecWithin w probeCheckCode d d' 9 ∧
+      d'.mem = d.mem ∧
+      d'.regs regCond =
+        (if slot ∈ otherOccupiedSlots (extractSlots base U n_max d.mem) u then 1 else 0) ∧
+      ∀ r : Fin 12, r ≠ regAddr → r ≠ regCond → d'.regs r = d.regs r := by
+  have hslot_lt := slot.isLt
+  have hsp : space U n_max = slotOffset U n_max + 3 * numBuckets n_max := rfl
+  have hfit_0 : Fits w 0 := hS.of_le (by omega)
+  have hfit_1 : Fits w 1 := hS.of_le (by omega)
+  let sBase := base + slotOffset U n_max
+  let m := numBuckets n_max
+  have hfit_a0 : Fits w (sBase + slot.val) := hS.of_le (by omega)
+  have hfit_a1 : Fits w (sBase + slot.val + m) := hS.of_le (by omega)
+  set s1 := d.set regAddr (sBase + slot.val)
+  have e1 : Exec w (.op (.exactBin .add regAddr regSlotBase regSlot) : Code .exact 12) d s1 1 :=
+    Exec.alu (by simp +decide [StandardOp.evalExact, hsbase, hslot, sBase]) hfit_a0
+  let usedVal := d.mem (sBase + slot.val)
+  set s2 := s1.set regCond usedVal
+  have e2 : Exec w (.op (.load regCond regAddr) : Code .exact 12) s1 s2 1 := by
+    simpa +decide [s2, s1, usedVal] using
+      (Exec.load (B := .exact) (w := w) (d := regCond) (a := regAddr) (x := s1))
+  rcases (hwf slot).1 with hused0 | hused1
+  · have hc : (Cond.eq regCond regZero).Holds s2 := by
+      simp +decide [Cond.Holds, s2, s1, usedVal, sBase, hused0, hzero]
+    set s3 := s2.set regCond 0
+    have e3 : Exec w (.op (.const regCond 0) : Code .exact 12) s2 s3 1 := Exec.const hfit_0
+    have hnot_mem : slot ∉ otherOccupiedSlots (extractSlots base U n_max d.mem) u := by
+      rw [mem_otherOccupiedSlots_extractSlots_iff hwf]
+      omega
+    refine ⟨s3,
+      (e1.within.seq (e2.within.seq (ExecWithin.branch_pos hc e3.within))).mono (by omega),
+      rfl, ?_, ?_⟩
+    · simp +decide [s3, hnot_mem]
+    · intro r hr1 hr2
+      simp [s3, s2, s1, Data.set, Function.update_of_ne hr2, Function.update_of_ne hr1]
+  · have hc : ¬(Cond.eq regCond regZero).Holds s2 := by
+      simp +decide [Cond.Holds, s2, s1, usedVal, sBase, hused1, hzero]
+    set s3 := s2.set regAddr (sBase + slot.val + m)
+    have e3 : Exec w (.op (.exactBin .add regAddr regAddr regM) : Code .exact 12) s2 s3 1 :=
+      Exec.alu (by simp +decide [StandardOp.evalExact, s2, s1, hm, m]) hfit_a1
+    have haddr_eq : sBase + slot.val + m = sBase + m + slot.val := by omega
+    let keyVal := d.mem (sBase + m + slot.val)
+    set s4 := s3.set regCond keyVal
+    have e4 : Exec w (.op (.load regCond regAddr) : Code .exact 12) s3 s4 1 := by
+      simpa +decide [s4, s3, s2, s1, haddr_eq, keyVal] using
+        (Exec.load (B := .exact) (w := w) (d := regCond) (a := regAddr) (x := s3))
+    by_cases hkey : keyVal = u.val
+    · have hc2 : (Cond.eq regCond regU).Holds s4 := by
+        simp +decide [Cond.Holds, s4, s3, s2, s1, hkey, hu]
+      set s5 := s4.set regCond 0
+      have e5 : Exec w (.op (.const regCond 0) : Code .exact 12) s4 s5 1 := Exec.const hfit_0
+      have hnot_mem : slot ∉ otherOccupiedSlots (extractSlots base U n_max d.mem) u := by
+        rw [mem_otherOccupiedSlots_extractSlots_iff hwf]
+        exact fun h => h.2 hkey
+      refine ⟨s5,
+        (e1.within.seq (e2.within.seq
+          (ExecWithin.branch_neg hc
+            (e3.within.seq (e4.within.seq (ExecWithin.branch_pos hc2 e5.within)))))).mono
+          (by omega),
+        rfl, ?_, ?_⟩
+      · simp +decide [s5, hnot_mem]
+      · intro r hr1 hr2
+        simp [s5, s4, s3, s2, s1, Data.set, Function.update_of_ne hr2, Function.update_of_ne hr1]
+    · have hc2 : ¬(Cond.eq regCond regU).Holds s4 := by
+        simp +decide [Cond.Holds, s4, s3, s2, s1, hkey, hu]
+      set s5 := s4.set regCond 1
+      have e5 : Exec w (.op (.const regCond 1) : Code .exact 12) s4 s5 1 := Exec.const hfit_1
+      have hmem : slot ∈ otherOccupiedSlots (extractSlots base U n_max d.mem) u := by
+        rw [mem_otherOccupiedSlots_extractSlots_iff hwf]
+        exact ⟨hused1, hkey⟩
+      refine ⟨s5,
+        (e1.within.seq (e2.within.seq
+          (ExecWithin.branch_neg hc
+            (e3.within.seq (e4.within.seq (ExecWithin.branch_neg hc2 e5.within)))))).mono
+          (by omega),
+        rfl, ?_, ?_⟩
+      · simp +decide [s5, hmem]
+      · intro r hr1 hr2
+        simp [s5, s4, s3, s2, s1, Data.set, Function.update_of_ne hr2, Function.update_of_ne hr1]
+
+/-- One iteration of the probe loop (`≤ 11` instructions): advances `regSlot` by `regStride` modulo
+`numBuckets n_max` (`regMaskM`) and runs `probeCheckCode`. -/
+def probeStepCode : Code .exact 12 :=
+  .seq (.op (.exactBin .add regSlot regSlot regStride))
+  (.seq (.op (.exactBin .and regSlot regSlot regMaskM))
+        probeCheckCode)
+
+/-- Probe loop: continues advancing `regSlot` while `0 < regCond` (i.e., while `regSlot` is occupied
+by a key other than `u`). -/
+def probeLoop : Code .exact 12 :=
+  .loop (.lt regZero regCond) probeStepCode
+
+theorem probeLoop_execWithin_aux {w base U n_max : ℕ} (θ : Seed U n_max)
+    (hS : Fits w (base + space U n_max))
+    {mem : ℕ → ℕ} (hwf : SlotArrayWF base U n_max mem)
+    (u : Fin U)
+    (hO : (otherOccupiedSlots (extractSlots base U n_max mem) u).card < numBuckets n_max) :
+    let T := extractSlots base U n_max mem
+    let O := otherOccupiedSlots T u
+    let k := missedProbes O (probePerm θ u)
+    ∀ (rem i : ℕ) (hi_lt : i < numBuckets n_max) (d : Data 12),
+      i + rem = k →
+      d.mem = mem →
+      d.regs regSlotBase = base + slotOffset U n_max →
+      d.regs regMaskM = numBuckets n_max - 1 →
+      d.regs regStride = (strideHash θ u).val →
+      d.regs regM = numBuckets n_max →
+      d.regs regZero = 0 →
+      d.regs regU = u.val →
+      d.regs regSlot = (probePerm θ u ⟨i, hi_lt⟩).val →
+      d.regs regCond = (if probePerm θ u ⟨i, hi_lt⟩ ∈ O then 1 else 0) →
+      ∃ d' : Data 12,
+        ExecWithin w probeLoop d d' (13 * rem + 2) ∧
+        d'.mem = mem ∧
+        d'.regs regSlot = (targetSlot (probePerm θ) T u hO).val ∧
+        ∀ r : Fin 12, r ≠ regSlot → r ≠ regAddr → r ≠ regCond → d'.regs r = d.regs r := by
+  intro T O k rem
+  have hk_lt : k < numBuckets n_max := missedProbes_lt_of_card_lt hO (probePerm θ u)
+  induction rem with
+  | zero =>
+    intro i hi_lt d hik hmem hsbase hmask hstride hm hzero hu hslot hcond
+    have hi_eq : i = k := by omega
+    have hnot_mem : probePerm θ u ⟨i, hi_lt⟩ ∉ O := by
+      have heq_idx : (⟨i, hi_lt⟩ : Fin (numBuckets n_max)) =
+          probeSlotIndex O (probePerm θ u) hO := Fin.ext hi_eq
+      rw [heq_idx]
+      exact notMem_apply_probeSlotIndex hO
+    have hcond0 : d.regs regCond = 0 := by
+      rw [hcond]
+      exact ite_eq_right_iff.mpr (fun h => False.elim (hnot_mem h))
+    have hc : ¬(Cond.lt regZero regCond).Holds d := by
+      simp [Cond.Holds, hzero, hcond0]
+    refine ⟨d, (Exec.loop_exit hc).within, hmem, ?_, fun _ _ _ _ => rfl⟩
+    rw [hslot]
+    dsimp only [targetSlot, probeSlotIndex]
+    congr 2
+    ext
+    exact hi_eq
+  | succ rem ih =>
+    intro i hi_lt d hik hmem hsbase hmask hstride hm hzero hu hslot hcond
+    have hi_lt_k : i < k := by omega
+    have hi1_lt : i + 1 < numBuckets n_max := by omega
+    have hmem_i : probePerm θ u ⟨i, hi_lt⟩ ∈ O :=
+      mem_of_lt_probeSlotIndex hO (i := ⟨i, hi_lt⟩) hi_lt_k
+    have hcond1 : d.regs regCond = 1 := by
+      rw [hcond]
+      exact ite_eq_left_iff.mpr (fun h => False.elim (h hmem_i))
+    have hc : (Cond.lt regZero regCond).Holds d := by
+      simp [Cond.Holds, hzero, hcond1]
+    let slot_i := probePerm θ u ⟨i, hi_lt⟩
+    let slot_next := probePerm θ u ⟨i + 1, hi1_lt⟩
+    have hsp : space U n_max = slotOffset U n_max + 3 * numBuckets n_max := rfl
+    have hfit_add : Fits w (slot_i.val + (strideHash θ u).val) := by
+      have := slot_i.isLt
+      have := (strideHash θ u).isLt
+      exact hS.of_le (by omega)
+    have hfit_next : Fits w slot_next.val := by
+      have := slot_next.isLt
+      exact hS.of_le (by omega)
+    set s1 := d.set regSlot (slot_i.val + (strideHash θ u).val)
+    have e1 : Exec w (.op (.exactBin .add regSlot regSlot regStride) : Code .exact 12) d s1 1 :=
+      Exec.alu (by simp +decide [StandardOp.evalExact, hslot, hstride, slot_i]) hfit_add
+    set s2 := s1.set regSlot slot_next.val
+    have e2 : Exec w (.op (.exactBin .and regSlot regSlot regMaskM) : Code .exact 12) s1 s2 1 := by
+      refine Exec.alu ?_ hfit_next
+      have hs1_slot : s1.regs regSlot = slot_i.val + (strideHash θ u).val := by
+        simp +decide [s1]
+      have hs1_mask : s1.regs regMaskM = numBuckets n_max - 1 := by
+        simp +decide [s1, hmask]
+      change some (s1.regs regSlot &&& s1.regs regMaskM) = some slot_next.val
+      rw [hs1_slot, hs1_mask]
+      exact congrArg some (val_probePerm_succ θ u hi1_lt).symm
+    have hwf_s2 : SlotArrayWF base U n_max s2.mem := by simpa [s2, s1, hmem] using hwf
+    obtain ⟨s3, e3, hs3_mem, hs3_cond, hs3_regs⟩ :=
+      probeCheckCode_execWithin hS hwf_s2 u slot_next
+        (by simp +decide [s2, s1, hsbase])
+        (by simp +decide [s2])
+        (by simp +decide [s2, s1, hm])
+        (by simp +decide [s2, s1, hzero])
+        (by simp +decide [s2, s1, hu])
+    have eStep : ExecWithin w probeStepCode d s3 11 :=
+      (e1.within.seq (e2.within.seq e3)).mono (by omega)
+    have hs2_mem_eq : s2.mem = mem := hmem
+    have hs3_mem_eq : s3.mem = mem := hs3_mem.trans hs2_mem_eq
+    have hs3_slot : s3.regs regSlot = slot_next.val := by
+      rw [hs3_regs regSlot (by decide) (by decide)]
+      simp +decide [s2]
+    have hs3_cond' : s3.regs regCond = (if slot_next ∈ O then 1 else 0) := by
+      rw [hs2_mem_eq] at hs3_cond
+      exact hs3_cond
+    obtain ⟨d', eRec, hd'_mem, hd'_slot, hd'_regs⟩ :=
+      ih (i + 1) hi1_lt s3 (by omega) hs3_mem_eq
+        (by rw [hs3_regs regSlotBase (by decide) (by decide)]; simp +decide [s2, s1, hsbase])
+        (by rw [hs3_regs regMaskM (by decide) (by decide)]; simp +decide [s2, s1, hmask])
+        (by rw [hs3_regs regStride (by decide) (by decide)]; simp +decide [s2, s1, hstride])
+        (by rw [hs3_regs regM (by decide) (by decide)]; simp +decide [s2, s1, hm])
+        (by rw [hs3_regs regZero (by decide) (by decide)]; simp +decide [s2, s1, hzero])
+        (by rw [hs3_regs regU (by decide) (by decide)]; simp +decide [s2, s1, hu])
+        hs3_slot
+        hs3_cond'
+    refine ⟨d', (ExecWithin.loop_iter hc eStep eRec).mono (by omega), hd'_mem, hd'_slot, ?_⟩
+    intro r hr_slot hr_addr hr_cond
+    rw [hd'_regs r hr_slot hr_addr hr_cond, hs3_regs r hr_addr hr_cond]
+    simp [s2, s1, Data.set, Function.update_of_ne hr_slot]
+
+/-- Deterministic 5-instruction glue before `MultiplyShift.evalCode`: saves the stride from
+`regAddr` into `regStride`, loads the multiply-shift seed from `base + tabSpace U n_max` into
+`regCond` (`msMap regB`), and copies `regU` into `regAddr` (`msMap regX`). -/
+def opPreMSCode (U n_max : ℕ) : Code .exact 12 :=
+  .seq (.op (.copy regStride regAddr))
+  (.seq (.op (.const regAddr (tabSpace U n_max)))
+  (.seq (.op (.exactBin .add regAddr regBase regAddr))
+  (.seq (.op (.load regCond regAddr))
+        (.op (.copy regAddr regU)))))
+
+/-- Deterministic 5-instruction glue after `MultiplyShift.evalCode`: initializes `regSlotBase`,
+`regMaskM`, `regM`, and `regZero`. -/
+def opPostMSCode (U n_max : ℕ) : Code .exact 12 :=
+  .seq (.op (.const regSlotBase (slotOffset U n_max)))
+  (.seq (.op (.exactBin .add regSlotBase regBase regSlotBase))
+  (.seq (.op (.const regMaskM (numBuckets n_max - 1)))
+  (.seq (.op (.const regM (numBuckets n_max)))
+        (.op (.const regZero 0)))))
+
+/-- Hash evaluation and probe-register setup `opEvalHashesCode U n_max`
+(`8 * numChars U n_max + 41` instructions): evaluates `strideHash θ u` into `regStride`,
+`primaryHash θ u` into `regSlot`, and initializes `regSlotBase`, `regMaskM`, `regM`,
+and `regZero`. -/
+def opEvalHashesCode (U n_max : ℕ) : Code .exact 12 :=
+  .seq (.op (.copy regCond regU))
+  (.seq ((TabulatedOddStride.evalCode (numChars U n_max)).rename tabMap)
+  (.seq (opPreMSCode U n_max)
+  (.seq ((MultiplyShift.evalCode (hashBits U n_max) (bucketBits n_max)).rename msMap)
+        (opPostMSCode U n_max))))
+
+theorem opEvalHashesCode_execWithin {w base U V n_max : ℕ} {θ : Seed U n_max}
+    {s : Dictionary.State U} {x : Data 12}
+    (hS : Fits w (base + space U n_max)) (hw : 2 * hashBits U n_max ≤ w)
+    (hrep : Rep w base U V n_max θ s x) (u : Fin U) (hu : x.regs regU = u.val) :
+    ∃ d : Data 12,
+      ExecWithin w (opEvalHashesCode U n_max) x d (8 * numChars U n_max + 41) ∧
+      d.mem = x.mem ∧
+      d.regs regBase = base ∧
+      d.regs regSlot = (probePerm θ u ⟨0, numBuckets_pos n_max⟩).val ∧
+      d.regs regSlotBase = base + slotOffset U n_max ∧
+      d.regs regMaskM = numBuckets n_max - 1 ∧
+      d.regs regStride = (strideHash θ u).val ∧
+      d.regs regM = numBuckets n_max ∧
+      d.regs regZero = 0 ∧
+      d.regs regOp = x.regs regOp ∧
+      d.regs regU = u.val ∧
+      d.regs regV = x.regs regV := by
+  obtain ⟨hfit_btab, _, hfit_powM, hfit_d, _, _⟩ := fits_of_space hS
+  have hsp : space U n_max = tabSpace U n_max + 1 + 3 * numBuckets n_max := rfl
+  have hso : slotOffset U n_max = tabSpace U n_max + 1 := rfl
+  have hM : 2 ^ bucketBits n_max = numBuckets n_max := rfl
+  have hfit_2powM : Fits w (2 * 2 ^ bucketBits n_max) := hS.of_le (by omega)
+  have hfit_u : Fits w u.val := by
+    rw [fits_iff]
+    have hu_lt : u.val < 2 ^ hashBits U n_max := (encodeKey n_max u).isLt
+    have hpow : 2 ^ hashBits U n_max ≤ 2 ^ w := Nat.pow_le_pow_right two_pos (by omega)
+    exact hu_lt.trans_le hpow
+  set s1 := x.set regCond u.val
+  have e1 : Exec w (.op (.copy regCond regU) : Code .exact 12) x s1 1 := by
+    simpa [s1, hu] using (Exec.copy (B := .exact) (w := w) (d := regCond) (s := regU) (x := x))
+  have hs1_base : (s1.comap tabMap).regs TabulatedOddStride.regBase = base := by
+    simpa +decide [s1, tabMap, Data.comap] using hrep.regs_base
+  have hs1_key : (s1.comap tabMap).regs TabulatedOddStride.regKey = u.val := by
+    simp +decide [s1, tabMap, Data.comap]
+  obtain ⟨yTab, htab_exec, hyTab_out, hyTab_base, hyTab_mem⟩ :=
+    TabulatedOddStride.evalCode_execWithin hrep.tab_rep hs1_base hs1_key
+      hfit_btab hfit_2powM hfit_d hfit_u
+  set s2 := yTab.extend tabMap s1
+  have e2 : ExecWithin w ((TabulatedOddStride.evalCode (numChars U n_max)).rename tabMap)
+      s1 s2 (8 * numChars U n_max + 21) :=
+    htab_exec.rename injective_tabMap
+  have hs2_mem : s2.mem = x.mem := by
+    change yTab.mem = x.mem
+    exact hyTab_mem
+  have hs2_base : s2.regs regBase = base := by
+    change (s2.comap tabMap).regs TabulatedOddStride.regBase = base
+    rw [Data.comap_extend injective_tabMap]
+    exact hyTab_base
+  have hs2_addr : s2.regs regAddr = (strideHash θ u).val := by
+    change (s2.comap tabMap).regs TabulatedOddStride.regOut = (strideHash θ u).val
+    rw [Data.comap_extend injective_tabMap]
+    exact hyTab_out
+  have hs2_op : s2.regs regOp = x.regs regOp := by
+    rw [Data.extend_regs_of_notMem _ _ (notMem_range_tabMap (by decide))]
+    simp +decide [s1]
+  have hs2_u : s2.regs regU = u.val := by
+    rw [Data.extend_regs_of_notMem _ _ (notMem_range_tabMap (by decide))]
+    simp +decide [s1, hu]
+  have hs2_v : s2.regs regV = x.regs regV := by
+    rw [Data.extend_regs_of_notMem _ _ (notMem_range_tabMap (by decide))]
+    simp +decide [s1]
+  -- Execute opPreMSCode
+  have hfit_tab : Fits w (tabSpace U n_max) := hfit_btab.of_le (by omega)
+  set s3 := s2.set regStride (strideHash θ u).val
+  have e3 : Exec w (.op (.copy regStride regAddr) : Code .exact 12) s2 s3 1 := by
+    simpa [s3, hs2_addr] using
+      (Exec.copy (B := .exact) (w := w) (d := regStride) (s := regAddr) (x := s2))
+  set s4 := s3.set regAddr (tabSpace U n_max)
+  have e4 : Exec w (.op (.const regAddr (tabSpace U n_max)) : Code .exact 12) s3 s4 1 :=
+    Exec.const hfit_tab
+  set s5 := s4.set regAddr (base + tabSpace U n_max)
+  have e5 : Exec w (.op (.exactBin .add regAddr regBase regAddr) : Code .exact 12) s4 s5 1 :=
+    Exec.alu (by simp +decide [StandardOp.evalExact, s4, s3, hs2_base]) hfit_btab
+  set s6 := s5.set regCond θ.1.val
+  have e6 : Exec w (.op (.load regCond regAddr) : Code .exact 12) s5 s6 1 := by
+    simpa +decide [s6, s5, s4, s3, hs2_mem, hrep.ms_seed] using
+      (Exec.load (B := .exact) (w := w) (d := regCond) (a := regAddr) (x := s5))
+  set s7 := s6.set regAddr u.val
+  have e7 : Exec w (.op (.copy regAddr regU) : Code .exact 12) s6 s7 1 := by
+    simpa +decide [s7, s6, s5, s4, s3, hs2_u] using
+      (Exec.copy (B := .exact) (w := w) (d := regAddr) (s := regU) (x := s6))
+  have ePre : Exec w (opPreMSCode U n_max) s2 s7 5 :=
+    e3.seq (e4.seq (e5.seq (e6.seq e7)))
+  -- Execute MultiplyShift.evalCode
+  have hs7_b : (s7.comap msMap).regs MultiplyShift.regB = θ.1.val := by
+    simp +decide [s7, s6, msMap, Data.comap]
+  have hs7_x : (s7.comap msMap).regs MultiplyShift.regX = (encodeKey n_max u).val := by
+    simp +decide [s7, msMap, Data.comap, encodeKey]
+  have hms_eval :=
+    MultiplyShift.evalCode_exec (w₀ := hashBits U n_max) (M := bucketBits n_max) (w := w)
+      (hashBits_pos U n_max) hw
+      (by rw [hs7_b]; exact θ.1.isLt)
+      (by rw [hs7_x]; exact (encodeKey n_max u).isLt)
+  set yMS := MultiplyShift.evalData (hashBits U n_max) (bucketBits n_max) (s7.comap msMap)
+  set s8 := yMS.extend msMap s7
+  have e8 : Exec w ((MultiplyShift.evalCode (hashBits U n_max) (bucketBits n_max)).rename msMap)
+      s7 s8 9 :=
+    hms_eval.rename injective_msMap
+  have hs8_mem : s8.mem = x.mem := by
+    change (s7.comap msMap).mem = x.mem
+    exact hs2_mem
+  have hs8_slot : s8.regs regSlot = (primaryHash θ u).val := by
+    change (s8.comap msMap).regs MultiplyShift.regOut = (primaryHash θ u).val
+    rw [Data.comap_extend injective_msMap]
+    exact MultiplyShift.evalData_regs_out_eq_multiplyShift
+      (hashBits U n_max) (bucketBits n_max) (s7.comap msMap) θ.1 (encodeKey n_max u) hs7_b hs7_x
+  have hs8_base : s8.regs regBase = base := by
+    rw [Data.extend_regs_of_notMem _ _ (notMem_range_msMap (by decide))]
+    simp +decide [s7, s6, s5, s4, s3, hs2_base]
+  have hs8_stride : s8.regs regStride = (strideHash θ u).val := by
+    rw [Data.extend_regs_of_notMem _ _ (notMem_range_msMap (by decide))]
+    simp +decide [s7, s6, s5, s4, s3]
+  have hs8_op : s8.regs regOp = x.regs regOp := by
+    rw [Data.extend_regs_of_notMem _ _ (notMem_range_msMap (by decide))]
+    simp +decide [s7, s6, s5, s4, s3, hs2_op]
+  have hs8_u : s8.regs regU = u.val := by
+    rw [Data.extend_regs_of_notMem _ _ (notMem_range_msMap (by decide))]
+    simp +decide [s7, s6, s5, s4, s3, hs2_u]
+  have hs8_v : s8.regs regV = x.regs regV := by
+    rw [Data.extend_regs_of_notMem _ _ (notMem_range_msMap (by decide))]
+    simp +decide [s7, s6, s5, s4, s3, hs2_v]
+  -- Execute opPostMSCode
+  have hfit_so : Fits w (slotOffset U n_max) := hS.of_le (by omega)
+  have hfit_bso : Fits w (base + slotOffset U n_max) := hS.of_le (by omega)
+  have hfit_mask : Fits w (numBuckets n_max - 1) := hS.of_le (by omega)
+  have hfit_m : Fits w (numBuckets n_max) := hS.of_le (by omega)
+  have hfit_0 : Fits w 0 := hS.of_le (by omega)
+  set s9 := s8.set regSlotBase (slotOffset U n_max)
+  have e9 : Exec w (.op (.const regSlotBase (slotOffset U n_max)) : Code .exact 12) s8 s9 1 :=
+    Exec.const hfit_so
+  set s10 := s9.set regSlotBase (base + slotOffset U n_max)
+  have e10 : Exec w (.op (.exactBin .add regSlotBase regBase regSlotBase) : Code .exact 12)
+      s9 s10 1 :=
+    Exec.alu (by simp +decide [StandardOp.evalExact, s9, hs8_base]) hfit_bso
+  set s11 := s10.set regMaskM (numBuckets n_max - 1)
+  have e11 : Exec w (.op (.const regMaskM (numBuckets n_max - 1)) : Code .exact 12) s10 s11 1 :=
+    Exec.const hfit_mask
+  set s12 := s11.set regM (numBuckets n_max)
+  have e12 : Exec w (.op (.const regM (numBuckets n_max)) : Code .exact 12) s11 s12 1 :=
+    Exec.const hfit_m
+  set s13 := s12.set regZero 0
+  have e13 : Exec w (.op (.const regZero 0) : Code .exact 12) s12 s13 1 :=
+    Exec.const hfit_0
+  have ePost : Exec w (opPostMSCode U n_max) s8 s13 5 :=
+    e9.seq (e10.seq (e11.seq (e12.seq e13)))
+  have eAll : ExecWithin w (opEvalHashesCode U n_max) x s13 (8 * numChars U n_max + 41) :=
+    (e1.within.seq (e2.seq (ePre.within.seq (e8.within.seq ePost.within)))).mono (by omega)
+  refine ⟨s13, eAll, hs8_mem,
+    by simp +decide [s13, s12, s11, s10, s9, hs8_base],
+    by rw [probePerm_zero]; simp +decide [s13, s12, s11, s10, s9, hs8_slot],
+    by simp +decide [s13, s12, s11, s10],
+    by simp +decide [s13, s12, s11],
+    by simp +decide [s13, s12, s11, s10, s9, hs8_stride],
+    by simp +decide [s13, s12],
+    by simp +decide [s13],
+    by simp +decide [s13, s12, s11, s10, s9, hs8_op],
+    by simp +decide [s13, s12, s11, s10, s9, hs8_u],
+    by simp +decide [s13, s12, s11, s10, s9, hs8_v]⟩
+
+/-- Lookup completion program `finishGetCode` (`≤ 9` instructions): inspects `used[regSlot]`;
+if `0`, writes `0` (`none`) into `regOp`, and if `1`, loads `val[regSlot]` and writes
+`val[regSlot] + 1` (`some v`) into `regOp`. -/
+def finishGetCode : Code .exact 12 :=
+  .seq (.op (.exactBin .add regAddr regSlotBase regSlot))
+  (.seq (.op (.load regCond regAddr))
+        (.branch (.eq regCond regZero)
+          (.op (.const regOp 0))
+          (.seq (.op (.exactBin .add regAddr regAddr regM))
+          (.seq (.op (.exactBin .add regAddr regAddr regM))
+          (.seq (.op (.load regOp regAddr))
+          (.seq (.op (.const regCond 1))
+                (.op (.exactBin .add regOp regOp regCond))))))))
+
+theorem finishGetCode_execWithin {w base U V n_max : ℕ} {θ : Seed U n_max}
+    {s : Dictionary.State U} {x d : Data 12}
+    (hS : Fits w (base + space U n_max)) (hV : Fits w V)
+    (hrep : Rep w base U V n_max θ s x)
+    (u : Fin U)
+    (hO : (otherOccupiedSlots (extractSlots base U n_max x.mem) u).card < numBuckets n_max)
+    (hmem : d.mem = x.mem)
+    (hbase : d.regs regBase = base)
+    (hsbase : d.regs regSlotBase = base + slotOffset U n_max)
+    (hslot : d.regs regSlot = (targetSlot (probePerm θ) (extractSlots base U n_max x.mem) u hO).val)
+    (hm : d.regs regM = numBuckets n_max)
+    (hzero : d.regs regZero = 0) :
+    ∃ y : Data 12,
+      ExecWithin w finishGetCode d y 9 ∧
+      y.mem = x.mem ∧
+      y.regs regBase = base ∧
+      y.regs regOp = (match s u with | none => 0 | some v => v + 1) := by
+  let T := extractSlots base U n_max x.mem
+  let slot := targetSlot (probePerm θ) T u hO
+  have hslot_lt := slot.isLt
+  have hsp : space U n_max = slotOffset U n_max + 3 * numBuckets n_max := rfl
+  have hfit_0 : Fits w 0 := hS.of_le (by omega)
+  have hfit_1 : Fits w 1 := hS.of_le (by omega)
+  let sBase := base + slotOffset U n_max
+  let m := numBuckets n_max
+  have hfit_a0 : Fits w (sBase + slot.val) := hS.of_le (by omega)
+  have hfit_a1 : Fits w (sBase + slot.val + m) := hS.of_le (by omega)
+  have hfit_a2 : Fits w (sBase + slot.val + m + m) := hS.of_le (by omega)
+  set s1 := d.set regAddr (sBase + slot.val)
+  have e1 : Exec w (.op (.exactBin .add regAddr regSlotBase regSlot) : Code .exact 12) d s1 1 :=
+    Exec.alu (by simp +decide [StandardOp.evalExact, hsbase, hslot, sBase, slot, T]) hfit_a0
+  let usedVal := x.mem (sBase + slot.val)
+  set s2 := s1.set regCond usedVal
+  have e2 : Exec w (.op (.load regCond regAddr) : Code .exact 12) s1 s2 1 := by
+    simpa +decide [s2, s1, hmem, usedVal] using
+      (Exec.load (B := .exact) (w := w) (d := regCond) (a := regAddr) (x := s1))
+  have htarget := hrep.table_rep.apply_targetSlot u hO
+  cases hsu : s u with
+  | none =>
+    have hT_none : extractSlots base U n_max x.mem slot = none := by
+      simpa [slot, T, hsu] using htarget
+    have hused0 : usedVal = 0 := (extractSlots_eq_none_iff hrep.slot_wf slot).mp hT_none
+    have hc : (Cond.eq regCond regZero).Holds s2 := by
+      simp +decide [Cond.Holds, s2, s1, hused0, hzero]
+    set s3 := s2.set regOp 0
+    have e3 : Exec w (.op (.const regOp 0) : Code .exact 12) s2 s3 1 := Exec.const hfit_0
+    refine ⟨s3,
+      (e1.within.seq (e2.within.seq (ExecWithin.branch_pos hc e3.within))).mono (by omega),
+      hmem, by simp +decide [s3, s2, s1, hbase], by simp +decide [s3]⟩
+  | some v =>
+    have hT_some : extractSlots base U n_max x.mem slot = some (u, v) := by
+      simpa [slot, T, hsu] using htarget
+    obtain ⟨hused1, _, hval_eq⟩ := (extractSlots_eq_some_iff hrep.slot_wf slot u v).mp hT_some
+    have hv_lt : v < V := hrep.vals_bounded u v hsu
+    have hfit_v1 : Fits w (v + 1) := hV.of_le (by omega)
+    have hc : ¬(Cond.eq regCond regZero).Holds s2 := by
+      simp +decide [Cond.Holds, s2, s1, usedVal, sBase, hused1, hzero]
+    set s3 := s2.set regAddr (sBase + slot.val + m)
+    have e3 : Exec w (.op (.exactBin .add regAddr regAddr regM) : Code .exact 12) s2 s3 1 :=
+      Exec.alu (by simp +decide [StandardOp.evalExact, s2, s1, hm, m]) hfit_a1
+    set s4 := s3.set regAddr (sBase + slot.val + m + m)
+    have e4 : Exec w (.op (.exactBin .add regAddr regAddr regM) : Code .exact 12) s3 s4 1 :=
+      Exec.alu (by simp +decide [StandardOp.evalExact, s3, s2, s1, hm, m]) hfit_a2
+    have haddr2_eq :
+        sBase + slot.val + m + m = base + slotOffset U n_max + 2 * numBuckets n_max + slot.val := by
+      dsimp only [sBase, m]
+      omega
+    set s5 := s4.set regOp v
+    have e5 : Exec w (.op (.load regOp regAddr) : Code .exact 12) s4 s5 1 := by
+      simpa +decide [s5, s4, s3, s2, s1, hmem, haddr2_eq, hval_eq] using
+        (Exec.load (B := .exact) (w := w) (d := regOp) (a := regAddr) (x := s4))
+    set s6 := s5.set regCond 1
+    have e6 : Exec w (.op (.const regCond 1) : Code .exact 12) s5 s6 1 := Exec.const hfit_1
+    set s7 := s6.set regOp (v + 1)
+    have e7 : Exec w (.op (.exactBin .add regOp regOp regCond) : Code .exact 12) s6 s7 1 :=
+      Exec.alu (by simp +decide [StandardOp.evalExact, s6, s5]) hfit_v1
+    refine ⟨s7,
+      (e1.within.seq (e2.within.seq
+        (ExecWithin.branch_neg hc
+          (e3.within.seq (e4.within.seq (e5.within.seq (e6.within.seq e7.within))))))).mono
+        (by omega),
+      hmem, by simp +decide [s7, s6, s5, s4, s3, s2, s1, hbase], by simp +decide [s7]⟩
+
+/-- Insertion completion program `finishInsertCode` (`8` instructions): writes `used[regSlot] := 1`,
+`key[regSlot] := regU`, `val[regSlot] := regV`, and sets `regOp := 0`. -/
+def finishInsertCode : Code .exact 12 :=
+  .seq (.op (.exactBin .add regAddr regSlotBase regSlot))
+  (.seq (.op (.const regCond 1))
+  (.seq (.op (.store regAddr regCond))
+  (.seq (.op (.exactBin .add regAddr regAddr regM))
+  (.seq (.op (.store regAddr regU))
+  (.seq (.op (.exactBin .add regAddr regAddr regM))
+  (.seq (.op (.store regAddr regV))
+        (.op (.const regOp 0))))))))
+
+theorem finishInsertCode_execWithin {w base U V n_max : ℕ} {θ : Seed U n_max}
+    {s : Dictionary.State U} {x d : Data 12}
+    (hS : Fits w (base + space U n_max))
+    (hrep : Rep w base U V n_max θ s x)
+    (u : Fin U) (v : ℕ)
+    (hvalid : ((Dictionary.spec U V n_max).valid s (.insert u v)))
+    (hO : (otherOccupiedSlots (extractSlots base U n_max x.mem) u).card < numBuckets n_max)
+    (hmem : d.mem = x.mem)
+    (hbase : d.regs regBase = base)
+    (hsbase : d.regs regSlotBase = base + slotOffset U n_max)
+    (hslot : d.regs regSlot = (targetSlot (probePerm θ) (extractSlots base U n_max x.mem) u hO).val)
+    (hm : d.regs regM = numBuckets n_max)
+    (hu : d.regs regU = u.val)
+    (hv : d.regs regV = v) :
+    ∃ y : Data 12,
+      ExecWithin w finishInsertCode d y 8 ∧
+      y.regs regBase = base ∧
+      y.regs regOp = 0 ∧
+      TabulatedOddStride.Rep base (charBits n_max) (numChars U n_max)
+        (bucketBits n_max) θ.2 y.mem ∧
+      y.mem (base + tabSpace U n_max) = θ.1.val ∧
+      SlotArrayWF base U n_max y.mem ∧
+      TableRep (probePerm θ) (Function.update s u (some v)) (extractSlots base U n_max y.mem) ∧
+      (Dictionary.dom (Function.update s u (some v))).card ≤ n_max ∧
+      Dictionary.ValuesBounded V (Function.update s u (some v)) ∧
+      Modifies (Block.mk base (space U n_max)).footprint x.mem y.mem := by
+  let T := extractSlots base U n_max x.mem
+  let slot := targetSlot (probePerm θ) T u hO
+  have hslot_lt := slot.isLt
+  have hsp : space U n_max = slotOffset U n_max + 3 * numBuckets n_max := rfl
+  have hso : slotOffset U n_max = tabSpace U n_max + 1 := rfl
+  have htab_eq : tabSpace U n_max = 4 + numChars U n_max * 2 ^ charBits n_max := rfl
+  have hfit_0 : Fits w 0 := hS.of_le (by omega)
+  have hfit_1 : Fits w 1 := hS.of_le (by omega)
+  let sBase := base + slotOffset U n_max
+  let m := numBuckets n_max
+  have hfit_a0 : Fits w (sBase + slot.val) := hS.of_le (by omega)
+  have hfit_a1 : Fits w (sBase + slot.val + m) := hS.of_le (by omega)
+  have hfit_a2 : Fits w (sBase + slot.val + m + m) := hS.of_le (by omega)
+  have ha1_eq : sBase + slot.val + m = sBase + m + slot.val := by omega
+  have ha2_eq : sBase + slot.val + m + m = sBase + 2 * m + slot.val := by omega
+  set s1 := d.set regAddr (sBase + slot.val)
+  have e1 : Exec w (.op (.exactBin .add regAddr regSlotBase regSlot) : Code .exact 12) d s1 1 :=
+    Exec.alu (by simp +decide [StandardOp.evalExact, hsbase, hslot, sBase, slot, T]) hfit_a0
+  set s2 := s1.set regCond 1
+  have e2 : Exec w (.op (.const regCond 1) : Code .exact 12) s1 s2 1 := Exec.const hfit_1
+  set s3 := s2.write (sBase + slot.val) 1
+  have e3 : Exec w (.op (.store regAddr regCond) : Code .exact 12) s2 s3 1 := by
+    simpa +decide [s3, s2, s1] using
+      (Exec.store (B := .exact) (w := w) (a := regAddr) (s := regCond) (x := s2))
+  set s4 := s3.set regAddr (sBase + slot.val + m)
+  have e4 : Exec w (.op (.exactBin .add regAddr regAddr regM) : Code .exact 12) s3 s4 1 :=
+    Exec.alu (by simp +decide [StandardOp.evalExact, s3, s2, s1, hm, m]) hfit_a1
+  set s5 := s4.write (sBase + m + slot.val) u.val
+  have e5 : Exec w (.op (.store regAddr regU) : Code .exact 12) s4 s5 1 := by
+    simpa +decide [s5, s4, s3, s2, s1, ha1_eq, hu] using
+      (Exec.store (B := .exact) (w := w) (a := regAddr) (s := regU) (x := s4))
+  set s6 := s5.set regAddr (sBase + slot.val + m + m)
+  have e6 : Exec w (.op (.exactBin .add regAddr regAddr regM) : Code .exact 12) s5 s6 1 :=
+    Exec.alu (by simp +decide [StandardOp.evalExact, s5, s4, s3, s2, s1, hm, m]) hfit_a2
+  set s7 := s6.write (sBase + 2 * m + slot.val) v
+  have e7 : Exec w (.op (.store regAddr regV) : Code .exact 12) s6 s7 1 := by
+    simpa +decide [s7, s6, s5, s4, s3, s2, s1, ha2_eq, hv] using
+      (Exec.store (B := .exact) (w := w) (a := regAddr) (s := regV) (x := s6))
+  set s8 := s7.set regOp 0
+  have e8 : Exec w (.op (.const regOp 0) : Code .exact 12) s7 s8 1 := Exec.const hfit_0
+  have eAll := (e1.seq (e2.seq (e3.seq (e4.seq (e5.seq (e6.seq (e7.seq e8))))))).within
+  have hs8_mem_below : ∀ a < sBase, s8.mem a = x.mem a := by
+    intro a ha
+    have hne0 : a ≠ sBase + slot.val := by omega
+    have hne1 : a ≠ sBase + m + slot.val := by omega
+    have hne2 : a ≠ sBase + 2 * m + slot.val := by omega
+    simp [s8, s7, s6, s5, s4, s3, s2, s1, Data.write,
+      Function.update_of_ne hne0, Function.update_of_ne hne1, Function.update_of_ne hne2, hmem]
+  have htab : TabulatedOddStride.Rep base (charBits n_max) (numChars U n_max)
+      (bucketBits n_max) θ.2 s8.mem := by
+    rcases hrep.tab_rep with ⟨hm0, hm1, hm2, hm3, hmt⟩
+    refine ⟨?_, ?_, ?_, ?_, fun i => ?_⟩
+    · rw [hs8_mem_below base (by omega), hm0]
+    · rw [hs8_mem_below (base + 1) (by omega), hm1]
+    · rw [hs8_mem_below (base + 2) (by omega), hm2]
+    · rw [hs8_mem_below (base + 3) (by omega), hm3]
+    · have hi := i.isLt
+      rw [hs8_mem_below (base + 4 + i.val) (by omega), hmt i]
+  have hms : s8.mem (base + tabSpace U n_max) = θ.1.val := by
+    rw [hs8_mem_below (base + tabSpace U n_max) (by omega), hrep.ms_seed]
+  have hs8_slot0 : s8.mem (sBase + slot.val) = 1 := by
+    have hne2 : sBase + slot.val ≠ sBase + 2 * m + slot.val := by omega
+    have hne1 : sBase + slot.val ≠ sBase + m + slot.val := by omega
+    simp [s8, s7, s6, s5, s4, s3, Data.write,
+      Function.update_of_ne hne2, Function.update_of_ne hne1]
+  have hs8_slot1 : s8.mem (sBase + m + slot.val) = u.val := by
+    have hne2 : sBase + m + slot.val ≠ sBase + 2 * m + slot.val := by omega
+    simp [s8, s7, s6, s5, Data.write, Function.update_of_ne hne2]
+  have hs8_slot2 : s8.mem (sBase + 2 * m + slot.val) = v := by
+    simp [s8, s7, Data.write]
+  have hwf : SlotArrayWF base U n_max s8.mem := by
+    intro j
+    have hj := j.isLt
+    by_cases hjs : j = slot
+    · subst hjs
+      exact ⟨Or.inr hs8_slot0, fun _ => hs8_slot1 ▸ u.isLt⟩
+    · have hne_val : j.val ≠ slot.val := fun h => hjs (Fin.ext h)
+      have h0 : s8.mem (sBase + j.val) = x.mem (sBase + j.val) := by
+        simp [s8, s7, s6, s5, s4, s3, s2, s1, Data.write,
+          Function.update_of_ne (show sBase + j.val ≠ sBase + 2 * m + slot.val by omega),
+          Function.update_of_ne (show sBase + j.val ≠ sBase + m + slot.val by omega),
+          Function.update_of_ne (show sBase + j.val ≠ sBase + slot.val by omega), hmem]
+      have h1 : s8.mem (sBase + m + j.val) = x.mem (sBase + m + j.val) := by
+        simp [s8, s7, s6, s5, s4, s3, s2, s1, Data.write,
+          Function.update_of_ne (show sBase + m + j.val ≠ sBase + 2 * m + slot.val by omega),
+          Function.update_of_ne (show sBase + m + j.val ≠ sBase + m + slot.val by omega),
+          Function.update_of_ne (show sBase + m + j.val ≠ sBase + slot.val by omega), hmem]
+      have hwf_j := hrep.slot_wf j
+      change (s8.mem (sBase + j.val) = 0 ∨ s8.mem (sBase + j.val) = 1) ∧
+        (s8.mem (sBase + j.val) = 1 → s8.mem (sBase + m + j.val) < U)
+      rw [h0, h1]
+      exact hwf_j
+  have hext : extractSlots base U n_max s8.mem =
+      tableInsert (numBuckets_pos n_max) (probePerm θ) T u v := by
+    rw [tableInsert_eq_update_targetSlot (numBuckets_pos n_max) (probePerm θ) T u v hO]
+    funext j
+    have hj := j.isLt
+    by_cases hjs : j = slot
+    · subst hjs
+      simp only [slot, Function.update_self]
+      rw [extractSlots_eq_some_iff hwf]
+      exact ⟨hs8_slot0, hs8_slot1, hs8_slot2⟩
+    · have hne_val : j.val ≠ slot.val := fun h => hjs (Fin.ext h)
+      simp only [slot, Function.update_of_ne hjs]
+      have h0 : s8.mem (sBase + j.val) = x.mem (sBase + j.val) := by
+        simp [s8, s7, s6, s5, s4, s3, s2, s1, Data.write,
+          Function.update_of_ne (show sBase + j.val ≠ sBase + 2 * m + slot.val by omega),
+          Function.update_of_ne (show sBase + j.val ≠ sBase + m + slot.val by omega),
+          Function.update_of_ne (show sBase + j.val ≠ sBase + slot.val by omega), hmem]
+      have h1 : s8.mem (sBase + m + j.val) = x.mem (sBase + m + j.val) := by
+        simp [s8, s7, s6, s5, s4, s3, s2, s1, Data.write,
+          Function.update_of_ne (show sBase + m + j.val ≠ sBase + 2 * m + slot.val by omega),
+          Function.update_of_ne (show sBase + m + j.val ≠ sBase + m + slot.val by omega),
+          Function.update_of_ne (show sBase + m + j.val ≠ sBase + slot.val by omega), hmem]
+      have h2 : s8.mem (sBase + 2 * m + j.val) = x.mem (sBase + 2 * m + j.val) := by
+        simp [s8, s7, s6, s5, s4, s3, s2, s1, Data.write,
+          Function.update_of_ne (show sBase + 2 * m + j.val ≠ sBase + 2 * m + slot.val by omega),
+          Function.update_of_ne (show sBase + 2 * m + j.val ≠ sBase + m + slot.val by omega),
+          Function.update_of_ne (show sBase + 2 * m + j.val ≠ sBase + slot.val by omega), hmem]
+      change extractSlots base U n_max s8.mem j = extractSlots base U n_max x.mem j
+      dsimp only [extractSlots]
+      rw [show base + slotOffset U n_max + j.val = sBase + j.val from rfl,
+        show base + slotOffset U n_max + numBuckets n_max + j.val = sBase + m + j.val from rfl,
+        show base + slotOffset U n_max + 2 * numBuckets n_max + j.val =
+          sBase + 2 * m + j.val from rfl,
+        h0, h1, h2]
+  have htrep : TableRep (probePerm θ) (Function.update s u (some v))
+      (extractSlots base U n_max s8.mem) := by
+    rw [hext]
+    exact hrep.table_rep.tableInsert (numBuckets_pos n_max) u v hO
+  have hdom_le : (Dictionary.dom (Function.update s u (some v))).card ≤ n_max :=
+    Dictionary.card_dom_step_le_of_valid (V := V) hrep.dom_le (o := .insert u v) hvalid
+  have hvals : Dictionary.ValuesBounded V (Function.update s u (some v)) :=
+    Dictionary.valuesBounded_step_of_valid (n_max := n_max) hrep.vals_bounded
+      (o := .insert u v) hvalid
+  have hmod : Modifies (Block.mk base (space U n_max)).footprint x.mem s8.mem := by
+    intro a ha
+    have ha_out : a < base ∨ base + space U n_max ≤ a := by
+      by_contra h
+      rw [not_or, not_lt, not_le] at h
+      exact ha (mem_footprint_of_lt_space h.1 h.2)
+    have hne0 : a ≠ sBase + slot.val := by omega
+    have hne1 : a ≠ sBase + m + slot.val := by omega
+    have hne2 : a ≠ sBase + 2 * m + slot.val := by omega
+    simp [s8, s7, s6, s5, s4, s3, s2, s1, Data.write,
+      Function.update_of_ne hne0, Function.update_of_ne hne1, Function.update_of_ne hne2, hmem]
+  exact ⟨s8, eAll,
+    by simp +decide [s8, s7, s6, s5, s4, s3, s2, s1, hbase],
+    by simp +decide [s8],
+    htab, hms, hwf, htrep, hdom_le, hvals, hmod⟩
+
+/-- Complete operation body `opCode U n_max` for both `get` and `insert`. -/
+def opCode (U n_max : ℕ) : Code .exact 12 :=
+  .seq (opEvalHashesCode U n_max)
+  (.seq probeCheckCode
+  (.seq probeLoop
+        (.branch (.eq regOp regZero) finishGetCode finishInsertCode)))
+
+/-- Exact pathwise instruction budget
+`13 * probeCount T u (probePerm θ u) + 8 * numChars U n_max + 49` for `opCode U n_max` on table `T`
+and key `u`. -/
+noncomputable def opPathSteps (U n_max : ℕ) (θ : Seed U n_max)
+    (T : UniformProbing.Table U (numBuckets n_max)) (u : Fin U) : ℕ :=
+  13 * probeCount T u (probePerm θ u) + 8 * numChars U n_max + 49
+
+/-- Worst-case instruction bound `13 * numBuckets n_max + 8 * numChars U n_max + 49` for
+`opCode`. -/
+def opSteps (U n_max : ℕ) : ℕ :=
+  13 * numBuckets n_max + 8 * numChars U n_max + 49
+
+theorem opPathSteps_le_opSteps {U n_max : ℕ} (θ : Seed U n_max)
+    (T : UniformProbing.Table U (numBuckets n_max)) (u : Fin U)
+    (hO : (otherOccupiedSlots T u).card < numBuckets n_max) :
+    opPathSteps U n_max θ T u ≤ opSteps U n_max := by
+  dsimp only [opPathSteps, opSteps, probeCount, unsuccessfulProbes]
+  have hlt := missedProbes_lt_of_card_lt hO (probePerm θ u)
+  omega
+
+/-- Key extracted from a `Dictionary.Op U`. -/
+def opKey {U : ℕ} : Dictionary.Op U → Fin U
+  | .get u => u
+  | .insert u _ => u
+
+/-- Operation tag (`0` for `get`, `1` for `insert`). -/
+def opTag {U : ℕ} : Dictionary.Op U → ℕ
+  | .get _ => 0
+  | .insert _ _ => 1
+
+/-- Encoded output word in `regOp` after executing `op` from state `s`. -/
+def opOutWord {U : ℕ} (s : Dictionary.State U) : Dictionary.Op U → ℕ
+  | .get u => match s u with | none => 0 | some v => v + 1
+  | .insert _ _ => 0
+
+/-- **Pathwise correctness and complexity of `opCode U n_max`**: for any seed `θ`, dictionary
+state `s`, machine state `x` satisfying `Rep w base U V n_max θ s x`, and admissible operation
+`op`, `opCode U n_max` halts deterministically in at most
+`opPathSteps U n_max θ (extractSlots base U n_max x.mem) (opKey op) ≤ opSteps U n_max` instructions,
+preserving `Rep` for `((Dictionary.spec U V n_max).step s op).1`, writing `opOutWord s op` into
+`regOp`, and modifying memory only within `[base, base + space U n_max)`. -/
+theorem opCode_execWithin {w base U V n_max : ℕ} {θ : Seed U n_max}
+    {s : Dictionary.State U} {x : Data 12}
+    (hS : Fits w (base + space U n_max)) (hw : 2 * hashBits U n_max ≤ w) (hV : Fits w V)
+    (hrep : Rep w base U V n_max θ s x) (op : Dictionary.Op U)
+    (hvalid : (Dictionary.spec U V n_max).valid s op)
+    (hop : x.regs regOp = opTag op)
+    (hu : x.regs regU = (opKey op).val)
+    (hv : ∀ u v, op = .insert u v → x.regs regV = v) :
+    ∃ y : Data 12,
+      ExecWithin w (opCode U n_max) x y
+        (opPathSteps U n_max θ (extractSlots base U n_max x.mem) (opKey op)) ∧
+      Rep w base U V n_max θ ((Dictionary.spec U V n_max).step s op).1 y ∧
+      y.regs regOp = opOutWord s op ∧
+      Modifies (Block.mk base (space U n_max)).footprint x.mem y.mem := by
+  have hO :
+      (otherOccupiedSlots (extractSlots base U n_max x.mem) (opKey op)).card < numBuckets n_max :=
+    lt_of_le_of_lt (hrep.table_rep.card_otherOccupiedSlots_le (opKey op))
+      (lt_of_le_of_lt hrep.dom_le (lt_numBuckets n_max))
+  obtain ⟨d1, e1, hd1_mem, hd1_base, hd1_slot, hd1_sbase, hd1_mask, hd1_stride, hd1_m,
+      hd1_zero, hd1_op, hd1_u, hd1_v⟩ :=
+    opEvalHashesCode_execWithin hS hw hrep (opKey op) hu
+  have hwf_d1 : SlotArrayWF base U n_max d1.mem := by simpa [hd1_mem] using hrep.slot_wf
+  obtain ⟨d2, e2, hd2_mem, hd2_cond, hd2_regs⟩ :=
+    probeCheckCode_execWithin hS hwf_d1 (opKey op)
+      (probePerm θ (opKey op) ⟨0, numBuckets_pos n_max⟩)
+      hd1_sbase hd1_slot hd1_m hd1_zero hd1_u
+  have hd2_mem_eq : d2.mem = x.mem := hd2_mem.trans hd1_mem
+  have hd2_cond' : d2.regs regCond =
+      (if probePerm θ (opKey op) ⟨0, numBuckets_pos n_max⟩ ∈
+          otherOccupiedSlots (extractSlots base U n_max x.mem) (opKey op) then 1 else 0) := by
+    rw [hd1_mem] at hd2_cond
+    exact hd2_cond
+  obtain ⟨d3, e3, hd3_mem, hd3_slot, hd3_regs⟩ :=
+    probeLoop_execWithin_aux θ hS hrep.slot_wf (opKey op) hO
+      (missedProbes (otherOccupiedSlots (extractSlots base U n_max x.mem) (opKey op))
+        (probePerm θ (opKey op))) 0 (numBuckets_pos n_max) d2
+      (zero_add _) hd2_mem_eq
+      (by rw [hd2_regs regSlotBase (by decide) (by decide), hd1_sbase])
+      (by rw [hd2_regs regMaskM (by decide) (by decide), hd1_mask])
+      (by rw [hd2_regs regStride (by decide) (by decide), hd1_stride])
+      (by rw [hd2_regs regM (by decide) (by decide), hd1_m])
+      (by rw [hd2_regs regZero (by decide) (by decide), hd1_zero])
+      (by rw [hd2_regs regU (by decide) (by decide), hd1_u])
+      (by rw [hd2_regs regSlot (by decide) (by decide), hd1_slot])
+      hd2_cond'
+  have hd3_base : d3.regs regBase = base := by
+    rw [hd3_regs regBase (by decide) (by decide) (by decide),
+      hd2_regs regBase (by decide) (by decide), hd1_base]
+  have hd3_sbase : d3.regs regSlotBase = base + slotOffset U n_max := by
+    rw [hd3_regs regSlotBase (by decide) (by decide) (by decide),
+      hd2_regs regSlotBase (by decide) (by decide), hd1_sbase]
+  have hd3_m : d3.regs regM = numBuckets n_max := by
+    rw [hd3_regs regM (by decide) (by decide) (by decide),
+      hd2_regs regM (by decide) (by decide), hd1_m]
+  have hd3_zero : d3.regs regZero = 0 := by
+    rw [hd3_regs regZero (by decide) (by decide) (by decide),
+      hd2_regs regZero (by decide) (by decide), hd1_zero]
+  have hd3_op : d3.regs regOp = opTag op := by
+    rw [hd3_regs regOp (by decide) (by decide) (by decide),
+      hd2_regs regOp (by decide) (by decide), hd1_op, hop]
+  have hd3_u : d3.regs regU = (opKey op).val := by
+    rw [hd3_regs regU (by decide) (by decide) (by decide),
+      hd2_regs regU (by decide) (by decide), hd1_u]
+  have hd3_v : d3.regs regV = x.regs regV := by
+    rw [hd3_regs regV (by decide) (by decide) (by decide),
+      hd2_regs regV (by decide) (by decide), hd1_v]
+  cases op with
+  | get u₀ =>
+    have hc : (Cond.eq regOp regZero).Holds d3 := by
+      simp [Cond.Holds, hd3_op, hd3_zero, opTag]
+    obtain ⟨y, eFin, hy_mem, hy_base, hy_op⟩ :=
+      finishGetCode_execWithin hS hV hrep u₀ hO hd3_mem hd3_base hd3_sbase hd3_slot hd3_m hd3_zero
+    have eBr : ExecWithin w (.branch (.eq regOp regZero) finishGetCode finishInsertCode) d3 y 10 :=
+      ExecWithin.branch_pos hc eFin
+    have eTot : ExecWithin w (opCode U n_max) x y
+        (opPathSteps U n_max θ (extractSlots base U n_max x.mem) u₀) := by
+      refine (e1.seq (e2.seq (e3.seq eBr))).mono ?_
+      dsimp only [opPathSteps, probeCount, unsuccessfulProbes, opKey] at *
+      omega
+    have hbdd_y : y.Bounded w := eTot.bounded hrep.bounded
+    have hrep_y : Rep w base U V n_max θ s y :=
+      hrep.congr hbdd_y (hy_base.trans hrep.regs_base.symm) (fun a _ => by rw [hy_mem])
+    have hmod : Modifies (Block.mk base (space U n_max)).footprint x.mem y.mem := by
+      intro a _
+      rw [hy_mem]
+    exact ⟨y, eTot, hrep_y, hy_op, hmod⟩
+  | insert u₀ v₀ =>
+    have hc : ¬(Cond.eq regOp regZero).Holds d3 := by
+      simp [Cond.Holds, hd3_op, hd3_zero, opTag]
+    have hd3_v₀ : d3.regs regV = v₀ := hd3_v.trans (hv u₀ v₀ rfl)
+    obtain ⟨y, eFin, hy_base, hy_op, hy_tab, hy_ms, hy_wf, hy_trep, hy_dom, hy_vals, hy_mod⟩ :=
+      finishInsertCode_execWithin hS hrep u₀ v₀ hvalid hO
+        hd3_mem hd3_base hd3_sbase hd3_slot hd3_m hd3_u hd3_v₀
+    have eBr : ExecWithin w (.branch (.eq regOp regZero) finishGetCode finishInsertCode) d3 y 10 :=
+      ExecWithin.branch_neg hc eFin
+    have eTot : ExecWithin w (opCode U n_max) x y
+        (opPathSteps U n_max θ (extractSlots base U n_max x.mem) u₀) := by
+      refine (e1.seq (e2.seq (e3.seq eBr))).mono ?_
+      dsimp only [opPathSteps, probeCount, unsuccessfulProbes, opKey] at *
+      omega
+    have hbdd_y : y.Bounded w := eTot.bounded hrep.bounded
+    exact ⟨y, eTot,
+      ⟨hbdd_y, hy_base, hy_tab, hy_ms, hy_wf, hy_trep, hy_dom, hy_vals⟩,
+      hy_op, hy_mod⟩
+
+/-! ## Section 5: `SubroutineCode`, `SubroutineDS`, and Expected Probe / Collision Bounds -/
+
+/-- Relocatable `SubroutineCode` over `Basis.exact` (`12` registers, `0` runtime init parameters)
+for the open-addressed permutation-probing dictionary. -/
+def subroutineCode (U n_max : ℕ) : SubroutineCode .exact 12 0 where
+  allocSpan := allocSpan U n_max
+  initSetup := initSetup U n_max
+  code := opCode U n_max
+  frontierReg := regV
+  baseReg := regBase
+  initParams := Fin.elim0
+  curReg := regCond
+  zeroReg := regAddr
+  oneReg := regSlot
+  incCur := .exactBin .add regCond regCond regSlot
+  input := fun i => decide (i ≠ regBase)
+  output := regOp
+
+/-- Standalone argument encoder for `Dictionary.Op U` on `12` registers. -/
+def encodeOp {U : ℕ} : Dictionary.Op U → Fin 12 → ℕ
+  | .get u, i =>
+      if i = regOp then 0
+      else if i = regU then u.val
+      else 0
+  | .insert u v, i =>
+      if i = regOp then 1
+      else if i = regU then u.val
+      else if i = regV then v
+      else 0
+
+/-- Partial argument-matching predicate for inline and standalone callers. -/
+def argMatch {U : ℕ} (op : Dictionary.Op U) (regs : Fin 12 → ℕ) : Prop :=
+  regs regOp = opTag op ∧
+  regs regU = (opKey op).val ∧
+  ∀ u v, op = .insert u v → regs regV = v
+
+/-- Output decoder reading typed operation observations from final registers. -/
+def decodeOp {U V n_max : ℕ} : (op : Dictionary.Op U) → (Fin 12 → ℕ) →
+    Option ((Dictionary.spec U V n_max).Result op)
+  | .get _, regs => some (if regs regOp = 0 then none else some (regs regOp - 1))
+  | .insert _ _, _ => some ()
+
+theorem encode_matches {U n_max : ℕ} (op : Dictionary.Op U) (regs : Fin 12 → ℕ) :
+    argMatch op (fun i => if (subroutineCode U n_max).input i then encodeOp op i else regs i) := by
+  cases op with
+  | get u =>
+    refine ⟨rfl, ?_, fun _ _ h => by nomatch h⟩
+    simp +decide [subroutineCode, encodeOp, opKey]
+  | insert u v =>
+    refine ⟨rfl, ?_, fun u' v' h => ?_⟩
+    · simp +decide [subroutineCode, encodeOp, opKey]
+    · cases h
+      simp +decide [subroutineCode, encodeOp]
+
+theorem arguments_fit {w U V n_max : ℕ}
+    (hw : 2 * hashBits U n_max ≤ w) (hV : Fits w V)
+    {s : Dictionary.State U} (op : Dictionary.Op U)
+    (hv : (Dictionary.spec U V n_max).valid s op)
+    (i : Fin 12) :
+    Fits w (encodeOp op i) := by
+  have hpos_hb := hashBits_pos U n_max
+  have hfit0 : Fits w 0 := fits_zero w
+  have hfit1 : Fits w 1 := fits_one (by omega)
+  have hfitU : ∀ u : Fin U, Fits w u.val := by
+    intro u
+    rw [fits_iff]
+    have hu_lt : u.val < 2 ^ hashBits U n_max := lt_two_pow_hashBits n_max u
+    have hpow : 2 ^ hashBits U n_max ≤ 2 ^ w := Nat.pow_le_pow_right two_pos (by omega)
+    exact hu_lt.trans_le hpow
+  cases op with
+  | get u =>
+    dsimp only [encodeOp]
+    split_ifs
+    · exact hfit0
+    · exact hfitU u
+    · exact hfit0
+  | insert u v =>
+    dsimp only [encodeOp]
+    split_ifs
+    · exact hfit1
+    · exact hfitU u
+    · exact hV.of_le (by have := hv.2; omega)
+    · exact hfit0
+
+theorem decodeOp_eq_step {U V n_max : ℕ} {s : Dictionary.State U}
+    (op : Dictionary.Op U) (regs : Fin 12 → ℕ)
+    (h : regs regOp = opOutWord s op) :
+    decodeOp (V := V) (n_max := n_max) op regs =
+      some ((Dictionary.spec U V n_max).step s op).2 := by
+  cases op with
+  | get u =>
+    dsimp only [decodeOp, Dictionary.spec, opOutWord] at h ⊢
+    rw [h]
+    cases s u with
+    | none => simp
+    | some v => simp
+  | insert u v =>
+    rfl
+
+theorem step_exec_spec {w base U V n_max : ℕ}
+    (hS : Fits w (base + space U n_max)) (hw : 2 * hashBits U n_max ≤ w) (hV : Fits w V)
+    {s : Dictionary.State U} (o : Dictionary.Op U)
+    (ν : PMF (Seed U n_max × Data 12))
+    (hv : (Dictionary.spec U V n_max).valid s o)
+    (hseed : ∀ θ, (ν.map Prod.fst) θ ≤ 1 * seedLaw U n_max θ)
+    (hsupp : ∀ p ∈ ν.support, Rep w base U V n_max p.1 s p.2 ∧ argMatch o p.2.regs) :
+    ∃ (μ_step : Seed U n_max × Data 12 → PMF (Seed U n_max × Data 12))
+      (T_step : Seed U n_max × Data 12 → ℝ≥0∞),
+      (∀ p ∈ ν.support,
+        ExecCodeDist w (opCode U n_max) p.2 ((μ_step p).map Prod.snd) (T_step p) ∧
+        ∀ q ∈ (μ_step p).support,
+          decodeOp (V := V) (n_max := n_max) o q.2.regs =
+            some ((Dictionary.spec U V n_max).step s o).2 ∧
+          Rep w base U V n_max q.1 ((Dictionary.spec U V n_max).step s o).1 q.2 ∧
+          Modifies (Block.mk base (space U n_max)).footprint p.2.mem q.2.mem) ∧
+      (∀ θ', ((ν.bind μ_step).map Prod.fst) θ' ≤ 1 * seedLaw U n_max θ') ∧
+      (∑' p, ν p * (T_step p + ∑' q, μ_step p q * ((0 : ℕ) : ℝ≥0∞))) ≤
+        (opSteps U n_max : ℝ≥0∞) + ∑' p, ν p * ((0 : ℕ) : ℝ≥0∞) := by
+  classical
+  have hEx : ∀ p : Seed U n_max × Data 12, ∃ y : Data 12,
+      p ∈ ν.support →
+        ExecWithin w (opCode U n_max) p.2 y (opSteps U n_max) ∧
+        Rep w base U V n_max p.1 ((Dictionary.spec U V n_max).step s o).1 y ∧
+        y.regs regOp = opOutWord s o ∧
+        Modifies (Block.mk base (space U n_max)).footprint p.2.mem y.mem := by
+    intro p
+    by_cases hp : p ∈ ν.support
+    · obtain ⟨hrep, harg1, harg2, harg3⟩ := hsupp p hp
+      have hO :
+          (otherOccupiedSlots (extractSlots base U n_max p.2.mem) (opKey o)).card <
+            numBuckets n_max :=
+        lt_of_le_of_lt (hrep.table_rep.card_otherOccupiedSlots_le (opKey o))
+          (lt_of_le_of_lt hrep.dom_le (lt_numBuckets n_max))
+      obtain ⟨y, e, hrep_y, hout, hmod⟩ :=
+        opCode_execWithin hS hw hV hrep o hv harg1 harg2 harg3
+      exact ⟨y, fun _ => ⟨e.mono (opPathSteps_le_opSteps p.1 _ _ hO), hrep_y, hout, hmod⟩⟩
+    · exact ⟨p.2, fun h => False.elim (hp h)⟩
+  let yOf : Seed U n_max × Data 12 → Data 12 := fun p => Classical.choose (hEx p)
+  refine ⟨fun p => PMF.pure (p.1, yOf p), fun _ => (opSteps U n_max : ℝ≥0∞), ?_, ?_, ?_⟩
+  · intro p hp
+    obtain ⟨e, hrep_y, hout, hmod⟩ := Classical.choose_spec (hEx p) hp
+    refine ⟨?_, ?_⟩
+    · simpa [yOf] using ExecCodeDist.of_execWithin e
+    · intro q hq
+      rw [PMF.support_pure, Set.mem_singleton_iff] at hq
+      subst hq
+      exact ⟨decodeOp_eq_step o (yOf p).regs hout, hrep_y, hmod⟩
+  · intro θ'
+    have hmap : ((ν.bind fun p => PMF.pure (p.1, yOf p)).map Prod.fst) = ν.map Prod.fst := by
+      rw [PMF.map_bind]
+      simp only [PMF.map, PMF.pure_bind]
+      rfl
+    rw [hmap]
+    exact hseed θ'
+  · simp [ENNReal.tsum_mul_right, ν.tsum_coe]
+
+/-- **Composable randomized Word-RAM `SubroutineDS` certificate over `Basis.exact`** for the
+open-addressed permutation-probing dictionary realizing `Dictionary.spec U V n_max`. -/
+noncomputable def subroutineDS {w base U V n_max : ℕ}
+    (hS : Fits w (base + space U n_max)) (hw : 2 * hashBits U n_max ≤ w) (hV : Fits w V) :
+    Randomized.SubroutineDS (subroutineCode U n_max)
+      (Dictionary.spec U V n_max) w base Fin.elim0 (Dictionary.empty U) where
+  Seed := Seed U n_max
+  seedLaw := seedLaw U n_max
+  seedSlack := 1
+  space := space U n_max
+  spanTime := 3
+  setupTime := (setupSteps U n_max : ℝ≥0∞)
+  initPotential := 0
+  charge _ _ := opSteps U n_max
+  rep := Rep w base U V n_max
+  potential _ _ := 0
+  encode := encodeOp
+  argMatch := argMatch
+  decode := decodeOp
+  bounded hrep := hrep.bounded
+  rep_unique h1 h2 := h1.unique h2
+  arguments_fit o hv i _ := arguments_fit hw hV o hv i
+  encode_matches := encode_matches
+  rep_supported {θ s x x'} hregs hmem hbdd hrep := by
+    have hbase : x'.regs regBase = x.regs regBase := hregs regBase rfl
+    exact hrep.congr hbdd hbase hmem
+  potential_supported _ _ _ := rfl
+  clear_nodup := by
+    dsimp only [subroutineCode]
+    decide
+  params_not_clear j := Fin.elim0 j
+  incCur_eval {x} h1 hfit := by
+    dsimp only [subroutineCode] at h1 hfit ⊢
+    simp [Op.exactBin, Op.eval, StandardOp.evalExact, Data.put, h1, hfit]
+  span_exec {x} _ hfr _ := by
+    obtain ⟨x₁, he, hm, hb, hfr'⟩ := allocSpan_execWithin hS hfr
+    exact ⟨x₁, he, hm, hb, hfr', fun j => Fin.elim0 j⟩
+  setup_exec {x₁} hx₁ hb hfr _ hz :=
+    setup_exec_spec hS hw hx₁ hb hfr hz
+  step_exec {s} o ν hv hseed hsupp :=
+    step_exec_spec hS hw hV o ν hv hseed hsupp
+
+/-- Standard-basis (`Basis.standard`) randomized `SubroutineDS` certificate for the open-addressed
+permutation-probing dictionary. -/
+noncomputable abbrev subroutineDSStandard {w base U V n_max : ℕ}
+    (hS : Fits w (base + space U n_max)) (hw : 2 * hashBits U n_max ≤ w) (hV : Fits w V) :
+    Randomized.SubroutineDS (subroutineCode U n_max).toStandard
+      (Dictionary.spec U V n_max) w base Fin.elim0 (Dictionary.empty U) :=
+  (subroutineDS hS hw hV).toStandard
+
+/-- **End-to-end multi-operation expected-time theorem (`seq_expected_amortized`)**:
+from fresh zeroed memory `[base, base + space U n_max)`, initializing the permutation-probing
+dictionary (`initFresh`) and executing the subroutine operation bodies (`ExecSteps`) across any
+admissible operation history `ops : List (Dictionary.Op U)` fixed independently of the sampled seed
+(oblivious adversary) takes at most `3 + setupSteps U n_max + ops.length * opSteps U n_max` expected
+Word-RAM instructions (charging the deterministic full-cycle body bound `opSteps U n_max` per
+operation and excluding caller argument delivery, caller control/dispatch loops, and
+code/configuration construction). -/
+theorem seq_expected_amortized {w base U V n_max : ℕ}
+    (hS : Fits w (base + space U n_max)) (hw : 2 * hashBits U n_max ≤ w) (hV : Fits w V)
+    {x : Data 12} (ops : List (Dictionary.Op U))
+    (hx : x.Bounded w) (hfr : x.regs regV = base)
+    (hz : ∀ a ∈ (Block.mk base (space U n_max)).footprint, x.mem a = 0)
+    (hv : (Dictionary.spec U V n_max).ValidHistory (Dictionary.empty U) ops) :
+    ∃ (ν₀ ν_final : PMF (Seed U n_max × Data 12)) (T_ops : ℝ≥0∞),
+      ExecCodeDist w (subroutineCode U n_max).initFresh x (ν₀.map Prod.snd)
+        (subroutineDS (V := V) hS hw hV).initTime ∧
+      (subroutineDS (V := V) hS hw hV).ExecSteps (Dictionary.empty U) ops ν₀ ν_final T_ops ∧
+      (∀ θ, (ν_final.map Prod.fst) θ ≤ seedLaw U n_max θ) ∧
+      (∀ p ∈ ν_final.support,
+        Rep w base U V n_max p.1
+          ((Dictionary.spec U V n_max).run (Dictionary.empty U) ops).1 p.2) ∧
+      (subroutineDS (V := V) hS hw hV).initTime + T_ops ≤
+        (3 + setupSteps U n_max : ℝ≥0∞) +
+          ((Dictionary.spec U V n_max).totalCost (fun _ _ => opSteps U n_max)
+            (Dictionary.empty U) ops : ℝ≥0∞) := by
+  obtain ⟨ν₀, ν_final, T_ops, he_init, hex_steps, hseed_final, hrep_final, hbound⟩ :=
+    (subroutineDS (V := V) hS hw hV).seq_expected_amortized ops hx hfr (fun j => Fin.elim0 j) hz hv
+  refine ⟨ν₀, ν_final, T_ops, he_init, hex_steps, ?_, hrep_final, ?_⟩
+  · intro θ
+    have h1 : (ν_final.map Prod.fst) θ ≤ 1 * seedLaw U n_max θ := hseed_final θ
+    rwa [one_mul] at h1
+  · have hinit : (subroutineDS (V := V) hS hw hV).initTime = (3 + setupSteps U n_max : ℝ≥0∞) := rfl
+    rw [hinit]
+    have h2 : (3 + (setupSteps U n_max : ℝ≥0∞)) + T_ops +
+        ∑' q : Seed U n_max × Data 12, ν_final q * ((0 : ℕ) : ℝ≥0∞) ≤
+        (3 + (setupSteps U n_max : ℝ≥0∞)) + ((0 : ℕ) : ℝ≥0∞) +
+          ((Dictionary.spec U V n_max).totalCost (fun _ _ => opSteps U n_max)
+            (Dictionary.empty U) ops : ℝ≥0∞) := hbound
+    simpa only [Nat.cast_zero, mul_zero, tsum_zero, add_zero, Nat.cast_add, Nat.cast_ofNat] using h2
+
+/-- The first projection of `seedLaw U n_max` is the uniform distribution on multiply-shift
+seeds `Fin (2 ^ (hashBits U n_max - 1))`. -/
+theorem map_fst_seedLaw (U n_max : ℕ) :
+    (seedLaw U n_max).map Prod.fst = PMF.uniformOfFintype (Fin (2 ^ (hashBits U n_max - 1))) :=
+  Cslib.Probability.PMF.uniformOfFintype_prod_map_fst
+
+/-- **Primary-slot `2 / numBuckets n_max`-universality (`isUniversalHash_primaryHash`)**:
+the primary hash `primaryHash θ : Fin U → Fin (numBuckets n_max)` under `seedLaw U n_max` is
+`(2 / numBuckets n_max)`-universal. -/
+theorem isUniversalHash_primaryHash (U n_max : ℕ) :
+    Cslib.Probability.IsUniversalHash (seedLaw U n_max) (primaryHash (U := U) (n_max := n_max))
+      (2 / (numBuckets n_max : ℝ≥0∞)) := by
+  intro u₁ u₂ hne
+  have h1 := Cslib.Probability.isUniversalHash_multiplyShift
+    (hashBits_pos U n_max) (bucketBits_le_hashBits U n_max)
+    (encodeKey n_max u₁) (encodeKey n_max u₂)
+    (fun h => hne (encodeKey_injective n_max h))
+  rw [← map_fst_seedLaw U n_max, PMF.toOuterMeasure_map_apply] at h1
+  have heq : (Prod.fst ⁻¹' {σ : Fin (2 ^ (hashBits U n_max - 1)) |
+      Cslib.Probability.multiplyShift (hashBits U n_max) (bucketBits n_max) σ
+        (encodeKey n_max u₁) =
+      Cslib.Probability.multiplyShift (hashBits U n_max) (bucketBits n_max) σ
+        (encodeKey n_max u₂)}) =
+      {θ : Seed U n_max | primaryHash θ u₁ = primaryHash θ u₂} := by
+    ext θ
+    simp [primaryHash, Fin.ext_iff]
+  rw [heq] at h1
+  have hnum : (2 / (numBuckets n_max : ℝ≥0∞)) = 2 / 2 ^ bucketBits n_max := by
+    simp [numBuckets]
+  rw [hnum]
+  exact h1
+
+/-- **Parametric expected-step bound from any expected-probe bound**:
+for any permutation distribution `μ : PMF α` and family
+`π : α → Equiv.Perm (Fin (numBuckets n_max))` whose expected probe count on table `T` and key `u`
+is at most `B`, the expected Word-RAM instruction count of the probe path is at most
+`13 * B + (8 * numChars U n_max + 49)`. -/
+theorem expect_opPathSteps_le_of_probeBound {α : Type*} {U n_max : ℕ}
+    (μ : PMF α) (π : α → Equiv.Perm (Fin (numBuckets n_max)))
+    (T : Fin (numBuckets n_max) → Option (Fin U × ℕ)) (u : Fin U) (B : ℝ≥0∞)
+    (hB : (∑' a, μ a * (UniformProbing.probeCount T u (π a) : ℝ≥0∞)) ≤ B) :
+    (∑' a, μ a *
+      ((13 * UniformProbing.probeCount T u (π a) + 8 * numChars U n_max + 49 : ℕ) : ℝ≥0∞)) ≤
+      13 * B + (8 * numChars U n_max + 49 : ℝ≥0∞) := by
+  have hterm : ∀ a : α,
+      μ a * ((13 * UniformProbing.probeCount T u (π a) + 8 * numChars U n_max + 49 : ℕ) : ℝ≥0∞) =
+        13 * (μ a * (UniformProbing.probeCount T u (π a) : ℝ≥0∞)) +
+          μ a * (8 * numChars U n_max + 49 : ℝ≥0∞) := by
+    intro a
+    push_cast
+    ring
+  simp_rw [hterm]
+  rw [tsum_add, ENNReal.tsum_mul_left, ENNReal.tsum_mul_right, μ.tsum_coe, one_mul]
+  gcongr
+
+/-- **Ideal uniform-probing expected-step corollary (`≤ 8 * numChars U n_max + 75`)**:
+when the probe permutation `π` is drawn uniformly from `Equiv.Perm (Fin (numBuckets n_max))` on a
+table `T` with at most `n_max` other occupied slots (`(otherOccupiedSlots T u).card ≤ n_max`), the
+expected Word-RAM step count `13 * probeCount T u π + 8 * numChars U n_max + 49` is at most
+`8 * numChars U n_max + 75` (combining `expect_opPathSteps_le_of_probeBound` with `B = 2` from
+`UniformProbing.expect_unsuccessfulProbes_le_two`). -/
+theorem expect_idealProbeSteps_le {U n_max : ℕ}
+    (T : Fin (numBuckets n_max) → Option (Fin U × ℕ)) (u : Fin U)
+    (hcard : (UniformProbing.otherOccupiedSlots T u).card ≤ n_max) :
+    (∑' π : Equiv.Perm (Fin (numBuckets n_max)),
+      (PMF.uniformOfFintype (Equiv.Perm (Fin (numBuckets n_max)))) π *
+        ((13 * UniformProbing.probeCount T u π + 8 * numChars U n_max + 49 : ℕ) : ℝ≥0∞)) ≤
+      (8 * numChars U n_max + 75 : ℝ≥0∞) := by
+  have h2m : 2 * (UniformProbing.otherOccupiedSlots T u).card ≤ numBuckets n_max := by
+    have h4 := four_mul_le_numBuckets n_max
+    omega
+  have hB : (∑' π : Equiv.Perm (Fin (numBuckets n_max)),
+      (PMF.uniformOfFintype (Equiv.Perm (Fin (numBuckets n_max)))) π *
+        (UniformProbing.probeCount T u π : ℝ≥0∞)) ≤ 2 :=
+    UniformProbing.expect_unsuccessfulProbes_le_two (numBuckets_pos n_max) h2m
+  have hstep := expect_opPathSteps_le_of_probeBound (U := U) (n_max := n_max)
+    (PMF.uniformOfFintype (Equiv.Perm (Fin (numBuckets n_max)))) id T u 2 hB
+  refine hstep.trans ?_
+  have heq : (13 : ℝ≥0∞) * 2 + (8 * numChars U n_max + 49 : ℝ≥0∞) =
+      (8 * numChars U n_max + 75 : ℝ≥0∞) := by
+    ring
+  exact le_of_eq heq
+
+end Cslib.Algorithms.WordRAM.Dictionary.UniformProbing
diff --git a/ComplexityTests/WordRAMUniformProbing.lean b/ComplexityTests/WordRAMUniformProbing.lean
new file mode 100644
index 000000000..bea269a9d
--- /dev/null
+++ b/ComplexityTests/WordRAMUniformProbing.lean
@@ -0,0 +1,222 @@
+/-
+Copyright (c) 2026 Renfei Zhou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Renfei Zhou
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.Lean.UniformProbing
+public import Complexity.Algorithms.WordRAM.Dictionary.UniformProbing
+
+/-!
+# Tests for Uniform Probing (`Lean.UniformProbing` and `WordRAM.Dictionary.UniformProbing`)
+
+This test file verifies:
+1. Concrete open-addressed probing behavior (`tableGet`, `tableInsert`, `runTable`, `probeCount`)
+   under primary-slot collisions and in-place updates, together with the textbook expected-probe
+   bounds (`≤ m / (m - n) ≤ 2` for unsuccessful lookups by [CLRS2009], third edition, Theorem 11.6
+   and Corollary 11.7, pp. 274–276, and for fixed-key successful lookups via the insertion-cost
+   identity and intermediate bound from the proof of Theorem 11.8, p. 276) and lazy random-oracle
+   equivalence in `Cslib.Algorithms.Lean.UniformProbing`.
+2. Concrete parameter values, full-cycle stride permutations, pathwise Word-RAM execution
+   (`opCode_execWithin`), composable `SubroutineDS` certificates over `Basis.exact` and
+   `Basis.standard`, end-to-end multi-operation expected complexity (`seq_expected_amortized`),
+   primary-slot universality (`isUniversalHash_primaryHash`), and expected-step transfer
+   (`expect_idealProbeSteps_le`) in `Cslib.Algorithms.WordRAM.Dictionary.UniformProbing`.
+-/
+
+public section
+
+namespace ComplexityTests.WordRAMUniformProbing
+
+open Cslib
+open Cslib.Algorithms.Lean
+open Cslib.Algorithms.Lean.UniformProbing
+open Cslib.Algorithms.WordRAM.Dictionary.UniformProbing
+open Cslib.Probability
+open Cslib.WordRAM
+open Cslib.WordRAM.Randomized
+open scoped ENNReal
+
+/-! ## Part 1: Pure Textbook Uniform Probing (`Cslib.Algorithms.Lean.UniformProbing`) -/
+
+/-- A concrete permutation family on `U = 4` keys and `m = 4` slots where keys `0` and `1` both
+start at slot `0`, and key `1` swaps slots `1` and `3`. -/
+def testPermFamily : Fin 4 → Equiv.Perm (Fin 4)
+  | ⟨0, _⟩ => Equiv.refl (Fin 4)
+  | ⟨1, _⟩ => Equiv.swap (1 : Fin 4) (3 : Fin 4)
+  | _ => Equiv.refl (Fin 4)
+
+/-- Concrete trace of `tableInsert`, `tableGet`, and `probeCount` under a primary-slot collision
+and an in-place overwrite at full capacity `n_max = 2`. -/
+theorem test_pure_collision_and_overwrite :
+    let hm : 0 < 4 := by decide
+    let T₀ := emptyTable 4 4
+    let u₀ : Fin 4 := ⟨0, by decide⟩
+    let u₁ : Fin 4 := ⟨1, by decide⟩
+    let u₂ : Fin 4 := ⟨2, by decide⟩
+    let T₁ := tableInsert hm testPermFamily T₀ u₀ 10
+    let T₂ := tableInsert hm testPermFamily T₁ u₁ 20
+    let T₃ := tableInsert hm testPermFamily T₂ u₁ 99
+    -- Initial empty table lookup misses in 1 probe:
+    tableGet hm testPermFamily T₀ u₀ = none ∧
+    probeCount T₀ u₀ (testPermFamily u₀) = 1 ∧
+    -- First insertion lands at primary slot 0 in 1 probe:
+    T₁ ⟨0, by decide⟩ = some (u₀, 10) ∧
+    probeCount T₁ u₀ (testPermFamily u₀) = 1 ∧
+    -- Colliding key u₁ probes slot 0 (occupied by u₀) and lands at testPermFamily u₁ 1 = 3:
+    probeCount T₁ u₁ (testPermFamily u₁) = 2 ∧
+    T₂ ⟨3, by decide⟩ = some (u₁, 20) ∧
+    tableGet hm testPermFamily T₂ u₀ = some 10 ∧
+    tableGet hm testPermFamily T₂ u₁ = some 20 ∧
+    tableGet hm testPermFamily T₂ u₂ = none ∧
+    -- In-place overwrite of u₁ updates slot 3 to 99 and preserves probeCount = 2:
+    T₃ ⟨3, by decide⟩ = some (u₁, 99) ∧
+    tableGet hm testPermFamily T₃ u₁ = some 99 ∧
+    probeCount T₃ u₁ (testPermFamily u₁) = 2 := by
+  decide
+
+/-- Concrete instantiation of the textbook expected-probe bounds (`≤ 2`) for both unsuccessful
+lookups (`[CLRS2009]`, third edition, Theorem 11.6 / Corollary 11.7, pp. 274–276) and fixed-key
+successful lookups (via the insertion-cost identity and intermediate bound from the proof of
+Theorem 11.8, p. 276) on a table of `m = 8` slots with `U = 16` keys and capacity `n_max = 4`. -/
+theorem test_expected_probes_le_two
+    (ops₁ ops₂ : List (Dictionary.Op 16))
+    (u u_abs : Fin 16) (v₀ : ℕ)
+    (hvh : (Dictionary.spec 16 100 4).ValidHistory (Dictionary.empty 16)
+      (ops₁ ++ (.insert u v₀ :: ops₂)))
+    (hu₁ : ((Dictionary.spec 16 100 4).run (Dictionary.empty 16) ops₁).1 u = none)
+    (habs :
+      ((Dictionary.spec 16 100 4).run (Dictionary.empty 16)
+        (ops₁ ++ (.insert u v₀ :: ops₂))).1 u_abs = none) :
+    let hm : 0 < 8 := by decide
+    let ops := ops₁ ++ (.insert u v₀ :: ops₂)
+    let μ := PMF.uniformOfFintype (Fin 16 → Equiv.Perm (Fin 8))
+    (∑' π : Fin 16 → Equiv.Perm (Fin 8),
+      μ π * (probeCount (runTable hm π ops) u (π u) : ℝ≥0∞)) ≤ 2 ∧
+    (∑' π : Fin 16 → Equiv.Perm (Fin 8),
+      μ π * (probeCount (runTable hm π ops) u_abs (π u_abs) : ℝ≥0∞)) ≤ 2 := by
+  have hm : 0 < 8 := by decide
+  have h2m : 2 * 4 ≤ 8 := by decide
+  exact ⟨expect_probeCount_of_mem_dom_le_two hm h2m hvh hu₁,
+    expect_probeCount_of_eq_none_le_two hm h2m hvh habs⟩
+
+/-- Concrete instantiation of the lazy random-oracle equivalence for uniform probing on `U = 16`
+keys and `m = 8` slots. -/
+theorem test_lazy_random_oracle_equiv
+    (prog : OracleComp (fun _ : Fin 16 => Equiv.Perm (Fin 8)) Bool) :
+    (do
+      let π ← PMF.uniformOfFintype (Fin 16 → Equiv.Perm (Fin 8))
+      OracleComp.interpret (fun u => PMF.pure (π u)) prog) =
+      ((OracleComp.interpret
+        (Cslib.RandomOracle.answer (fun _ : Fin 16 => PMF.uniformOfFintype (Equiv.Perm (Fin 8))))
+        prog).run (fun _ => none)).map Prod.fst :=
+  uniform_interpret_eq_lazy_perm prog
+
+/-! ## Part 2: Word-RAM Realization (`Cslib.Algorithms.WordRAM.Dictionary.UniformProbing`) -/
+
+/-- Verify concrete table dimension parameters at `U = 16`, `n_max = 2`. -/
+theorem test_wordram_params :
+    bucketBits 2 = 3 ∧
+    numBuckets 2 = 8 ∧
+    hashBits 16 2 = 4 ∧
+    charBits 2 = 1 ∧
+    numChars 16 2 = 4 ∧
+    tabSpace 16 2 = 12 ∧
+    slotOffset 16 2 = 13 ∧
+    space 16 2 = 37 ∧
+    setupSteps 16 2 = 65 ∧
+    opSteps 16 2 = 185 := by
+  decide
+
+/-- For every seed `θ : Seed 16 2` and key `u : Fin 16`, `probePerm θ u` is a bijection on the `8`
+table slots, and its `0`-th probe slot is `primaryHash θ u`. -/
+theorem test_wordram_probePerm_bijective (θ : Seed 16 2) (u : Fin 16) :
+    Function.Bijective (probePerm θ u) ∧
+    probePerm θ u ⟨0, by decide⟩ = primaryHash θ u :=
+  ⟨(probePerm θ u).bijective, probePerm_zero θ u⟩
+
+/-- Concrete admissible operation sequence on `U = 16`, `V = 100`, `n_max = 2` exercising fresh
+insertions up to full capacity `n_max = 2`, an in-place overwrite at full capacity, successful
+lookups, and an unsuccessful lookup of an absent key. -/
+def testOps : List (Dictionary.Op 16) :=
+  [ .insert ⟨3, by decide⟩ 42,
+    .insert ⟨11, by decide⟩ 77,
+    .insert ⟨3, by decide⟩ 88,
+    .get ⟨3, by decide⟩,
+    .get ⟨11, by decide⟩,
+    .get ⟨5, by decide⟩ ]
+
+theorem testOps_validHistory :
+    (Dictionary.spec 16 100 2).ValidHistory (Dictionary.empty 16) testOps := by
+  dsimp only [testOps, Cslib.Stateful.Spec.ValidHistory, Dictionary.spec]
+  decide
+
+/-- Concrete instantiation of the `Basis.exact` and `Basis.standard` `SubroutineDS` certificates
+and end-to-end `seq_expected_amortized` bound at `w = 64`, `base = 16`, `U = 16`, `V = 100`,
+`n_max = 2`. -/
+theorem test_wordram_seq_expected_amortized :
+    have hS : Fits 64 (16 + space 16 2) := by decide
+    have hw : 2 * hashBits 16 2 ≤ 64 := by decide
+    have hV : Fits 64 100 := by decide
+    let x₀ : Data 12 := (⟨fun _ => 0, fun _ => 0⟩ : Data 12).set regV 16
+    ∃ (ν₀ ν_final : PMF (Seed 16 2 × Data 12)) (T_ops : ℝ≥0∞),
+      ExecCodeDist 64 (subroutineCode 16 2).initFresh x₀ (ν₀.map Prod.snd)
+        (subroutineDS (V := 100) hS hw hV).initTime ∧
+      (subroutineDS (V := 100) hS hw hV).ExecSteps (Dictionary.empty 16) testOps ν₀ ν_final
+        T_ops ∧
+      (∀ θ, (ν_final.map Prod.fst) θ ≤ seedLaw 16 2 θ) ∧
+      (∀ p ∈ ν_final.support,
+        Rep 64 16 16 100 2 p.1
+          ((Dictionary.spec 16 100 2).run (Dictionary.empty 16) testOps).1 p.2) ∧
+      (subroutineDS (V := 100) hS hw hV).initTime + T_ops ≤ (1178 : ℝ≥0∞) := by
+  have hS : Fits 64 (16 + space 16 2) := by decide
+  have hw : 2 * hashBits 16 2 ≤ 64 := by decide
+  have hV : Fits 64 100 := by decide
+  let x₀ : Data 12 := (⟨fun _ => 0, fun _ => 0⟩ : Data 12).set regV 16
+  have hx₀ : x₀.Bounded 64 := by
+    refine ⟨fun i => ?_, fun a => ?_⟩
+    · fin_cases i <;> decide
+    · change Fits 64 0
+      exact fits_zero 64
+  have hfr : x₀.regs regV = 16 := rfl
+  have hz : ∀ a ∈ (Block.mk 16 (space 16 2)).footprint, x₀.mem a = 0 := fun _ _ => rfl
+  obtain ⟨ν₀, ν_final, T_ops, he_init, hex_steps, hseed, hrep, hbound⟩ :=
+    seq_expected_amortized (V := 100) hS hw hV testOps hx₀ hfr hz testOps_validHistory
+  refine ⟨ν₀, ν_final, T_ops, he_init, hex_steps, hseed, hrep, hbound.trans ?_⟩
+  have htot : (3 + setupSteps 16 2 : ℝ≥0∞) +
+      ((Dictionary.spec 16 100 2).totalCost (fun _ _ => opSteps 16 2)
+        (Dictionary.empty 16) testOps : ℝ≥0∞) = 1178 := by
+    have h1 : setupSteps 16 2 = 65 := by decide
+    have h2 : (Dictionary.spec 16 100 2).totalCost (fun _ _ => opSteps 16 2)
+        (Dictionary.empty 16) testOps = 1110 := by decide
+    rw [h1, h2]
+    norm_num
+  exact le_of_eq htot
+
+/-- Concrete instantiation of the standard-basis (`Basis.standard`) certificate, primary-slot
+`1/4`-universality (`2 / 8`), and ideal uniform-probing expected-step bound (`≤ 107` steps) at
+`U = 16`, `n_max = 2`. -/
+theorem test_wordram_standard_and_collision_bounds :
+    have hS : Fits 64 (16 + space 16 2) := by decide
+    have hw : 2 * hashBits 16 2 ≤ 64 := by decide
+    have hV : Fits 64 100 := by decide
+    (subroutineDSStandard (V := 100) hS hw hV).space = 37 ∧
+    Cslib.Probability.IsUniversalHash (seedLaw 16 2) (primaryHash (U := 16) (n_max := 2))
+      (2 / (8 : ℝ≥0∞)) ∧
+    ∀ (T : Fin (numBuckets 2) → Option (Fin 16 × ℕ)) (u : Fin 16),
+      (otherOccupiedSlots T u).card ≤ 2 →
+      (∑' π : Equiv.Perm (Fin (numBuckets 2)),
+        (PMF.uniformOfFintype (Equiv.Perm (Fin (numBuckets 2)))) π *
+          ((13 * probeCount T u π + 8 * numChars 16 2 + 49 : ℕ) : ℝ≥0∞)) ≤ 107 := by
+  refine ⟨by decide, isUniversalHash_primaryHash 16 2, fun T u hcard => ?_⟩
+  have h := expect_idealProbeSteps_le T u hcard
+  have heq : (8 * numChars 16 2 + 75 : ℝ≥0∞) = 107 := by
+    have hc : numChars 16 2 = 4 := by decide
+    rw [hc]
+    norm_num
+  rwa [heq] at h
+
+end ComplexityTests.WordRAMUniformProbing