Fibonacci Heap: decreaseKey and Cascading Cuts

This file proves the exact-Word-RAM specification decreaseKeyCode_exec (O(1) amortized time under potential = 80 * (numRoots + 2 * numMarked)):

• No-cut key decrease (ValidSubtree.lower_key_no_cut): When v is already a root or lowering key[v] to k ≤ key[v] preserves IndexedMinPQ.PrioLT (p, key[p]) (v, k), FibRawInv holds without cutting any edges.
• Single-edge cut (cutNodeCode_raw, cutNode_forest): Executes cutNodeCode in at most 36 instructions, splicing cur into the circular root list, updating parent degree/child pointers, clearing par[cur] and mark[cur], and adjusting potential by -80 when cur was marked or +80 when cur was unmarked.
• Cascading cuts (decreaseKeyCode_exec): Applies ExecWithin.loop_potential_retain to pay every cascading-cut iteration (≤ 50 instructions including loop step) out of the -80 drop in potential, marks the stopping non-root ancestor (+160), updates minRootReg, and restores FibInv within amortized charge 330 (335 ≤ tDec n including dispatch).

Main definitions

• cutNodeCode and decreaseKeyCode are defined in Complexity/Algorithms/WordRAM/PriorityQueue/FibonacciHeap/Program.lean and verified here against CutInv and FibInv.

Main results

• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.cutNodeCode_raw, cutNode_forest: single-edge pointer and forest cut specifications.
• Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.decreaseKeyCode_exec: O(1) amortized decreaseKey specification with cascading cuts.

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

Pure forest lemmas for decreaseKey

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidRoot.par_eq_zero_iff_root {n : ℕ} {st : RawState n} {pending : Option (Fin n)} {T : FHTree n} (hT : ValidRoot st pending T) {u : Fin n} (hu : u ∈ T.nodes) : st.par u = 0 ↔ u = T.root

Inside a valid root tree T with Nodup nodes, st.par u = 0 holds iff u = T.root.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.ValidSubtree.lower_key_no_cut {n : ℕ} {st st' : RawState n} {T : FHTree n} (hT : ValidSubtree st none T) (hnd : T.nodes.Nodup) {v : Fin n} {k : ℕ} (hv : v ∈ T.nodes) (hle : k ≤ st.key v) (hk_v : st'.key v = k) (hk_other : ∀ x ∈ T.nodes, x ≠ v → st'.key x = st.key x) (hunch : ∀ 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) (hptr : ∀ x ∈ forestNodes T.children, st'.par x = st.par x ∧ st'.left x = st.left x ∧ st'.right x = st.right x) (hord : v = T.root ∨ ∃ (p : Fin n), st.par v = ↑p + 1 ∧ ¬Lean.IndexedMinPQ.PrioLT (v, k) (p, st.key p)) : ValidSubtree st' none T

Lowering key[v] to k ≤ st.key v preserves ValidSubtree st' none T whenever v = T.root or v has parent p (st.par v = p.val + 1) with ¬IndexedMinPQ.PrioLT (v, k) (p, st.key p).

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

Scalar counter bounds under CutInv.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.CutInv.to_fibRawInv {n K_max : ℕ} {s : Lean.IndexedMinPQ.State n} {st st' : RawState n} {v m : Fin n} (h : CutInv n K_max s st v m none) (heq : st'.key = st.key ∧ st'.par = st.par ∧ st'.child = st.child ∧ st'.left = st.left ∧ st'.right = st.right ∧ st'.deg = st.deg ∧ st'.mark = st.mark ∧ st'.inHeap = st.inHeap ∧ st'.cons = st.cons ∧ st'.numRoots = st.numRoots ∧ st'.numMarked = st.numMarked ∧ st'.sz = st.sz) (hmin : Lean.IndexedMinPQ.PrioLT (v, st.key v) (m, st.key m) ∧ st'.minRoot = ↑v + 1 ∨ ¬Lean.IndexedMinPQ.PrioLT (v, st.key v) (m, st.key m) ∧ st'.minRoot = ↑m + 1) : FibRawInv n K_max s st'

Once cascading cuts finish (pending = none) and minRoot is updated against (v, st.key v), CutInv upgrades back to FibRawInv.

evalCascGuard specification

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.evalCascGuard_exec {n base w : ℕ} {x : WordRAM.Data rFib} (hb : WordRAM.Data.Bounded w x) (hbr : BaseRegs n base x) {cur : Fin n} (hz_reg : x.regs zReg = ↑cur) : have st := RawState.ofData n base x; have gval := if st.par cur ≠ 0 ∧ st.mark cur ≠ 0 then 1 else 0; ∃ (y : WordRAM.Data rFib), WordRAM.ExecWithin w evalCascGuard x y 8 ∧ BaseRegs n base y ∧ RawState.ofData n base y = st ∧ y.mem = x.mem ∧ y.regs iterCur = gval ∧ ∀ (r : Fin rFib), r ≠ s0 → r ≠ s1 → r ≠ s2 → r ≠ iterCur → y.regs r = x.regs r

evalCascGuard sets iterCur ← 1 iff par[cur] ≠ 0 ∧ mark[cur] ≠ 0, and 0 otherwise, in at most 8 instructions while preserving BaseRegs, RawState.ofData, and all registers other than s0, s1, s2, iterCur.

cutNodeCode machine execution

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.cutNodeCode_raw {n base w : ℕ} {x : WordRAM.Data rFib} (hb : WordRAM.Data.Bounded w x) (hbr : BaseRegs n base x) {cur p m : Fin n} {rtail : List (Fin n)} (hz_reg : x.regs zReg = ↑cur) (hp_reg : x.regs pReg = ↑p) (hdp_pos : 1 ≤ (RawState.ofData n base x).deg p) (hdp_le : (RawState.ofData n base x).deg p ≤ n) (hdp2 : 2 ≤ (RawState.ofData n base x).deg p → ∃ (h : Fin n) (tail : List (Fin n)), (RawState.ofData n base x).child p = ↑h + 1 ∧ IsCircList (RawState.ofData n base x).left (RawState.ofData n base x).right (h :: tail) ∧ cur ∈ h :: tail ∧ 2 ≤ (h :: tail).length ∧ ∀ u ∈ h :: tail, (RawState.ofData n base x).par u = ↑p + 1) (hmin : (RawState.ofData n base x).minRoot = ↑m + 1) (hcirc_r : IsCircList (RawState.ofData n base x).left (RawState.ofData n base x).right (m :: rtail)) (hroots_par0 : ∀ u ∈ m :: rtail, (RawState.ofData n base x).par u = 0) (hpar_cur : (RawState.ofData n base x).par cur = ↑p + 1) (hin_cur : (RawState.ofData n base x).inHeap cur ≠ 0) (hnm : (RawState.ofData n base x).numMarked = markedCount (RawState.ofData n base x)) (hnr_le : (RawState.ofData n base x).numRoots + 1 ≤ n) : ∃ (y : WordRAM.Data rFib), WordRAM.ExecWithin w cutNodeCode x y 36 ∧ BaseRegs n base y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ (∀ (r : Fin rFib), r ≠ s0 → r ≠ s1 → r ≠ s2 → r ≠ s3 → r ≠ s4 → r ≠ numMarkedReg → r ≠ numRootsReg → y.regs r = x.regs r) ∧ have st := RawState.ofData n base x; have st' := RawState.ofData n base y; st'.key = st.key ∧ st'.inHeap = st.inHeap ∧ st'.cons = st.cons ∧ st'.minRoot = st.minRoot ∧ st'.sz = st.sz ∧ st'.numRoots = st.numRoots + 1 ∧ st'.numMarked = markedCount st' ∧ ((st.mark cur ≠ 0 → potential y + unitCredit = potential x) ∧ (st.mark cur = 0 → potential y = potential x + unitCredit)) ∧ (st'.mark cur = 0 ∧ ∀ (u : Fin n), u ≠ cur → st'.mark u = st.mark u) ∧ (st'.deg p + 1 = st.deg p ∧ ∀ (u : Fin n), u ≠ p → st'.deg u = st.deg u) ∧ (st'.par cur = 0 ∧ ∀ (u : Fin n), u ≠ cur → st'.par u = st.par u) ∧ (∀ (u : Fin n), u ≠ p → st'.child u = st.child u) ∧ (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_c : Fin n) (rest : List (Fin n)), st'.child p = ↑r_c + 1 ∧ IsCircList st'.left st'.right (r_c :: rest) ∧ (r_c :: rest).Perm ((h :: tail).erase cur)) ∧ IsCircList st'.left st'.right (m :: cur :: rtail) ∧ ∀ (u : Fin n), st.par u ≠ ↑p + 1 → st.par u ≠ 0 → st'.left u = st.left u ∧ st'.right u = st.right u

Raw machine specification of cutNodeCode: cuts cur (zReg) from p (pReg) and splices cur after m (minRootReg = m.val + 1) in at most 36 instructions.

Forest-level cut transition (cutNode_forest)

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.cutNode_forest {n K_max base w : ℕ} {s' : Lean.IndexedMinPQ.State n} {x : WordRAM.Data rFib} (hb : WordRAM.Data.Bounded w x) (hbr : BaseRegs n base x) {cur p v m : Fin n} {pending : Option (Fin n)} {st_pre : RawState n} {ts : List (FHTree n)} {rtail : List (Fin n)} (hz_reg : x.regs zReg = ↑cur) (hp_reg : x.regs pReg = ↑p) (hpend : pending = none ∨ pending = some cur) (hst_agree : have st := RawState.ofData n base x; st.par = st_pre.par ∧ st.child = st_pre.child ∧ st.left = st_pre.left ∧ st.right = st_pre.right ∧ st.deg = st_pre.deg ∧ st.mark = st_pre.mark ∧ st.inHeap = st_pre.inHeap ∧ st.key cur ≤ st_pre.key cur ∧ ∀ (u : Fin n), u ≠ cur → st.key u = st_pre.key u) (hts : ∀ T ∈ ts, ValidRoot st_pre pending T) (hnd : (forestNodes ts).Nodup) (hdom : ∀ (u : Fin n), u ∈ forestNodes ts ↔ (s' u).isSome = true) (hin : ∀ (u : Fin n), ((RawState.ofData n base x).inHeap u ≠ 0 ↔ (s' u).isSome = true) ∧ (RawState.ofData n base x).inHeap u ≤ 1) (hkeys : ∀ (u : Fin n) (ku : ℕ), s' u = some ku → (RawState.ofData n base x).key u = ku ∧ ku ≤ K_max) (hsz : (RawState.ofData n base x).sz = (Lean.IndexedMinPQ.dom s').card) (hnr : (RawState.ofData n base x).numRoots = ts.length) (hnm : (RawState.ofData n base x).numMarked = markedCount (RawState.ofData n base x)) (hcons : ∀ d ≤ n, (RawState.ofData n base x).cons d = 0) (hmin : (RawState.ofData n base x).minRoot = ↑m + 1) (hcirc_r : IsCircList (RawState.ofData n base x).left (RawState.ofData n base x).right (m :: rtail)) (hperm_r : (m :: rtail).Perm (List.map FHTree.root ts)) (hmin_other : ∀ T ∈ ts, T.root ≠ v → Lean.IndexedMinPQ.PrioLE (m, (RawState.ofData n base x).key m) (T.root, (RawState.ofData n base x).key T.root)) (hv_root : cur = v ∨ (RawState.ofData n base x).key cur = st_pre.key cur ∧ ∃ T_v ∈ ts, T_v.root = v) (hcur_tree_ne_v : ∀ T ∈ ts, cur ∈ T.nodes → T.root ≠ v) (hcur_in_fn : cur ∈ forestNodes ts) (hpar_cur : (RawState.ofData n base x).par cur = ↑p + 1) : ∃ (y : WordRAM.Data rFib), WordRAM.ExecWithin w cutNodeCode x y 36 ∧ WordRAM.Data.Bounded w y ∧ BaseRegs n base y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ (∀ (r : Fin rFib), r ≠ s0 → r ≠ s1 → r ≠ s2 → r ≠ s3 → r ≠ s4 → r ≠ numMarkedReg → r ≠ numRootsReg → y.regs r = x.regs r) ∧ (((RawState.ofData n base x).mark cur ≠ 0 → potential y + unitCredit = potential x) ∧ ((RawState.ofData n base x).mark cur = 0 → potential y = potential x + unitCredit)) ∧ ∃ (ts' : List (FHTree n)), (∀ T ∈ ts', ValidRoot (RawState.ofData n base y) (some p) T) ∧ (forestNodes ts').Nodup ∧ (∀ (u : Fin n), u ∈ forestNodes ts' ↔ (s' u).isSome = true) ∧ (RawState.ofData n base y).numRoots = ts'.length ∧ (∃ (rtail' : List (Fin n)), (RawState.ofData n base y).minRoot = ↑m + 1 ∧ IsCircList (RawState.ofData n base y).left (RawState.ofData n base y).right (m :: rtail') ∧ (m :: rtail').Perm (List.map FHTree.root ts')) ∧ (∃ T_v ∈ ts', T_v.root = v) ∧ (∀ T ∈ ts', T.root ≠ v → Lean.IndexedMinPQ.PrioLE (m, (RawState.ofData n base y).key m) (T.root, (RawState.ofData n base y).key T.root)) ∧ (∀ T ∈ ts', p ∈ T.nodes → T.root ≠ v) ∧ CutInv n K_max s' (RawState.ofData n base y) v m (some p)

Unified forest transition for cutNodeCode: given a pre-key-decrease witness st_pre agreeing with st = RawState.ofData n base x everywhere except possibly st.key cur ≤ st_pre.key cur, cutting cur (st.par cur = p.val + 1) establishes CutInv n K_max s' st' v m (some p) and preserves ∀ T ∈ ts', p ∈ T.nodes → T.root ≠ v.

Final minRootReg update tail and decreaseKeyCode_exec

theorem Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.decreaseKeyCode_exec {n K_max w base : ℕ} {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data rFib} (v : Fin n) (k : ℕ) (hinv : FibInv n K_max w base s x) (hval : (∃ (k₀ : ℕ), s v = some k₀ ∧ k ≤ k₀) ∧ k ≤ K_max) (hv_reg : x.regs argV = ↑v) (hk_reg : x.regs argK = k) : ∃ (y : WordRAM.Data rFib) (t : ℕ), WordRAM.ExecWithin w decreaseKeyCode x y t ∧ FibInv n K_max w base (Function.update s v (some k)) y ∧ WordRAM.Modifies { base := base, length := space n }.footprint x.mem y.mem ∧ t + potential y ≤ 330 + potential x

decreaseKeyCode lowers key[v] to k ≤ k₀ (s v = some k₀), performs cascading cuts when parent heap order is violated, updates minRootReg, and restores FibInv in amortized time t + potential y ≤ 330 + potential x.