diff --git a/Cslib.lean b/Cslib.lean
index eea1f4491..7cc7b9fb7 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -2,6 +2,10 @@ module  -- shake: keep-all --deprecated_module: ignore
 
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.Algorithms.Lean.UnionFind.Basic
+public import Cslib.Algorithms.Lean.UnionFind.Cost
+public import Cslib.Algorithms.Lean.UnionFind.Operations
+public import Cslib.Algorithms.Lean.UnionFind.RankBound
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Computability.Automata.DA.Basic
diff --git a/Cslib/Algorithms/Lean/UnionFind/Basic.lean b/Cslib/Algorithms/Lean/UnionFind/Basic.lean
new file mode 100644
index 000000000..512c2e256
--- /dev/null
+++ b/Cslib/Algorithms/Lean/UnionFind/Basic.lean
@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2026 Aviv Bar Natan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aviv Bar Natan
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.Finset.Card
+public import Mathlib.Data.Fintype.Basic
+
+/-!
+# Union-Find Forest Model
+
+This file defines a mathematical model of a union-by-rank union-find forest over `Fin n`.
+
+## Main definitions
+
+* `UnionFind`: A forest over `n` elements given by parent and rank functions.
+* `UnionFind.IsRoot`: A node is a root iff it is its own parent.
+* `UnionFind.reaches`: Reachability by following parent pointers.
+* `UnionFind.subtree`: The set of nodes that reach a given root.
+* `UnionFind.subtreeSize`: The cardinality of a subtree.
+* `UnionFind.WellFormed`: Well-formedness for union by rank.
+
+## Main results
+
+* `UnionFind.self_mem_subtree`: Every node belongs to its own subtree.
+* `UnionFind.one_le_subtreeSize`: Every subtree is nonempty.
+* `UnionFind.subtreeSize_le`: Every subtree has at most `n` nodes.
+-/
+
+@[expose] public section
+
+set_option autoImplicit false
+
+namespace Cslib.Algorithms.Lean
+
+variable {n : ℕ}
+
+/-- A union-find forest over `n` elements, given by parent and rank functions. -/
+structure UnionFind (n : ℕ) where
+  /-- Parent pointer; roots point to themselves. -/
+  parent : Fin n → Fin n
+  /-- Rank (an upper bound on subtree height) of each node. -/
+  rank : Fin n → ℕ
+
+namespace UnionFind
+
+variable (uf : UnionFind n)
+
+/-- `i` is a root iff it is its own parent. -/
+def IsRoot (i : Fin n) : Prop := uf.parent i = i
+
+instance (i : Fin n) : Decidable (uf.IsRoot i) := by unfold IsRoot; infer_instance
+
+/-- `j` reaches `i` by following parent pointers some number of times. -/
+def reaches (j i : Fin n) : Prop := ∃ k, uf.parent^[k] j = i
+
+open Classical in
+/-- The set of all nodes `j` that reach `i` by following parent pointers. -/
+noncomputable def subtree (i : Fin n) : Finset (Fin n) :=
+  Finset.univ.filter (fun j => uf.reaches j i)
+
+/-- The number of nodes in the subtree rooted at `i`. -/
+noncomputable def subtreeSize (i : Fin n) : ℕ := (uf.subtree i).card
+
+/-- Well-formedness for union by rank: ranks increase toward roots, and a rank-`r` node
+owns at least `2 ^ r` nodes. -/
+structure WellFormed : Prop where
+  /-- Non-root nodes have strictly smaller rank than their parent. -/
+  rank_lt : ∀ i, ¬ uf.IsRoot i → uf.rank i < uf.rank (uf.parent i)
+  /-- A rank-`r` node owns at least `2 ^ r` nodes. -/
+  size_ge : ∀ i, 2 ^ uf.rank i ≤ uf.subtreeSize i
+
+/-- Every node reaches itself in zero steps. -/
+@[simp] lemma reaches_self (i : Fin n) : uf.reaches i i := ⟨0, rfl⟩
+
+open Classical in
+/-- A node is always in its own subtree. -/
+@[simp] lemma self_mem_subtree (i : Fin n) : i ∈ uf.subtree i := by
+  simp only [subtree, Finset.mem_filter, Finset.mem_univ, reaches_self, and_self]
+
+/-- Every subtree is nonempty. -/
+@[simp] lemma one_le_subtreeSize (i : Fin n) : 1 ≤ uf.subtreeSize i := by
+  unfold subtreeSize
+  exact Finset.card_pos.mpr ⟨i, uf.self_mem_subtree i⟩
+
+open Classical in
+/-- A subtree has at most `n` nodes. -/
+lemma subtreeSize_le (i : Fin n) : uf.subtreeSize i ≤ n := by
+  unfold subtreeSize subtree
+  have hle : (Finset.univ.filter (fun j => uf.reaches j i)).card ≤ Finset.univ.card :=
+    Finset.card_le_card (Finset.filter_subset _ _)
+  have huniv : (Finset.univ : Finset (Fin n)).card = n := by
+    simp [Finset.card_def, Fin.univ_def, List.length_finRange]
+  omega
+
+end UnionFind
+
+end Cslib.Algorithms.Lean
diff --git a/Cslib/Algorithms/Lean/UnionFind/Cost.lean b/Cslib/Algorithms/Lean/UnionFind/Cost.lean
new file mode 100644
index 000000000..f1fc58fa2
--- /dev/null
+++ b/Cslib/Algorithms/Lean/UnionFind/Cost.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Aviv Bar Natan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aviv Bar Natan
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Algorithms.Lean.UnionFind.RankBound
+public import Cslib.Algorithms.Lean.TimeM
+
+/-!
+# Timed `find` for Union-Find
+
+This file expresses the `find` operation of union-find in the `TimeM` cost monad,
+charging one tick per parent dereference. We prove that `find` returns the correct
+root (`find_ret`), that its tick cost equals the find depth (`find_time`), and that
+in a well-formed union-by-rank forest it runs in at most `⌊log₂ n⌋` ticks
+(`find_time_le_log`).
+
+Following the `TimeM` convention, correctness is proved on `.ret` and complexity on
+`.time`.
+
+## Main definitions
+
+* `UnionFind.findAux`: follow `k` parent pointers from `x`, charging one tick per hop.
+* `UnionFind.find`: follow parent pointers to the root, charging one tick per dereference.
+
+## Main results
+
+* `UnionFind.find_ret`: `find` returns the root of `i`.
+* `UnionFind.find_time`: `find`'s tick cost equals the find depth.
+* `UnionFind.find_time_le_log`: `find` runs in at most `⌊log₂ n⌋` ticks.
+-/
+
+@[expose] public section
+
+set_option autoImplicit false
+
+namespace Cslib.Algorithms.Lean.UnionFind
+
+open Cslib.Algorithms.Lean (TimeM)
+
+variable {n : ℕ} (uf : UnionFind n)
+
+/-- Auxiliary for `find`: follow `k` parent pointers from `x`, charging one tick per hop. -/
+def findAux (uf : UnionFind n) : ℕ → Fin n → TimeM ℕ (Fin n)
+  | 0, x => pure x
+  | (k + 1), x => do ✓ uf.findAux k (uf.parent x)
+
+/-- The value returned by `findAux k x` is the `k`-th parent iterate of `x`. -/
+@[simp] lemma findAux_ret (k : ℕ) (x : Fin n) : (uf.findAux k x).ret = uf.parent^[k] x := by
+  induction k generalizing x with
+  | zero => simp [findAux]
+  | succ k ih => simp [findAux, ih]
+
+/-- `findAux k x` costs exactly `k` ticks. -/
+@[simp] lemma findAux_time (k : ℕ) (x : Fin n) : (uf.findAux k x).time = k := by
+  induction k generalizing x with
+  | zero => simp [findAux]
+  | succ k ih => simp [findAux, ih]; omega
+
+/-- `find i` follows parent pointers to `i`'s root, charging one tick per dereference. -/
+noncomputable def find (hwf : uf.WellFormed) (i : Fin n) : TimeM ℕ (Fin n) :=
+  uf.findAux (uf.findDepth hwf i) i
+
+/-- `find` returns the root of `i`. -/
+lemma find_ret (hwf : uf.WellFormed) (i : Fin n) : (uf.find hwf i).ret = uf.findRoot hwf i := by
+  simp [find, findAux_ret, findRoot]
+
+/-- `find`'s tick cost is exactly the find depth. -/
+lemma find_time (hwf : uf.WellFormed) (i : Fin n) : (uf.find hwf i).time = uf.findDepth hwf i := by
+  simp [find, findAux_time]
+
+/-- `find` runs in at most `⌊log₂ n⌋` ticks. -/
+theorem find_time_le_log (hwf : uf.WellFormed) (i : Fin n) :
+    (uf.find hwf i).time ≤ Nat.log 2 n := by
+  rw [uf.find_time hwf i]; exact uf.findDepth_le_log hwf i
+
+end Cslib.Algorithms.Lean.UnionFind
diff --git a/Cslib/Algorithms/Lean/UnionFind/Operations.lean b/Cslib/Algorithms/Lean/UnionFind/Operations.lean
new file mode 100644
index 000000000..669bd98ba
--- /dev/null
+++ b/Cslib/Algorithms/Lean/UnionFind/Operations.lean
@@ -0,0 +1,293 @@
+/-
+Copyright (c) 2026 Aviv Bar Natan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aviv Bar Natan
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Algorithms.Lean.UnionFind.Basic
+
+/-!
+# Union-Find Operations
+
+This file constructs the initial `singleton` forest, in which every element is its own
+root with rank `0`, and proves it well-formed. This witnesses that the `WellFormed`
+hypothesis used throughout the rank-bound development is satisfiable, so the
+`findDepth_le_log` bound is non-vacuous.
+
+It also defines the `link` operation (union by rank) and the reusable helper lemmas about
+reachability under a parent-pointer `Function.update` that underpin its correctness.
+
+## Main definitions
+
+* `UnionFind.singleton`: The forest where every element is its own root with rank `0`.
+* `UnionFind.link`: Union by rank, attaching the lower-rank root under the higher-rank one.
+
+## Main results
+
+* `UnionFind.singleton_wellFormed`: The singleton forest is well-formed.
+* `UnionFind.iterate_parent_isRoot`: Following parents from a root stays at that root.
+* `UnionFind.reaches_root_unique`: Each node reaches a unique root.
+* `UnionFind.iterate_update_eq_of_forall_ne`: Updating a parent pointer leaves a path
+  unchanged as long as the path avoids the updated key.
+* `UnionFind.subtree_subset_attach`: Attaching a root under another node only grows subtrees.
+* `UnionFind.subtree_root_subset_attach`: After attaching root `a` under root `b`, every node of
+  `a`'s old subtree lands in `b`'s new subtree.
+* `UnionFind.subtreeSize_attach_ge`: After attaching root `a` under root `b`, the new subtree of
+  `b` is at least as large as the two old subtrees combined.
+* `UnionFind.link_wellFormed`: Union by rank preserves well-formedness — linking two distinct
+  roots of a well-formed forest yields a well-formed forest. Consequently the `findDepth_le_log`
+  bound applies to every forest built from singletons by unions.
+-/
+
+@[expose] public section
+
+set_option autoImplicit false
+
+namespace Cslib.Algorithms.Lean.UnionFind
+
+variable {n : ℕ} (uf : UnionFind n)
+
+/-- The forest where every element is its own root with rank `0`. -/
+def singleton (n : ℕ) : UnionFind n where
+  parent := id
+  rank := fun _ => 0
+
+/-- The parent function of the singleton forest is the identity. -/
+@[simp] lemma singleton_parent (i : Fin n) : (singleton n).parent i = i := rfl
+
+/-- Every element of a singleton forest is a root. -/
+@[simp] lemma singleton_isRoot (i : Fin n) : (singleton n).IsRoot i := rfl
+
+/-- The singleton forest is well-formed, so the `WellFormed` hypothesis is satisfiable. -/
+theorem singleton_wellFormed : (singleton n).WellFormed where
+  rank_lt i h := absurd (singleton_isRoot i) h
+  size_ge i := by
+    change 2 ^ 0 ≤ (singleton n).subtreeSize i
+    simp only [Nat.pow_zero]
+    exact (singleton n).one_le_subtreeSize i
+
+/-- Link two roots `a` and `b` using union by rank: attach the lower-rank root under the
+  higher-rank one; on a tie, attach `a` under `b` and increment `b`'s rank. Only the parent of
+  the demoted root, and (on a tie) the rank of `b`, change. -/
+def link (uf : UnionFind n) (a b : Fin n) : UnionFind n :=
+  if uf.rank a < uf.rank b then
+    { uf with parent := Function.update uf.parent a b }
+  else if uf.rank b < uf.rank a then
+    { uf with parent := Function.update uf.parent b a }
+  else
+    { uf with
+      parent := Function.update uf.parent a b
+      rank := Function.update uf.rank b (uf.rank b + 1) }
+
+/-- Following parents from a root stays at that root. -/
+lemma iterate_parent_isRoot {x : Fin n} (hx : uf.IsRoot x) (m : ℕ) :
+    uf.parent^[m] x = x := by
+  induction m with
+  | zero => rfl
+  | succ k ih => rw [Function.iterate_succ_apply', ih]; exact hx
+
+/-- A node reaches at most one root: the root reached by following parents is unique. -/
+lemma reaches_root_unique {j r₁ r₂ : Fin n}
+    (h₁ : uf.reaches j r₁) (hr₁ : uf.IsRoot r₁)
+    (h₂ : uf.reaches j r₂) (hr₂ : uf.IsRoot r₂) : r₁ = r₂ := by
+  obtain ⟨k₁, hk₁⟩ := h₁
+  obtain ⟨k₂, hk₂⟩ := h₂
+  rcases le_total k₁ k₂ with hle | hle
+  · have heq : uf.parent^[k₂] j = uf.parent^[k₂ - k₁] (uf.parent^[k₁] j) := by
+      rw [← Function.iterate_add_apply, Nat.sub_add_cancel hle]
+    rw [hk₁, uf.iterate_parent_isRoot hr₁] at heq
+    rw [hk₂] at heq
+    exact heq.symm
+  · have heq : uf.parent^[k₁] j = uf.parent^[k₁ - k₂] (uf.parent^[k₂] j) := by
+      rw [← Function.iterate_add_apply, Nat.sub_add_cancel hle]
+    rw [hk₂, uf.iterate_parent_isRoot hr₂] at heq
+    rw [hk₁] at heq
+    exact heq
+
+/-- Iterating an updated parent function agrees with the original as long as the path from
+`j` never visits the updated key `a` (within the first `k` steps). -/
+lemma iterate_update_eq_of_forall_ne {p : Fin n → Fin n} {a b j : Fin n} {k : ℕ}
+    (h : ∀ m, m < k → p^[m] j ≠ a) :
+    (Function.update p a b)^[k] j = p^[k] j := by
+  induction k with
+  | zero => rfl
+  | succ k ih =>
+    rw [Function.iterate_succ_apply', Function.iterate_succ_apply',
+      ih (fun m hm => h m (by omega))]
+    exact Function.update_of_ne (h k (by omega)) b p
+
+/-- Attaching root `a` under another node `b` only grows subtrees: every old subtree
+is contained in the corresponding subtree of the updated forest. -/
+lemma subtree_subset_attach {a b : Fin n} (ha : uf.IsRoot a)
+    (uf' : UnionFind n) (hp : uf'.parent = Function.update uf.parent a b) (i : Fin n) :
+    uf.subtree i ⊆ uf'.subtree i := by
+  classical
+  intro j hj
+  simp only [subtree, Finset.mem_filter, Finset.mem_univ, true_and] at hj ⊢
+  obtain ⟨k₀, hk₀⟩ := hj
+  -- minimal step count reaching `i`
+  let k := Nat.find (⟨k₀, hk₀⟩ : ∃ k, uf.parent^[k] j = i)
+  have hk : uf.parent^[k] j = i := Nat.find_spec (⟨k₀, hk₀⟩ : ∃ k, uf.parent^[k] j = i)
+  have hmin : ∀ m, m < k → ¬ (uf.parent^[m] j = i) :=
+    fun m hm => Nat.find_min (⟨k₀, hk₀⟩ : ∃ k, uf.parent^[k] j = i) hm
+  -- the path avoids `a` strictly before reaching `i`
+  have key : ∀ m, m < k → uf.parent^[m] j ≠ a := by
+    intro m hm hma
+    -- if the path hits `a` at step m, then it stays at `a = i` from then on
+    have hcancel : uf.parent^[k] j = uf.parent^[k - m] (uf.parent^[m] j) := by
+      rw [← Function.iterate_add_apply, Nat.sub_add_cancel hm.le]
+    rw [hma, uf.iterate_parent_isRoot ha] at hcancel
+    rw [hk] at hcancel
+    -- so `i = a`, hence `uf.parent^[m] j = i`, contradicting minimality
+    exact hmin m hm (by rw [hma, ← hcancel])
+  refine ⟨k, ?_⟩
+  rw [hp, iterate_update_eq_of_forall_ne key, hk]
+
+/-- If `a`'s parent pointer is redirected to `b`, every node of `a`'s old subtree lands in
+`b`'s new subtree. -/
+lemma subtree_root_subset_attach {a b : Fin n}
+    (uf' : UnionFind n) (hp : uf'.parent = Function.update uf.parent a b) :
+    uf.subtree a ⊆ uf'.subtree b := by
+  classical
+  intro j hj
+  simp only [subtree, Finset.mem_filter, Finset.mem_univ, true_and] at hj ⊢
+  obtain ⟨k₀, hk₀⟩ := hj
+  -- minimal step count reaching `a`
+  let k := Nat.find (⟨k₀, hk₀⟩ : ∃ k, uf.parent^[k] j = a)
+  have hk : uf.parent^[k] j = a := Nat.find_spec (⟨k₀, hk₀⟩ : ∃ k, uf.parent^[k] j = a)
+  have hmin : ∀ m, m < k → ¬ (uf.parent^[m] j = a) :=
+    fun m hm => Nat.find_min (⟨k₀, hk₀⟩ : ∃ k, uf.parent^[k] j = a) hm
+  have key := hmin
+  -- after `k` steps in `uf'` we are at `a`; one more step lands at `b`
+  have hk' : uf'.parent^[k] j = a := by
+    rw [hp, iterate_update_eq_of_forall_ne key, hk]
+  refine ⟨k + 1, ?_⟩
+  rw [Function.iterate_succ_apply', hk', hp, Function.update_self]
+
+/-- After attaching root `a` under root `b`, the new subtree of `b` is at least as large as the
+two old subtrees combined. -/
+lemma subtreeSize_attach_ge {a b : Fin n} (ha : uf.IsRoot a) (hb : uf.IsRoot b) (hab : a ≠ b)
+    (uf' : UnionFind n) (hp : uf'.parent = Function.update uf.parent a b) :
+    uf.subtreeSize b + uf.subtreeSize a ≤ uf'.subtreeSize b := by
+  classical
+  have hsub_b : uf.subtree b ⊆ uf'.subtree b := uf.subtree_subset_attach ha uf' hp b
+  have hsub_a : uf.subtree a ⊆ uf'.subtree b := uf.subtree_root_subset_attach uf' hp
+  have hdisj : Disjoint (uf.subtree b) (uf.subtree a) := by
+    rw [Finset.disjoint_left]
+    intro j hjb hja
+    simp only [subtree, Finset.mem_filter, Finset.mem_univ, true_and] at hjb hja
+    exact hab (uf.reaches_root_unique hja ha hjb hb)
+  calc uf.subtreeSize b + uf.subtreeSize a
+      = (uf.subtree b ∪ uf.subtree a).card := (Finset.card_union_of_disjoint hdisj).symm
+    _ ≤ (uf'.subtree b).card := Finset.card_le_card (Finset.union_subset hsub_b hsub_a)
+    _ = uf'.subtreeSize b := rfl
+
+/-- Subtree sizes only grow when a root `a` is attached under `b`. -/
+private lemma subtreeSize_le_attach {a b : Fin n} (ha : uf.IsRoot a)
+    (uf' : UnionFind n) (hp : uf'.parent = Function.update uf.parent a b) (i : Fin n) :
+    uf.subtreeSize i ≤ uf'.subtreeSize i :=
+  Finset.card_le_card (uf.subtree_subset_attach ha uf' hp i)
+
+/-- Attaching a strictly-lower-rank root `a` under root `b` (ranks unchanged) preserves
+well-formedness. -/
+private lemma attach_lt_wellFormed (hwf : uf.WellFormed) {a b : Fin n}
+    (ha : uf.IsRoot a) (hr : uf.rank a < uf.rank b) :
+    ({ uf with parent := Function.update uf.parent a b }).WellFormed := by
+  set uf' : UnionFind n := { uf with parent := Function.update uf.parent a b } with huf'
+  refine ⟨fun i hi => ?_, fun i => ?_⟩
+  · -- rank_lt
+    by_cases hia : i = a
+    · subst hia
+      have hp : uf'.parent i = b := Function.update_self ..
+      rw [hp]
+      exact hr
+    · have hp : uf'.parent i = uf.parent i := Function.update_of_ne hia b uf.parent
+      have hnr : ¬ uf.IsRoot i := by
+        intro hroot
+        apply hi
+        change uf'.parent i = i
+        rw [hp]; exact hroot
+      rw [hp]
+      exact hwf.rank_lt i hnr
+  · -- size_ge
+    exact (hwf.size_ge i).trans (uf.subtreeSize_le_attach ha uf' rfl i)
+
+/-- The tie case: attaching `a` under `b` and incrementing `b`'s rank preserves
+well-formedness. -/
+private lemma attach_eq_wellFormed (hwf : uf.WellFormed) {a b : Fin n}
+    (ha : uf.IsRoot a) (hb : uf.IsRoot b) (hab : a ≠ b) (hr : uf.rank a = uf.rank b) :
+    ({ uf with parent := Function.update uf.parent a b,
+               rank := Function.update uf.rank b (uf.rank b + 1) }).WellFormed := by
+  set uf' : UnionFind n :=
+    { uf with parent := Function.update uf.parent a b,
+              rank := Function.update uf.rank b (uf.rank b + 1) } with huf'
+  have hba : b ≠ a := fun h => hab h.symm
+  refine ⟨fun i hi => ?_, fun i => ?_⟩
+  · -- rank_lt
+    by_cases hia : i = a
+    · subst hia
+      have hpi : uf'.parent i = b := Function.update_self ..
+      have hri : uf'.rank i = uf.rank i := Function.update_of_ne hab _ _
+      have hrb : uf'.rank b = uf.rank b + 1 := Function.update_self ..
+      rw [hpi, hri, hrb]
+      omega
+    · have hpi : uf'.parent i = uf.parent i := Function.update_of_ne hia b uf.parent
+      have hnr : ¬ uf.IsRoot i := by
+        intro hroot
+        apply hi
+        change uf'.parent i = i
+        rw [hpi]; exact hroot
+      have hlt := hwf.rank_lt i hnr
+      by_cases hib : i = b
+      · -- vacuous: b is a root in uf', contradicting hi
+        exfalso
+        apply hi
+        change uf'.parent i = i
+        rw [hpi, hib]
+        exact hb
+      · have hri : uf'.rank i = uf.rank i := Function.update_of_ne hib _ _
+        rw [hpi, hri]
+        by_cases hpb : uf.parent i = b
+        · have hrp : uf'.rank (uf.parent i) = uf.rank b + 1 := by
+            rw [hpb]; exact Function.update_self ..
+          rw [hrp]
+          rw [hpb] at hlt
+          omega
+        · have hrp : uf'.rank (uf.parent i) = uf.rank (uf.parent i) :=
+            Function.update_of_ne hpb _ _
+          rw [hrp]
+          exact hlt
+  · -- size_ge
+    by_cases hib : i = b
+    · subst hib
+      have hri : uf'.rank i = uf.rank i + 1 := Function.update_self ..
+      rw [hri]
+      have hpow : 2 ^ (uf.rank i + 1) = 2 ^ uf.rank i + 2 ^ uf.rank i := by
+        rw [Nat.pow_succ]; omega
+      have hsb : 2 ^ uf.rank i ≤ uf.subtreeSize i := hwf.size_ge i
+      have hsa : 2 ^ uf.rank i ≤ uf.subtreeSize a := by
+        have := hwf.size_ge a
+        rwa [hr] at this
+      have hgrow : uf.subtreeSize i + uf.subtreeSize a ≤ uf'.subtreeSize i :=
+        uf.subtreeSize_attach_ge ha hb hab uf' rfl
+      rw [hpow]
+      omega
+    · have hri : uf'.rank i = uf.rank i := Function.update_of_ne hib _ _
+      rw [hri]
+      exact (hwf.size_ge i).trans (uf.subtreeSize_le_attach ha uf' rfl i)
+
+/-- Union by rank preserves well-formedness: linking two distinct roots of a well-formed
+forest yields a well-formed forest. -/
+theorem link_wellFormed (hwf : uf.WellFormed) {a b : Fin n}
+    (ha : uf.IsRoot a) (hb : uf.IsRoot b) (hab : a ≠ b) :
+    (uf.link a b).WellFormed := by
+  rw [link]
+  split_ifs with h1 h2
+  · exact uf.attach_lt_wellFormed hwf ha h1
+  · exact uf.attach_lt_wellFormed hwf hb h2
+  · exact uf.attach_eq_wellFormed hwf ha hb hab (by omega)
+
+end Cslib.Algorithms.Lean.UnionFind
diff --git a/Cslib/Algorithms/Lean/UnionFind/RankBound.lean b/Cslib/Algorithms/Lean/UnionFind/RankBound.lean
new file mode 100644
index 000000000..1f8be5dc7
--- /dev/null
+++ b/Cslib/Algorithms/Lean/UnionFind/RankBound.lean
@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2026 Aviv Bar Natan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aviv Bar Natan
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Algorithms.Lean.UnionFind.Basic
+public import Mathlib.Data.Nat.Log
+
+/-!
+# Rank Bound for Union-Find
+
+This file proves that in a well-formed union-by-rank forest, every rank is at
+most `⌊log₂ n⌋`, and uses this bound to define the `find` traversal abstractly.
+
+## Main definitions
+
+* `UnionFind.findDepth`: The number of parent dereferences needed to reach the root from `i`.
+* `UnionFind.findRoot`: The root reached from `i` by following `findDepth` parent pointers.
+
+## Main results
+
+* `UnionFind.rank_le_log`: In a well-formed forest, `rank i ≤ Nat.log 2 n` for all `i`.
+* `UnionFind.exists_isRoot_iterate`: Following parent pointers from any node eventually
+  reaches a root.
+* `UnionFind.isRoot_findRoot`: `findRoot hwf i` is always a root.
+* `UnionFind.not_isRoot_of_lt_findDepth`: Every step strictly before `findDepth` lands on
+  a non-root.
+* `UnionFind.rank_iterate_ge`: Along the find path, the rank grows by at least one per step.
+* `UnionFind.findDepth_le_log`: In a well-formed forest, `find` dereferences at most
+  `⌊log₂ n⌋` parent pointers.
+-/
+
+@[expose] public section
+
+set_option autoImplicit false
+
+namespace Cslib.Algorithms.Lean.UnionFind
+
+variable {n : ℕ} (uf : UnionFind n)
+
+/-- In a well-formed forest, every rank is at most `⌊log₂ n⌋`. -/
+theorem rank_le_log (hwf : uf.WellFormed) (i : Fin n) : uf.rank i ≤ Nat.log 2 n := by
+  have hsize_ge : 2 ^ uf.rank i ≤ uf.subtreeSize i := hwf.size_ge i
+  have hsize_le : uf.subtreeSize i ≤ n := uf.subtreeSize_le i
+  have h1 : uf.rank i ≤ Nat.log 2 (uf.subtreeSize i) :=
+    Nat.le_log_of_pow_le (by omega) hsize_ge
+  exact h1.trans (Nat.log_mono_right hsize_le)
+
+/-- Following parent pointers from any node reaches a root in finitely many steps. -/
+theorem exists_isRoot_iterate (hwf : uf.WellFormed) (i : Fin n) :
+    ∃ k, uf.IsRoot (uf.parent^[k] i) := by
+  by_contra h
+  push Not at h
+  set f : ℕ → ℕ := fun k => uf.rank (uf.parent^[k] i) with hf
+  have hmono : StrictMono f := by
+    apply strictMono_nat_of_lt_succ
+    intro k
+    have hk : ¬ uf.IsRoot (uf.parent^[k] i) := h k
+    have := hwf.rank_lt (uf.parent^[k] i) hk
+    simp only [hf]
+    rw [Function.iterate_succ_apply']
+    exact this
+  have hle : ∀ k, k ≤ f k := by
+    intro k
+    induction k with
+    | zero => exact Nat.zero_le _
+    | succ m ih => exact Nat.succ_le_of_lt (lt_of_le_of_lt ih (hmono (Nat.lt_succ_self m)))
+  have hbound : ∀ k, f k ≤ Nat.log 2 n := fun k => uf.rank_le_log hwf _
+  have h1 := hle (Nat.log 2 n + 1)
+  have h2 := hbound (Nat.log 2 n + 1)
+  omega
+
+/-- The number of parent dereferences `find` performs to take `i` to its root. -/
+noncomputable def findDepth (hwf : uf.WellFormed) (i : Fin n) : ℕ :=
+  Nat.find (uf.exists_isRoot_iterate hwf i)
+
+/-- The root that `find` returns for `i`. -/
+noncomputable def findRoot (hwf : uf.WellFormed) (i : Fin n) : Fin n :=
+  uf.parent^[uf.findDepth hwf i] i
+
+/-- `findRoot` indeed lands on a root. -/
+lemma isRoot_findRoot (hwf : uf.WellFormed) (i : Fin n) : uf.IsRoot (uf.findRoot hwf i) := by
+  unfold findRoot findDepth
+  exact Nat.find_spec (uf.exists_isRoot_iterate hwf i)
+
+/-- Every step strictly before `findDepth` lands on a non-root. -/
+lemma not_isRoot_of_lt_findDepth (hwf : uf.WellFormed) (i : Fin n) {k : ℕ}
+    (hk : k < uf.findDepth hwf i) : ¬ uf.IsRoot (uf.parent^[k] i) := by
+  unfold findDepth at hk
+  exact Nat.find_min (uf.exists_isRoot_iterate hwf i) hk
+
+/-- For every `k ≤ findDepth`, the rank has grown by at least `k` along the find path. -/
+lemma rank_iterate_ge (hwf : uf.WellFormed) (i : Fin n) :
+    ∀ k, k ≤ uf.findDepth hwf i → uf.rank i + k ≤ uf.rank (uf.parent^[k] i) := by
+  intro k
+  induction k with
+  | zero => simp
+  | succ k ih =>
+    intro hk
+    have hk' : k < uf.findDepth hwf i := by omega
+    have hkle : k ≤ uf.findDepth hwf i := by omega
+    have hnot : ¬ uf.IsRoot (uf.parent^[k] i) := uf.not_isRoot_of_lt_findDepth hwf i hk'
+    have hstep : uf.rank (uf.parent^[k] i) < uf.rank (uf.parent (uf.parent^[k] i)) :=
+      hwf.rank_lt (uf.parent^[k] i) hnot
+    have hih := ih hkle
+    rw [Function.iterate_succ_apply']
+    omega
+
+/-- `find` dereferences at most `⌊log₂ n⌋` parent pointers. -/
+theorem findDepth_le_log (hwf : uf.WellFormed) (i : Fin n) :
+    uf.findDepth hwf i ≤ Nat.log 2 n := by
+  have h := uf.rank_iterate_ge hwf i (uf.findDepth hwf i) le_rfl
+  have hroot : uf.parent^[uf.findDepth hwf i] i = uf.findRoot hwf i := rfl
+  rw [hroot] at h
+  have hbound := uf.rank_le_log hwf (uf.findRoot hwf i)
+  omega
+
+end Cslib.Algorithms.Lean.UnionFind
diff --git a/CslibTests.lean b/CslibTests.lean
index 3380bb5e1..def52828d 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -1,13 +1,16 @@
-import CslibTests.Bisimulation
-import CslibTests.CCS
-import CslibTests.CLL
-import CslibTests.DFA
-import CslibTests.FreeMonad
-import CslibTests.GrindLint
-import CslibTests.HML
-import CslibTests.HasFresh
-import CslibTests.ImportWithMathlib
-import CslibTests.LTS
-import CslibTests.LambdaCalculus
-import CslibTests.MLL
-import CslibTests.Reduction
+module  -- shake: keep-all --deprecated_module: ignore
+
+public import CslibTests.Bisimulation
+public import CslibTests.CCS
+public import CslibTests.CLL
+public import CslibTests.DFA
+public import CslibTests.FreeMonad
+public import CslibTests.GrindLint
+public import CslibTests.HML
+public import CslibTests.HasFresh
+public import CslibTests.ImportWithMathlib
+public import CslibTests.LTS
+public import CslibTests.LambdaCalculus
+public import CslibTests.MLL
+public import CslibTests.Reduction
+public import CslibTests.UnionFind
diff --git a/CslibTests/UnionFind.lean b/CslibTests/UnionFind.lean
new file mode 100644
index 000000000..1101fc39d
--- /dev/null
+++ b/CslibTests/UnionFind.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Aviv Bar Natan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aviv Bar Natan
+-/
+
+import Cslib.Algorithms.Lean.UnionFind.Cost
+import Cslib.Algorithms.Lean.UnionFind.Operations
+
+namespace CslibTests
+
+/-! # Tests for union-by-rank union-find
+
+These tests exercise the public union-find API: the singleton forest is
+well-formed, `find` on a singleton takes zero steps, linking two distinct roots
+preserves well-formedness, and the `find_time_le_log` bound instantiates
+concretely.
+-/
+
+open Cslib.Algorithms.Lean.UnionFind
+
+-- `singleton` from this namespace is shadowed by the `{·}` set-builder `Singleton.singleton`,
+-- so we expose the union-find constructor under an unambiguous local name.
+open Cslib.Algorithms.Lean.UnionFind renaming singleton → ufSingleton
+
+/-- The singleton forest is well-formed. -/
+example : (ufSingleton 8).WellFormed := singleton_wellFormed
+
+/-- In a singleton forest every node is already a root, so `find` takes zero steps. -/
+example (i : Fin 8) : (ufSingleton 8).findDepth singleton_wellFormed i = 0 := by
+  unfold findDepth
+  rw [Nat.find_eq_zero]
+  simp
+
+/-- Linking two distinct singleton roots preserves well-formedness. -/
+example : ((ufSingleton 3).link 0 1).WellFormed :=
+  link_wellFormed (ufSingleton 3) singleton_wellFormed
+    (singleton_isRoot 0) (singleton_isRoot 1) (by decide)
+
+/-- The O(log n) bound instantiated: `find` on 8 elements costs at most `⌊log₂ 8⌋ = 3` ticks. -/
+example (i : Fin 8) : ((ufSingleton 8).find singleton_wellFormed i).time ≤ Nat.log 2 8 :=
+  find_time_le_log (ufSingleton 8) singleton_wellFormed i
+
+end CslibTests