Chapter 19 - Fibonacci Heaps

Chapter 19 starts with a first-pass abstract Fibonacci-heap model. The current Lean surface represents a heap by a finite set of integer keys plus root/mark counters, proves operation-level set specifications and direct membership facts plus direct operation-key corollaries for insertion, extract-min, decrease-key, and deletion, adds old-key preservation corollaries for the set-updating operations and exact failed membership specifications after heap operations, direct failed-membership preservation wrappers, exposes direct operation-result validity wrappers for normalized counters, adds direct minimum membership/lower-bound wrappers plus insert/union/extract-min-remaining/decrease-key/delete minimum direct membership/lower-bound wrappers, direct minimum/extract-min empty-result wrappers, remaining/delete minimum nonempty-result wrappers, and positive/empty-result minimum-after-update specifications plus nonempty-result query wrappers, exposes the standard potential function with zero-initial and nonnegativity facts, and packages a conservative degree-bound wrapper for later subtree-size strengthening, together with a Fibonacci-style lower-bound recurrence, positivity, adjacent monotonicity, monotonicity, and the first exponential growth bridge over even and half indices, plus conditional natural-log degree budget wrappers. The query surface includes empty-result specifications for minimum and extract-min. A second, implementation-facing layer now provides key-carrying heap-ordered forests with marks, executable equal-degree LINK/CONSOLIDATE, a cached minimum, duplicate-safe occurrence paths and zippers, arbitrary-node CUT and CASCADING-CUT, executable extractMin, decreaseKey, and delete, exact multiset representation and a global FH.Valid invariant. The costed layer proves constant amortized decrease-key, logarithmic extract-min/delete, and a genuine trace-level potential telescope for the standard t(H) + 2m(H) potential.

Sections

• 19.1 gives the abstract finite-set model and operation contracts.

• 19.2 implements mergeable-heap operations, including LINK, CONSOLIDATE, and extractMin.

• 19.3 implements handle-directed CUT, CASCADING-CUT, decrease-key, delete, and their amortized costs.

• 19.4 proves Fibonacci subtree-size and logarithmic maximum-degree bounds.

Together these sections are main-proof-complete-for-correctness for the persistent executable model. Main results: CLRS.Chapter19.FibHeap.makeHeap_correct, CLRS.Chapter19.FibHeap.makeHeap_valid, CLRS.Chapter19.FibHeap.makeHeap_minimum_none, CLRS.Chapter19.FibHeap.potential_makeHeap, CLRS.Chapter19.FibHeap.potential_nonneg, CLRS.Chapter19.FibHeap.minimum_correct, CLRS.Chapter19.FibHeap.minimum_mem, CLRS.Chapter19.FibHeap.minimum_le, CLRS.Chapter19.FibHeap.minimum_none_iff, CLRS.Chapter19.FibHeap.minimum_none_of_empty, CLRS.Chapter19.FibHeap.minimum_ne_none_of_nonempty, CLRS.Chapter19.FibHeap.insert_correct, CLRS.Chapter19.FibHeap.insert_valid, CLRS.Chapter19.FibHeap.insert_mem_iff, CLRS.Chapter19.FibHeap.insert_mem_self, CLRS.Chapter19.FibHeap.insert_mem_old, CLRS.Chapter19.FibHeap.insert_not_mem_iff, CLRS.Chapter19.FibHeap.insert_not_mem_of_ne, CLRS.Chapter19.FibHeap.insert_minimum_correct, CLRS.Chapter19.FibHeap.insert_minimum_mem, CLRS.Chapter19.FibHeap.insert_minimum_le_inserted, CLRS.Chapter19.FibHeap.insert_minimum_le_old, CLRS.Chapter19.FibHeap.insert_minimum_none_iff, CLRS.Chapter19.FibHeap.insert_minimum_ne_none, CLRS.Chapter19.FibHeap.union_correct, CLRS.Chapter19.FibHeap.union_valid, CLRS.Chapter19.FibHeap.union_mem_iff, CLRS.Chapter19.FibHeap.union_mem_left, CLRS.Chapter19.FibHeap.union_mem_right, CLRS.Chapter19.FibHeap.union_not_mem_iff, CLRS.Chapter19.FibHeap.union_not_mem_of_not_mem, CLRS.Chapter19.FibHeap.union_minimum_correct, CLRS.Chapter19.FibHeap.union_minimum_mem, CLRS.Chapter19.FibHeap.union_minimum_le_left, CLRS.Chapter19.FibHeap.union_minimum_le_right, CLRS.Chapter19.FibHeap.union_minimum_none_iff, CLRS.Chapter19.FibHeap.union_minimum_none_of_empty, CLRS.Chapter19.FibHeap.union_minimum_ne_none_of_left, CLRS.Chapter19.FibHeap.union_minimum_ne_none_of_right, CLRS.Chapter19.FibHeap.extractMin_correct, CLRS.Chapter19.FibHeap.extractMin_valid, CLRS.Chapter19.FibHeap.extractMin_mem_iff, CLRS.Chapter19.FibHeap.extractMin_not_mem, CLRS.Chapter19.FibHeap.extractMin_mem_of_ne, CLRS.Chapter19.FibHeap.extractMin_not_mem_iff, CLRS.Chapter19.FibHeap.extractMin_not_mem_old, CLRS.Chapter19.FibHeap.extractMin_none_iff, CLRS.Chapter19.FibHeap.extractMin_none_of_empty, CLRS.Chapter19.FibHeap.extractMin_ne_none_of_nonempty, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_correct, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_ne, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_mem, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_le_old, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_none_iff, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_none_of_all_eq, CLRS.Chapter19.FibHeap.extractMin_remaining_minimum_ne_none_of_remaining, CLRS.Chapter19.FibHeap.decreaseKey_correct, CLRS.Chapter19.FibHeap.decreaseKey_valid, CLRS.Chapter19.FibHeap.decreaseKey_mem_iff, CLRS.Chapter19.FibHeap.decreaseKey_mem_new, CLRS.Chapter19.FibHeap.decreaseKey_mem_old, CLRS.Chapter19.FibHeap.decreaseKey_oldKey_mem_iff, CLRS.Chapter19.FibHeap.decreaseKey_oldKey_not_mem_of_ne, CLRS.Chapter19.FibHeap.decreaseKey_not_mem_iff, CLRS.Chapter19.FibHeap.decreaseKey_not_mem_of_ne, CLRS.Chapter19.FibHeap.decreaseKey_minimum_correct, CLRS.Chapter19.FibHeap.decreaseKey_minimum_mem, CLRS.Chapter19.FibHeap.decreaseKey_minimum_le_new, CLRS.Chapter19.FibHeap.decreaseKey_minimum_le_old, CLRS.Chapter19.FibHeap.decreaseKey_minimum_none_iff, CLRS.Chapter19.FibHeap.decreaseKey_minimum_ne_none, CLRS.Chapter19.FibHeap.delete_correct, CLRS.Chapter19.FibHeap.delete_valid, CLRS.Chapter19.FibHeap.delete_mem_iff, CLRS.Chapter19.FibHeap.delete_not_mem, CLRS.Chapter19.FibHeap.delete_mem_of_ne, CLRS.Chapter19.FibHeap.delete_not_mem_iff, CLRS.Chapter19.FibHeap.delete_not_mem_old, CLRS.Chapter19.FibHeap.delete_not_mem_of_eq, CLRS.Chapter19.FibHeap.delete_minimum_correct, CLRS.Chapter19.FibHeap.delete_minimum_ne, CLRS.Chapter19.FibHeap.delete_minimum_mem, CLRS.Chapter19.FibHeap.delete_minimum_le_old, CLRS.Chapter19.FibHeap.delete_minimum_none_iff, CLRS.Chapter19.FibHeap.delete_minimum_none_of_all_eq, CLRS.Chapter19.FibHeap.delete_minimum_ne_none_of_remaining, CLRS.Chapter19.FibHeap.heapPotential_telescope, CLRS.Chapter19.FibHeap.fibLowerBound_step, CLRS.Chapter19.FibHeap.fibLowerBound_pos, CLRS.Chapter19.FibHeap.fibLowerBound_le_succ, CLRS.Chapter19.FibHeap.fibLowerBound_monotone, CLRS.Chapter19.FibHeap.fibLowerBound_add_two_ge_double, CLRS.Chapter19.FibHeap.fibLowerBound_even_lower_bound, CLRS.Chapter19.FibHeap.fibLowerBound_half_lower_bound, CLRS.Chapter19.FibHeap.degreeIndex_half_le_log_card, CLRS.Chapter19.FibHeap.degreeIndex_le_twice_log_card_add_one, and CLRS.Chapter19.FibHeap.degree_bound_log.

The executable forest layer additionally exposes CLRS.Chapter19.FHNode.keyBag, CLRS.Chapter19.FHNode.forestKeyBag, CLRS.Chapter19.FHNode.forestSize, CLRS.Chapter19.FHNode.RootsUnmarked, CLRS.Chapter19.FHNode.consolidateList_keys, CLRS.Chapter19.FHNode.consolidateList_keyBag, CLRS.Chapter19.FHNode.consolidateList_forestSize, CLRS.Chapter19.FHNode.consolidateList_rootsUnmarked, CLRS.Chapter19.FHNode.consolidateList_good, CLRS.Chapter19.FHNode.consolidateList_degreeStrict, CLRS.Chapter19.FH.keyBag, CLRS.Chapter19.FH.Represents, CLRS.Chapter19.FH.Valid, CLRS.Chapter19.FH.makeHeap_valid, CLRS.Chapter19.FH.insert_valid, CLRS.Chapter19.FH.union_valid, CLRS.Chapter19.FH.removeMinRoot, CLRS.Chapter19.FH.removeMinRoot_none_iff, CLRS.Chapter19.FH.removeMinRoot_perm, CLRS.Chapter19.FH.removeMinRoot_min, CLRS.Chapter19.FH.extractMin, CLRS.Chapter19.FH.extractMin_correct, CLRS.Chapter19.FH.extractMin_keyBag, CLRS.Chapter19.FH.extractMin_valid, CLRS.Chapter19.FH.extractMin_degreeStrict, CLRS.Chapter19.FH.extractMin_size, CLRS.Chapter19.FH.extractMin_minimum, CLRS.Chapter19.FH.extractMin_mem_iff_of_ne, CLRS.Chapter19.FH.extractMin_none_iff, CLRS.Chapter19.FH.extractMin_none_iff_size_zero, CLRS.Chapter19.FH.cutChildAt_keys, CLRS.Chapter19.FH.cutChildAt_heapOrdered, CLRS.Chapter19.FH.cutChildAt_wellformed, CLRS.Chapter19.FH.cutRootChildAt_keys, CLRS.Chapter19.FH.cutRootChildAt_size, CLRS.Chapter19.FH.cutRootChildAt_roots_length, CLRS.Chapter19.FH.cutRootChildAt_good, CLRS.Chapter19.FH.potential_makeHeap, CLRS.Chapter19.FH.potential_insert, CLRS.Chapter19.FH.cutRootChildAt_potential_eq, and CLRS.Chapter19.FH.cutRootChildAt_potential_le.

• 19.4 Bounding the maximum degree: partial. A concrete rooted-tree model (FTree) with the CLRS Lemma 19.1 marked-tree invariant (CLRS.Chapter19.FTree.Wellformed), the true subtree-size theorem, its golden-ratio consequence, and the logarithmic maximum-degree bound. Main results: CLRS.Chapter19.FTree.wellformed_size_ge_fibLowerBound, CLRS.Chapter19.FTree.goldenRatio_pow_le_fibLowerBound, CLRS.Chapter19.FTree.wellformed_goldenRatio_pow_le_size, CLRS.Chapter19.FTree.wellformed_degree_le_logb, CLRS.Chapter19.FTree.wellformed_degree_le_floor_logb, CLRS.Chapter19.FTree.wellformed_degree_le_twice_log_two, CLRS.Chapter19.FTree.wellformed_append_child, CLRS.Chapter19.FTree.link_wellformed, and CLRS.Chapter19.FTree.exists_wellformed_size_eq_fibLowerBound.

Current Gaps

A cached minimum pointer, stable node identity/handles for duplicate keys, arbitrary-node paths, cascading cuts, executable decreaseKey/delete, and actual operation-cost accounting remain strengthening targets. Circular pointer lists are a lower-level refinement of the executable persistent forest. Section 19.4 seals the structural combinatorial core: size(x) ≥ F(d+2) ≥ φ^d, hence D(n) ≤ ⌊log_φ n⌋.