diff --git a/Complexity.lean b/Complexity.lean
index 6a055a9d4..90e94fc6d 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -33,8 +33,11 @@ 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.Erase
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Insert
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Layout
+public import Complexity.Algorithms.Lean.VanEmdeBoas.Predecessor
+public import Complexity.Algorithms.Lean.VanEmdeBoas.Stateful
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Successor
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.Alphabets
 public import Complexity.Algorithms.MatrixMultiplication.Schonhage.BandBounds
diff --git a/Complexity/Algorithms/Lean/VanEmdeBoas/Elements.lean b/Complexity/Algorithms/Lean/VanEmdeBoas/Elements.lean
index 1477b1452..7cd78a185 100644
--- a/Complexity/Algorithms/Lean/VanEmdeBoas/Elements.lean
+++ b/Complexity/Algorithms/Lean/VanEmdeBoas/Elements.lean
@@ -7,8 +7,11 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
+public import Complexity.Algorithms.Lean.VanEmdeBoas.Erase
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Insert
+public import Complexity.Algorithms.Lean.VanEmdeBoas.Predecessor
 public import Complexity.Algorithms.Lean.VanEmdeBoas.Successor
+public import Mathlib.Data.Finset.Erase
 public import Mathlib.Data.Finset.Filter
 public import Mathlib.Data.Finset.Range
 
@@ -26,9 +29,12 @@ the observation.
 ## Main results
 
 * `Tree.mem_elements_iff`: the finite set agrees with the recursive mathematical interpretation.
-* `Tree.elements_insert`: insertion adds exactly one key to the finite set.
+* `Tree.elements_insert`, `Tree.elements_erase`: insertion and deletion commute with the
+  finite-set observation.
 * `Tree.successor_elements_some_iff`, `Tree.successor_elements_none_iff`: strict successor and
   its absence are characterized by the finite set.
+* `Tree.predecessor_elements_some_iff`, `Tree.predecessor_elements_none_iff`: strict predecessor
+  and its absence are characterized by the finite set.
 
 ## References
 
@@ -77,4 +83,24 @@ theorem successor_elements_none_iff {t : Tree d} (ht : t.Valid) (x : ℕ) :
   simp only [mem_elements_iff ht]
   exact successor_eq_none_iff ht x
 
+/-- The finite-set observation commutes with deletion of any key `x : ℕ`. -/
+theorem elements_erase {t : Tree d} (ht : t.Valid) (x : ℕ) :
+    (t.erase x).elements = t.elements.erase x := by
+  ext y
+  rw [mem_elements_iff (valid_erase ht x), Finset.mem_erase, mem_elements_iff ht]
+  exact contains_erase ht x y
+
+/-- A successful predecessor is the greatest finite-set element strictly below the query. -/
+theorem predecessor_elements_some_iff {t : Tree d} (ht : t.Valid) (x y : ℕ) :
+    t.predecessor x = some y ↔ y ∈ t.elements ∧ y < x ∧
+      ∀ z, z ∈ t.elements → z < x → z ≤ y := by
+  simp only [mem_elements_iff ht]
+  exact predecessor_eq_some_iff ht x y
+
+/-- An absent predecessor means that every finite-set element is at least the query. -/
+theorem predecessor_elements_none_iff {t : Tree d} (ht : t.Valid) (x : ℕ) :
+    t.predecessor x = none ↔ ∀ z, z ∈ t.elements → x ≤ z := by
+  simp only [mem_elements_iff ht]
+  exact predecessor_eq_none_iff ht x
+
 end Cslib.Algorithms.Lean.VanEmdeBoas.Tree
diff --git a/Complexity/Algorithms/Lean/VanEmdeBoas/Erase.lean b/Complexity/Algorithms/Lean/VanEmdeBoas/Erase.lean
new file mode 100644
index 000000000..f3d667a89
--- /dev/null
+++ b/Complexity/Algorithms/Lean/VanEmdeBoas/Erase.lean
@@ -0,0 +1,664 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.Lean.VanEmdeBoas.Insert
+import Mathlib.Tactic.Linarith
+
+/-!
+# Single-recursion van Emde Boas deletion
+
+This module defines and verifies key deletion on recursive minimum-excluded van Emde Boas trees
+([Demaine2015VanEmdeBoas], pp. 5–6; [CLRS2009], Section 20.3, p. 554).
+
+At each internal depth `d + 1`:
+* If the tree is empty or the query lies outside `[m, M]`, deletion returns immediately with no
+  recursive call.
+* If `m = M` (and hence `x = m`), the valid minimum-exclusion invariant guarantees that all
+  clusters and the summary are already empty, so clearing the local header clears the node in
+  `O(1)`.
+* Otherwise (`m < M` and `m ≤ x ≤ M`), if `x = m`, the smallest key stored in the clusters is
+  located via `summary.minimum` and `(cluster i).minimum` in `O(1)` header reads, promoted to
+  become `newMin`, and targeted for deletion from `cluster i`; if `x ≠ m`, `newMin = m` is kept
+  and `x % universeSize d` is targeted for deletion from `cluster (x / universeSize d)`.
+* Inspecting `(cluster i).bounds` then chooses **at most one** recursive deletion:
+  when `cluster i` is a singleton `{low}`, `cluster i` is cleared in `O(1)` via `withBounds none`
+  and `erase` recurses only on `summary`; when `cluster i` has distinct extrema (`cm ≠ cM`), at
+  least one key remains after deleting `low`, so `summary` stays unchanged and `erase` recurses
+  only on `cluster i`.
+* Finally, `clusterMax` reconstructs the updated maximum in `O(1)` from `newMin`, `s'.maximum`,
+  and the maximal occupied cluster's cached `maximum`.
+
+These are mathematical correctness statements about the functional Lean representation, without a
+machine running-time claim.
+
+## Main definitions
+
+* `Tree.EraseTarget`, `Tree.eraseTarget`: non-recursive `O(1)` header selection of
+  `(newMin, i, low)`.
+* `Tree.clusterMax`: non-recursive `O(1)` reconstruction of a node's maximum from its summary and
+  clusters.
+* `Tree.erase`: single-recursion key deletion on `Tree d`.
+
+## Main results
+
+* `Tree.erase_empty`: deleting from `empty d` returns `empty d`.
+* `Tree.valid_erase`: deletion of any key `x : ℕ` preserves `Tree.Valid`.
+* `Tree.contains_erase`: `(t.erase x).Contains y ↔ y ≠ x ∧ t.Contains y`.
+* `Tree.erase_eq_of_not_contains`: deleting an absent key from a valid tree returns `t` unchanged.
+
+## References
+
+* [E. Demaine, *Divide and conquer: van Emde Boas trees*, Lecture 4][Demaine2015VanEmdeBoas]
+* [T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, *Introduction to Algorithms*,
+  Section 20.3][CLRS2009]
+-/
+
+public section
+
+namespace Cslib.Algorithms.Lean.VanEmdeBoas.Tree
+
+variable {d : ℕ}
+
+/-- Header-selected cluster target for an internal-node deletion step (`m < M` and `m ≤ x ≤ M`). -/
+structure EraseTarget (d : ℕ) where
+  /-- Updated local minimum of the parent node. -/
+  newMin : ℕ
+  /-- Index of the cluster from which `low` is to be removed. -/
+  clusterIdx : Fin (universeSize d)
+  /-- Low-order coordinate to remove from `cluster clusterIdx`. -/
+  low : ℕ
+
+/-- Non-recursive `O(1)` header helper selecting `(newMin, clusterIdx, low)` when `m < M` and
+`m ≤ x ≤ M` ([Demaine2015VanEmdeBoas], p. 6; [CLRS2009], Section 20.3, p. 554). -/
+@[expose] def eraseTarget {d : ℕ} (m x : ℕ) (s : Tree d)
+    (c : Fin (universeSize d) → Tree d) : Option (EraseTarget d) :=
+  if x = m then
+    match s.minimum with
+    | none => none
+    | some j =>
+      if hj : j < universeSize d then
+        let i : Fin (universeSize d) := ⟨j, hj⟩
+        (c i).minimum.map fun low => ⟨j * universeSize d + low, i, low⟩
+      else none
+  else if hx : x / universeSize d < universeSize d then
+    some ⟨m, ⟨x / universeSize d, hx⟩, x % universeSize d⟩
+  else none
+
+/-- Reconstruct a node's maximum in `O(1)` header reads from `newMin`, `s.maximum`, and the
+maximal occupied cluster's cached `maximum` ([Demaine2015VanEmdeBoas], p. 6; [CLRS2009],
+Section 20.3, p. 554). -/
+@[expose] def clusterMax {d : ℕ} (newMin : ℕ) (s : Tree d)
+    (c : Fin (universeSize d) → Tree d) : ℕ :=
+  match s.maximum with
+  | none => newMin
+  | some j =>
+    if hj : j < universeSize d then
+      match (c ⟨j, hj⟩).maximum with
+      | none => newMin
+      | some y => j * universeSize d + y
+    else newMin
+
+/-- Delete a key from a van Emde Boas tree, performing at most one recursive call per depth level
+([Demaine2015VanEmdeBoas], pp. 5–6; [CLRS2009], Section 20.3, p. 554). -/
+@[expose] def erase : {d : ℕ} → Tree d → ℕ → Tree d
+  | 0, .leaf b, x => match b with
+    | none => .leaf none
+    | some (m, M) =>
+      if x = m ∧ x = M then .leaf none
+      else if x = m then .leaf (some (M, M))
+      else if x = M then .leaf (some (m, m))
+      else .leaf (some (m, M))
+  | _ + 1, .node b s c, x => match b with
+    | none => .node none s c
+    | some (m, M) =>
+      if x < m ∨ M < x then .node (some (m, M)) s c
+      else if m = M then .node none s c
+      else
+        match eraseTarget m x s c with
+        | none => .node (some (m, M)) s c
+        | some ⟨newMin, i, low⟩ =>
+          match (c i).bounds with
+          | none => .node (some (m, M)) s c
+          | some (cm, cM) =>
+            if cm = cM then
+              if low = cm then
+                let c' := Function.update c i ((c i).withBounds none)
+                let s' := erase s i.val
+                .node (some (newMin, clusterMax newMin s' c')) s' c'
+              else .node (some (m, M)) s c
+            else
+              let c' := Function.update c i (erase (c i) low)
+              .node (some (newMin, clusterMax newMin s c')) s c'
+
+/-- Deleting any key from the empty tree at depth `d` returns `empty d`. -/
+@[simp] theorem erase_empty (d x : ℕ) : (empty d).erase x = empty d := by
+  cases d <;> rfl
+
+private theorem index_lt_index {u i j a b : ℕ} (ha : a < u) (hij : i < j) :
+    i * u + a < j * u + b := by
+  have h := Nat.mul_le_mul_right u (show i + 1 ≤ j by omega)
+  nlinarith
+
+private theorem singleton_contains_of_bounds_eq {t : Tree d} (ht : t.Valid) {m : ℕ}
+    (hb : t.bounds = some (m, m)) (y : ℕ) : t.Contains y ↔ y = m := by
+  have he := ht.extrema
+  simp only [Extrema, hb] at he
+  constructor
+  · intro hy
+    have := he.2.2.2.2 y hy
+    omega
+  · rintro rfl
+    exact he.2.2.1
+
+/-- Clearing the local header of a valid singleton node yields a valid empty node in `O(1)` because
+minimum exclusion already forces its summary and clusters to be empty. -/
+private theorem empty_of_bounds_eq {t : Tree d} (ht : t.Valid) {m : ℕ}
+    (hb : t.bounds = some (m, m)) :
+    (t.withBounds none).Valid ∧ (t.withBounds none).bounds = none ∧
+      ∀ y, ¬(t.withBounds none).Contains y := by
+  cases t with
+  | leaf b =>
+    simp only [bounds] at hb
+    subst b
+    refine ⟨?_, rfl, not_contains_of_bounds_none rfl⟩
+    simp [withBounds, Valid, Extrema, bounds, Contains]
+  | @node d b s c =>
+    simp only [bounds] at hb
+    subst b
+    obtain ⟨he, hs, hc, ho, hmin⟩ := ht
+    simp only [Extrema, bounds] at he
+    have hcb : ∀ i, (c i).bounds = none := by
+      intro i
+      cases hbi : (c i).bounds with
+      | none => rfl
+      | some b' =>
+        obtain ⟨cm, cM⟩ := b'
+        have hcm := (hc i).contains_minimum hbi
+        have hlt := hmin i cm hcm
+        have hle := (he.2.2.2.2 (i.val * universeSize d + cm)
+          ⟨m, m, rfl, Or.inr ⟨i, cm, hcm, rfl⟩⟩).2
+        omega
+    have hsb : s.bounds = none := by
+      cases hbs : s.bounds with
+      | none => rfl
+      | some b' =>
+        obtain ⟨sm, sM⟩ := b'
+        have hsm := hs.contains_minimum hbs
+        have hsmlt := hs.contains_lt hsm
+        have his := (ho ⟨sm, hsmlt⟩).mp hsm
+        simp [hcb ⟨sm, hsmlt⟩] at his
+    have hbnone : (node none s c).bounds = none := rfl
+    refine ⟨⟨?_, hs, hc, ho, hsb, hcb⟩, rfl, not_contains_of_bounds_none hbnone⟩
+    simp only [Extrema, hbnone]
+    exact not_contains_of_bounds_none hbnone
+
+/-- Any valid summary/cluster pair whose keys strictly exceed `newMin < universeSize (d + 1)` forms
+a valid node when paired with `clusterMax newMin s' c'`. -/
+private theorem valid_node_of_clusterMax {newMin : ℕ} {s' : Tree d}
+    {c' : Fin (universeSize d) → Tree d}
+    (hmin_lt : newMin < universeSize (d + 1))
+    (hs' : s'.Valid) (hc' : ∀ k, (c' k).Valid)
+    (ho' : ∀ k, s'.Contains k.val ↔ (c' k).bounds.isSome = true)
+    (hexcl : ∀ k y, (c' k).Contains y → newMin < k.val * universeSize d + y) :
+    (node (some (newMin, clusterMax newMin s' c')) s' c').Valid := by
+  refine ⟨?_, hs', hc', ho', hexcl⟩
+  cases hbs : s'.bounds with
+  | none =>
+    have hcnone : ∀ k y, ¬(c' k).Contains y := by
+      intro k y hy
+      have hsk : s'.Contains k.val := (ho' k).mpr ((hc' k).bounds_isSome_iff.mpr ⟨y, hy⟩)
+      exact not_contains_of_bounds_none hbs k.val hsk
+    have hmax : clusterMax newMin s' c' = newMin := by
+      simp [clusterMax, maximum, hbs]
+    rw [hmax]
+    simp only [Extrema, bounds, contains_node_some]
+    refine ⟨le_rfl, hmin_lt, Or.inl trivial, Or.inl trivial, ?_⟩
+    rintro z (rfl | ⟨k, y, hy, _⟩)
+    · exact ⟨le_rfl, le_rfl⟩
+    · exact False.elim (hcnone k y hy)
+  | some sb =>
+    obtain ⟨sm, sM⟩ := sb
+    have hse := hs'.extrema
+    simp only [Extrema, hbs] at hse
+    let j : Fin (universeSize d) := ⟨sM, hse.2.1⟩
+    have hbj_some : (c' j).bounds.isSome = true := (ho' j).mp hse.2.2.2.1
+    cases hbj : (c' j).bounds with
+    | none => simp [hbj] at hbj_some
+    | some cb =>
+      obtain ⟨cm, cM⟩ := cb
+      have hce := (hc' j).extrema
+      simp only [Extrema, hbj] at hce
+      have hmax : clusterMax newMin s' c' = sM * universeSize d + cM := by
+        simp [clusterMax, maximum, hbs, hse.2.1, j, hbj]
+      rw [hmax]
+      simp only [Extrema, bounds]
+      have hgt : newMin < sM * universeSize d + cM := hexcl j cM hce.2.2.2.1
+      have hM_lt : sM * universeSize d + cM < universeSize (d + 1) := by
+        rw [universeSize_succ]
+        have hmul := Nat.mul_le_mul_right (universeSize d)
+          (show sM + 1 ≤ universeSize d by omega)
+        have hcM_lt := hce.2.1
+        nlinarith
+      refine ⟨hgt.le, hM_lt, ⟨newMin, _, rfl, Or.inl rfl⟩,
+        ⟨newMin, _, rfl, Or.inr ⟨j, cM, hce.2.2.2.1, rfl⟩⟩, ?_⟩
+      intro z hz
+      simp only [contains_node_some] at hz
+      rcases hz with rfl | ⟨k, y, hy, rfl⟩
+      · exact ⟨le_rfl, hgt.le⟩
+      · refine ⟨(hexcl k y hy).le, ?_⟩
+        have hsk : s'.Contains k.val := (ho' k).mpr ((hc' k).bounds_isSome_iff.mpr ⟨y, hy⟩)
+        have hk_le : k.val ≤ sM := (hse.2.2.2.2 k.val hsk).2
+        by_cases hkj : k = j
+        · subst k
+          exact Nat.add_le_add_left (hce.2.2.2.2 y hy).2 (j.val * universeSize d)
+        · have hk_lt : k.val < sM := by
+            have : k.val ≠ sM := fun h => hkj (Fin.ext h)
+            omega
+          exact (index_lt_index ((hc' k).contains_lt hy) hk_lt).le
+
+private theorem update_cluster_erase_spec {c : Fin (universeSize d) → Tree d}
+    (hc : ∀ k, (c k).Valid) {i : Fin (universeSize d)} {low : ℕ} {t : Tree d}
+    (ht : t.Valid) (hs : ∀ y, t.Contains y ↔ y ≠ low ∧ (c i).Contains y) :
+    (∀ k, (Function.update c i t k).Valid) ∧
+      ∀ k y, (Function.update c i t k).Contains y ↔
+        ¬(k = i ∧ y = low) ∧ (c k).Contains y := by
+  constructor
+  · intro k
+    by_cases h : k = i
+    · subst k
+      simpa only [Function.update_self] using ht
+    · simpa only [Function.update_of_ne h] using hc k
+  · intro k y
+    by_cases h : k = i
+    · subst k
+      simpa only [Function.update_self, true_and] using hs y
+    · simp [h]
+
+private theorem erase_cluster_branch {s : Tree d} {c : Fin (universeSize d) → Tree d}
+    {m M x newMin low cm cM : ℕ} {i : Fin (universeSize d)}
+    (hs : s.Valid) (hc : ∀ k, (c k).Valid)
+    (ho : ∀ k, s.Contains k.val ↔ (c k).bounds.isSome = true)
+    (ih : ∀ {t : Tree d}, t.Valid → ∀ z,
+      (t.erase z).Valid ∧ ∀ y, (t.erase z).Contains y ↔ y ≠ z ∧ t.Contains y)
+    (hmin_lt : newMin < universeSize (d + 1))
+    (hbi : (c i).bounds = some (cm, cM))
+    (hlow_eq : cm = cM → low = cm)
+    (hexcl' : ∀ k y, ¬(k = i ∧ y = low) → (c k).Contains y →
+      newMin < k.val * universeSize d + y)
+    (hset_eq : ∀ (s' : Tree d) (c' : Fin (universeSize d) → Tree d) (M' : ℕ),
+      (∀ k y, (c' k).Contains y ↔ ¬(k = i ∧ y = low) ∧ (c k).Contains y) →
+        ∀ y, (node (some (newMin, M')) s' c').Contains y ↔
+          y ≠ x ∧ (node (some (m, M)) s c).Contains y) :
+    (let t' :=
+      if cm = cM then
+        if low = cm then
+          let c' := Function.update c i ((c i).withBounds none)
+          let s' := erase s i.val
+          node (some (newMin, clusterMax newMin s' c')) s' c'
+        else node (some (m, M)) s c
+      else
+        let c' := Function.update c i (erase (c i) low)
+        node (some (newMin, clusterMax newMin s c')) s c'
+    t'.Valid ∧ ∀ y, t'.Contains y ↔ y ≠ x ∧ (node (some (m, M)) s c).Contains y) := by
+  dsimp only
+  by_cases hcm : cm = cM
+  · have hlow : low = cm := hlow_eq hcm
+    rw [ite_eq_left hcm, ite_eq_left hlow]
+    have hbi' : (c i).bounds = some (cm, cm) := hcm ▸ hbi
+    obtain ⟨hci_val, hci_b, hci_none⟩ := empty_of_bounds_eq (hc i) hbi'
+    have hci_set : ∀ y, ((c i).withBounds none).Contains y ↔ y ≠ low ∧ (c i).Contains y := by
+      intro y
+      rw [singleton_contains_of_bounds_eq (hc i) hbi', hlow]
+      exact ⟨fun hy => False.elim (hci_none y hy), fun h => False.elim (h.1 h.2)⟩
+    obtain ⟨hcv, hcs⟩ := update_cluster_erase_spec hc hci_val hci_set
+    obtain ⟨hsv, hss⟩ := ih hs i.val
+    let c' := Function.update c i ((c i).withBounds none)
+    let s' := erase s i.val
+    have ho' : ∀ k, s'.Contains k.val ↔ (c' k).bounds.isSome = true := by
+      intro k
+      rw [hss]
+      by_cases hki : k = i
+      · subst k
+        simp [c', hci_b]
+      · have hval : k.val ≠ i.val := fun h => hki (Fin.ext h)
+        simp [c', hki, hval, ho k]
+    have hexcl : ∀ k y, (c' k).Contains y → newMin < k.val * universeSize d + y := by
+      intro k y hy
+      obtain ⟨hne, hyc⟩ := (hcs k y).mp hy
+      exact hexcl' k y hne hyc
+    exact ⟨valid_node_of_clusterMax hmin_lt hsv hcv ho' hexcl, hset_eq s' c' _ hcs⟩
+  · rw [ite_eq_right hcm]
+    obtain ⟨hci_val, hci_set⟩ := ih (hc i) low
+    obtain ⟨hcv, hcs⟩ := update_cluster_erase_spec hc hci_val hci_set
+    let c' := Function.update c i (erase (c i) low)
+    have hci_nonempty : ∃ y, ((c i).erase low).Contains y := by
+      by_cases hlow : low = cm
+      · refine ⟨cM, (hci_set cM).mpr ⟨fun h => hcm (hlow.symm.trans h.symm), ?_⟩⟩
+        exact (hc i).contains_maximum hbi
+      · refine ⟨cm, (hci_set cm).mpr ⟨fun h => hlow h.symm, ?_⟩⟩
+        exact (hc i).contains_minimum hbi
+    have ho' : ∀ k, s.Contains k.val ↔ (c' k).bounds.isSome = true := by
+      intro k
+      by_cases hki : k = i
+      · subst k
+        simp only [c', Function.update_self, hci_val.bounds_isSome_iff]
+        have his : s.Contains i.val := (ho i).mpr (by simp only [hbi, Option.isSome_some])
+        exact ⟨fun _ => hci_nonempty, fun _ => his⟩
+      · simpa only [c', Function.update_of_ne hki] using ho k
+    have hexcl : ∀ k y, (c' k).Contains y → newMin < k.val * universeSize d + y := by
+      intro k y hy
+      obtain ⟨hne, hyc⟩ := (hcs k y).mp hy
+      exact hexcl' k y hne hyc
+    exact ⟨valid_node_of_clusterMax hmin_lt hs hcv ho' hexcl, hset_eq s c' _ hcs⟩
+
+private theorem erase_spec {t : Tree d} (ht : t.Valid) (x : ℕ) :
+    (t.erase x).Valid ∧ ∀ y, (t.erase x).Contains y ↔ y ≠ x ∧ t.Contains y := by
+  induction d generalizing x with
+  | zero =>
+    cases t with
+    | leaf b =>
+      cases b with
+      | none =>
+        refine ⟨ht, fun y => ?_⟩
+        simp [erase, Contains]
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        have he := ht.extrema
+        simp only [Extrema, bounds] at he
+        by_cases hboth : x = m ∧ x = M
+        · rw [erase, ite_eq_left hboth]
+          refine ⟨valid_empty 0, fun y => ?_⟩
+          simp only [contains_leaf_some]
+          rcases hboth with ⟨rfl, hM⟩
+          rw [← hM]
+          simp [Contains]
+        · by_cases hxm : x = m
+          · rw [erase, ite_eq_right hboth, ite_eq_left hxm]
+            have hmM : m < M := by omega
+            refine ⟨?_, fun y => ?_⟩
+            · simp only [Valid, Extrema, bounds, contains_leaf_some]
+              exact ⟨le_rfl, he.2.1, Or.inl trivial, Or.inl trivial, fun z hz => by omega⟩
+            · simp only [contains_leaf_some]
+              omega
+          · by_cases hxM : x = M
+            · rw [erase, ite_eq_right hboth, ite_eq_right hxm, ite_eq_left hxM]
+              have hmM : m < M := by omega
+              refine ⟨?_, fun y => ?_⟩
+              · simp only [Valid, Extrema, bounds, contains_leaf_some]
+                exact ⟨le_rfl, by omega, Or.inl trivial, Or.inl trivial, fun z hz => by omega⟩
+              · simp only [contains_leaf_some]
+                omega
+            · rw [erase, ite_eq_right hboth, ite_eq_right hxm, ite_eq_right hxM]
+              refine ⟨ht, fun y => ?_⟩
+              simp only [contains_leaf_some]
+              omega
+  | succ d ih =>
+    cases t with
+    | node b s c =>
+      cases b with
+      | none =>
+        refine ⟨ht, fun y => ?_⟩
+        simp [erase, Contains]
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        have he := ht.extrema
+        simp only [Extrema, bounds] at he
+        by_cases hout : x < m ∨ M < x
+        · rw [erase, ite_eq_left hout]
+          refine ⟨ht, fun y => ?_⟩
+          constructor
+          · intro hy
+            have hyb := he.2.2.2.2 y hy
+            exact ⟨by omega, hy⟩
+          · exact And.right
+        · by_cases heq : m = M
+          · rw [erase, ite_eq_right hout, ite_eq_left heq]
+            have hxm : x = m := by omega
+            subst M
+            obtain ⟨hv, _, hnone⟩ := empty_of_bounds_eq ht (m := m) rfl
+            refine ⟨hv, fun y => ?_⟩
+            rw [singleton_contains_of_bounds_eq ht (m := m) rfl y, hxm]
+            exact ⟨fun hy => False.elim (hnone y hy), fun h => False.elim (h.1 h.2)⟩
+          · have ⟨_, hs, hc, ho, hmin⟩ := ht
+            by_cases hxm : x = m
+            · -- Deleting the excluded minimum `m`: promote the least cluster key to `newMin`.
+              have hM_mem : (node (some (m, M)) s c).Contains M := he.2.2.2.1
+              simp only [contains_node_some] at hM_mem
+              rcases hM_mem with hMm | ⟨kM, yM, hyM, _⟩
+              · exact False.elim (heq hMm.symm)
+              · have hs_kM : s.Contains kM.val :=
+                  (ho kM).mpr ((hc kM).bounds_isSome_iff.mpr ⟨yM, hyM⟩)
+                cases hbs : s.bounds with
+                | none => exact False.elim (not_contains_of_bounds_none hbs kM.val hs_kM)
+                | some sb =>
+                  obtain ⟨sm, sM⟩ := sb
+                  have hse := hs.extrema
+                  simp only [Extrema, hbs] at hse
+                  have hsm_lt : sm < universeSize d := hs.contains_lt hse.2.2.1
+                  let i : Fin (universeSize d) := ⟨sm, hsm_lt⟩
+                  have hbi_some : (c i).bounds.isSome = true := (ho i).mp hse.2.2.1
+                  cases hbi : (c i).bounds with
+                  | none => simp [hbi] at hbi_some
+                  | some cb =>
+                    obtain ⟨cm, cM⟩ := cb
+                    have hce := (hc i).extrema
+                    simp only [Extrema, hbi] at hce
+                    let newMin := sm * universeSize d + cm
+                    have hnewMin_mem : (node (some (m, M)) s c).Contains newMin :=
+                      ⟨m, M, rfl, Or.inr ⟨i, cm, hce.2.2.1, rfl⟩⟩
+                    have hnewMin_lt : newMin < universeSize (d + 1) := ht.contains_lt hnewMin_mem
+                    have htarget : eraseTarget m x s c = some ⟨newMin, i, cm⟩ := by
+                      simp [eraseTarget, hxm, minimum, hbs, hsm_lt, i, hbi, newMin]
+                    have hexcl' : ∀ k y, ¬(k = i ∧ y = cm) → (c k).Contains y →
+                        newMin < k.val * universeSize d + y := by
+                      intro k y hne hy
+                      have hsk : s.Contains k.val :=
+                        (ho k).mpr ((hc k).bounds_isSome_iff.mpr ⟨y, hy⟩)
+                      have hik : sm ≤ k.val := (hse.2.2.2.2 k.val hsk).1
+                      by_cases hki : k = i
+                      · subst k
+                        have hyne : y ≠ cm := fun h => hne ⟨rfl, h⟩
+                        have hcmy : cm ≤ y := (hce.2.2.2.2 y hy).1
+                        dsimp only [newMin, i]
+                        omega
+                      · have hlt : sm < k.val := by
+                          have : k.val ≠ sm := fun h => hki (Fin.ext h)
+                          omega
+                        exact index_lt_index (Nat.lt_of_le_of_lt hce.1 hce.2.1) hlt
+                    have hset_eq : ∀ (s' : Tree d) (c' : Fin (universeSize d) → Tree d) (M' : ℕ),
+                        (∀ k y, (c' k).Contains y ↔ ¬(k = i ∧ y = cm) ∧ (c k).Contains y) →
+                          ∀ y, (node (some (newMin, M')) s' c').Contains y ↔
+                            y ≠ x ∧ (node (some (m, M)) s c).Contains y := by
+                      intro s' c' M' hcs y
+                      simp only [contains_node_some, hcs]
+                      constructor
+                      · rintro (rfl | ⟨k, a, ⟨hne, ha⟩, rfl⟩)
+                        · have hm_lt : m < newMin := hmin i cm hce.2.2.1
+                          exact ⟨by omega, Or.inr ⟨i, cm, hce.2.2.1, rfl⟩⟩
+                        · have hm_lt : m < k.val * universeSize d + a := hmin k a ha
+                          exact ⟨by omega, Or.inr ⟨k, a, ha, rfl⟩⟩
+                      · rintro ⟨hyx, rfl | ⟨k, a, ha, rfl⟩⟩
+                        · exact False.elim (hyx hxm.symm)
+                        · by_cases hka : k = i ∧ a = cm
+                          · rcases hka with ⟨rfl, rfl⟩
+                            exact Or.inl rfl
+                          · exact Or.inr ⟨k, a, ⟨hka, ha⟩, rfl⟩
+                    have hres := erase_cluster_branch (m := m) (M := M) (x := x)
+                      hs hc ho ih hnewMin_lt hbi (fun _ => rfl) hexcl' hset_eq
+                    rw [erase, ite_eq_right hout, ite_eq_right heq, htarget]
+                    dsimp only at hres ⊢
+                    rw [hbi]
+                    exact hres
+            · -- Deleting `x ≠ m` (`m < x ≤ M`): keep `m` and delete `x % u` from `c (x / u)`.
+              have hx_lt : x < universeSize (d + 1) :=
+                Nat.lt_of_le_of_lt (show x ≤ M by omega) he.2.1
+              have hx_div : x / universeSize d < universeSize d :=
+                (Nat.div_lt_iff_lt_mul (universeSize_pos d)).mpr hx_lt
+              let i : Fin (universeSize d) := ⟨x / universeSize d, hx_div⟩
+              let low := x % universeSize d
+              have hx_decomp : x = i.val * universeSize d + low := by
+                simpa only [i, low, Nat.mul_comm] using
+                  (Nat.div_add_mod x (universeSize d)).symm
+              have htarget : eraseTarget m x s c = some ⟨m, i, low⟩ := by
+                simp [eraseTarget, hxm, hx_div, i, low]
+              have hnot_mem_of_not_low : ¬(c i).Contains low →
+                  ¬(node (some (m, M)) s c).Contains x := by
+                intro hnot hx_mem
+                simp only [contains_node_some] at hx_mem
+                rcases hx_mem with hxm' | ⟨k, a, ha, hxa⟩
+                · exact hxm hxm'
+                · have hcoord := cluster_coordinates (i := k.val) (universeSize_pos d)
+                    ((hc k).contains_lt ha)
+                  have hki : i = k := Fin.ext (by simp [i, hxa, hcoord.1])
+                  have halow : low = a := by simp [low, hxa, hcoord.2]
+                  subst k a
+                  exact hnot ha
+              rw [erase, ite_eq_right hout, ite_eq_right heq, htarget]
+              dsimp only
+              cases hbi : (c i).bounds with
+              | none =>
+                have hnot := hnot_mem_of_not_low (not_contains_of_bounds_none hbi low)
+                refine ⟨ht, fun y => ?_⟩
+                exact ⟨fun hy => ⟨fun hyx => hnot (hyx ▸ hy), hy⟩, And.right⟩
+              | some cb =>
+                obtain ⟨cm, cM⟩ := cb
+                dsimp only
+                by_cases hsingleton_miss : cm = cM ∧ low ≠ cm
+                · rcases hsingleton_miss with ⟨rfl, hne⟩
+                  rw [ite_eq_left rfl, ite_eq_right hne]
+                  have hnot_low : ¬(c i).Contains low := by
+                    rw [singleton_contains_of_bounds_eq (hc i) hbi]
+                    exact hne
+                  have hnot := hnot_mem_of_not_low hnot_low
+                  refine ⟨ht, fun y => ?_⟩
+                  exact ⟨fun hy => ⟨fun hyx => hnot (hyx ▸ hy), hy⟩, And.right⟩
+                · have hlow_eq : cm = cM → low = cm := by
+                    intro hcm
+                    by_cases hl : low = cm
+                    · exact hl
+                    · exact False.elim (hsingleton_miss ⟨hcm, hl⟩)
+                  have hm_lt : m < universeSize (d + 1) := ht.contains_lt he.2.2.1
+                  have hexcl' : ∀ k y, ¬(k = i ∧ y = low) → (c k).Contains y →
+                      m < k.val * universeSize d + y := fun k y _ hy => hmin k y hy
+                  have hset_eq : ∀ (s' : Tree d) (c' : Fin (universeSize d) → Tree d) (M' : ℕ),
+                      (∀ k y, (c' k).Contains y ↔ ¬(k = i ∧ y = low) ∧ (c k).Contains y) →
+                        ∀ y, (node (some (m, M')) s' c').Contains y ↔
+                          y ≠ x ∧ (node (some (m, M)) s c).Contains y := by
+                    intro s' c' M' hcs y
+                    simp only [contains_node_some, hcs]
+                    constructor
+                    · rintro (rfl | ⟨k, a, ⟨hne, ha⟩, rfl⟩)
+                      · exact ⟨Ne.symm hxm, Or.inl rfl⟩
+                      · refine ⟨?_, Or.inr ⟨k, a, ha, rfl⟩⟩
+                        intro hyx
+                        have hcoord := cluster_coordinates (i := k.val) (universeSize_pos d)
+                          ((hc k).contains_lt ha)
+                        have hki : k = i := Fin.ext (by simp [i, ← hyx, hcoord.1])
+                        have halow : a = low := by simp [low, ← hyx, hcoord.2]
+                        exact hne ⟨hki, halow⟩
+                    · rintro ⟨hyx, rfl | ⟨k, a, ha, rfl⟩⟩
+                      · exact Or.inl rfl
+                      · refine Or.inr ⟨k, a, ⟨?_, ha⟩, rfl⟩
+                        rintro ⟨rfl, rfl⟩
+                        exact hyx hx_decomp.symm
+                  exact erase_cluster_branch (m := m) (M := M) (x := x)
+                    hs hc ho ih hm_lt hbi hlow_eq hexcl' hset_eq
+
+/-- Deletion of any key preserves the recursive van Emde Boas representation invariant. -/
+theorem valid_erase {t : Tree d} (ht : t.Valid) (x : ℕ) : (t.erase x).Valid :=
+  (erase_spec ht x).1
+
+/-- Deletion removes `x` and preserves membership of every other key. -/
+theorem contains_erase {t : Tree d} (ht : t.Valid) (x y : ℕ) :
+    (t.erase x).Contains y ↔ y ≠ x ∧ t.Contains y :=
+  (erase_spec ht x).2 y
+
+private theorem clusterMax_eq_of_valid {m M : ℕ} {s : Tree d}
+    {c : Fin (universeSize d) → Tree d} (ht : (node (some (m, M)) s c).Valid) :
+    clusterMax m s c = M := by
+  have he := ht.extrema
+  simp only [Extrema, bounds] at he
+  have ⟨_, hs, hc, ho, hmin⟩ := ht
+  have hv' := valid_node_of_clusterMax (ht.contains_lt he.2.2.1) hs hc ho hmin
+  have he' := hv'.extrema
+  simp only [Extrema, bounds] at he'
+  have hsame : ∀ z, (node (some (m, clusterMax m s c)) s c).Contains z ↔
+      (node (some (m, M)) s c).Contains z := by
+    intro z
+    simp [contains_node_some]
+  have h1 : clusterMax m s c ≤ M := (he.2.2.2.2 _ ((hsame _).mp he'.2.2.2.1)).2
+  have h2 : M ≤ clusterMax m s c := (he'.2.2.2.2 _ ((hsame _).mpr he.2.2.2.1)).2
+  omega
+
+/-- Deleting a key not represented by a valid tree returns the exact tree `t`. -/
+theorem erase_eq_of_not_contains {t : Tree d} (ht : t.Valid) {x : ℕ}
+    (hx : ¬t.Contains x) : t.erase x = t := by
+  induction d generalizing x with
+  | zero =>
+    cases t with
+    | leaf b =>
+      cases b with
+      | none => rfl
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        simp only [contains_leaf_some, not_or] at hx
+        simp [erase, hx.1, hx.2]
+  | succ d ih =>
+    cases t with
+    | node b s c =>
+      cases b with
+      | none => rfl
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        have he := ht.extrema
+        simp only [Extrema, bounds] at he
+        by_cases hout : x < m ∨ M < x
+        · rw [erase, ite_eq_left hout]
+        · have hxm : x ≠ m := fun h => hx (h ▸ he.2.2.1)
+          have heq : m ≠ M := by
+            intro h
+            apply hxm
+            omega
+          have hx_lt : x < universeSize (d + 1) :=
+            Nat.lt_of_le_of_lt (show x ≤ M by omega) he.2.1
+          have hx_div : x / universeSize d < universeSize d :=
+            (Nat.div_lt_iff_lt_mul (universeSize_pos d)).mpr hx_lt
+          let i : Fin (universeSize d) := ⟨x / universeSize d, hx_div⟩
+          let low := x % universeSize d
+          have hx_decomp : x = i.val * universeSize d + low := by
+            simpa only [i, low, Nat.mul_comm] using
+              (Nat.div_add_mod x (universeSize d)).symm
+          have hnot_low : ¬(c i).Contains low := by
+            intro hlow
+            exact hx ⟨m, M, rfl, Or.inr ⟨i, low, hlow, hx_decomp⟩⟩
+          have htarget : eraseTarget m x s c = some ⟨m, i, low⟩ := by
+            simp [eraseTarget, hxm, hx_div, i, low]
+          rw [erase, ite_eq_right hout, ite_eq_right heq, htarget]
+          dsimp only
+          cases hbi : (c i).bounds with
+          | none => rfl
+          | some cb =>
+            obtain ⟨cm, cM⟩ := cb
+            dsimp only
+            by_cases hcm : cm = cM
+            · subst cM
+              have hne : low ≠ cm := fun h =>
+                hnot_low (h ▸ (ht.2.2.1 i).contains_minimum hbi)
+              rw [ite_eq_left rfl, ite_eq_right hne]
+            · rw [ite_eq_right hcm]
+              have hci_eq : erase (c i) low = c i := ih (ht.2.2.1 i) hnot_low
+              have hc_eq : Function.update c i (erase (c i) low) = c := by
+                rw [hci_eq]
+                funext k
+                by_cases hk : k = i
+                · subst k; simp
+                · simp [hk]
+              rw [hc_eq, clusterMax_eq_of_valid ht]
+
+end Cslib.Algorithms.Lean.VanEmdeBoas.Tree
diff --git a/Complexity/Algorithms/Lean/VanEmdeBoas/Predecessor.lean b/Complexity/Algorithms/Lean/VanEmdeBoas/Predecessor.lean
new file mode 100644
index 000000000..d6f89523b
--- /dev/null
+++ b/Complexity/Algorithms/Lean/VanEmdeBoas/Predecessor.lean
@@ -0,0 +1,311 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.Lean.VanEmdeBoas.Basic
+import Mathlib.Tactic.Linarith
+
+/-!
+# Strict van Emde Boas predecessor
+
+This module defines and verifies strict predecessor lookup on recursive minimum-excluded
+van Emde Boas trees ([Demaine2015VanEmdeBoas], p. 5; [CLRS2009], Section 20.3, p. 552).
+The algorithm returns the greatest represented key strictly less than its query, or `none` when
+every represented key is at least the query. Queries need not lie inside `[0, universeSize d)`.
+
+Because each internal node stores its minimum `m` outside its clusters, `predecessor` is slightly
+asymmetric with `successor`: when `m < x ≤ M` and neither `x`'s cluster nor any earlier nonempty
+cluster recorded in `summary` contains a key below `x`, `predecessor` falls back to returning
+`some m` in `O(1)`. These are mathematical correctness statements, without a machine cost claim.
+
+## Main definitions
+
+* `Tree.predecessor`: strict predecessor query on `Tree d`.
+
+## Main results
+
+* `Tree.predecessor_empty`: predecessor lookup on `empty d` returns `none`.
+* `Tree.predecessor_spec`: the successful and unsuccessful result specifications.
+* `Tree.predecessor_eq_some_iff`: success is equivalent to being the greatest smaller stored key.
+* `Tree.predecessor_eq_none_iff`: failure is equivalent to having no smaller stored key.
+* `Tree.predecessor_isSome_of_gt_min`: a query strictly above the cached minimum always has a
+  strict predecessor in `[0, universeSize d)`.
+
+## References
+
+* [E. Demaine, *Divide and conquer: van Emde Boas trees*, Lecture 4][Demaine2015VanEmdeBoas]
+* [T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, *Introduction to Algorithms*,
+  Section 20.3][CLRS2009]
+-/
+
+public section
+
+namespace Cslib.Algorithms.Lean.VanEmdeBoas.Tree
+
+/-- The greatest stored key strictly less than the query, or `none` if it does not exist.
+The cached cluster minimum chooses between one cluster recursion and one summary recursion;
+when no cluster entry precedes `x > m`, the excluded node minimum `m` is returned
+([Demaine2015VanEmdeBoas], p. 5; [CLRS2009], Section 20.3, p. 552). -/
+@[expose] def predecessor : {d : ℕ} → Tree d → ℕ → Option ℕ
+  | 0, .leaf b, x => match b with
+    | none => none
+    | some (m, M) => if M < x then some M else if m < x then some m else none
+  | d + 1, .node b s c, x => match b with
+    | none => none
+    | some (m, M) =>
+      if M < x then some M
+      else if x ≤ m then none
+      else if h : x / universeSize d < universeSize d then
+        let i : Fin (universeSize d) := ⟨x / universeSize d, h⟩
+        let low := x % universeSize d
+        if (c i).minimum.any (· < low) then
+          (predecessor (c i) low).map (i.val * universeSize d + ·)
+        else
+          match predecessor s i.val with
+          | some j =>
+            if hj : j < universeSize d then
+              (c ⟨j, hj⟩).maximum.map (j * universeSize d + ·)
+            else none
+          | none => some m
+      else none
+
+/-- Predecessor lookup on the empty tree at depth `d` always returns `none`. -/
+@[simp] theorem predecessor_empty (d x : ℕ) : (empty d).predecessor x = none := by
+  cases d <;> rfl
+
+private theorem index_lt_index {u i j a b : ℕ} (ha : a < u) (hij : i < j) :
+    i * u + a < j * u + b := by
+  have h := Nat.mul_le_mul_right u (show i + 1 ≤ j by omega)
+  nlinarith
+
+private theorem bounds_isSome_of_contains {d : ℕ} {t : Tree d} {x : ℕ}
+    (hx : t.Contains x) : t.bounds.isSome = true := by
+  cases hb : t.bounds with
+  | none => exact False.elim (not_contains_of_bounds_none hb x hx)
+  | some _ => rfl
+
+private theorem minimum_any_iff {d x : ℕ} {t : Tree d} :
+    t.minimum.any (· < x) = true ↔ ∃ m M, t.bounds = some (m, M) ∧ m < x := by
+  cases hb : t.bounds with
+  | none => simp [minimum, hb]
+  | some b => obtain ⟨m, M⟩ := b; simp [minimum, hb]
+
+/-- A returned key is the greatest represented key strictly below the query; failure certifies
+that every represented key is at least the query. No bound on the query is required. -/
+theorem predecessor_spec {d : ℕ} {t : Tree d} (ht : t.Valid) (x : ℕ) :
+    match t.predecessor x with
+    | some y => t.Contains y ∧ y < x ∧ ∀ z, t.Contains z → z < x → z ≤ y
+    | none => ∀ z, t.Contains z → x ≤ z := by
+  induction d generalizing x with
+  | zero =>
+    cases t with
+    | leaf b =>
+      cases b with
+      | none => simp [predecessor, Contains]
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        have he := ht.extrema
+        simp only [Extrema, bounds] at he
+        by_cases hM : M < x
+        · rw [predecessor, ite_eq_left hM]
+          exact ⟨he.2.2.2.1, hM, fun z hz _ => (he.2.2.2.2 z hz).2⟩
+        · by_cases hm : m < x
+          · rw [predecessor, ite_eq_right hM, ite_eq_left hm]
+            refine ⟨he.2.2.1, hm, ?_⟩
+            intro z hz hzx
+            obtain ⟨m', M', hb, hz⟩ := hz
+            cases hb
+            rcases hz with rfl | rfl <;> omega
+          · rw [predecessor, ite_eq_right hM, ite_eq_right hm]
+            intro z hz
+            have := (he.2.2.2.2 z hz).1
+            omega
+  | succ d ih =>
+    cases t with
+    | node b s c =>
+      cases b with
+      | none => simp [predecessor, Contains]
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        have he := ht.extrema
+        simp only [Extrema, bounds] at he
+        by_cases hM : M < x
+        · rw [predecessor, ite_eq_left hM]
+          exact ⟨he.2.2.2.1, hM, fun z hz _ => (he.2.2.2.2 z hz).2⟩
+        · by_cases hm : x ≤ m
+          · rw [predecessor, ite_eq_right hM, ite_eq_left hm]
+            intro z hz
+            exact hm.trans (he.2.2.2.2 z hz).1
+          · have hi : x / universeSize d < universeSize d := by
+              apply (Nat.div_lt_iff_lt_mul (universeSize_pos d)).mpr
+              exact Nat.lt_of_le_of_lt (show x ≤ M by omega) he.2.1
+            let i : Fin (universeSize d) := ⟨x / universeSize d, hi⟩
+            have hx : x = i.val * universeSize d + x % universeSize d := by
+              simpa only [i, Nat.mul_comm] using (Nat.div_add_mod x (universeSize d)).symm
+            have hoc : ∀ j y, (c j).Contains y → s.Contains j.val := by
+              intro j y hy
+              exact (ht.2.2.2.1 j).mpr (bounds_isSome_of_contains hy)
+            rw [predecessor, ite_eq_right hM, ite_eq_right hm, dite_eq_left hi]
+            by_cases hc : (c i).minimum.any (· < x % universeSize d) = true
+            · rw [ite_eq_left hc]
+              have hp := ih (ht.2.2.1 i) (x % universeSize d)
+              cases hpred : (c i).predecessor (x % universeSize d) with
+              | none =>
+                simp only [hpred] at hp
+                obtain ⟨cm, cM, hb, hlt⟩ := minimum_any_iff.mp hc
+                have := hp cm ((ht.2.2.1 i).contains_minimum hb)
+                omega
+              | some y =>
+                simp only [hpred] at hp
+                simp only [Option.map_some]
+                refine ⟨⟨m, M, rfl, Or.inr ⟨i, y, hp.1, rfl⟩⟩, ?_, ?_⟩
+                · exact (Nat.add_lt_add_left hp.2.1 (i.val * universeSize d)).trans_eq hx.symm
+                · intro z hz hzx
+                  obtain ⟨m', M', hb, hz⟩ := hz
+                  cases hb
+                  rcases hz with rfl | ⟨j, a, ha, rfl⟩
+                  · exact (ht.2.2.2.2 i y hp.1).le
+                  · have hja := cluster_coordinates (i := j.val) (universeSize_pos d)
+                      ((ht.2.2.1 j).contains_lt ha)
+                    have hji : j.val ≤ i.val := by
+                      have h := Nat.div_le_div_right (c := universeSize d) (Nat.le_of_lt hzx)
+                      simpa only [i, hja.1] using h
+                    by_cases hij' : j = i
+                    · subst j
+                      have hlow : a < x % universeSize d := by omega
+                      exact Nat.add_le_add_left (hp.2.2 a ha hlow) (i.val * universeSize d)
+                    · have hlt : j.val < i.val := by
+                        have : j.val ≠ i.val := fun h => hij' (Fin.ext h)
+                        omega
+                      exact (index_lt_index ((ht.2.2.1 j).contains_lt ha) hlt).le
+            · rw [ite_eq_right hc]
+              have hge : ∀ a, (c i).Contains a → x % universeSize d ≤ a := by
+                intro a ha
+                have hce := (ht.2.2.1 i).extrema
+                cases hb : (c i).bounds with
+                | none => exact False.elim (not_contains_of_bounds_none hb a ha)
+                | some b =>
+                  obtain ⟨cm, cM⟩ := b
+                  simp only [Extrema, hb] at hce
+                  have hn : ¬cm < x % universeSize d := by
+                    intro hlt
+                    exact hc (minimum_any_iff.mpr ⟨cm, cM, hb, hlt⟩)
+                  have := (hce.2.2.2.2 a ha).1
+                  omega
+              have hearlier : ∀ j a, (c j).Contains a →
+                  j.val * universeSize d + a < x → j.val < i.val := by
+                intro j a ha hax
+                have hja := cluster_coordinates (i := j.val) (universeSize_pos d)
+                  ((ht.2.2.1 j).contains_lt ha)
+                have hji : j.val ≤ i.val := by
+                  have h := Nat.div_le_div_right (c := universeSize d) (Nat.le_of_lt hax)
+                  simpa only [i, hja.1] using h
+                by_cases hlt : j.val < i.val
+                · exact hlt
+                · have hij' : i = j := Fin.ext (by omega)
+                  subst j
+                  have := hge a ha
+                  omega
+              have hp := ih ht.2.1 i.val
+              cases hpred : s.predecessor i.val with
+              | none =>
+                simp only [hpred] at hp
+                refine ⟨he.2.2.1, by omega, ?_⟩
+                intro z hz hzx
+                obtain ⟨m', M', hb, hz⟩ := hz
+                cases hb
+                rcases hz with rfl | ⟨j, a, ha, rfl⟩
+                · exact le_rfl
+                · have := hearlier j a ha hzx
+                  have := hp j.val (hoc j a ha)
+                  omega
+              | some j =>
+                simp only [hpred] at hp
+                have hj := ht.2.1.contains_lt hp.1
+                let k : Fin (universeSize d) := ⟨j, hj⟩
+                have hk : (c k).bounds.isSome = true := (ht.2.2.2.1 k).mp hp.1
+                cases hb : (c k).bounds with
+                | none => simp [hb] at hk
+                | some b =>
+                  obtain ⟨cm, cM⟩ := b
+                  have hce := (ht.2.2.1 k).extrema
+                  simp only [Extrema, hb] at hce
+                  dsimp only
+                  rw [dite_eq_left hj, maximum, hb]
+                  simp only [Option.map_some]
+                  refine ⟨⟨m, M, rfl, Or.inr ⟨k, cM, hce.2.2.2.1, rfl⟩⟩, ?_, ?_⟩
+                  · exact (index_lt_index (b := x % universeSize d) hce.2.1 hp.2.1).trans_eq hx.symm
+                  · intro z hz hzx
+                    obtain ⟨m', M', hb', hz⟩ := hz
+                    cases hb'
+                    rcases hz with rfl | ⟨l, a, ha, rfl⟩
+                    · exact (ht.2.2.2.2 k cM hce.2.2.2.1).le
+                    · have hli := hearlier l a ha hzx
+                      have hlk := hp.2.2 l.val (hoc l a ha) hli
+                      by_cases hlk' : l = k
+                      · subst l
+                        exact Nat.add_le_add_left (hce.2.2.2.2 a ha).2
+                          (k.val * universeSize d)
+                      · have hlt : l.val < k.val := by
+                          have : l.val ≠ k.val := fun h => hlk' (Fin.ext h)
+                          change l.val < j
+                          change l.val ≠ j at this
+                          omega
+                        exact (index_lt_index ((ht.2.2.1 l).contains_lt ha) hlt).le
+
+/-- A successful result is exactly the greatest represented key strictly less than the query. -/
+theorem predecessor_eq_some_iff {d : ℕ} {t : Tree d} (ht : t.Valid) (x y : ℕ) :
+    t.predecessor x = some y ↔
+      t.Contains y ∧ y < x ∧ ∀ z, t.Contains z → z < x → z ≤ y := by
+  have hp := predecessor_spec ht x
+  cases h : t.predecessor x with
+  | none =>
+    simp only [h] at hp
+    simp only [reduceCtorEq, false_iff]
+    intro hy
+    have := hp y hy.1
+    omega
+  | some z =>
+    simp only [h] at hp
+    constructor
+    · intro hy
+      cases hy
+      exact hp
+    · intro hy
+      have := hp.2.2 y hy.1 hy.2.1
+      have := hy.2.2 z hp.1 hp.2.1
+      congr 1
+      omega
+
+/-- Failure is exactly the absence of a represented key strictly below the query. -/
+theorem predecessor_eq_none_iff {d : ℕ} {t : Tree d} (ht : t.Valid) (x : ℕ) :
+    t.predecessor x = none ↔ ∀ z, t.Contains z → x ≤ z := by
+  have hp := predecessor_spec ht x
+  cases h : t.predecessor x with
+  | none => simp only [h] at hp; exact ⟨fun _ => hp, fun _ => rfl⟩
+  | some y =>
+    simp only [h] at hp
+    simp only [reduceCtorEq, false_iff]
+    intro hn
+    have := hn y hp.1
+    omega
+
+/-- A valid node with a query strictly above its cached minimum always has a strict predecessor
+in `[0, universeSize d)`. -/
+theorem predecessor_isSome_of_gt_min {d m M query : ℕ} {tree : Tree d}
+    (ht : tree.Valid) (hb : tree.bounds = some (m, M)) (hq : m < query) :
+    ∃ ans < universeSize d, tree.predecessor query = some ans := by
+  cases hp : tree.predecessor query with
+  | none =>
+    have hge := (predecessor_eq_none_iff ht query).mp hp m (ht.contains_minimum hb)
+    omega
+  | some ans =>
+    have hspec := (predecessor_eq_some_iff ht query ans).mp hp
+    exact ⟨ans, ht.contains_lt hspec.1, rfl⟩
+
+end Cslib.Algorithms.Lean.VanEmdeBoas.Tree
diff --git a/Complexity/Algorithms/Lean/VanEmdeBoas/Stateful.lean b/Complexity/Algorithms/Lean/VanEmdeBoas/Stateful.lean
new file mode 100644
index 000000000..eee8b5dbf
--- /dev/null
+++ b/Complexity/Algorithms/Lean/VanEmdeBoas/Stateful.lean
@@ -0,0 +1,584 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.Lean.VanEmdeBoas.Elements
+public import Complexity.Foundations.Data.OrderedSet.Spec
+public import Complexity.Foundations.Semantics.Stateful.Resource
+public import Mathlib.Data.Fintype.Fin
+public import Mathlib.Order.Fin.Basic
+
+/-!
+# Stateful ordered-set realization by recursive van Emde Boas trees
+
+This module realizes the shared `Cslib.OrderedSet.spec (Fin (universeSize d))` interface
+(`contains`, `insert`, `erase`, `minimum`, `successor`) using recursive minimum-excluded
+van Emde Boas trees `Tree d` over the bounded universe `Fin (universeSize d)` of size
+`universeSize d = 2 ^ (2 ^ d)`, and supplies an active-recursive-call depth certificate
+`callDepthBound` of `d + 1` per operation ([Demaine2015VanEmdeBoas], pp. 4–6; [CLRS2009],
+Section 20.3).
+
+Alongside `Cslib.Algorithms.Lean.SearchTree` (linear worst-case bound `s.card`), this provides a
+bounded-universe realization of `Cslib.OrderedSet.spec` with doubly-logarithmic recursion depth
+`d + 1` on bounded integer keys.
+
+## Cost model and limitations
+
+Native operation traces count **active recursive van Emde Boas calls** (`1` at the root plus the
+active calls of the single recursive subcall, if any, at each internal level; at most `d + 1` per
+operation). In particular:
+* Empty-node insertion (`bounds = none`) and singleton-node deletion (`bounds = some (m, m)`)
+  terminate in `1` active call without recursing into children.
+* Non-recursive `O(1)` child-header reads and updates (`bounds`, `minimum`, `maximum`,
+  `withBounds`, `eraseTarget`, `clusterMax`), immutable `Function.update` cluster-array updates,
+  initial tree allocation (`Tree.empty d`, whose span is `O(universeSize d)`), division/modulo
+  coordinate arithmetic, `Fin` bounds wrapping, and pure client continuations are **not** charged
+  here. See `Complexity.Algorithms.WordRAM.VanEmdeBoas.Model` (and its companion initialization,
+  membership, insertion, and successor modules; Word-RAM deletion and predecessor remain separate)
+  for explicit Word-RAM memory and instruction accounting.
+
+## Main definitions
+
+* `Tree.memberVisits`, `Tree.insertVisits`, `Tree.eraseVisits`, `Tree.minimumVisits`,
+  `Tree.successorVisits`, `Tree.predecessorVisits`: active recursive-call counts for `Tree d`
+  operations.
+* `Tree.finElements`, `Tree.finMinimum`, `Tree.finSuccessor`, `Tree.finPredecessor`: typed
+  `Fin (universeSize d)` observations and queries.
+* `step`, `Exec`, `run`: concrete `OrderedSet.Op (Fin (universeSize d))` step, native execution
+  relation, and executable client interpreter.
+* `Rep`, `realization`, `callDepthBound`: representation relation, semantic realization of
+  `OrderedSet.spec (Fin (universeSize d))`, and uniform `d + 1` per-operation resource bound.
+
+## Main results
+
+* `Tree.memberVisits_le`, `Tree.insertVisits_le`, `Tree.eraseVisits_le`,
+  `Tree.minimumVisits_le`, `Tree.successorVisits_le`, `Tree.predecessorVisits_le`: each operation
+  makes at most `d + 1` active recursive calls.
+* `Tree.insertVisits_of_bounds_none`, `Tree.eraseVisits_of_bounds_eq`: `O(1)` single-call base
+  cases on empty insertion and singleton deletion.
+* `Rep.valid`, `Rep.finElements_eq`, `rep_empty`, `realization_rep`: representation projections
+  and empty-set initialization.
+* `callDepthBound`, `realized_client`, `run_correct`: adaptive `OrderedSet` clients execute with
+  finite-set correctness and total active-call cost at most `history.length * (d + 1)`.
+
+## References
+
+* [E. Demaine, *Divide and conquer: van Emde Boas trees*, Lecture 4][Demaine2015VanEmdeBoas]
+* [T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, *Introduction to Algorithms*,
+  Section 20.3][CLRS2009]
+-/
+
+public section
+
+namespace Cslib.Algorithms.Lean.VanEmdeBoas
+
+open Cslib.Stateful Cslib.OrderedSet
+
+/-- Every van Emde Boas universe size is nonzero, enabling `OfNat (Fin (universeSize d))` numerals
+for bounded-key clients. -/
+instance instNeZeroUniverseSize (d : ℕ) : NeZero (universeSize d) :=
+  ⟨(universeSize_pos d).ne'⟩
+
+namespace Tree
+
+variable {d : ℕ}
+
+/-- Active recursive calls performed by `Tree.minimum` (`1` root header read). -/
+@[expose] def minimumVisits (_ : Tree d) : ℕ := 1
+
+/-- Active recursive calls performed by `Tree.member`. -/
+@[expose] def memberVisits : {d : ℕ} → Tree d → ℕ → ℕ
+  | 0, .leaf _, _ => 1
+  | d + 1, .node b _ c, x => match b with
+    | none => 1
+    | some (m, _) =>
+      if x = m then 1
+      else if h : x / universeSize d < universeSize d then
+        1 + memberVisits (c ⟨x / universeSize d, h⟩) (x % universeSize d)
+      else 1
+
+/-- Active recursive calls performed by `Tree.insert`. -/
+@[expose] def insertVisits : {d : ℕ} → Tree d → ℕ → ℕ
+  | 0, .leaf _, _ => 1
+  | d + 1, .node b s c, x => match b with
+    | none => 1
+    | some (m, _) =>
+      if x = m then 1
+      else
+        let displaced := max m x
+        if h : displaced / universeSize d < universeSize d then
+          let i : Fin (universeSize d) := ⟨displaced / universeSize d, h⟩
+          match (c i).bounds with
+          | none => 1 + insertVisits s i.val
+          | some _ => 1 + insertVisits (c i) (displaced % universeSize d)
+        else 1
+
+/-- Active recursive calls performed by `Tree.erase`. -/
+@[expose] def eraseVisits : {d : ℕ} → Tree d → ℕ → ℕ
+  | 0, .leaf _, _ => 1
+  | _ + 1, .node b s c, x => match b with
+    | none => 1
+    | some (m, M) =>
+      if x < m ∨ M < x then 1
+      else if m = M then 1
+      else
+        match eraseTarget m x s c with
+        | none => 1
+        | some ⟨_, i, low⟩ =>
+          match (c i).bounds with
+          | none => 1
+          | some (cm, cM) =>
+            if cm = cM then
+              if low = cm then 1 + eraseVisits s i.val else 1
+            else 1 + eraseVisits (c i) low
+
+/-- Active recursive calls performed by `Tree.successor`. -/
+@[expose] def successorVisits : {d : ℕ} → Tree d → ℕ → ℕ
+  | 0, .leaf _, _ => 1
+  | d + 1, .node b s c, x => match b with
+    | none => 1
+    | some (m, M) =>
+      if x < m then 1
+      else if M ≤ x then 1
+      else if h : x / universeSize d < universeSize d then
+        let i : Fin (universeSize d) := ⟨x / universeSize d, h⟩
+        let low := x % universeSize d
+        if (c i).maximum.any (low < ·) then
+          1 + successorVisits (c i) low
+        else
+          1 + successorVisits s i.val
+      else 1
+
+/-- Active recursive calls performed by `Tree.predecessor`. -/
+@[expose] def predecessorVisits : {d : ℕ} → Tree d → ℕ → ℕ
+  | 0, .leaf _, _ => 1
+  | d + 1, .node b s c, x => match b with
+    | none => 1
+    | some (m, M) =>
+      if M < x then 1
+      else if x ≤ m then 1
+      else if h : x / universeSize d < universeSize d then
+        let i : Fin (universeSize d) := ⟨x / universeSize d, h⟩
+        let low := x % universeSize d
+        if (c i).minimum.any (· < low) then
+          1 + predecessorVisits (c i) low
+        else
+          1 + predecessorVisits s i.val
+      else 1
+
+/-- `minimum` performs `1 ≤ d + 1` active calls. -/
+theorem minimumVisits_le (t : Tree d) : t.minimumVisits ≤ d + 1 :=
+  Nat.succ_le_succ (Nat.zero_le d)
+
+/-- `member` performs at most `d + 1` active recursive calls. -/
+theorem memberVisits_le (t : Tree d) (x : ℕ) : t.memberVisits x ≤ d + 1 := by
+  induction d generalizing x with
+  | zero => cases t; exact le_rfl
+  | succ d ih =>
+    cases t with
+    | node b s c =>
+      cases b with
+      | none => exact Nat.succ_le_succ (Nat.zero_le _)
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        simp only [memberVisits]
+        split_ifs with hm hi
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+        · have := ih (c ⟨x / universeSize d, hi⟩) (x % universeSize d)
+          omega
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+
+/-- Inserting into an empty node performs only `1` active call at any depth. -/
+theorem insertVisits_of_bounds_none {t : Tree d} (hb : t.bounds = none) (x : ℕ) :
+    t.insertVisits x = 1 := by
+  cases t with
+  | leaf b => rfl
+  | node b s c =>
+    simp only [bounds] at hb
+    subst b
+    rfl
+
+/-- `insert` performs at most `d + 1` active recursive calls. -/
+theorem insertVisits_le (t : Tree d) (x : ℕ) : t.insertVisits x ≤ d + 1 := by
+  induction d generalizing x with
+  | zero => cases t; exact le_rfl
+  | succ d ih =>
+    cases t with
+    | node b s c =>
+      cases b with
+      | none => exact Nat.succ_le_succ (Nat.zero_le _)
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        simp only [insertVisits]
+        split_ifs with hm hi
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+        · cases (c ⟨max m x / universeSize d, hi⟩).bounds with
+          | none =>
+            dsimp only
+            have := ih s (max m x / universeSize d)
+            omega
+          | some _ =>
+            dsimp only
+            have := ih (c ⟨max m x / universeSize d, hi⟩) (max m x % universeSize d)
+            omega
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+
+/-- Deleting from a singleton node (`bounds = some (m, m)`) performs only `1` active call at any
+depth. -/
+theorem eraseVisits_of_bounds_eq {t : Tree d} {m : ℕ} (hb : t.bounds = some (m, m)) (x : ℕ) :
+    t.eraseVisits x = 1 := by
+  cases t with
+  | leaf b => rfl
+  | node b s c =>
+    simp only [bounds] at hb
+    subst b
+    simp [eraseVisits]
+
+/-- `erase` performs at most `d + 1` active recursive calls. -/
+theorem eraseVisits_le (t : Tree d) (x : ℕ) : t.eraseVisits x ≤ d + 1 := by
+  induction d generalizing x with
+  | zero => cases t; exact le_rfl
+  | succ d ih =>
+    cases t with
+    | node b s c =>
+      cases b with
+      | none => exact Nat.succ_le_succ (Nat.zero_le _)
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        simp only [eraseVisits]
+        split_ifs with hout heq
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+        · cases eraseTarget m x s c with
+          | none =>
+            dsimp only
+            exact Nat.succ_le_succ (Nat.zero_le _)
+          | some tgt =>
+            obtain ⟨newMin, i, low⟩ := tgt
+            dsimp only
+            cases (c i).bounds with
+            | none =>
+              dsimp only
+              exact Nat.succ_le_succ (Nat.zero_le _)
+            | some cb =>
+              obtain ⟨cm, cM⟩ := cb
+              dsimp only
+              split_ifs
+              · have := ih s i.val
+                omega
+              · exact Nat.succ_le_succ (Nat.zero_le _)
+              · have := ih (c i) low
+                omega
+
+/-- `successor` performs at most `d + 1` active recursive calls. -/
+theorem successorVisits_le (t : Tree d) (x : ℕ) : t.successorVisits x ≤ d + 1 := by
+  induction d generalizing x with
+  | zero => cases t; exact le_rfl
+  | succ d ih =>
+    cases t with
+    | node b s c =>
+      cases b with
+      | none => exact Nat.succ_le_succ (Nat.zero_le _)
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        simp only [successorVisits]
+        split_ifs with hm hM hi hc
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+        · have := ih (c ⟨x / universeSize d, hi⟩) (x % universeSize d)
+          omega
+        · have := ih s (x / universeSize d)
+          omega
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+
+/-- `predecessor` performs at most `d + 1` active recursive calls. -/
+theorem predecessorVisits_le (t : Tree d) (x : ℕ) : t.predecessorVisits x ≤ d + 1 := by
+  induction d generalizing x with
+  | zero => cases t; exact le_rfl
+  | succ d ih =>
+    cases t with
+    | node b s c =>
+      cases b with
+      | none => exact Nat.succ_le_succ (Nat.zero_le _)
+      | some b =>
+        obtain ⟨m, M⟩ := b
+        simp only [predecessorVisits]
+        split_ifs with hM hm hi hc
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+        · have := ih (c ⟨x / universeSize d, hi⟩) (x % universeSize d)
+          omega
+        · have := ih s (x / universeSize d)
+          omega
+        · exact Nat.succ_le_succ (Nat.zero_le _)
+
+/-- Mathematical finite-set observation in `Fin (universeSize d)`. -/
+@[expose] def finElements (t : Tree d) : Finset (Fin (universeSize d)) :=
+  Finset.univ.filter fun x => t.member x.val
+
+/-- Membership in `finElements` agrees with `Tree.Contains` on valid trees. -/
+theorem mem_finElements_iff {t : Tree d} (ht : t.Valid) (x : Fin (universeSize d)) :
+    x ∈ t.finElements ↔ t.Contains x.val := by
+  simp only [finElements, Finset.mem_filter, Finset.mem_univ, true_and, member_iff_contains ht]
+
+/-- Membership in `finElements` agrees with `Tree.elements` on `x.val`. -/
+theorem mem_finElements_iff_val_mem_elements {t : Tree d} (ht : t.Valid)
+    (x : Fin (universeSize d)) : x ∈ t.finElements ↔ x.val ∈ t.elements := by
+  rw [mem_finElements_iff ht, mem_elements_iff ht]
+
+/-- The empty tree represents the empty finite set of bounded keys. -/
+@[simp] theorem finElements_empty (d : ℕ) : (empty d).finElements = ∅ := by
+  ext x
+  simp only [mem_finElements_iff (valid_empty d), contains_empty, Finset.notMem_empty]
+
+/-- Bounded insertion commutes with `finElements`. -/
+theorem finElements_insert {t : Tree d} (ht : t.Valid) (x : Fin (universeSize d)) :
+    (t.insert x.val).finElements = Insert.insert x t.finElements := by
+  ext y
+  simp only [mem_finElements_iff (valid_insert ht x.isLt), Finset.mem_insert,
+    mem_finElements_iff ht, contains_insert ht x.isLt, Fin.ext_iff]
+
+/-- Deletion commutes with `finElements`. -/
+theorem finElements_erase {t : Tree d} (ht : t.Valid) (x : Fin (universeSize d)) :
+    (t.erase x.val).finElements = t.finElements.erase x := by
+  ext y
+  simp only [mem_finElements_iff (valid_erase ht x.val), Finset.mem_erase,
+    mem_finElements_iff ht, contains_erase ht, ne_eq, Fin.ext_iff]
+
+/-- Typed `Fin (universeSize d)` minimum read from the cached root bounds. -/
+@[expose] def finMinimum (t : Tree d) : Option (Fin (universeSize d)) :=
+  match t.minimum with
+  | none => none
+  | some m => if hm : m < universeSize d then some ⟨m, hm⟩ else none
+
+/-- Typed `Fin (universeSize d)` strict successor query. -/
+@[expose] def finSuccessor (t : Tree d) (x : Fin (universeSize d)) :
+    Option (Fin (universeSize d)) :=
+  match t.successor x.val with
+  | none => none
+  | some y => if hy : y < universeSize d then some ⟨y, hy⟩ else none
+
+/-- Typed `Fin (universeSize d)` strict predecessor query. -/
+@[expose] def finPredecessor (t : Tree d) (x : Fin (universeSize d)) :
+    Option (Fin (universeSize d)) :=
+  match t.predecessor x.val with
+  | none => none
+  | some y => if hy : y < universeSize d then some ⟨y, hy⟩ else none
+
+/-- `finMinimum` satisfies the optional-minimum contract for `t.finElements`. -/
+theorem finMinimum_spec {t : Tree d} (ht : t.Valid) :
+    LeastResult t.finElements t.finMinimum := by
+  cases hb : t.bounds with
+  | none =>
+    simp only [finMinimum, minimum, hb, Option.map_none, LeastResult]
+    ext x
+    simp only [mem_finElements_iff ht, Finset.notMem_empty, iff_false]
+    exact not_contains_of_bounds_none hb x.val
+  | some b =>
+    obtain ⟨m, M⟩ := b
+    have he := ht.extrema
+    simp only [Extrema, hb] at he
+    have hm : m < universeSize d := ht.contains_lt he.2.2.1
+    simp only [finMinimum, minimum, hb, Option.map_some, dite_eq_left hm, LeastResult,
+      mem_finElements_iff ht]
+    exact ⟨he.2.2.1, fun z hz => (he.2.2.2.2 z.val hz).1⟩
+
+/-- `finSuccessor` satisfies the optional-minimum contract for keys strictly above `x`. -/
+theorem finSuccessor_spec {t : Tree d} (ht : t.Valid) (x : Fin (universeSize d)) :
+    LeastResult (t.finElements.filter (x < ·)) (t.finSuccessor x) := by
+  cases hs : t.successor x.val with
+  | none =>
+    simp only [finSuccessor, hs, LeastResult]
+    have hnone := (successor_eq_none_iff ht x.val).mp hs
+    ext z
+    simp only [Finset.mem_filter, mem_finElements_iff ht, Finset.notMem_empty, iff_false, not_and]
+    intro hz
+    have hle := hnone z.val hz
+    exact not_lt_of_ge hle
+  | some y =>
+    have hy_spec := (successor_eq_some_iff ht x.val y).mp hs
+    have hy : y < universeSize d := ht.contains_lt hy_spec.1
+    simp only [finSuccessor, hs, dite_eq_left hy, LeastResult, Finset.mem_filter,
+      mem_finElements_iff ht]
+    refine ⟨⟨hy_spec.1, hy_spec.2.1⟩, ?_⟩
+    intro z ⟨hz, hxz⟩
+    exact hy_spec.2.2 z.val hz hxz
+
+/-- A successful `finPredecessor` returns the greatest element of `t.finElements` strictly below
+`x`. -/
+theorem finPredecessor_eq_some_iff {t : Tree d} (ht : t.Valid)
+    (x y : Fin (universeSize d)) :
+    t.finPredecessor x = some y ↔
+      y ∈ t.finElements ∧ y < x ∧ ∀ z ∈ t.finElements, z < x → z ≤ y := by
+  constructor
+  · intro h
+    unfold finPredecessor at h
+    cases hp : t.predecessor x.val with
+    | none => simp [hp] at h
+    | some w =>
+      simp only [hp] at h
+      split_ifs at h with hw
+      cases h
+      have hspec := (predecessor_eq_some_iff ht x.val w).mp hp
+      simp only [mem_finElements_iff ht]
+      exact ⟨hspec.1, hspec.2.1, fun z hz hzx => hspec.2.2 z.val hz hzx⟩
+  · rintro ⟨hy, hyx, hmax⟩
+    rw [mem_finElements_iff ht] at hy
+    have hp : t.predecessor x.val = some y.val := by
+      rw [predecessor_eq_some_iff ht]
+      refine ⟨hy, hyx, fun z hz hzx => ?_⟩
+      let z' : Fin (universeSize d) := ⟨z, ht.contains_lt hz⟩
+      exact hmax z' ((mem_finElements_iff ht z').mpr hz) hzx
+    simp [finPredecessor, hp, y.isLt]
+
+/-- `finPredecessor` returns `none` iff every element of `t.finElements` is at least `x`. -/
+theorem finPredecessor_eq_none_iff {t : Tree d} (ht : t.Valid) (x : Fin (universeSize d)) :
+    t.finPredecessor x = none ↔ ∀ z ∈ t.finElements, x ≤ z := by
+  cases hp : t.predecessor x.val with
+  | none =>
+    simp only [finPredecessor, hp, true_iff, mem_finElements_iff ht]
+    have hnone := (predecessor_eq_none_iff ht x.val).mp hp
+    exact fun z hz => hnone z.val hz
+  | some y =>
+    have hspec := (predecessor_eq_some_iff ht x.val y).mp hp
+    have hy : y < universeSize d := ht.contains_lt hspec.1
+    simp only [finPredecessor, hp, dite_eq_left hy, reduceCtorEq, false_iff, not_forall]
+    exact ⟨⟨y, hy⟩, (mem_finElements_iff ht ⟨y, hy⟩).mpr hspec.1, not_le_of_gt hspec.2.1⟩
+
+end Tree
+
+section OrderedSetRealization
+
+variable {d : ℕ}
+
+/-- Execute a single `OrderedSet.Op (Fin (universeSize d))` on `t : Tree d`, returning the updated
+tree, result, and active recursive-call count. -/
+@[expose] def step (t : Tree d) (o : Op (Fin (universeSize d))) :
+    Tree d × (spec (Fin (universeSize d))).Result o × ℕ :=
+  match o with
+  | .contains x => (t, t.member x.val, t.memberVisits x.val)
+  | .insert x => (t.insert x.val, (), t.insertVisits x.val)
+  | .erase x => (t.erase x.val, (), t.eraseVisits x.val)
+  | .minimum => (t, t.finMinimum, t.minimumVisits)
+  | .successor x => (t, t.finSuccessor x, t.successorVisits x.val)
+
+/-- Native execution relation for `OrderedSet.spec (Fin (universeSize d))` over `Tree d`. -/
+@[expose] def Exec (d : ℕ) : Execution (spec (Fin (universeSize d))) (Tree d) ℕ :=
+  fun t o a t' n => step t o = (t', a, n)
+
+/-- Representation relation coupling a finite set `s : Finset (Fin (universeSize d))` with a valid
+van Emde Boas tree `t : Tree d`. -/
+@[expose] def Rep (s : Finset (Fin (universeSize d))) (t : Tree d) : Prop :=
+  t.Valid ∧ t.finElements = s
+
+/-- Extract `Tree.Valid` from `Rep`. -/
+theorem Rep.valid {s : Finset (Fin (universeSize d))} {t : Tree d} (hr : Rep s t) :
+    t.Valid := hr.1
+
+/-- Extract the `finElements` equality from `Rep`. -/
+theorem Rep.finElements_eq {s : Finset (Fin (universeSize d))} {t : Tree d} (hr : Rep s t) :
+    t.finElements = s := hr.2
+
+/-- `Tree.empty d` represents the empty `Finset (Fin (universeSize d))`. -/
+theorem rep_empty (d : ℕ) : Rep (∅ : Finset (Fin (universeSize d))) (Tree.empty d) :=
+  ⟨Tree.valid_empty d, Tree.finElements_empty d⟩
+
+/-- Semantic realization of `OrderedSet.spec (Fin (universeSize d))` by `Tree d`. -/
+@[expose] def realization (d : ℕ) :
+    Realization (spec (Fin (universeSize d))) (Exec d) where
+  rep := Rep
+  total {_ t} o _ _ :=
+    match h : step t o with
+    | (t', a, n) => ⟨a, t', n, h⟩
+  correct {s t o a t' n} hr _ he := by
+    obtain ⟨ht, rfl⟩ := hr
+    cases o with
+    | contains x =>
+      cases he
+      refine ⟨?_, ht, rfl⟩
+      have h := (Tree.member_iff_contains ht x.val).trans (Tree.mem_finElements_iff ht x).symm
+      by_cases hx : x ∈ t.finElements <;> simp_all
+    | insert x =>
+      cases he
+      exact ⟨rfl, Tree.valid_insert ht x.isLt, Tree.finElements_insert ht x⟩
+    | erase x =>
+      cases he
+      exact ⟨rfl, Tree.valid_erase ht x.val, Tree.finElements_erase ht x⟩
+    | minimum =>
+      cases he
+      exact ⟨(Tree.finMinimum_spec ht).eq_least, ht, rfl⟩
+    | successor x =>
+      cases he
+      exact ⟨(Tree.finSuccessor_spec ht x).eq_least, ht, rfl⟩
+
+/-- `(realization d).rep` is definitionally `Rep`. -/
+@[simp] theorem realization_rep (d : ℕ) : (realization d).rep = Rep := rfl
+
+/-- Every native `OrderedSet` operation on `Tree d` performs at most `d + 1` active recursive
+calls. -/
+theorem exec_visits_le {t t' : Tree d} {o : Op (Fin (universeSize d))}
+    {a : (spec (Fin (universeSize d))).Result o} {n : ℕ} (he : Exec d t o a t' n) :
+    n ≤ d + 1 := by
+  cases o with
+  | contains x => cases he; exact Tree.memberVisits_le t x.val
+  | insert x => cases he; exact Tree.insertVisits_le t x.val
+  | erase x => cases he; exact Tree.eraseVisits_le t x.val
+  | minimum => cases he; exact Tree.minimumVisits_le t
+  | successor x => cases he; exact Tree.successorVisits_le t x.val
+
+/-- Uniform `d + 1` active-call depth bound (`O(log log U)` since `universeSize d = 2 ^ (2 ^ d)`)
+for `VanEmdeBoas.realization d`. -/
+theorem callDepthBound (d : ℕ) : Bound (realization d) id (fun _ _ => d + 1) := by
+  intro _ _ _ _ _ _ _ _ he
+  exact exec_visits_le he
+
+/-- Every adaptive `OrderedSet` client over `Fin (universeSize d)` executes on `Tree d` with
+finite-set correctness and total active recursive calls at most `history.length * (d + 1)`. -/
+theorem realized_client {β : Type} (p : (spec (Fin (universeSize d))).Client β)
+    {s : Finset (Fin (universeSize d))} {t : Tree d} (hr : Rep s t) :
+    ∃ t' ns, Executes (Exec d) p t ((spec (Fin (universeSize d))).runClient s p).1 t' ns ∧
+      Rep ((spec (Fin (universeSize d))).runClient s p).2.1 t' ∧
+      total id ns ≤ ((spec (Fin (universeSize d))).runClient s p).2.2.length * (d + 1) := by
+  have hv := (spec (Fin (universeSize d))).validHistory_of_forall_valid (fun _ _ => trivial)
+    s ((spec (Fin (universeSize d))).runClient s p).2.2
+  exact Bound.exists_executes_const (callDepthBound d) p hr hv
+
+/-- Execute an `OrderedSet` client concretely on `Tree d`, recording active recursive-call counts
+per operation. -/
+@[expose] def run {β : Type} (t : Tree d) :
+    (spec (Fin (universeSize d))).Client β → β × Tree d × List ℕ
+  | .pure a => (a, t, [])
+  | .liftBind o k =>
+      let (t', a, c) := step t o
+      let (res, t'', cs) := run t' (k a)
+      (res, t'', c :: cs)
+
+/-- The concrete runner produces a valid `Executes (Exec d)` derivation. -/
+theorem run_exec {β : Type} (p : (spec (Fin (universeSize d))).Client β) (t : Tree d) :
+    Executes (Exec d) p t (run t p).1 (run t p).2.1 (run t p).2.2 := by
+  induction p generalizing t with
+  | pure a => exact .pure a t
+  | liftBind o k ih => exact .call rfl (ih _ _)
+
+/-- Running the concrete vEB interpreter agrees with abstract `Finset (Fin (universeSize d))`
+semantics, preserves `Rep`, and satisfies the `history.length * (d + 1)` active-call bound. -/
+theorem run_correct {β : Type} (p : (spec (Fin (universeSize d))).Client β)
+    {s : Finset (Fin (universeSize d))} {t : Tree d} (hr : Rep s t) :
+    (run t p).1 = ((spec (Fin (universeSize d))).runClient s p).1 ∧
+      Rep ((spec (Fin (universeSize d))).runClient s p).2.1 (run t p).2.1 ∧
+      total id (run t p).2.2 ≤
+        ((spec (Fin (universeSize d))).runClient s p).2.2.length * (d + 1) := by
+  have hv := (spec (Fin (universeSize d))).validHistory_of_forall_valid (fun _ _ => trivial)
+    s ((spec (Fin (universeSize d))).runClient s p).2.2
+  have hexec := run_exec p t
+  have hc := (realization d).correct_client hr hv hexec
+  exact ⟨hc.1, hc.2, Bound.client_const (callDepthBound d) hr hv hexec⟩
+
+end OrderedSetRealization
+
+end Cslib.Algorithms.Lean.VanEmdeBoas
diff --git a/ComplexityTests/VanEmdeBoas.lean b/ComplexityTests/VanEmdeBoas.lean
index d3d96ccca..9476e677e 100644
--- a/ComplexityTests/VanEmdeBoas.lean
+++ b/ComplexityTests/VanEmdeBoas.lean
@@ -5,16 +5,19 @@ Authors: Samuel Schlesinger
 -/
 
 module
--- upstream: candidate
+-- upstream: local-only (test driver)
 
-public import Complexity.Algorithms.Lean.VanEmdeBoas.Elements
+public import Complexity.Algorithms.Lean.VanEmdeBoas.Stateful
+public import ComplexityTests.OrderedSet
 
 /-!
-Boundary and adaptive examples for the recursive vEB algorithms. These evaluate Lean functions;
-they do not measure or certify RAM running time.
+Boundary and adaptive examples for the recursive vEB algorithms (`member`, `insert`, `erase`,
+`minimum`, `successor`, `predecessor`) and their `OrderedSet` realization. These evaluate Lean
+functions and active recursive-call counts; they do not measure or certify RAM running time.
 -/
 
 open Cslib.Algorithms.Lean.VanEmdeBoas
+open Cslib.OrderedSet Cslib.Stateful
 
 @[expose] public section
 
@@ -30,37 +33,120 @@ private def membership (d : ℕ) (xs : List ℕ) : List Bool :=
 private def successors (d : ℕ) (xs : List ℕ) : List (Option ℕ) :=
   (List.range (universeSize d + 1)).map (ofList d xs).successor
 
+private def predecessors (d : ℕ) (xs : List ℕ) : List (Option ℕ) :=
+  (List.range (universeSize d + 1)).map (ofList d xs).predecessor
+
 /-- The representation invariant holds on the empty tree and after descending/duplicate
-insertions. -/
-theorem valid_empty_and_inserted :
-    (Tree.empty 2).Valid ∧ (ofList 2 [15, 12, 8, 4, 0, 15]).Valid := by
-  refine ⟨Tree.valid_empty 2, ?_⟩
-  unfold ofList
-  simp only [List.foldl_cons, List.foldl_nil]
-  iterate 6 apply Tree.valid_insert (hx := by decide)
-  exact Tree.valid_empty 2
-
--- Base-case (`d = 0`), descending-minima (`d = 2`), and duplicate-insertion membership and
--- successor evaluations.
+insertions and deletions. -/
+theorem valid_empty_inserted_and_erased :
+    (Tree.empty 2).Valid ∧
+      (ofList 2 [15, 12, 8, 4, 0, 15]).Valid ∧
+      (((ofList 2 [15, 12, 8, 4, 0, 15]).erase 0).erase 15).Valid := by
+  have hv : (ofList 2 [15, 12, 8, 4, 0, 15]).Valid := by
+    unfold ofList
+    simp only [List.foldl_cons, List.foldl_nil]
+    iterate 6 apply Tree.valid_insert (hx := by decide)
+    exact Tree.valid_empty 2
+  exact ⟨Tree.valid_empty 2, hv, Tree.valid_erase (Tree.valid_erase hv 0) 15⟩
+
+/-- Deleting absent keys (empty cluster, singleton-cluster miss, multi-key cluster miss, and
+out-of-range) leaves a valid tree structurally unchanged. -/
+theorem erase_absent_keys_eq :
+    let t := ofList 2 [0, 4, 5, 12, 15]
+    let ts := ofList 2 [0, 4, 12, 15]
+    t.erase 2 = t ∧ ts.erase 6 = ts ∧ t.erase 6 = t ∧ t.erase 13 = t ∧ t.erase 99 = t := by
+  have hv : (ofList 2 [0, 4, 5, 12, 15]).Valid := by
+    unfold ofList
+    simp only [List.foldl_cons, List.foldl_nil]
+    iterate 5 apply Tree.valid_insert (hx := by decide)
+    exact Tree.valid_empty 2
+  have hvs : (ofList 2 [0, 4, 12, 15]).Valid := by
+    unfold ofList
+    simp only [List.foldl_cons, List.foldl_nil]
+    iterate 4 apply Tree.valid_insert (hx := by decide)
+    exact Tree.valid_empty 2
+  have hnot {u : Tree 2} (hu : u.Valid) (x : ℕ) (hm : u.member x = false) :
+      ¬u.Contains x := by
+    rw [← Tree.member_iff_contains hu]
+    simp only [hm, Bool.false_eq_true, not_false_eq_true]
+  exact ⟨Tree.erase_eq_of_not_contains hv (hnot hv 2 (by decide)),
+    Tree.erase_eq_of_not_contains hvs (hnot hvs 6 (by decide)),
+    Tree.erase_eq_of_not_contains hv (hnot hv 6 (by decide)),
+    Tree.erase_eq_of_not_contains hv (hnot hv 13 (by decide)),
+    Tree.erase_eq_of_not_contains hv (hnot hv 99 (by decide))⟩
+
+-- Base-case (`d = 0`), descending-minima (`d = 2`), and duplicate-insertion membership,
+-- successor, and predecessor evaluations (including minimum-exclusion fallback `predecessor 4 = 0`
+-- and out-of-universe query `16`).
 example :
     (membership 0 [] = [false, false, false] ∧
       successors 0 [] = [none, none, none] ∧
+      predecessors 0 [] = [none, none, none] ∧
       membership 0 [0, 0] = [true, false, false] ∧
       successors 0 [0, 0] = [none, none, none] ∧
+      predecessors 0 [0, 0] = [none, some 0, some 0] ∧
       membership 0 [1, 1] = [false, true, false] ∧
       successors 0 [1, 1] = [some 1, none, none] ∧
+      predecessors 0 [1, 1] = [none, none, some 1] ∧
       membership 0 [1, 0, 1, 0] = [true, true, false] ∧
-      successors 0 [1, 0, 1, 0] = [some 1, none, none]) ∧
+      successors 0 [1, 0, 1, 0] = [some 1, none, none] ∧
+      predecessors 0 [1, 0, 1, 0] = [none, some 0, some 1]) ∧
     membership 2 [15, 12, 8, 4, 0] =
       [true, false, false, false, true, false, false, false, true, false, false, false,
         true, false, false, true, false] ∧
     successors 2 [15, 12, 8, 4, 0] =
       [some 4, some 4, some 4, some 4, some 8, some 8, some 8, some 8,
         some 12, some 12, some 12, some 12, some 15, some 15, some 15, none, none] ∧
+    predecessors 2 [15, 12, 8, 4, 0] =
+      [none, some 0, some 0, some 0, some 0, some 4, some 4, some 4,
+        some 4, some 8, some 8, some 8, some 8, some 12, some 12, some 12, some 15] ∧
     membership 2 [8, 4, 12, 2, 10, 0, 15, 8, 4, 12, 2, 10, 0, 15] =
       membership 2 [0, 2, 4, 8, 10, 12, 15] ∧
     successors 2 [8, 4, 12, 2, 10, 0, 15, 8, 4, 12, 2, 10, 0, 15] =
-      successors 2 [0, 2, 4, 8, 10, 12, 15] := by
+      successors 2 [0, 2, 4, 8, 10, 12, 15] ∧
+    predecessors 2 [8, 4, 12, 2, 10, 0, 15, 8, 4, 12, 2, 10, 0, 15] =
+      predecessors 2 [0, 2, 4, 8, 10, 12, 15] := by
+  decide
+
+-- Intra-cluster vs summary-fallback predecessor queries on `[0, 4, 5, 12, 15]`.
+example :
+    let t := ofList 2 [0, 4, 5, 12, 15]
+    t.predecessor 0 = none ∧
+      t.predecessor 4 = some 0 ∧ -- minimum-exclusion fallback (`0` is not in any cluster)
+      t.predecessor 5 = some 4 ∧ -- intra-cluster predecessor (`cluster 1` has min `0 < 1`)
+      t.predecessor 6 = some 5 ∧ -- intra-cluster `M < x`
+      t.predecessor 12 = some 5 ∧ -- summary predecessor (`cluster 3` min `0` not `< 0`, prev `1`)
+      t.predecessor 15 = some 12 ∧ -- intra-cluster predecessor in `cluster 3`
+      t.predecessor 16 = some 15 := by
+  decide
+
+-- Single-recursion deletion cases on `d = 0` and `d = 2`:
+-- excluded-minimum promotion (`erase 0`), singleton-cluster summary deletion (`erase 4`),
+-- multi-key cluster deletion (`erase 15`), and singleton-root `O(1)` clearing (`eraseVisits = 1`).
+example :
+    let t0 := ofList 0 [0, 1]
+    ((t0.erase 2).bounds = some (0, 1) ∧
+      (t0.erase 0).bounds = some (1, 1) ∧
+      (t0.erase 1).bounds = some (0, 0) ∧
+      ((t0.erase 0).erase 1).bounds = none) ∧
+    let t := ofList 2 [0, 4, 5, 12, 15]
+    let t1 := t.erase 0 -- promotes `4` from two-key cluster `1` (`{0, 1}` -> `{1}`)
+    let t2 := t1.erase 4 -- promotes `5` from singleton cluster `1` and erases `1` from summary
+    let t3 := t2.erase 15 -- erases `3` from two-key cluster `3` (`{0, 3}` -> `{0}`), updates max
+    let t4 := t3.erase 5 -- promotes `12`, emptying cluster `3` (`m = M = 12`)
+    let t5 := t4.erase 12 -- singleton root cleared in 1 active call
+    t1.bounds = some (4, 15) ∧
+      t2.bounds = some (5, 15) ∧
+      t3.bounds = some (5, 12) ∧
+      t4.bounds = some (12, 12) ∧
+      t4.eraseVisits 12 = 1 ∧
+      t5.bounds = none ∧
+      (List.range 17).map t3.member =
+        (List.range 17).map ([5, 12].contains ·) ∧
+      (List.range 17).map t3.predecessor =
+        [none, none, none, none, none, none,
+          some 5, some 5, some 5, some 5, some 5, some 5, some 5,
+          some 12, some 12, some 12, some 12] := by
   decide
 
 private def adaptive (choosePresent : Bool) : Bool × Option ℕ × Bool :=
@@ -83,7 +169,7 @@ private def agrees (xs : List ℕ) : Bool :=
     t.member x == xs.contains x &&
       t.successor x == ((List.range 4).filter fun y => xs.contains y && x < y).head?
 
--- Adaptive branching and all 256 four-insertion histories over the four-key universe.
+-- Adaptive branching and all 256 four-insertion histories over the four-key universe (`d = 1`).
 example :
     (adaptive true = (true, some 7, false) ∧ adaptive false = (false, some 3, true)) ∧
     (histories 3).all (fun xs => agrees (0 :: xs)) = true ∧
@@ -92,6 +178,55 @@ example :
     (histories 3).all (fun xs => agrees (3 :: xs)) = true := by
   decide
 
+private def agreesInsertThenErase (ins dels : List ℕ) : Bool :=
+  let t := dels.foldl Tree.erase (ofList 1 ins)
+  let present := fun y => ins.contains y && !dels.contains y
+  (List.range 5).all fun x =>
+    t.member x == present x &&
+      t.successor x == ((List.range 4).filter fun y => present y && x < y).head? &&
+      t.predecessor x == ((List.range 4).filter fun y => present y && y < x).getLast?
+
+-- All 256 mixed 2-insert + 2-erase histories over the four-key universe (`d = 1`), checking
+-- `member`, `successor`, and `predecessor` simultaneously.
+example :
+    (histories 2).all (fun ins =>
+      (histories 2).all (fun dels => agreesInsertThenErase ins dels)) = true := by
+  decide
+
+/-- Adaptive `OrderedSet` client (`insertAll`, `firstTwo`, and two `extractMin` steps) over
+`Fin (universeSize 2)`. -/
+def priorityWorkflow :
+    (spec (Fin (universeSize 2))).Client
+      ((Option (Fin (universeSize 2)) × Option (Fin (universeSize 2))) ×
+        Option (Fin (universeSize 2)) × Option (Fin (universeSize 2))) := do
+  insertAll [12, 5, 0, 15, 4, 5]
+  let pair ← firstTwo
+  let first ← extractMin
+  let second ← extractMin
+  pure (pair, first, second)
+
+private def priorityRes := run (Tree.empty 2) priorityWorkflow
+
+-- Shared `OrderedSet` clients executed on `Tree 2` (`Fin (universeSize 2)`), checking answers,
+-- final `finElements`, and active recursive-call traces (`≤ d + 1 = 3`).
+example :
+    priorityRes.1 = ((some 0, some 4), some 0, some 4) ∧
+      priorityRes.2.1.finElements = {5, 12, 15} ∧
+      priorityRes.2.2 = [1, 2, 3, 3, 3, 3, 1, 2, 1, 3, 1, 3] ∧
+      priorityRes.2.2.all (· ≤ 3) = true := by
+  decide
+
+/-- End-to-end instantiation of `run_correct` and `Bound.client_const (callDepthBound 2)` on an
+adaptive `OrderedSet` client over `Tree.empty 2`. -/
+theorem priorityWorkflow_correct_and_bounded :
+    (run (Tree.empty 2) priorityWorkflow).1 =
+      ((spec (Fin (universeSize 2))).runClient ∅ priorityWorkflow).1 ∧
+    Rep ((spec (Fin (universeSize 2))).runClient ∅ priorityWorkflow).2.1
+      (run (Tree.empty 2) priorityWorkflow).2.1 ∧
+    total id (run (Tree.empty 2) priorityWorkflow).2.2 ≤
+      ((spec (Fin (universeSize 2))).runClient ∅ priorityWorkflow).2.2.length * 3 :=
+  run_correct priorityWorkflow (rep_empty 2)
+
 /--
 info: 'Cslib.Algorithms.Lean.VanEmdeBoas.Tree.valid_empty' depends on axioms: [propext, Quot.sound]
 -/