diff --git a/GraphAlgorithms/DataStructures/BinaryTree.lean b/GraphAlgorithms/DataStructures/BinaryTree.lean
index 51468d0..e013352 100644
--- a/GraphAlgorithms/DataStructures/BinaryTree.lean
+++ b/GraphAlgorithms/DataStructures/BinaryTree.lean
@@ -73,22 +73,85 @@ because a binary tree could have q >/< key while being in
 the left/right subtree of key respectively.
 If `contains t q` is true, then `q` is in `t`; but
 the converse need not necessarily hold true. The
-converse is true for a binary search tree.
+converse is true for a binary search tree. Hence the name of it.
 -/
-def contains [LinearOrder α] (t : Tree α) (q : α) : Prop :=
+def BST_contains [LinearOrder α] (t : Tree α) (q : α) : Prop :=
   match t with
   | nil => False
   | l △[key] r =>
     if q < key then
-      l.contains q
+      l.BST_contains q
     else if key < q then
-      r.contains q
+      r.BST_contains q
     else
       True
 
 end CoreDefs
 
 
+/-! ### Membership -/
+section Membership
+
+/-- Inductive membership relation on binary trees, modelled on `List.Mem`. -/
+inductive Mem (a : α) : Tree α → Prop where
+  /-- `a` is the key at the root. -/
+  | here  {l r : Tree α} : Mem a (l △[a] r)
+  /-- `a` lies in the left subtree. -/
+  | left  {k : α} {l r : Tree α} : Mem a l → Mem a (l △[k] r)
+  /-- `a` lies in the right subtree. -/
+  | right {k : α} {l r : Tree α} : Mem a r → Mem a (l △[k] r)
+
+instance : Membership α (Tree α) := ⟨fun t a => Mem a t⟩
+
+@[simp] lemma not_mem_nil (a : α) : a ∉ (nil : Tree α) := nofun
+
+@[simp] lemma mem_node_iff {a k : α} {l r : Tree α} :
+    a ∈ (l △[k] r) ↔ a = k ∨ a ∈ l ∨ a ∈ r := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · cases h with
+    | here    => exact Or.inl rfl
+    | left h  => exact Or.inr (Or.inl h)
+    | right h => exact Or.inr (Or.inr h)
+  · rcases h with rfl | h | h
+    · exact .here
+    · exact .left h
+    · exact .right h
+
+/-- Membership agrees with membership in the in-order key list. -/
+theorem mem_iff_mem_toKeyList {a : α} {t : Tree α} :
+    a ∈ t ↔ a ∈ t.toKeyList := by
+  induction t with
+  | nil => simp
+  | node k l r ihl ihr =>
+    rw [toKeyList_node, mem_node_iff]
+    simp only [List.mem_append, List.mem_singleton, ihl, ihr]
+    tauto
+
+instance decidableMem [DecidableEq α] (a : α) : ∀ t : Tree α, Decidable (a ∈ t)
+  | .nil       => isFalse nofun
+  | l △[k] r =>
+    haveI : Decidable (a ∈ l) := decidableMem a l
+    haveI : Decidable (a ∈ r) := decidableMem a r
+    decidable_of_iff (a = k ∨ a ∈ l ∨ a ∈ r) mem_node_iff.symm
+
+/-- The search-path `contains` implies membership. The converse needs the BST
+invariant. -/
+theorem contains_imp_mem [LinearOrder α] {t : Tree α} {q : α} :
+    t.BST_contains q → q ∈ t := by
+  induction t with
+  | nil => simp [BST_contains]
+  | node k l r ihl ihr =>
+    intro h
+    simp only [BST_contains] at h
+    split_ifs at h with h1 h2
+    · exact .left (ihl h)
+    · exact .right (ihr h)
+    · have hqk : q = k := le_antisymm (not_lt.mp h2) (not_lt.mp h1)
+      exact hqk ▸ .here
+
+end Membership
+
+
 /-! ### Rotations and Mirroring -/
 section Transformations
 
@@ -143,24 +206,24 @@ end Transformations
 section ContainsLemmas
 
 @[simp] lemma not_contains_empty [LinearOrder α] (q : α) :
-    ¬ (nil : Tree α).contains q := nofun
+    ¬ (nil : Tree α).BST_contains q := nofun
 
 @[simp] lemma contains_node_lt [LinearOrder α] {l : Tree α} {k q : α}
     {r : Tree α} (h : q < k) :
-    (l △[k] r).contains q ↔ l.contains q := by
-  simp [contains, h]
+    (l △[k] r).BST_contains q ↔ l.BST_contains q := by
+  simp [BST_contains, h]
 
 @[simp] lemma contains_node_gt [LinearOrder α] {l : Tree α} {k q : α}
     {r : Tree α} (h : k < q) :
-    (l △[k] r).contains q ↔ r.contains q := by
-  simp [contains, h, not_lt_of_gt h]
+    (l △[k] r).BST_contains q ↔ r.BST_contains q := by
+  simp [BST_contains, h, not_lt_of_gt h]
 
 @[simp] lemma contains_node_not_eq_not_lt [LinearOrder α]
     {l : Tree α} {k q : α} {r : Tree α}
     (h1 : ¬ q = k) (h2 : ¬ q < k) :
-    (l △[k] r).contains q ↔ r.contains q := by
+    (l △[k] r).BST_contains q ↔ r.BST_contains q := by
   have hgt : k < q := lt_of_le_of_ne (Std.not_lt.mp h2) (Ne.symm (Ne.intro h1))
-  simp [contains, hgt, not_lt_of_gt hgt]
+  simp [BST_contains, hgt, not_lt_of_gt hgt]
 
 end ContainsLemmas
 
@@ -204,22 +267,62 @@ section IsBSTAccessors
 
 end IsBSTAccessors
 
-end Tree
-
-
-/-! ### BST Structure -/
-section BSTStructure
 
-structure BST (α : Type) [LinearOrder α] where
-  tree : Tree α
-  hBST : Tree.IsBST tree
+/-! ### BST Membership -/
+section BSTMembership
+
+/-- In a BST subtree with upper bound `some ub`, every member is `< ub`. -/
+private lemma IsBSTAux.lt_of_mem_ub [LinearOrder α] {t : Tree α} {q ub : α}
+    {lb : Option α} (h : IsBSTAux t lb (some ub)) (hmem : q ∈ t) : q < ub := by
+  induction t generalizing lb ub with
+  | nil => simp at hmem
+  | node k l r ihl ihr =>
+    obtain ⟨_, hub, hl, hr⟩ := (IsBSTAux_node l k r lb (some ub)).mp h
+    rcases mem_node_iff.mp hmem with rfl | hml | hmr
+    · exact hub
+    · exact lt_trans (ihl hl hml) hub
+    · exact ihr hr hmr
+
+/-- In a BST subtree with lower bound `some lb`, every member is `> lb`. -/
+private lemma IsBSTAux.gt_of_mem_lb [LinearOrder α] {t : Tree α} {q lb : α}
+    {ub : Option α} (h : IsBSTAux t (some lb) ub) (hmem : q ∈ t) : lb < q := by
+  induction t generalizing lb ub with
+  | nil => simp at hmem
+  | node k l r ihl ihr =>
+    obtain ⟨hlb, _, hl, hr⟩ := (IsBSTAux_node l k r (some lb) ub).mp h
+    rcases mem_node_iff.mp hmem with rfl | hml | hmr
+    · exact hlb
+    · exact ihl hl hml
+    · exact lt_trans hlb (ihr hr hmr)
+
+/-- Membership implies the BST search path finds the key, for any bound
+configuration. -/
+private theorem IsBSTAux.mem_imp_contains [LinearOrder α] {t : Tree α} {q : α}
+    {lb ub : Option α} (h : IsBSTAux t lb ub) (hmem : q ∈ t) : t.BST_contains q := by
+  induction t generalizing lb ub with
+  | nil => simp at hmem
+  | node k l r ihl ihr =>
+    obtain ⟨_, _, hl, hr⟩ := (IsBSTAux_node l k r lb ub).mp h
+    rcases mem_node_iff.mp hmem with rfl | hml | hmr
+    · simp [BST_contains]
+    · have hlt : q < k := IsBSTAux.lt_of_mem_ub hl hml
+      simp only [BST_contains, if_pos hlt]
+      exact ihl hl hml
+    · have hgt : k < q := IsBSTAux.gt_of_mem_lb hr hmr
+      simp only [BST_contains, if_neg (not_lt.mpr hgt.le), if_pos hgt]
+      exact ihr hr hmr
+
+/-- Converse of `contains_imp_mem` for BSTs: membership implies the search-path
+`contains` succeeds. -/
+theorem mem_imp_contains [LinearOrder α] {t : Tree α} (hbst : IsBST t)
+    {q : α} (hmem : q ∈ t) : t.BST_contains q :=
+  IsBSTAux.mem_imp_contains hbst hmem
+
+/-- For BSTs, the search-path `contains` coincides with membership. -/
+theorem contains_iff_mem [LinearOrder α] {t : Tree α} (hbst : IsBST t) {q : α} :
+    t.BST_contains q ↔ q ∈ t :=
+  ⟨contains_imp_mem, mem_imp_contains hbst⟩
+
+end BSTMembership
 
-namespace BST
-
-/-- Checks if the BST contains a given key by delegating to the underlying tree. -/
-def contains [LinearOrder α] (t : BST α) (q : α) : Prop :=
-  t.tree.contains q
-
-end BST
-
-end BSTStructure
+end Tree
diff --git a/GraphAlgorithms/DataStructures/SplayTree/Correctness.lean b/GraphAlgorithms/DataStructures/SplayTree/Correctness.lean
index f0e36b3..2e637f5 100644
--- a/GraphAlgorithms/DataStructures/SplayTree/Correctness.lean
+++ b/GraphAlgorithms/DataStructures/SplayTree/Correctness.lean
@@ -175,12 +175,12 @@ section RootOfContainedKey
 /-- If `t.contains q`, the subtree reached by `descend` is a node whose key
 equals `q`. Mirrors how `descend` and `Tree.contains` follow the same
 comparison path. -/
-theorem descend_contains [LinearOrder α] (t : Tree α) (q : α) (h : t.contains q) :
+theorem descend_contains [LinearOrder α] (t : Tree α) (q : α) (h : t.BST_contains q) :
     ∃ l r, (descend t q).1 = l △[q] r := by
   induction t with
-  | nil => simp [contains] at h
+  | nil => simp [BST_contains] at h
   | node k lt rt ihl ihr =>
-    simp only [contains] at h
+    simp only [BST_contains] at h
     by_cases hlt : q < k
     · simp only [hlt, ite_true] at h
       obtain ⟨l', r', hd⟩ := ihl h
@@ -193,6 +193,12 @@ theorem descend_contains [LinearOrder α] (t : Tree α) (q : α) (h : t.contains
       · have hqk : q = k := le_antisymm (not_lt.mp hgt) (not_lt.mp hlt)
         subst hqk; exact ⟨lt, rt, by rw [descend_node_eq]⟩
 
+/-- Membership-style variant of `descend_contains`: in a BST, if `q ∈ t` then
+`descend` reaches the node with key `q`. -/
+theorem descend_contains' [LinearOrder α] (t : Tree α) (q : α) (hbst : IsBST t)
+    (h : q ∈ t) : ∃ l r, (descend t q).1 = l △[q] r :=
+  descend_contains t q (mem_imp_contains hbst h)
+
 /-- Splaying a node `c = l △[k] r` upward along any path yields a tree
 whose root key is still `k`. Each rotation step brings `c` one level higher
 without changing its root key. -/
@@ -218,7 +224,7 @@ theorem splayUp_root_key_of_node :
 
 /-- If `t.contains q`, the bottom-up splay of `t` at `q` has `q` at the root. -/
 theorem splay_root_of_contains [LinearOrder α] (t : Tree α) (q : α)
-    (hc : t.contains q) : ∃ l r, splay t q = l △[q] r := by
+    (hc : t.BST_contains q) : ∃ l r, splay t q = l △[q] r := by
   obtain ⟨lr, rr, hd⟩ := descend_contains t q hc
   unfold splay
   rcases hdecomp : descend t q with ⟨reached, path⟩
@@ -226,6 +232,12 @@ theorem splay_root_of_contains [LinearOrder α] (t : Tree α) (q : α)
   subst hd
   exact splayUp_root_key_of_node path lr q rr
 
+/-- Membership-style variant of `splay_root_of_contains`: in a BST, if `q ∈ t`
+then splaying brings `q` to the root. -/
+theorem splay_root_of_contains' [LinearOrder α] (t : Tree α) (q : α)
+    (hbst : IsBST t) (h : q ∈ t) : ∃ l r, splay t q = l △[q] r :=
+  splay_root_of_contains t q (mem_imp_contains hbst h)
+
 end RootOfContainedKey
 
 end SplayTree
diff --git a/GraphLib/DataStructures/InverseAckermann.lean b/GraphLib/DataStructures/InverseAckermann.lean
deleted file mode 100644
index 83bc3fa..0000000
--- a/GraphLib/DataStructures/InverseAckermann.lean
+++ /dev/null
@@ -1,296 +0,0 @@
-/-
-Copyright (c) 2026 CSlib contributors. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Antoine du Fresne
--/
-
-import Mathlib.Computability.Ackermann
-import Mathlib.Data.Nat.Find
-import Mathlib.Logic.Function.Iterate
-import Mathlib.Tactic
-
-
---- Maybe it should technically go to the computability folder of CSlib.
-/-!
-# Inverse Ackermann Function
-
-This file defines the **inverse Ackermann function** `α(n)` and establishes its key properties.
-The inverse Ackermann function arises naturally in the amortised complexity analysis of
-Union-Find (disjoint-set forests with union-by-rank and path compression), where a sequence
-of `m` operations on `n` elements runs in `O(m · α(n))` time.
-
-## Mathematical background
-
-Recall Mathlib's standard (two-argument) Ackermann function `ack : ℕ → ℕ → ℕ`:
-
-```
-  ack 0 n       = n + 1
-  ack (m+1) 0   = ack m 1
-  ack (m+1)(n+1) = ack m (ack (m+1) n)
-```
-
-The *diagonal* `ack k k` grows extraordinarily fast:
-
-| k | ack k k      |
-|---|-------------|
-| 0 | 1           |
-| 1 | 3           |
-| 2 | 7           |
-| 3 | 61          |
-| 4 | 2^2^2^… − 3 (a tower of 65536 twos minus 3) |
-
-The **inverse Ackermann function** `α(n)` is defined as
-```
-  α(n) = min { k : ack k k ≥ n }
-```
-It grows *incredibly* slowly: `α(n) ≤ 4` for all `n ≤ 2^(2^(2^65536))`, which vastly exceeds
-the number of atoms in the observable universe.
-
-## Main definitions
-
-* `InverseAckermann.ackDiag`: The diagonal Ackermann function `n ↦ ack n n`.
-* `InverseAckermann.alpha`: The inverse Ackermann function `α(n) = Nat.find (∃ k, n ≤ ack k k)`.
-
-## Main results (stated, proofs TODO)
-
-* `alpha_le_iff`: `α(n) ≤ k ↔ n ≤ ack k k`.
-* `alpha_mono`: `α` is monotone.
-* `alpha_zero`: `α 0 = 0`.
-* `alpha_one`: `α 1 = 0`.
-* `alpha_le_four`: `α n ≤ 4` for `n ≤ ack 4 4` (i.e., all practical inputs).
-* `alpha_lt_id`: For `n ≥ 5`, `α n < n`.
-* `ackDiag_alpha`: `n ≤ ack (α n) (α n)` (the defining property).
-
-## Design notes
-
-- We build on Mathlib's `ack` rather than defining a separate hierarchy. This avoids
-  duplication and gives us access to all existing Ackermann lemmas (monotonicity, growth
-  bounds, strict monotonicity in both arguments, etc.).
-- An alternative definition sometimes used in the literature is
-  `α(m, n) = min { i ≥ 1 : ack(i, ⌊m/n⌋) ≥ log₂ n }`, which is a two-argument version.
-  For the Union-Find bound, the single-argument diagonal inverse suffices.
-- This file is designed to be independently useful and PR-able to Mathlib's
-  `Mathlib.Computability.Ackermann`.
-
-## References
-
-* R. E. Tarjan, "Efficiency of a good but not linear set union algorithm", *JACM* 22(2), 1975.
-* R. E. Tarjan, J. van Leeuwen, "Worst-case analysis of set union algorithms", *JACM* 31(2), 1984.
-* R. Seidel, M. Sharir, "Top-down analysis of path compression", *SIAM J. Comput.* 34(3), 2005.
-
-## TODO
-
-- Prove remaining sorry'd lemmas below (currently all proven!).
-- Add `Decidable` instance for `α` (it is computable).
-- Prove `α` grows slower than any primitive recursive function of the form `n ↦ f(n)`.
-- Connect to the two-argument inverse `α(m, n)` used in some references.
--/
-
-namespace InverseAckermann
-
-open Nat
-
-/-! ### Diagonal Ackermann function -/
-
-/-- The diagonal Ackermann function `ackDiag n = ack n n`. -/
-def ackDiag (n : ℕ) : ℕ := ack n n
-
-@[simp] theorem ackDiag_zero : ackDiag 0 = 1 := by simp [ackDiag]
-@[simp] theorem ackDiag_one : ackDiag 1 = 3 := by simp [ackDiag]
-@[simp] theorem ackDiag_two : ackDiag 2 = 7 := by simp [ackDiag]
-@[simp] theorem ackDiag_three : ackDiag 3 = 61 := by simp [ackDiag]
-
-/-- `ackDiag` is strictly monotone. -/
-theorem ackDiag_strictMono : StrictMono ackDiag := by
-  intro a b hab
-  exact calc ack a a < ack a b := ack_strictMono_right a hab
-    _ ≤ ack b b := ack_mono_left b (le_of_lt hab)
-
-/-- `ackDiag` is monotone. -/
-theorem ackDiag_mono : Monotone ackDiag := ackDiag_strictMono.monotone
-
-/-- `ackDiag n > 0` for all `n`. -/
-theorem ackDiag_pos (n : ℕ) : 0 < ackDiag n := ack_pos n n
-
-/-- `ackDiag n ≥ n` for all `n`. -/
-theorem le_ackDiag (n : ℕ) : n ≤ ackDiag n := le_of_lt (lt_ack_right n n)
-
-/-- `ackDiag` is unbounded: for every `N`, there exists `k` with `ackDiag k ≥ N`. -/
-theorem ackDiag_unbounded (N : ℕ) : ∃ k, N ≤ ackDiag k :=
-  ⟨N, le_ackDiag N⟩
-
-/-! ### Inverse Ackermann function -/
-
-/-- Auxiliary: the predicate `n ≤ ack k k` is decidable. -/
-instance (n k : ℕ) : Decidable (n ≤ ack k k) := inferInstance
-
-/-- The **inverse Ackermann function**.
-  `alpha n = min { k : ℕ | n ≤ ack k k }`.
-
-  This is the standard single-argument inverse used in the Union-Find amortised bound.
-  It grows incredibly slowly: `alpha n ≤ 4` for all practically occurring `n`. -/
-noncomputable def alpha (n : ℕ) : ℕ :=
-  Nat.find (ackDiag_unbounded n)
-
--- Some computational checks (via native_decide or norm_num in proofs)
--- α(0) = 0,  α(1) = 0,  α(2) = 1,  α(3) = 1,
--- α(4) = 2,  α(5) = 2, ..., α(7) = 2,
--- α(8) = 3, ..., α(61) = 3,
--- α(62) = 4, ...
-
-/-! ### Core characterisation -/
-
-/-- The defining property: `n ≤ ack (alpha n) (alpha n)`. -/
-theorem ackDiag_alpha (n : ℕ) : n ≤ ackDiag (alpha n) :=
-  Nat.find_spec (ackDiag_unbounded n)
-
-/-- `alpha n ≤ k` if and only if `n ≤ ack k k`. -/
-theorem alpha_le_iff {n k : ℕ} : alpha n ≤ k ↔ n ≤ ackDiag k := by
-  constructor
-  · intro h
-    exact le_trans (ackDiag_alpha n) (ackDiag_mono h)
-  · intro h
-    exact Nat.find_le h
-
-/-- `k < alpha n` if and only if `ack k k < n`. -/
-theorem lt_alpha_iff {n k : ℕ} : k < alpha n ↔ ackDiag k < n := by
-  rw [← not_le, ← not_le]
-  exact not_congr alpha_le_iff
-
-/-! ### Basic values -/
-
-/-- `α(0) = 0`. -/
-@[simp] theorem alpha_zero : alpha 0 = 0 := by
-  apply le_antisymm
-  · exact alpha_le_iff.mpr (by simp [ackDiag])
-  · exact Nat.zero_le _
-
-/-- `α(1) = 0`. -/
-@[simp] theorem alpha_one : alpha 1 = 0 := by
-  apply le_antisymm
-  · exact alpha_le_iff.mpr (by simp [ackDiag])
-  · exact Nat.zero_le _
-
-/-- `α(2) = 1`. -/
-theorem alpha_two : alpha 2 = 1 := by
-  apply le_antisymm
-  · exact alpha_le_iff.mpr (by simp [ackDiag])
-  · exact lt_alpha_iff.mpr (by simp [ackDiag])
-
-/-- `α(3) = 1`. -/
-theorem alpha_three : alpha 3 = 1 := by
-  apply le_antisymm
-  · exact alpha_le_iff.mpr (by simp [ackDiag])
-  · exact lt_alpha_iff.mpr (by simp [ackDiag])
-
-/-! ### Monotonicity -/
-
-/-- `α` is monotone: if `a ≤ b` then `α(a) ≤ α(b)`. -/
-theorem alpha_mono : Monotone alpha := by
-  intro a b hab
-  exact alpha_le_iff.mpr (le_trans hab (ackDiag_alpha b))
-
-/-! ### Growth bounds -/
-
-/-- For all `n`, `α(n) ≤ n`. In fact `α` grows much slower, but this is a simple upper bound. -/
-theorem alpha_le_self (n : ℕ) : alpha n ≤ n :=
-  alpha_le_iff.mpr (le_ackDiag n)
-
-/-- The key "practically constant" bound: `α(n) ≤ 4` whenever `n ≤ ack 4 4`.
-Since `ack 4 4` is a number with about `10^(10^(10^19728))` digits, this covers
-every input that could ever arise in practice. -/
-theorem alpha_le_four_of_le_ack44 (n : ℕ) (h : n ≤ ack 4 4) : alpha n ≤ 4 :=
-  alpha_le_iff.mpr (by rwa [ackDiag])
-
-/-! ### Interaction with `ack` -/
-
-/-- `alpha (ack k k) ≤ k` for all `k`. -/
-theorem alpha_ackDiag_le (k : ℕ) : alpha (ackDiag k) ≤ k :=
-  alpha_le_iff.mpr (le_refl _)
-
-/-- `alpha (ack k k + 1) = k + 1`.
-  (Going one above the diagonal value bumps the inverse.) -/
-theorem alpha_ackDiag_succ (k : ℕ) : alpha (ackDiag k + 1) = k + 1 := by
-  -- By definition of `alpha`, we know that `alpha (ackDiag k + 1) = k + 1`.
-  apply le_antisymm;
-  · apply alpha_le_iff.mpr;
-    exact Nat.succ_le_of_lt (ackDiag_strictMono (Nat.lt_succ_self k));
-  · exact Nat.succ_le_of_lt (lt_of_not_ge fun h => by linarith [alpha_le_iff.mp h,
-    ackDiag_strictMono.monotone, h])
-
-/-
-`alpha` composed with `ackDiag` is the identity.
--/
-theorem alpha_ackDiag (k : ℕ) : alpha (ackDiag k) = k := by sorry
-/-
-  exact le_antisymm (alpha_ackDiag_le _)
-    (Nat.le_of_not_lt fun h => by have := lt_alpha_iff.2
-  (show ackDiag (alpha (ackDiag k)) < ackDiag k from StrictMono.lt_iff_lt (ackDiag_strictMono) |>.2 h)
-   aesop)
--/
-
-/-! ### Iterated / levelled inverse (for the full Tarjan analysis)
-
-For the full Tarjan–van Leeuwen amortised analysis of Union-Find, one needs a
-finer decomposition using iterated applications of `ack`. The *level* of a node `x`
-with parent `p` and `rank r` is
-  `level(x) = max { k : ack k (rank x) ≤ rank (root x) }`
-and the *index* is
-  `index(x) = max { i : ack^[i]_{level(x)} (rank x) ≤ rank (root x) }`.
-
-We define the iterated version here for use in the potential function.
-
-**Blueprint:** See `CSlib.DataStructures.UnionFind.Blueprint` for how these
-are used in the potential function.
--/
-
-/-- The *level function* `ufLevel r R` for Union-Find complexity analysis.
-  Given a node rank `r` and the rank of its root `R` (with `r < R`), the level is
-  `max { k ≥ 0 : ack k r ≤ R }`.
-
-  This is well-defined because `ack k r` is strictly increasing in `k` and eventually
-  exceeds any bound. -/
-noncomputable def ufLevel (r R : ℕ) : ℕ :=
-  Nat.find (⟨R, lt_ack_left R r⟩ : ∃ k, R < ack k r) - 1
-
-/-
-The *index function* `ufIndex r R k` for Union-Find complexity analysis.
-  Given rank `r`, root rank `R`, and level `k`, the index is
-  `max { i ≥ 1 : (ack k)^[i](r) ≤ R }`.
--/
-noncomputable def ufIndex (r R k : ℕ) : ℕ :=
-  Nat.find (⟨R + 1, by
-    -- By induction on $i$, we show that $(ack k)^[i] r \geq r + i$.
-    have h_ind : ∀ i : ℕ, (ack k)^[i] r ≥ r + i := by
-      intro i;
-      induction' i with i ih;
-      · rfl;
-      · rw [ Function.iterate_succ_apply' ];
-        exact Nat.succ_le_of_lt ( lt_of_le_of_lt ih ( lt_ack_right _ _ ) );
-    linarith [ h_ind ( R + 1 ) ] -- need: (ack k)^[R+1] r > R, which follows from ack k being inflationary
-  ⟩ : ∃ i, R < (ack k)^[i] r) - 1
-
-/-!
-## Roadmap for this file
-
-### Immediate TODO (needed for Union-Find correctness + complexity)
-1. ✅ Define `alpha`, `ackDiag`
-2. ✅ Prove `alpha_le_iff`, `ackDiag_alpha` (core characterisation)
-3. ✅ Prove `alpha_mono`, `alpha_zero`, `alpha_one`
-4. ✅ Prove `alpha_ackDiag` and `alpha_ackDiag_succ`
-5. 🔲 Prove `alpha_lt_id` for `n ≥ 5`
-6. 🔲 Make `alpha` computable (provide a `DecidableEq`-based algorithm)
-
-### Medium-term TODO (for Mathlib PR)
-7. 🔲 Prove `alpha` grows slower than `log* n`
-8. 🔲 Connect `ufLevel` and `ufIndex` to the iterated Ackermann hierarchy
-9. 🔲 Prove `ufLevel` and `ufIndex` are well-defined and bounded
-10. 🔲 Add simp lemmas for small values of `alpha`
-
-### Long-term TODO
-11. 🔲 Two-argument inverse `α(m, n)` for the most refined bounds
-12. 🔲 Connection to the Davenport–Schinzel sequence bounds
-    (relate to `KlazarAckermann.alpha` in `Ackermann_Function.lean`)
--/
-
-end InverseAckermann
diff --git a/GraphLib/DataStructures/InverseAckermann/Basic.lean b/GraphLib/DataStructures/InverseAckermann/Basic.lean
new file mode 100644
index 0000000..1962dca
--- /dev/null
+++ b/GraphLib/DataStructures/InverseAckermann/Basic.lean
@@ -0,0 +1,340 @@
+/-
+Copyright (c) 2026 GraphLib contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine du Fresne
+-/
+
+import Mathlib.Computability.Ackermann
+import Mathlib.Computability.Primrec.List
+import Mathlib.Data.List.GetD
+
+/-!
+# Inverse Ackermann function
+
+Given Mathlib's Ackermann function `ack : ℕ → ℕ → ℕ`, the diagonal `ack k k` is
+strictly increasing in `k`, so we may define the inverse Ackermann function
+
+  `invAck n = min { k | n ≤ ack k k }`.
+
+Values: `invAck 0 = invAck 1 = 0`, `invAck 2 = invAck 3 = 1`, and `invAck n ≤ 4`
+whenever `n ≤ ack 4 4`.
+
+## Main definitions
+
+* `ackDiag n = ack n n`.
+* `invAck n` is the inverse Ackermann function.
+* `ackBdd B k m = min (ack k m) B` is a truncated `ack`, computed via a table
+  of fixed-width rows, which makes it primitive recursive.
+
+## Main results
+
+* `invAck_le_iff : invAck n ≤ k ↔ n ≤ ack k k`.
+* `invAck_mono`, `invAck_ackDiag : invAck (ack k k) = k`.
+* `invAck_primrec`: `invAck` is primitive recursive (whereas `fun k ↦ ack k k`
+  is not, by `not_nat_primrec_ack_self`).
+
+## AI usage
+
+AI assistance was used to draft boilerplate API, docstrings, and several of
+the proofs in the primitive-recursiveness section, following Mathlib and
+CSlib naming and style conventions. All statements and proofs were reviewed
+and verified.
+
+-/
+
+namespace InverseAckermann
+
+open Nat
+
+
+/-! ### Diagonal Ackermann function -/
+
+section AckDiag
+
+/-- The diagonal Ackermann function `ackDiag n = ack n n`. -/
+def ackDiag (n : ℕ) : ℕ := ack n n
+
+@[simp] theorem ackDiag_zero : ackDiag 0 = 1 := by simp [ackDiag]
+@[simp] theorem ackDiag_one : ackDiag 1 = 3 := by simp [ackDiag]
+@[simp] theorem ackDiag_two : ackDiag 2 = 7 := by simp [ackDiag]
+@[simp] theorem ackDiag_three : ackDiag 3 = 61 := by simp [ackDiag]
+
+/-- `ackDiag` is strictly monotone. -/
+theorem ackDiag_strictMono : StrictMono ackDiag := fun _ _ hab =>
+  (ack_strictMono_right _ hab).trans_le (ack_mono_left _ hab.le)
+
+/-- `ackDiag` is monotone. -/
+theorem ackDiag_mono : Monotone ackDiag := ackDiag_strictMono.monotone
+
+/-- `ackDiag n` is positive. -/
+theorem ackDiag_pos (n : ℕ) : 0 < ackDiag n := ack_pos n n
+
+/-- `n ≤ ackDiag n`. -/
+theorem le_ackDiag (n : ℕ) : n ≤ ackDiag n := (lt_ack_right n n).le
+
+/-- For every `N`, some `k` satisfies `N ≤ ackDiag k`. -/
+theorem ackDiag_unbounded (N : ℕ) : ∃ k, N ≤ ackDiag k := ⟨N, le_ackDiag N⟩
+
+end AckDiag
+
+
+/-! ### Inverse Ackermann function -/
+
+section InvAck
+
+/-! #### Definition -/
+
+/-- The inverse Ackermann function `invAck n = min { k | n ≤ ack k k }`. -/
+def invAck (n : ℕ) : ℕ := Nat.find (ackDiag_unbounded n)
+
+/-- Defining property: `n ≤ ackDiag (invAck n)`. -/
+theorem ackDiag_invAck (n : ℕ) : n ≤ ackDiag (invAck n) :=
+  Nat.find_spec (ackDiag_unbounded n)
+
+
+/-! #### Characterisation -/
+
+/-- `invAck n ≤ k ↔ n ≤ ackDiag k`. -/
+theorem invAck_le_iff {n k : ℕ} : invAck n ≤ k ↔ n ≤ ackDiag k :=
+  ⟨fun h => (ackDiag_invAck n).trans (ackDiag_mono h), fun h => Nat.find_le h⟩
+
+/-- `k < invAck n ↔ ackDiag k < n`. -/
+theorem lt_invAck_iff {n k : ℕ} : k < invAck n ↔ ackDiag k < n := by
+  rw [← not_le, invAck_le_iff, not_le]
+
+/-- `invAck n < k + 1 ↔ n ≤ ackDiag k`. -/
+theorem invAck_lt_add_one_iff {n k : ℕ} : invAck n < k + 1 ↔ n ≤ ackDiag k := by
+  rw [Nat.lt_succ_iff, invAck_le_iff]
+
+/-- `k + 1 ≤ invAck n ↔ ackDiag k < n`. -/
+theorem add_one_le_invAck_iff {n k : ℕ} : k + 1 ≤ invAck n ↔ ackDiag k < n := by
+  rw [Nat.succ_le_iff, lt_invAck_iff]
+
+/-- `invAck (ackDiag k) ≤ k`. -/
+theorem invAck_ackDiag_le (k : ℕ) : invAck (ackDiag k) ≤ k := invAck_le_iff.mpr le_rfl
+
+/-- `invAck` is a left inverse of `ackDiag`. -/
+@[simp]
+theorem invAck_ackDiag (k : ℕ) : invAck (ackDiag k) = k :=
+  le_antisymm (invAck_ackDiag_le k) (ackDiag_strictMono.le_iff_le.mp (ackDiag_invAck _))
+
+/-- One past the diagonal: `invAck (ackDiag k + 1) = k + 1`. -/
+theorem invAck_ackDiag_add_one (k : ℕ) : invAck (ackDiag k + 1) = k + 1 :=
+  le_antisymm
+    (invAck_le_iff.mpr (ackDiag_strictMono k.lt_succ_self))
+    (lt_invAck_iff.mpr (Nat.lt_succ_self _))
+
+
+/-! #### Basic values -/
+
+@[simp] theorem invAck_zero : invAck 0 = 0 :=
+  Nat.le_zero.mp (invAck_le_iff.mpr (Nat.zero_le _))
+
+@[simp] theorem invAck_one : invAck 1 = 0 :=
+  Nat.le_zero.mp (invAck_le_iff.mpr (by simp))
+
+@[simp] theorem invAck_two : invAck 2 = 1 :=
+  le_antisymm (invAck_le_iff.mpr (by simp)) (lt_invAck_iff.mpr (by simp))
+
+@[simp] theorem invAck_three : invAck 3 = 1 :=
+  le_antisymm (invAck_le_iff.mpr (by simp)) (lt_invAck_iff.mpr (by simp))
+
+
+/-! #### Monotonicity and bounds -/
+
+/-- `invAck` is monotone. -/
+theorem invAck_mono : Monotone invAck := fun _ _ hab =>
+  invAck_le_iff.mpr (hab.trans (ackDiag_invAck _))
+
+/-- `invAck n ≤ n`. -/
+theorem invAck_le_self (n : ℕ) : invAck n ≤ n := invAck_le_iff.mpr (le_ackDiag n)
+
+end InvAck
+
+
+/-! ### `invAck` is primitive recursive
+
+Define a truncated `ackBdd B k m = min (ack k m) B`, computed as a table whose
+rows have fixed length `B + 1`; this is primitive recursive. Then the graph
+
+  `invAck n = b ↔ n ≤ ack b b ∧ (b = 0 ∨ ack (b - 1) (b - 1) < n)`
+
+becomes primitive recursive (using `ackBdd` for the comparisons), and the bound
+`invAck n ≤ n` lets us apply `Primrec.of_graph`. -/
+
+section InvAckPrimrec
+
+/-! #### Bounded Ackermann -/
+
+/-- Entry `m` of row `k + 1`, computed from the previous row `prev`. Uses
+`ackBdd B (k+1) m = ackBdd B k (ackBdd B (k+1) (m-1))` and
+`ackBdd B (k+1) 0 = ackBdd B k 1`. -/
+def ackBddEntry (B : ℕ) (prev : List ℕ) : ℕ → ℕ
+  | 0     => prev.getD 1 B
+  | m + 1 => prev.getD (ackBddEntry B prev m) B
+
+/-- Row `k` of the `ackBdd` table: a list of length `B + 1` with
+`(ackBddRow B k)[i] = ackBdd B k i`. -/
+def ackBddRow (B : ℕ) : ℕ → List ℕ
+  | 0     => (List.range (B + 1)).map fun m => min (m + 1) B
+  | k + 1 => (List.range (B + 1)).map (ackBddEntry B (ackBddRow B k))
+
+/-- The bounded Ackermann function `ackBdd B k m = min (ack k m) B`, set up to
+be primitive recursive (`ack` itself is not). -/
+def ackBdd (B k m : ℕ) : ℕ := (ackBddRow B k).getD m B
+
+/-- Every row of the `ackBdd` table has length `B + 1`. -/
+@[simp]
+lemma ackBddRow_length (B k : ℕ) : (ackBddRow B k).length = B + 1 := by
+  cases k <;> simp [ackBddRow]
+
+/-- Truncating the argument before applying `ack k` does not change the
+truncated value. -/
+private lemma ack_min_arg (k B x : ℕ) :
+    min (ack k (min x B)) B = min (ack k x) B := by
+  rcases le_or_gt x B with h | h
+  · rw [min_eq_left h]
+  · have hB : B < ack k B := lt_ack_right k B
+    rw [min_eq_right h.le, min_eq_right hB.le,
+      min_eq_right (hB.trans_le (ack_mono_right k h.le)).le]
+
+/-- Out-of-range entries of `ackBdd` saturate at `B`. -/
+private lemma ackBdd_of_ge {B k m : ℕ} (h : B + 1 ≤ m) :
+    ackBdd B k m = min (ack k m) B := by
+  have hB : B < ack k m := (Nat.lt_of_succ_le h).trans (lt_ack_right k m)
+  rw [ackBdd, List.getD_eq_default _ _ (by simp [h]), min_eq_right hB.le]
+
+/-- Closed form: `ackBdd B k m = min (ack k m) B`. -/
+theorem ackBdd_eq (B k m : ℕ) : ackBdd B k m = min (ack k m) B := by
+  induction k generalizing m with
+  | zero =>
+    rcases lt_or_ge m (B + 1) with hm | hm
+    · unfold ackBdd ackBddRow
+      rw [ack_zero, List.getD_eq_getElem _ _ (by simp [hm])]
+      simp [List.getElem_map, List.getElem_range]
+    · exact ackBdd_of_ge hm
+  | succ k ih =>
+    rcases lt_or_ge m (B + 1) with hm | hm
+    · unfold ackBdd ackBddRow
+      rw [List.getD_eq_getElem _ _ (by simp [hm])]
+      simp only [List.getElem_map, List.getElem_range]
+      clear hm
+      induction m with
+      | zero =>
+        change ackBdd B k 1 = min (ack (k + 1) 0) B
+        rw [ack_succ_zero]; exact ih 1
+      | succ m ih_m =>
+        change ackBdd B k (ackBddEntry B (ackBddRow B k) m) = min (ack (k + 1) (m + 1)) B
+        rw [ih, ih_m, ack_succ_succ, ack_min_arg]
+    · exact ackBdd_of_ge hm
+
+/-- `ackBdd B k m ≤ B`. -/
+lemma ackBdd_le (B k m : ℕ) : ackBdd B k m ≤ B := by
+  rw [ackBdd_eq]; exact min_le_right _ _
+
+/-- `n ≤ ack k k` rephrased via `ackBdd`. -/
+private lemma le_ack_iff_ackBdd_eq (n k : ℕ) : n ≤ ack k k ↔ ackBdd n k k = n := by
+  rw [ackBdd_eq, min_eq_right_iff]
+
+/-- `ack k k < n` rephrased via `ackBdd`. -/
+private lemma ack_lt_iff_ackBdd_lt (n k : ℕ) : ack k k < n ↔ ackBdd n k k < n := by
+  rw [ackBdd_eq, min_lt_iff, or_iff_left (lt_irrefl n)]
+
+
+/-! #### Primitive recursiveness of `ackBdd` -/
+
+/-- `ackBddEntry` is primitive recursive. -/
+lemma ackBddEntry_primrec :
+    Primrec fun p : (ℕ × List ℕ) × ℕ => ackBddEntry p.1.1 p.1.2 p.2 := by
+  -- Rephrase `ackBddEntry` as an `ℕ.rec`-shaped term on the third argument so we
+  -- can hand it to `Primrec.nat_rec'`: base case `prev.getD 1 B`, step case
+  -- `prev.getD ih B`. The pattern-match definition itself is not directly in
+  -- the shape `Primrec.nat_rec'` expects.
+  have h_rec : ∀ p : (ℕ × List ℕ) × ℕ, ackBddEntry p.1.1 p.1.2 p.2 =
+      p.2.rec (p.1.2.getD 1 p.1.1) fun _ ih => p.1.2.getD ih p.1.1 := by
+    rintro ⟨⟨B, prev⟩, m⟩
+    induction m with
+    | zero      => rfl
+    | succ m ih => simp [ackBddEntry, ih]
+  refine (Primrec.nat_rec' (f := fun p : (ℕ × List ℕ) × ℕ => p.2)
+      (g := fun p => p.1.2.getD 1 p.1.1)
+      (h := fun p q => p.1.2.getD q.2 p.1.1)
+      Primrec.snd ?_ ?_).of_eq fun p => (h_rec p).symm
+  · exact Primrec.option_getD.comp
+      (Primrec.list_getElem?.comp (Primrec.snd.comp Primrec.fst) (Primrec.const 1))
+      (Primrec.fst.comp Primrec.fst)
+  · exact Primrec.option_getD.comp
+      (Primrec.list_getElem?.comp
+        (Primrec.snd.comp <| Primrec.fst.comp Primrec.fst)
+        (Primrec.snd.comp Primrec.snd))
+      (Primrec.fst.comp <| Primrec.fst.comp Primrec.fst)
+
+/-- `ackBddRow` is primitive recursive. -/
+lemma ackBddRow_primrec : Primrec₂ ackBddRow := by
+  have h_base : Primrec fun B : ℕ => (List.range (B + 1)).map fun m => min (m + 1) B := by
+    refine Primrec.list_map (Primrec.list_range.comp Primrec.succ) ?_
+    exact Primrec.nat_min.comp (Primrec.succ.comp Primrec.snd) Primrec.fst
+  have h_step_curried : Primrec₂ fun (B : ℕ) (prev : List ℕ) =>
+      (List.range (B + 1)).map (ackBddEntry B prev) :=
+    Primrec.list_map (Primrec.list_range.comp (Primrec.succ.comp Primrec.fst))
+      ackBddEntry_primrec
+  have h_step : Primrec₂ fun (B : ℕ) (p : ℕ × List ℕ) =>
+      (List.range (B + 1)).map (ackBddEntry B p.2) :=
+    h_step_curried.comp Primrec.fst (Primrec.snd.comp Primrec.snd)
+  refine (Primrec.nat_rec h_base h_step).of_eq fun B k => ?_
+  induction k with
+  | zero      => rfl
+  | succ k ih => simp [ackBddRow, ih]
+
+/-- `ackBdd` is primitive recursive. -/
+lemma ackBdd_primrec :
+    Primrec fun p : (ℕ × ℕ) × ℕ => ackBdd p.1.1 p.1.2 p.2 :=
+  let h_row : Primrec fun p : (ℕ × ℕ) × ℕ => ackBddRow p.1.1 p.1.2 :=
+    ackBddRow_primrec.comp (Primrec.fst.comp Primrec.fst) (Primrec.snd.comp Primrec.fst)
+  Primrec.option_getD.comp
+    (Primrec.list_getElem?.comp h_row Primrec.snd)
+    (Primrec.fst.comp Primrec.fst)
+
+
+/-! #### Primitive recursiveness of `invAck` -/
+
+/-- Characterisation of the graph of `invAck` used to show it is primitive
+recursive. -/
+lemma invAck_eq_iff (n b : ℕ) :
+    invAck n = b ↔ n ≤ ack b b ∧ (b = 0 ∨ ack (b - 1) (b - 1) < n) := by
+  refine ⟨fun h => h ▸ ⟨ackDiag_invAck n, ?_⟩,
+    fun ⟨h1, h2⟩ => le_antisymm (invAck_le_iff.mpr h1) ?_⟩
+  · rcases Nat.eq_zero_or_pos (invAck n) with hα | hα
+    · exact .inl hα
+    · exact .inr (lt_invAck_iff.mp (Nat.sub_lt hα Nat.one_pos))
+  · rcases h2 with rfl | hlt
+    · exact Nat.zero_le _
+    · have := lt_invAck_iff.mpr hlt; omega
+
+/-- The graph of `invAck` is a primitive recursive relation. -/
+private lemma invAck_graph_primrec : PrimrecRel fun (n b : ℕ) => invAck n = b := by
+  have h_bb : Primrec fun p : ℕ × ℕ => ackBdd p.1 p.2 p.2 :=
+    ackBdd_primrec.comp (Primrec.pair (Primrec.pair Primrec.fst Primrec.snd) Primrec.snd)
+  have h_pred : Primrec fun p : ℕ × ℕ => ackBdd p.1 (p.2 - 1) (p.2 - 1) :=
+    let h_b1 : Primrec fun p : ℕ × ℕ => p.2 - 1 :=
+      Primrec.nat_sub.comp Primrec.snd (Primrec.const 1)
+    ackBdd_primrec.comp (Primrec.pair (Primrec.pair Primrec.fst h_b1) h_b1)
+  have h_eq : PrimrecRel fun n b : ℕ => ackBdd n b b = n :=
+    Primrec.eq.comp h_bb Primrec.fst
+  have h_lt : PrimrecRel fun n b : ℕ => ackBdd n (b - 1) (b - 1) < n :=
+    Primrec.nat_lt.comp h_pred Primrec.fst
+  have h_zero : PrimrecRel fun (_ b : ℕ) => b = 0 :=
+    Primrec.eq.comp Primrec.snd (Primrec.const 0)
+  refine (h_eq.and (h_zero.or h_lt)).of_eq fun ⟨n, b⟩ => ?_
+  simp only [invAck_eq_iff, le_ack_iff_ackBdd_eq, ack_lt_iff_ackBdd_lt]
+
+/-- `invAck` is primitive recursive, even though `fun k => ack k k` is not (see
+`not_nat_primrec_ack_self`). The bounded search uses `invAck_le_self` together
+with `invAck_graph_primrec`. -/
+theorem invAck_primrec : Nat.Primrec invAck := by
+  rw [← Primrec.nat_iff]
+  exact Primrec.of_graph ⟨id, Primrec.id, invAck_le_self⟩ invAck_graph_primrec
+
+end InvAckPrimrec
+
+end InverseAckermann
diff --git a/GraphLib/DataStructures/InverseAckermann/Nivasch.lean b/GraphLib/DataStructures/InverseAckermann/Nivasch.lean
new file mode 100644
index 0000000..dfa71fe
--- /dev/null
+++ b/GraphLib/DataStructures/InverseAckermann/Nivasch.lean
@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2026 GraphLib contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine du Fresne
+-/
+
+import GraphLib.DataStructures.InverseAckermann.Basic
+
+/-!
+# Nivasch's hierarchy: the inverse Ackermann function without `ack`
+
+An alternative definition of the inverse Ackermann function due to Nivasch
+that avoids any reference to `ack`. Set
+`invAckHier 0 n = ⌈n / 2⌉`, and
+`invAckHier (k+1) n = min { i | (invAckHier k)^[i] n ≤ 3 }`;
+then `invAckNivasch n = min { k | invAckHier k n ≤ 3 }`.
+
+## Main definitions
+
+* `Nivasch.invAckHier`: the slow-growing hierarchy `αₖ`.
+* `Nivasch.invAckNivasch`: Nivasch's `α`, defined via the hierarchy.
+
+## Main results (all `sorry`)
+
+* `invAckNivasch_le_invAck`: `invAckNivasch n ≤ invAck n` (unconditional).
+* `invAck_le_invAckNivasch_add_two`: `invAck n ≤ invAckNivasch n + 2`
+  (depends on `findBdd` fuel being sufficient at every level).
+* `invAck_agree_Nivasch`: the two-sided bound.
+
+The constant `2` is tight: at `n = 4`, `invAck 4 = 2` and
+`invAckNivasch 4 = 0`. The `+2` arises from two structural offsets:
+  - level `0` here is halving, not `log` (Nivasch's `α₁`): one off-by-one;
+  - `bound_k(3)` (the threshold of the `α_k`-hierarchy) lies between
+    `ack k k` and `ack (k+2) (k+2)`: one more off-by-one.
+
+## Status
+
+Work in progress.
+
+## AI usage
+
+The definitions in this file were drafted by AI from Nivasch's writeup and
+reviewed by the author. The agreement theorem with `invAck` is stated but
+not yet proved.
+
+## References
+
+* G. Nivasch, *Inverse Ackermann without Ackermann*,
+  <https://www.gabrielnivasch.org/fun/inverse-ackermann>.
+-/
+
+namespace InverseAckermann
+namespace Nivasch
+
+/-- Bounded least-search: the smallest `k' ∈ [k, k + fuel)` with `p k'`, or `0`
+if none. Used to express the inner searches in `invAckHier` and
+`invAckNivasch`.
+
+Implemented via `List.find?` on `List.range'`; the `0` fallback matches the
+expected case-analysis behaviour at call sites (see the TODO on `invAckHier`
+about justifying the chosen `fuel = n + 2`). -/
+private def findBdd (p : ℕ → Bool) (k fuel : ℕ) : ℕ :=
+  ((List.range' k fuel).find? p).getD 0
+
+/-- Nivasch's slow-growing hierarchy `αₖ`:
+`invAckHier 0 n = ⌈n / 2⌉`, and
+`invAckHier (k+1) n = min { i | (invAckHier k)^[i] n ≤ 3 }`.
+
+TODO: prove that `n + 2` always suffices for the inner search. Without this
+lemma, `invAckHier` and `invAckNivasch` silently return `0` when the search
+fails. The bound should follow from `αₖ`'s growth rate; see Nivasch's writeup. -/
+def invAckHier : ℕ → ℕ → ℕ
+  | 0,     n => (n + 1) / 2
+  | k + 1, n => findBdd (fun i => decide ((invAckHier k)^[i] n ≤ 3)) 0 (n + 2)
+
+/-- Nivasch's inverse Ackermann:
+`invAckNivasch n = min { k | invAckHier k n ≤ 3 }`. See the TODO on
+`invAckHier` about the `n + 2` search bound. -/
+def invAckNivasch (n : ℕ) : ℕ :=
+  findBdd (fun k => decide (invAckHier k n ≤ 3)) 0 (n + 2)
+
+end Nivasch
+
+/-- Lower bound: `invAckNivasch n ≤ invAck n` for every `n`. Holds even when
+the bounded search inside `invAckHier`/`invAckNivasch` returns the `0`
+fallback, since `0 ≤ invAck n` is trivial. -/
+theorem invAckNivasch_le_invAck (n : ℕ) :
+    Nivasch.invAckNivasch n ≤ invAck n := by
+  sorry
+
+/-- Upper bound: `invAck n ≤ invAckNivasch n + 2`. The constant `2` is tight,
+witnessed at `n = 4` where `invAck 4 = 2` and `invAckNivasch 4 = 0`.
+
+This direction depends on the bounded search inside `invAckHier` and
+`invAckNivasch` actually finding the minimum (rather than hitting the `0`
+fallback); see the TODO on `invAckHier`. -/
+theorem invAck_le_invAckNivasch_add_two (n : ℕ) :
+    invAck n ≤ Nivasch.invAckNivasch n + 2 := by
+  sorry
+
+/-- `invAck` and `Nivasch.invAckNivasch` agree pointwise up to the explicit
+constant `2`. The constant is tight (witnessed at `n = 4`). -/
+theorem invAck_agree_Nivasch (n : ℕ) :
+    Nivasch.invAckNivasch n ≤ invAck n ∧
+      invAck n ≤ Nivasch.invAckNivasch n + 2 :=
+  ⟨invAckNivasch_le_invAck n, invAck_le_invAckNivasch_add_two n⟩
+
+end InverseAckermann
diff --git a/GraphLib/DataStructures/UnionFind/Blueprint.lean b/GraphLib/DataStructures/UnionFind/Blueprint.lean
index 3352765..c43a507 100644
--- a/GraphLib/DataStructures/UnionFind/Blueprint.lean
+++ b/GraphLib/DataStructures/UnionFind/Blueprint.lean
@@ -5,10 +5,11 @@ Authors: [your name here]
 -/
 
 import Batteries.Data.UnionFind
+import Mathlib.Algebra.BigOperators.Group.Finset.Defs
 import Mathlib.Data.Finset.Sum
 import Mathlib.Data.Nat.Log
-import Mathlib.Tactic
-import GraphLib.DataStructures.InverseAckermann
+import Mathlib.Tactic.Linarith
+import GraphLib.DataStructures.InverseAckermann.Basic
 
 /-!
 # `GraphLib.Algorithms.UnionFind`
@@ -16,7 +17,11 @@ import GraphLib.DataStructures.InverseAckermann
 Placeholder. Disjoint-set forests with union-by-rank and path compression.
 -/
 
-
+/-
+The inverse Ackermann function arises naturally in the amortised complexity
+analysis of Union-Find (disjoint-set forests with union-by-rank and path compression),
+where a sequence of `m` operations on `n` elements runs in `O(m · α(n))` time.
+-/
 /-!
 # Union-Find: Blueprint and Roadmap
 
@@ -212,11 +217,11 @@ theorem union_equiv_iff (s : UnionFind) (x y : Fin s.size) (a b : ℕ)
       s.Equiv a b ∨ (s.Equiv a x ∧ s.Equiv b y) ∨ (s.Equiv a y ∧ s.Equiv b x) := by
   convert union_equiv_of_equiv s x y using 1;
   rotate_left;
-  exact b;
-  exact a;
-  rw [ show ( s.union x y ).Equiv a b ↔ ( s.union x y ).Equiv b a from ?_ ];
-  · grind +suggestions;
-  · exact ⟨ fun h => equiv_symm _ h, fun h => equiv_symm _ h ⟩
+  · exact b;
+  · exact a;
+  · rw [ show ( s.union x y ).Equiv a b ↔ ( s.union x y ).Equiv b a from ?_ ];
+    · grind +suggestions;
+    · exact ⟨ fun h => equiv_symm _ h, fun h => equiv_symm _ h ⟩
 
 /-!
 ### 3.4  `push` adds an isolated element
@@ -313,11 +318,15 @@ Maximum rank is at most `⌊log₂ n⌋`.
 -/
 theorem rank_lt_log (s : UnionFind) (x : ℕ) (hx : x < s.size) :
     s.rank x ≤ Nat.log 2 s.size := by
-  refine' Nat.le_log_of_pow_le ( by decide ) _;
-  have h_card : (Finset.univ.filter fun i : Fin s.size => s.rank i = s.rank x).card ≥ 1 := by
-    exact Finset.card_pos.mpr ⟨ ⟨ x, hx ⟩, by aesop ⟩;
-  have := UnionFind.RankInvariant.count_rank_le s ( s.rank x );
-  nlinarith [ Nat.div_mul_le_self s.size ( 2 ^ s.rank x ), Nat.one_le_pow ( s.rank x ) 2 zero_lt_two ]
+  refine Nat.le_log_of_pow_le (by decide) ?_
+  have h_card : 1 ≤ (Finset.univ.filter fun i : Fin s.size => s.rank i = s.rank x).card :=
+    Finset.card_pos.mpr ⟨⟨x, hx⟩, by aesop⟩
+  have h_le := UnionFind.RankInvariant.count_rank_le s (s.rank x)
+  have h_one : 1 ≤ s.size / 2 ^ s.rank x := h_card.trans h_le
+  calc 2 ^ s.rank x
+      = 1 * 2 ^ s.rank x := (one_mul _).symm
+    _ ≤ (s.size / 2 ^ s.rank x) * 2 ^ s.rank x := Nat.mul_le_mul_right _ h_one
+    _ ≤ s.size := Nat.div_mul_le_self _ _
 
 /-!
 ### 4.2  Rank is unchanged by `find`
@@ -377,10 +386,59 @@ A simplified presentation appears in Cormen, Leiserson, Rivest, Stein (CLRS), Ch
 
 An alternative (and arguably cleaner) analysis is given by Seidel & Sharir (2005), who use
 a top-down approach with a simpler potential function. Both yield the same `O(m · α(n))` bound.
+
+Full citations:
+
+* R. E. Tarjan, *Efficiency of a good but not linear set union algorithm*,
+  JACM 22(2), 1975, pp. 215–225.
+* R. E. Tarjan and J. van Leeuwen, *Worst-case analysis of set union algorithms*,
+  JACM 31(2), 1984, pp. 245–281.
+* R. Seidel and M. Sharir, *Top-down analysis of path compression*,
+  SIAM J. Comput. 34(3), 2005, pp. 515–525.
 -/
 
 namespace UnionFind.Potential
 
+/-! ### Iterated / levelled inverse (Tarjan helpers)
+
+For the full Tarjan–van Leeuwen amortised analysis of Union-Find, one needs a
+finer decomposition using iterated applications of `ack`. The *level* of a node
+`x` with rank `r` whose root has rank `R` is
+
+  `level(x) = max { k : ack k r ≤ R }`
+
+and the *index* is
+
+  `index(x) = max { i : ack^[i]_{level(x)} r ≤ R }`.
+
+The two abstract definitions below operate purely on natural-number ranks and
+serve as low-level helpers for `nodeLevel` and `nodeIndex` further down. -/
+
+/-- The *level function* `ufLevel r R` for Union-Find complexity analysis.
+  Given a node rank `r` and the rank of its root `R` (with `r < R`), the level is
+  `max { k ≥ 0 : ack k r ≤ R }`.
+
+  This is well-defined because `ack k r` is strictly increasing in `k` and eventually
+  exceeds any bound. -/
+noncomputable def ufLevel (r R : ℕ) : ℕ :=
+  Nat.find (⟨R, lt_ack_left R r⟩ : ∃ k, R < ack k r) - 1
+
+/-- The *index function* `ufIndex r R k` for Union-Find complexity analysis.
+  Given rank `r`, root rank `R`, and level `k`, the index is
+  `max { i ≥ 1 : (ack k)^[i](r) ≤ R }`. -/
+noncomputable def ufIndex (r R k : ℕ) : ℕ :=
+  Nat.find (⟨R + 1, by
+    have h_ind : ∀ i : ℕ, r + i ≤ (ack k)^[i] r := by
+      intro i
+      induction i with
+      | zero => simp
+      | succ i ih =>
+        rw [Function.iterate_succ_apply']
+        exact Nat.succ_le_of_lt (lt_of_le_of_lt ih (lt_ack_right _ _))
+    have := h_ind (R + 1)
+    omega
+  ⟩ : ∃ i, R < (ack k)^[i] r) - 1
+
 /-!
 ### 5.1  Level and index of a node
 
@@ -429,7 +487,7 @@ noncomputable def nodeIndex (s : UnionFind) (x : ℕ) : ℕ :=
   - For a root node: `φ(x) = α(n) · rank(x)`
   - For a non-root node: `φ(x) = (α(n) - level(x)) · rank(x) - index(x)` -/
 noncomputable def nodePotential (s : UnionFind) (n : ℕ) (x : ℕ) : ℤ :=
-  let α_n := alpha n
+  let α_n := invAck n
   if s.parent x = x then
     -- Root node
     ↑α_n * ↑(s.rank x)
@@ -452,7 +510,7 @@ theorem potential_nonneg (s : UnionFind) : 0 ≤ potential s := by
 /-- Level of a non-root node is at most `α(n)`. -/
 theorem nodeLevel_le_alpha (s : UnionFind) (x : ℕ) (hx : s.parent x ≠ x)
     (hx_lt : x < s.size) :
-    nodeLevel s x ≤ alpha s.size := by
+    nodeLevel s x ≤ invAck s.size := by
   sorry
 
 /-- Index of a non-root node is at most `rank(x)`. -/
@@ -519,7 +577,7 @@ decreasing_by
   This is the key lemma in the Tarjan analysis. -/
 theorem find_amortised_cost (s : UnionFind) (x : Fin s.size) :
     (findCost s x : ℤ) + Potential.potential (s.find x).1 - Potential.potential s
-      ≤ ↑(alpha s.size) + 2 := by
+      ≤ ↑(invAck s.size) + 2 := by
   sorry
 
 end UnionFind.AmortisedFind
@@ -552,7 +610,7 @@ namespace UnionFind.AmortisedUnion
 theorem link_potential_change (s : UnionFind) (rx ry : Fin s.size)
     (hry : s.parent ry = ry) :
     Potential.potential (s.link rx ry hry) - Potential.potential s
-      ≤ ↑(alpha s.size) := by
+      ≤ ↑(invAck s.size) := by
   sorry
 
 /-- **Main amortised bound for `union`:**
@@ -564,7 +622,7 @@ theorem link_potential_change (s : UnionFind) (rx ry : Fin s.size)
   - `link`:    potential change ≤ `α(n)` -/
 theorem union_amortised_cost (s : UnionFind) (x y : Fin s.size) :
     Potential.potential (s.union x y) - Potential.potential s
-      ≤ 3 * ↑(alpha s.size) + 4 := by
+      ≤ 3 * ↑(invAck s.size) + 4 := by
   sorry
 
 end UnionFind.AmortisedUnion