feat(Algorithms/Lean): stateful disjoint-set interface and logarithmic bounds for Batteries.UnionFind #1810

Introduce a representation-independent stateful disjoint-set specification over Fin n and certify Batteries.UnionFind as a realization with explicit logarithmic worst-case step bounds. This is a bounded data-structure prerequisite toward the spanning-tree and matroid optimization track in ROADMAP.md ("minimum spanning trees with sorting and disjoint-set costs") and CSLib's verified Batteries data-structures track.

Scope and completion criteria:

• Complexity/Algorithms/Lean/DisjointSet.lean: computable Partition n over Fin n with Setoid and Relation.EqvGen bridges, component set and numComponents laws (numComponents_discrete = n, effective merges decrement numComponents by 1), and Cslib.Algorithms.Lean.DisjointSet.spec n : Cslib.Stateful.Spec (same, union returning whether two distinct components were merged, and numComponents).
• Complexity/Algorithms/Lean/DisjointSet/UnionFind.lean: reuse Batteries.UnionFind directly; prove the root equivalence-class size invariant 2 ^ uf.rank r ≤ |{i < uf.size | uf.rootD i = r}| across empty, push, find (path compression), link (on roots), checkEquiv, and union ([CLRS2009], Section 21.3, Lemma 21.4 and Exercise 21.4-2); deduce uf.rank u ≤ Nat.log 2 uf.size and bound findAux parent-pointer accesses by Nat.log 2 n + 1, giving a Cslib.Stateful.Bound on adaptive clients.
• ComplexityTests/DisjointSet.lean: checked concrete instances covering n = 0, n = 1, chain construction and path-compression flattening, duplicate vs effective unions, EqvGen equivalence, and an adaptive cycle-detection / component-counting client.
• Full validation (scripts/check.sh, hygiene, changed-files audit) and independent correctness/API review before integration.

Out of scope (remaining open in ROADMAP.md): Tarjan's amortized O(m α(n)) inverse-Ackermann analysis, native Word-RAM SubroutineDS realization (here findSteps counts parent-pointer hops rather than array-copy or RAM instructions), and Kruskal's minimum spanning forest algorithm.

Worker/session: worker-jetski-54df4165. Branch: feat/disjoint-set-union-find-54df4165.