Forest invariants and pure state transitions for a Fibonacci heap

This file lifts the single-tree model of Trees.lean to the full multi-root forest invariant FibRawInv and proves the structural transitions required by all priority-queue operations:

• Subtree cutting (exists_parent_info, ValidSubtree.exists_cut): Severing a non-root node cur from its parent p splits T into a new valid root tree T_cut rooted at cur and a modified tree T' with pending = some p while preserving the multiset of tree nodes.
• Full heap invariant (FibRawInv): Relates s : IndexedMinPQ.State n to st : RawState n with exact domain, key, size, root-count, marked-count, minRoot, and cons-zeroing invariants, proving IndexedMinPQ.findMin agreement (FibRawInv.findMin_eq_some) and scalar bounds.
• Transient cut invariant (CutInv): Loop invariant for cascading cuts during decreaseKey, allowing a single pending ancestor whose child was just severed.

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibRawInv: full multi-root forest representation invariant relating IndexedMinPQ.State n to RawState n.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.CutInv: transient forest invariant during cascading cuts in decreaseKey.

Main results

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.exists_cut: severing a non-root node splits its enclosing tree into a valid root tree and a pending-parent tree.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibRawInv.findMin_eq_some: minRoot identifies the exact IndexedMinPQ.findMin element.

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

List surgery lemmas for child removal and replacement

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.map_root_nodup {n : ℕ} {cs : List (FHTree n)} (hnd : (forestNodes cs).Nodup) : (List.map FHTree.root cs).Nodup

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.forestNodes_nodup_idx_disjoint {n : ℕ} {cs : List (FHTree n)} (hnd : (forestNodes cs).Nodup) {i j : ℕ} (hi : i < cs.length) (hj : j < cs.length) (hij : i ≠ j) {x : Fin n} (hxi : x ∈ cs[i].nodes) (hxj : x ∈ cs[j].nodes) : False

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.forestNodes_eraseIdx_perm {n : ℕ} (cs : List (FHTree n)) (i : ℕ) (hi : i < cs.length) : (cs[i].nodes ++ forestNodes (cs.eraseIdx i)).Perm (forestNodes cs)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.forestNodes_set_perm {n : ℕ} (cs : List (FHTree n)) (i : ℕ) (hi : i < cs.length) (T_cut c' : FHTree n) : (T_cut.nodes ++ c'.nodes).Perm cs[i].nodes → (T_cut.nodes ++ forestNodes (cs.set i c')).Perm (forestNodes cs)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.map_root_set_eq {n : ℕ} (cs : List (FHTree n)) (i : ℕ) (hi : i < cs.length) (c' : FHTree n) : c'.root = cs[i].root → List.map FHTree.root (cs.set i c') = List.map FHTree.root cs

Parent witnesses and subtree cutting

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.par_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 → ∃ q ∈ T.nodes, st.par x = ↑q + 1

Every strict descendant x of T has st.par x = q.val + 1 for some q ∈ T.nodes.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.frame_root_mark {n : ℕ} {st st' : RawState n} {pending pending' : Option (Fin n)} {T : FHTree n} (hT : ValidSubtree st pending T) (hnd : T.nodes.Nodup) (hrm : st'.mark T.root ≤ 1) (hroot : st'.inHeap T.root = st.inHeap T.root ∧ st'.deg T.root = st.deg T.root ∧ st'.child T.root = st.child T.root ∧ st'.key T.root = st.key T.root) (hdesc_node : ∀ x ∈ forestNodes T.children, 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_ptr : ∀ 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

Updating only the root's mark to a value ≤ 1 while keeping all other subtree fields fixed preserves ValidSubtree.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.exists_parent_info {n : ℕ} {st : RawState n} {pending : Option (Fin n)} {T : FHTree n} (hT : ValidSubtree st pending T) {cur p : Fin n} (hcur : cur ∈ forestNodes T.children) (hpar_cur : st.par cur = ↑p + 1) : p ∈ T.nodes ∧ st.inHeap p ≠ 0 ∧ st.mark p ≤ 1 ∧ st.inHeap cur ≠ 0 ∧ st.mark cur ≤ 1 ∧ 1 ≤ st.deg p ∧ (2 ≤ st.deg p → ∃ (h : Fin n) (tail : List (Fin n)), st.child p = ↑h + 1 ∧ IsCircList st.left st.right (h :: tail) ∧ cur ∈ h :: tail ∧ 2 ≤ (h :: tail).length ∧ ∀ x ∈ h :: tail, st.par x = ↑p + 1)

Pre-cut structural properties of cur and its parent p inside any valid subtree containing cur as a strict descendant.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.exists_cut {n : ℕ} {st st' : RawState n} {pending : Option (Fin n)} {T : FHTree n} (hT : ValidSubtree st pending T) (hnd : T.nodes.Nodup) {cur p : Fin n} (hcur : cur ∈ forestNodes T.children) (hpar_cur : st.par cur = ↑p + 1) (hpend : pending = none ∨ pending = some cur) (hin_eq : ∀ x ∈ T.nodes, st'.inHeap x = st.inHeap x ∧ st'.key x = st.key x) (hmark' : st'.mark cur = 0 ∧ ∀ x ∈ T.nodes, x ≠ cur → st'.mark x = st.mark x) (hdeg' : st'.deg p + 1 = st.deg p ∧ ∀ x ∈ T.nodes, x ≠ p → st'.deg x = st.deg x) (hpar' : st'.par cur = 0 ∧ ∀ x ∈ T.nodes, x ≠ cur → st'.par x = st.par x) (hchild_p : (st.deg p = 1 → st'.child p = 0) ∧ ∀ (h : Fin n) (tail : List (Fin n)), 2 ≤ st.deg p → st.child p = ↑h + 1 → IsCircList st.left st.right (h :: tail) → cur ∈ h :: tail → ∃ (r : Fin n) (rest : List (Fin n)), st'.child p = ↑r + 1 ∧ IsCircList st'.left st'.right (r :: rest) ∧ (r :: rest).Perm ((h :: tail).erase cur)) (hchild_other : ∀ x ∈ T.nodes, x ≠ p → st'.child x = st.child x) (hlr_other : ∀ x ∈ T.nodes, st.par x ≠ ↑p + 1 → st.par x ≠ 0 → st'.left x = st.left x ∧ st'.right x = st.right x) : ∃ (T_cut : FHTree n) (T' : FHTree n), T_cut.root = cur ∧ T'.root = T.root ∧ p ∈ T'.nodes ∧ (T_cut.nodes ++ T'.nodes).Perm T.nodes ∧ ValidRoot st' none T_cut ∧ ValidSubtree st' (some p) T'

Cutting a strict descendant cur (with st.par cur = p.val + 1) from T splits T into a new root tree T_cut (T_cut.root = cur) and a pruned tree T' (T'.root = T.root, p ∈ T'.nodes) satisfying ValidRoot st' none T_cut and ValidSubtree st' (some p) T'.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.mark_pending {n : ℕ} {st st' : RawState n} {z : Fin n} {T : FHTree n} (hT : ValidSubtree st (some z) T) (hm0 : st.mark z = 0) (hm1 : st'.mark z = 1) (hm_other : ∀ x ∈ T.nodes, x ≠ z → st'.mark x = st.mark x) (hunch : ∀ x ∈ T.nodes, st'.inHeap x = st.inHeap x ∧ st'.deg x = st.deg x ∧ st'.child x = st.child x ∧ st'.key x = st.key x) (hptr : ∀ x ∈ forestNodes T.children, st'.par x = st.par x ∧ st'.left x = st.left x ∧ st'.right x = st.right x) : ValidSubtree st' none T

Marking an unmarked pending = some z node (st.mark z = 0, st'.mark z = 1) absorbs the transient rank slack and restores ValidSubtree st' none T.

Full heap representation invariant and core consequences

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibRawInv (n K_max : ℕ) (s : Lean.IndexedMinPQ.State n) (st : RawState n) : Prop

Full structural, key, counter, and root-list invariant relating s : IndexedMinPQ.State n to st : RawState n.

def Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.CutInv (n K_max : ℕ) (s : Lean.IndexedMinPQ.State n) (st : RawState n) (v m : Fin n) (pending : Option (Fin n)) : Prop

Transient forest invariant during decreaseKey v k while cascading cuts propagate from pending.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibRawInv.empty {n K_max : ℕ} {st : RawState n} (hin : ∀ (v : Fin n), st.inHeap v = 0) (hcons : ∀ d ≤ n, st.cons d = 0) (hmin : st.minRoot = 0) (hnr : st.numRoots = 0) (hnm : st.numMarked = 0) (hsz : st.sz = 0) : FibRawInv n K_max (Lean.IndexedMinPQ.empty n) st

FibRawInv holds on the empty priority queue whenever inHeap and cons[0..n] are zeroed and the four scalar counters are 0.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibRawInv.bounds {n K_max : ℕ} {s : Lean.IndexedMinPQ.State n} {st : RawState n} (h : FibRawInv n K_max s st) : st.sz ≤ n ∧ st.numRoots ≤ n ∧ st.numMarked ≤ n ∧ st.minRoot ≤ n

All scalar counters of a valid Fibonacci heap are bounded by n.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibRawInv.unique {n K_max : ℕ} {s₁ s₂ : Lean.IndexedMinPQ.State n} {st : RawState n} (h₁ : FibRawInv n K_max s₁ st) (h₂ : FibRawInv n K_max s₂ st) : s₁ = s₂

Concrete state uniquely determines the represented IndexedMinPQ.State n.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibRawInv.findMin_eq_none {n K_max : ℕ} {s : Lean.IndexedMinPQ.State n} {st : RawState n} (h : FibRawInv n K_max s st) (h0 : st.minRoot = 0) : Lean.IndexedMinPQ.dom s = ∅ ∧ Lean.IndexedMinPQ.findMin s = none

When st.minRoot = 0, dom s = ∅ and IndexedMinPQ.findMin s = none.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.FibRawInv.findMin_eq_some {n K_max : ℕ} {s : Lean.IndexedMinPQ.State n} {st : RawState n} (h : FibRawInv n K_max s st) {z : Fin n} (hz : st.minRoot = ↑z + 1) : Lean.IndexedMinPQ.findMin s = some (z, st.key z) ∧ s z = some (st.key z) ∧ st.key z ≤ K_max

When st.minRoot = z.val + 1, IndexedMinPQ.findMin s = some (z, st.key z).