Mathematical model of a static-array Fibonacci heap

This file develops the pure-Lean invariants and structural lemmas underlying the static-array Word-RAM Fibonacci heap Fredman and Tarjan Cormen et al., Chapter 19:

1. Circular doubly-linked lists (ChainLinks, IsCircList): Pointer-level invariants over Fin n → ℕ supporting O(1) singleton creation, post-head insertion, cyclic rotation, arbitrary node removal, and disjoint-support framing without modular index arithmetic.
2. Pure-ℕ Fibonacci rank and degree bound: Proves the sum identity 1 + ∑_{i < k} fib ((i - 1) + 2) = fib (k + 2) and 2 ^ m ≤ fib (2 * m + 2), deriving d ≤ 2 * Nat.log 2 n + 1 from fib (d + 2) ≤ n without real numbers or floating-point logarithms.

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ChainLinks, IsCircList: pointer-level invariants for circular doubly-linked lists over Fin n → ℕ.

Main results

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.singleton, IsCircList.insertAfter, IsCircList.rotate_to, IsCircList.remove: circular-list operations.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.fib_sum_pred_add_two, deg_le_two_mul_log_add_one: pure-ℕ Fibonacci child-rank sum and 2 * Nat.log 2 n + 1 degree bound.

References

• M. L. Fredman and R. E. Tarjan, Fibonacci Heaps and Their Uses in Improved Network Optimization Algorithms
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 19

Circular doubly-linked lists over Fin n

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ChainLinks {n : ℕ} (left right : Fin n → ℕ) (first prev : Fin n) : List (Fin n) → Prop

Pointer chain from prev through xs closing back to first.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList {n : ℕ} (left right : Fin n → ℕ) : List (Fin n) → Prop

L is represented as a circular doubly-linked list by left and right (with [] vacuously valid and h :: tail forming a Nodup cycle starting at h).

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ChainLinks.frame {n : ℕ} {left left' right right' : Fin n → ℕ} {first prev : Fin n} {xs : List (Fin n)} (hc : ChainLinks left right first prev xs) (hfirst : left' first = left first) (hprev : right' prev = right prev) (hxs : ∀ x ∈ xs, left' x = left x ∧ right' x = right x) : ChainLinks left' right' first prev xs

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.frame {n : ℕ} {left left' right right' : Fin n → ℕ} {L : List (Fin n)} (hL : IsCircList left right L) (heq : ∀ x ∈ L, left' x = left x ∧ right' x = right x) : IsCircList left' right' L

IsCircList depends only on left and right at members of L.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.singleton {n : ℕ} (left right : Fin n → ℕ) (u : Fin n) : IsCircList (Function.update left u ↑u) (Function.update right u ↑u) [u]

Forming a singleton circular list [u].

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.right_head {n : ℕ} {left right : Fin n → ℕ} {h : Fin n} {tail : List (Fin n)} (hL : IsCircList left right (h :: tail)) : ∃ (r : Fin n), right h = ↑r ∧ r ∈ h :: tail

In a non-empty circular list h :: tail, right h is the index of (tail ++ [h])[0], hence strictly less than n and a member of h :: tail.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.insertAfter {n : ℕ} {left right : Fin n → ℕ} {h u : Fin n} {tail : List (Fin n)} (hL : IsCircList left right (h :: tail)) (hu : u ∉ h :: tail) {r : Fin n} (hr : right h = ↑r) : have left₁ := Function.update (Function.update left u ↑h) r ↑u; have right₁ := Function.update (Function.update right u ↑r) h ↑u; IsCircList left₁ right₁ (h :: u :: tail)

Inserting a fresh node u ∉ h :: tail immediately after h yields h :: u :: tail.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.rotate_one {n : ℕ} {left right : Fin n → ℕ} {h : Fin n} {tail : List (Fin n)} (hL : IsCircList left right (h :: tail)) : IsCircList left right (tail ++ [h])

Rotating a circular list by one element preserves IsCircList.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.rotate_to {n : ℕ} {left right : Fin n → ℕ} {L₁ L₂ : List (Fin n)} {v : Fin n} (hL : IsCircList left right (L₁ ++ v :: L₂)) : IsCircList left right (v :: (L₂ ++ L₁))

Splitting a circular list L₁ ++ v :: L₂ rotates v to the front as v :: (L₂ ++ L₁).

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.exists_head {n : ℕ} {left right : Fin n → ℕ} {L : List (Fin n)} {v : Fin n} (hL : IsCircList left right L) (hv : v ∈ L) : ∃ (tail : List (Fin n)), IsCircList left right (v :: tail) ∧ (v :: tail).Perm L

Any member v ∈ L of a circular list can be rotated to the head while preserving Perm.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.remove {n : ℕ} {left right : Fin n → ℕ} {L : List (Fin n)} {v : Fin n} (hL : IsCircList left right L) (hv : v ∈ L) (hlen : 2 ≤ L.length) : ∃ (r : Fin n) (l : Fin n) (rest : List (Fin n)), right v = ↑r ∧ left v = ↑l ∧ r ∈ L ∧ l ∈ L ∧ r ≠ v ∧ IsCircList (Function.update left r ↑l) (Function.update right l ↑r) (r :: rest) ∧ (r :: rest).Perm (L.erase v)

Removing v from a circular list L of length ≥ 2 (v ∈ L) by setting right[left[v]] ← right[v] and left[right[v]] ← left[v] produces a circular list starting at r (right v = r.val) that is a permutation of L.erase v.

Pure-ℕ Fibonacci rank and degree bounds

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.fib_sum_pred_add_two (k : ℕ) : 1 + ∑ i ∈ Finset.range k, Nat.fib (i - 1 + 2) = Nat.fib (k + 2)

Fundamental Fibonacci rank identity (used in the proof of Fredman and Tarjan, Corollary 1, p. 604; Cormen et al., Lemma 19.2): 1 + ∑_{i < k} fib ((i - 1) + 2) = fib (k + 2) in ℕ (where 0 - 1 = 0).

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.two_pow_le_fib (m : ℕ) : 2 ^ m ≤ Nat.fib (2 * m + 2)

Exponential lower bound on even-index Fibonacci numbers without golden-ratio reals: 2 ^ m ≤ fib (2 * m + 2) for all m : ℕ.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.deg_le_two_mul_log_add_one {d n : ℕ} (hfib : Nat.fib (d + 2) ≤ n) : d ≤ 2 * Nat.log 2 n + 1

Any node degree d satisfying Nat.fib (d + 2) ≤ n obeys the pure-ℕ logarithmic upper bound d ≤ 2 * Nat.log 2 n + 1.