Chronological heap-tree model for a static-array Fibonacci heap

This file defines the raw field view RawState n of a static-array Fibonacci heap together with an inductive rose-tree witness FHTree n whose children lists record the chronological linking order used in Fredman and Tarjan's child-loss rank invariant Fredman and Tarjan.

Representing trees inductively rather than by pointer reachability makes framing across disjoint subtrees structural: ValidSubtree inspects par, left, and right only at strict descendants of a subtree's root, so linking roots, rotating or splicing root lists, and updating the degree consolidation table leave existing subtrees valid by direct structural induction.

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.RawState: abstract view of the eight n-word node arrays, (n + 1)-word consolidation array, and four scalar heap counters.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree: rose tree over Fin n with chronological child lists.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree, ValidRoot: heap-order, pointer-realization, and Fredman–Tarjan chronological rank invariants (allowing at most one transient pending node during cascading cuts).

Main results

• ValidSubtree.fib_le_size, ValidSubtree.deg_bounds: fib (T.deg + 2) ≤ T.size, yielding both T.deg ≤ 2 * Nat.log 2 m + 1 and T.deg + 1 ≤ m whenever T.size ≤ m.
• ValidRoot.singleton, ValidRoot.link: creation of singleton root trees and degree-preserving root linking during consolidation.

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

Raw array/scalar state and marked-node counting

structure Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.RawState (n : ℕ) : Type

Decoded view of the static arrays and persistent scalar registers of a Fibonacci heap on n handles.

• key : Fin n → ℕ

  Key array key[v] (v < n).

• par : Fin n → ℕ

  Nullable parent pointer array par[v] (0 = root, p + 1 = parent p).

• child : Fin n → ℕ

  Nullable first-child pointer array child[v] (0 = leaf, c + 1 = child c).

• left : Fin n → ℕ

  Circular doubly-linked sibling predecessor array left[v].

• right : Fin n → ℕ

  Circular doubly-linked sibling successor array right[v].

• deg : Fin n → ℕ

  Child-list degree array deg[v].

• mark : Fin n → ℕ

  Cascading-cut mark array mark[v] (0 = unmarked, 1 = marked).

• inHeap : Fin n → ℕ

  Heap membership array inHeap[v] (0 = absent, 1 = present).

• cons : ℕ → ℕ

  Degree-consolidation scratch table A[d] (0 = empty, u + 1 = root u).

• minRoot : ℕ

  Nullable minimum-root pointer minRoot (0 = empty, r + 1 = root r).

• numRoots : ℕ

  Number of trees in the root list.

• numMarked : ℕ

  Number of currently live, marked handles.

• sz : ℕ

  Total number of live handles in the heap.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.markedSet {n : ℕ} (st : RawState n) : Finset (Fin n)

Set of currently live, marked handles.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.markedCount {n : ℕ} (st : RawState n) : ℕ

Number of currently live, marked handles.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.markedCount_le_n {n : ℕ} (st : RawState n) : markedCount st ≤ n

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.markedCount_congr {n : ℕ} {st st' : RawState n} (h : ∀ (u : Fin n), st'.inHeap u ≠ 0 ∧ st'.mark u ≠ 0 ↔ st.inHeap u ≠ 0 ∧ st.mark u ≠ 0) : markedCount st' = markedCount st

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.markedCount_clear_one {n : ℕ} {st st' : RawState n} {u : Fin n} (hin : st.inHeap u ≠ 0) (hm : st.mark u ≠ 0) (hu : st'.mark u = 0) (hother : ∀ (x : Fin n), x ≠ u → (st'.inHeap x ≠ 0 ∧ st'.mark x ≠ 0 ↔ st.inHeap x ≠ 0 ∧ st.mark x ≠ 0)) : markedCount st' + 1 = markedCount st

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.markedCount_set_one {n : ℕ} {st st' : RawState n} {u : Fin n} (hin : st'.inHeap u ≠ 0) (hm0 : st.mark u = 0) (hm1 : st'.mark u ≠ 0) (hother : ∀ (x : Fin n), x ≠ u → (st'.inHeap x ≠ 0 ∧ st'.mark x ≠ 0 ↔ st.inHeap x ≠ 0 ∧ st.mark x ≠ 0)) : markedCount st' = markedCount st + 1

Forward pointer chains for consolidation traversal

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

One-way right-pointer chain through a remaining list of roots or children.

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

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.IsCircList.rightChain {n : ℕ} {left right : Fin n → ℕ} {L : List (Fin n)} (hL : IsCircList left right L) : RightChain right L

Every circular doubly-linked list forms a RightChain.

Chronological rose-tree witnesses

inductive Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree (n : ℕ) : Type

Rose tree over Fin n whose children list is ordered chronologically by linking time.

• node {n : ℕ} (root : Fin n) (children : List (FHTree n)) : FHTree n

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.root {n : ℕ} : FHTree n → Fin n

Root handle of T.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.children {n : ℕ} : FHTree n → List (FHTree n)

Chronological child list of T.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.deg {n : ℕ} (T : FHTree n) : ℕ

Root degree of T.

@[simp]

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.root_node {n : ℕ} (u : Fin n) (cs : List (FHTree n)) : (node u cs).root = u

@[simp]

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.children_node {n : ℕ} (u : Fin n) (cs : List (FHTree n)) : (node u cs).children = cs

@[simp]

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.deg_node {n : ℕ} (u : Fin n) (cs : List (FHTree n)) : (node u cs).deg = cs.length

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.nodes {n : ℕ} : FHTree n → List (Fin n)

Preorder list of all handles in T.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.forestNodes {n : ℕ} : List (FHTree n) → List (Fin n)

Concatenated handle lists of a forest ts.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.size {n : ℕ} (T : FHTree n) : ℕ

Number of nodes in T.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.nodes_eq {n : ℕ} (T : FHTree n) : T.nodes = T.root :: forestNodes T.children

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.root_mem_nodes {n : ℕ} (T : FHTree n) : T.root ∈ T.nodes

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FHTree.size_pos {n : ℕ} (T : FHTree n) : 1 ≤ T.size

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.forestNodes_append {n : ℕ} (ts₁ ts₂ : List (FHTree n)) : forestNodes (ts₁ ++ ts₂) = forestNodes ts₁ ++ forestNodes ts₂

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.mem_forestNodes_iff {n : ℕ} {ts : List (FHTree n)} {x : Fin n} : x ∈ forestNodes ts ↔ ∃ T ∈ ts, x ∈ T.nodes

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.forestNodes_perm {n : ℕ} {ts₁ ts₂ : List (FHTree n)} (hp : ts₁.Perm ts₂) : (forestNodes ts₁).Perm (forestNodes ts₂)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.forestNodes_length_ge {n : ℕ} (ts : List (FHTree n)) : ts.length ≤ (forestNodes ts).length

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.forestNodes_nodup_tree {n : ℕ} {ts : List (FHTree n)} (hnd : (forestNodes ts).Nodup) {T : FHTree n} (hT : T ∈ ts) : T.nodes.Nodup

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.forestNodes_nodup_disjoint {n : ℕ} {ts : List (FHTree n)} (hnd : (forestNodes ts).Nodup) {T₁ T₂ : FHTree n} (h₁ : T₁ ∈ ts) (h₂ : T₂ ∈ ts) (hne : T₁ ≠ T₂) {x : Fin n} (hx₁ : x ∈ T₁.nodes) (hx₂ : x ∈ T₂.nodes) : False

Subtree and root invariants

inductive Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree {n : ℕ} (st : RawState n) (pending : Option (Fin n)) : FHTree n → Prop

Structural heap-order, child-list, and chronological rank invariant on a subtree T (hrank, a strengthening of Fredman and Tarjan, Lemma 1, p. 604; Cormen et al., Lemma 19.1). When pending = some w, w has just lost a child during cascading cuts and is permitted one extra unit of slack before either being cut itself (mark w = 1) or becoming marked (mark w = 0).

• mk {n : ℕ} {st : RawState n} {pending : Option (Fin n)} {u : Fin n} {cs : List (FHTree n)} (hin : st.inHeap u ≠ 0) (hmark : st.mark u ≤ 1) (hdeg : st.deg u = cs.length) (hchild : cs = [] ∧ st.child u = 0 ∨ ∃ (h : Fin n) (tail : List (Fin n)), st.child u = ↑h + 1 ∧ IsCircList st.left st.right (h :: tail) ∧ (h :: tail).Perm (List.map FHTree.root cs)) (hpar : ∀ T ∈ cs, st.par T.root = ↑u + 1) (hprio : ∀ T ∈ cs, Lean.IndexedMinPQ.PrioLT (u, st.key u) (T.root, st.key T.root)) (hrank : ∀ (i : ℕ) (hi : i < cs.length), i ≤ st.deg cs[i].root + st.mark cs[i].root + if some cs[i].root = pending then 1 else 0) (hsub : ∀ T ∈ cs, ValidSubtree st pending T) : ValidSubtree st pending (FHTree.node u cs)

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidRoot {n : ℕ} (st : RawState n) (pending : Option (Fin n)) (T : FHTree n) : Prop

A valid root tree is a valid subtree whose root has par = 0 and mark = 0.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.frame {n : ℕ} {st st' : RawState n} {pending pending' : Option (Fin n)} {T : FHTree n} (hT : ValidSubtree st pending T) (hnode : ∀ x ∈ T.nodes, st'.inHeap x = st.inHeap x ∧ st'.mark x = st.mark x ∧ st'.deg x = st.deg x ∧ st'.child x = st.child x ∧ st'.key x = st.key x) (hdesc : ∀ x ∈ forestNodes T.children, st'.par x = st.par x ∧ st'.left x = st.left x ∧ st'.right x = st.right x ∧ (some x = pending' ↔ some x = pending)) : ValidSubtree st' pending' T

ValidSubtree inspects par, left, right, and pending only on strict descendants forestNodes T.children, never on T.root itself.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.weaken_pending {n : ℕ} {st : RawState n} (pending : Option (Fin n)) {T : FHTree n} (hT : ValidSubtree st none T) : ValidSubtree st pending T

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.clear_pending {n : ℕ} {st : RawState n} {z : Fin n} {T : FHTree n} (hT : ValidSubtree st (some z) T) (hz : z ∉ forestNodes T.children) : ValidSubtree st none T

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.prioLT_of_mem_children {n : ℕ} {st : RawState n} {pending : Option (Fin n)} {T : FHTree n} (hT : ValidSubtree st pending T) (x : Fin n) : x ∈ forestNodes T.children → Lean.IndexedMinPQ.PrioLT (T.root, st.key T.root) (x, st.key x)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.prioLE_of_mem {n : ℕ} {st : RawState n} {pending : Option (Fin n)} {T : FHTree n} (hT : ValidSubtree st pending T) {x : Fin n} (hx : x ∈ T.nodes) : Lean.IndexedMinPQ.PrioLE (T.root, st.key T.root) (x, st.key x)

Fibonacci subtree-size and degree bounds

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.deg_add_one_le_fib (d : ℕ) : d + 1 ≤ Nat.fib (d + 2)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.fib_le_size {n : ℕ} {st : RawState n} {T : FHTree n} (hT : ValidSubtree st none T) : Nat.fib (T.deg + 2) ≤ T.size

Fredman–Tarjan subtree size lower bound (Fredman and Tarjan, Corollary 1, p. 604; Cormen et al., Lemma 19.4): in any subtree with no pending cascading cut, Nat.fib (T.deg + 2) ≤ T.size.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.deg_bounds {n : ℕ} {st : RawState n} {T : FHTree n} (hT : ValidSubtree st none T) {m : ℕ} (hm : T.size ≤ m) : T.deg ≤ 2 * Nat.log 2 m + 1 ∧ T.deg + 1 ≤ m

Any valid subtree of size at most m has degree ≤ 2 * Nat.log 2 m + 1 and deg + 1 ≤ m.

Constructing and linking root trees

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidRoot.singleton {n : ℕ} {st : RawState n} {v : Fin n} (hin : st.inHeap v ≠ 0) (hpar : st.par v = 0) (hchild : st.child v = 0) (hdeg : st.deg v = 0) (hmark : st.mark v = 0) : ValidRoot st none (FHTree.node v [])

Creating a singleton root tree .node v [].

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.link_nodes_eq {n : ℕ} (u : Fin n) (cs₁ : List (FHTree n)) (T₂ : FHTree n) : (FHTree.node u (cs₁ ++ [T₂])).nodes = (FHTree.node u cs₁).nodes ++ T₂.nodes

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidRoot.link {n : ℕ} {st st' : RawState n} {T₁ T₂ : FHTree n} (h₁ : ValidRoot st none T₁) (h₂ : ValidRoot st none T₂) (hnd : (T₁.nodes ++ T₂.nodes).Nodup) (hdeg_eq : T₁.deg = T₂.deg) (hprio_lt : Lean.IndexedMinPQ.PrioLT (T₁.root, st.key T₁.root) (T₂.root, st.key T₂.root)) (hunch : ∀ x ∈ T₁.nodes ++ T₂.nodes, st'.inHeap x = st.inHeap x ∧ st'.mark x = st.mark x ∧ st'.key x = st.key x) (hdeg' : st'.deg T₁.root = T₁.deg + 1 ∧ ∀ x ∈ T₁.nodes ++ T₂.nodes, x ≠ T₁.root → st'.deg x = st.deg x) (hpar' : st'.par T₁.root = 0 ∧ st'.par T₂.root = ↑T₁.root + 1 ∧ ∀ x ∈ T₁.nodes ++ T₂.nodes, x ≠ T₂.root → st'.par x = st.par x) (hchild' : (∃ (h : Fin n) (tail : List (Fin n)), st'.child T₁.root = ↑h + 1 ∧ IsCircList st'.left st'.right (h :: tail) ∧ (h :: tail).Perm (List.map FHTree.root (T₁.children ++ [T₂]))) ∧ ∀ x ∈ T₁.nodes ++ T₂.nodes, x ≠ T₁.root → st'.child x = st.child x) (hlr' : ∀ x ∈ T₁.nodes ++ T₂.nodes, x ≠ T₂.root → (∀ c ∈ T₁.children, x ≠ c.root) → st'.left x = st.left x ∧ st'.right x = st.right x) : ValidRoot st' none (FHTree.node T₁.root (T₁.children ++ [T₂]))

Linking an equal-degree root tree T₂ as the newest child of T₁ preserves ValidRoot when (T₁.root, key₁) strictly precedes (T₂.root, key₂) under IndexedMinPQ.PrioLT.