Ackermann hierarchy and the inverse-Ackermann function

import Std

set_option autoImplicit true
set_option backward.isDefEq.respectTransparency false
set_option backward.defeqAttrib.useBackward true



set_option backward.isDefEq.respectTransparency false
set_option backward.defeqAttrib.useBackward true

/-!
The Ackermann hierarchy used in the union-find amortized analysis.
`ack 0 r = r + 1` and `ack (k + 1) r` applies `ack k` exactly `r + 1`
times to `r`. The inverse `alpha n` is the least positive hierarchy index
whose value at one exceeds `n`. All arithmetic facts are independent of
program execution and of the union-find representation.
-/

namespace Algo2Lean.Ackermann

/-- Apply a natural-number function a fixed number of times. -/
def iterate (f : Nat → Nat) : Nat → Nat → Nat
  | 0, value => value
  | count + 1, value => f (iterate f count value)

@[simp] theorem iterate_zero (f : Nat → Nat) (value : Nat) :
    iterate f 0 value = value := rfl

@[simp] theorem iterate_succ (f : Nat → Nat) (count value : Nat) :
    iterate f (count + 1) value = f (iterate f count value) := rfl









theorem iterate_mono_count {f : Nat → Nat}
    (grow : ∀ value, value ≤ f value) {first second : Nat} (ordered : first ≤ second)
    (value : Nat) : iterate f first value ≤ iterate f second value := by
  induction second generalizing first with
  | zero =>
    have zero : first = 0 := by omega
    simp [zero]
  | succ second ih =>
    by_cases same : first = second + 1
    · subst first; exact Nat.le_refl _
    · exact Nat.le_trans (ih (by omega)) (grow _)

theorem iterate_strict_count {f : Nat → Nat}
    (grow : ∀ value, value < f value) {first second : Nat} (ordered : first < second)
    (value : Nat) : iterate f first value < iterate f second value := by
  have step := grow (iterate f first value)
  have rest := iterate_mono_count (fun x => Nat.le_of_lt (grow x)) ordered value
  exact Nat.lt_of_lt_of_le step rest



/-- The increasing hierarchy obtained by repeated iteration. -/
def ack : Nat → Nat → Nat
  | 0, value => value + 1
  | level + 1, value => iterate (ack level) (value + 1) value

@[simp] theorem ack_zero (value : Nat) : ack 0 value = value + 1 := rfl



theorem ack_gt (level value : Nat) : value < ack level value := by
  induction level generalizing value with
  | zero => simp
  | succ level ih =>
    have start := ih value
    have rest := iterate_mono_count (fun x => Nat.le_of_lt (ih x))
      (Nat.succ_le_succ (Nat.zero_le value)) value
    exact Nat.lt_of_lt_of_le start rest









theorem ack_lt_succ (level : Nat) {value : Nat} (positive : 0 < value) :
    ack level value < ack (level + 1) value := by
  exact iterate_strict_count (ack_gt level) (by omega : 1 < value + 1) value

theorem index_bound (level : Nat) : level + 2 ≤ ack level 1 := by
  induction level with
  | zero => simp
  | succ level ih =>
    have growing := ack_lt_succ level (by decide : 0 < 1)
    omega

/-- Every inhabited natural-number predicate has a least witness. -/
 theorem least_exists (property : Nat → Prop) (inhabited : ∃ value, property value) :
    ∃ value, property value ∧ ∀ other, other < value → ¬ property other := by
  classical
  obtain ⟨bound, holds⟩ := inhabited
  induction bound using Nat.strongRecOn with
  | ind bound ih =>
    by_cases earlier : ∃ other, other < bound ∧ property other
    · obtain ⟨other, smaller, valid⟩ := earlier
      exact ih other smaller valid
    · exact ⟨bound, holds, fun other smaller valid => earlier ⟨other, smaller, valid⟩⟩

 theorem inverse_exists (n : Nat) :
    ∃ level, (0 < level ∧ n < ack level 1) ∧
      ∀ other, other < level → ¬ (0 < other ∧ n < ack other 1) := by
  apply least_exists
  refine ⟨n + 1, by omega, ?_⟩
  have := index_bound (n + 1)
  omega

/-- Least positive level whose Ackermann value at one exceeds the input. -/
noncomputable def alpha (n : Nat) : Nat := Classical.choose (inverse_exists n)





















end Algo2Lean.Ackermann

• Endorsed by Shuze Chen · Oct 11, 2026

  Confirmed by the moderator at approval.

• Endorsed by lunjia · Oct 11, 2026

  Confirmed by the mission captain (proposal self-audit).