feat(Algorithms/Lean/VanEmdeBoas): recursive predecessor, single-recursion deletion, and OrderedSet realization #1855

Scope & motivation

ROADMAP.md ("Stateful algorithms and data structures") lists deletion and predecessor for van Emde Boas sets alongside Cslib.Algorithms.Lean.VanEmdeBoas's existing bounded-universe member, insert, and successor ([Demaine2015VanEmdeBoas], Lecture 4; [CLRS2009], Section 20.3).

This milestone completes the functional Lean vEB set operations without modifying VanEmdeBoas/Basic.lean (keeping downstream WordRAM/VanEmdeBoas caches warm) and connects VanEmdeBoas.Tree d to the shared Cslib.OrderedSet.spec (Fin (universeSize d)) stateful interface:

1. Complexity/Algorithms/Lean/VanEmdeBoas/Predecessor.lean:
   • Define Tree.predecessor over all x : ℕ (including queries outside [0, universeSize d)), using cached minimum/maximum headers to choose between at most one cluster recursion and one summary recursion (fallback to some m when s.predecessor i.val = none and m < x).
   • Prove predecessor_spec, predecessor_eq_some_iff, predecessor_eq_none_iff, predecessor_empty, and predecessor_isSome_of_gt_min.
2. Complexity/Algorithms/Lean/VanEmdeBoas/Erase.lean:
   • Define Tree.erase with at most one recursive call per depth level ([Demaine2015VanEmdeBoas], pp. 5–6; [CLRS2009], Section 20.3): singleton clusters are cleared in O(1) via withBounds none (recursing only on summary), while multi-element clusters stay nonempty (recursing only on the cluster without touching summary), and deleting the excluded minimum m promotes the minimum of cluster s.minimum before deleting it from that cluster.
   • Prove valid_erase, contains_erase (∀ y, (t.erase x).Contains y ↔ y ≠ x ∧ t.Contains y), erase_empty, and erase_eq_of_not_contains.
3. Complexity/Algorithms/Lean/VanEmdeBoas/Elements.lean:
   • Add elements_erase ((t.erase x).elements = t.elements.erase x) and predecessor_elements_some_iff / predecessor_elements_none_iff.
4. Complexity/Algorithms/Lean/VanEmdeBoas/Stateful.lean & ComplexityTests/VanEmdeBoas.lean:
   • Define exact recursive vEB tree-node visit counters (memberVisits, insertVisits, eraseVisits, successorVisits, predecessorVisits, all bounded by d + 1) and realize Cslib.OrderedSet.spec (Fin (universeSize d)) with uniform d + 1 (O(log log U)) tree-node visit bounds (nodeVisitBound, realized_client, run, run_correct).
   • Extend ComplexityTests/VanEmdeBoas.lean with exhaustive history checks, multi-depth deletion/predecessor boundary cases, choice-freeness #print axioms checks, and shared OrderedSet client (extractMin, firstTwo, insertAll) executions; leave Word-RAM erase/predecessor assembly programs as explicit remaining work in ROADMAP.md.

Task ownership

• Role: Worker (worker-jetski-54df4165)
• State: active
• Branch: feat/veb-predecessor-erase-54df4165