Chapter 6 - Heapsort

Chapter 6 introduces heaps, the heapsort algorithm, and max-priority queues. The current CLRS-Lean pass has two layers. The compact functional layer remains as a small mathematical scaffold for sortedness and permutation facts. The reader-facing array layer now contains the zero-based CLRS child/parent formulas, an indexed heap predicate, MAX-HEAPIFY's recursive repair theorem, bottom-up BUILD-MAX-HEAP by repeated heapify, the executable in-place HEAPSORT loop with a proved sorted-suffix invariant and sortedness theorem, and the array-level HEAP-MAXIMUM theorem. The heapsort execution also has an erasure-linked unit control-step layer that counts visited MAX-HEAPIFY frames and nontrivial extraction transitions.

Sections

• 6.1 Heaps: proved for the indexed heap predicate and root maximum. Main results: CLRS.Chapter06.parent_lt_self, CLRS.Chapter06.eq_left_or_right_parent, CLRS.Chapter06.ArrayMaxHeap.getElem_le_root, and CLRS.Chapter06.orderedDesc_arrayMaxHeap; localized predicates: CLRS.Chapter06.ArrayMaxHeapFrom.to_global and CLRS.Chapter06.ArrayMaxHeapExceptFrom.to_global.

• 6.2 Maintaining the heap property: proved for fuelled MAX-HEAPIFY recursive repair. Main results: CLRS.Chapter06.swapAt_perm, CLRS.Chapter06.maxHeapifyFuel_perm, CLRS.Chapter06.maxHeapifyFuel_valAt_of_heapSize_le, and CLRS.Chapter06.arrayMaxHeap_of_except_of_maxChildIndex_self; recursive repair: CLRS.Chapter06.maxHeapifyFuel_child_repair_after_swap, CLRS.Chapter06.maxHeapifyFuel_swap_branch_repair, CLRS.Chapter06.maxHeapifyFuel_repair_subtree and CLRS.Chapter06.maxHeapifyFuel_root_isMaxHeap.

• 6.3 Building a heap: proved for the bottom-up repeated MAX-HEAPIFY builder. Main results: CLRS.Chapter06.ArrayMaxHeapFrom.of_half, CLRS.Chapter06.buildMaxHeapLoop_isMaxHeap, CLRS.Chapter06.buildMaxHeapLoop_perm, CLRS.Chapter06.arrayBuildMaxHeap_isMaxHeap and CLRS.Chapter06.arrayBuildMaxHeap_correct.

• 6.4 The heapsort algorithm: proved for the in-place CLRS loop refinement. Loop facts: CLRS.Chapter06.arrayHeapSortInPlaceLoop_length, CLRS.Chapter06.arrayHeapSortInPlaceLoop_perm, CLRS.Chapter06.arrayHeapSortInPlace_length, and CLRS.Chapter06.arrayHeapSortInPlace_perm; invariant facts: CLRS.Chapter06.HeapSortLoopInvariant.initial, CLRS.Chapter06.arrayHeapSortStep_suffix_head_eq_root, CLRS.Chapter06.arrayHeapSortStep_suffix_head_bounds_prefix, CLRS.Chapter06.HeapSortLoopInvariant.step, CLRS.Chapter06.arrayHeapSortStep_state_correct, CLRS.Chapter06.arrayHeapSortInPlaceLoop_exact_shrink_invariant, CLRS.Chapter06.arrayHeapSortInPlaceLoop_exact_terminal_invariant, CLRS.Chapter06.arrayHeapSortInPlaceLoop_terminal_invariant, and CLRS.Chapter06.arrayHeapSortInPlaceLoop_orderedAsc; state package: CLRS.Chapter06.arrayHeapSortInPlaceLoop_state_correct and CLRS.Chapter06.arrayHeapSortInPlaceLoop_exact_state_correct. Main specification results: CLRS.Chapter06.arrayHeapSortInPlace_terminal_invariant, CLRS.Chapter06.arrayHeapSortInPlace_orderedAsc, CLRS.Chapter06.arrayHeapSortInPlace_state_correct, CLRS.Chapter06.arrayHeapSortInPlace_exact_state_correct, CLRS.Chapter06.arrayHeapSortInPlace_correct, CLRS.Chapter06.arrayHeapSort_eq_arrayHeapSortInPlace, CLRS.Chapter06.arrayHeapSort_terminal_invariant, CLRS.Chapter06.arrayHeapSort_state_correct, CLRS.Chapter06.arrayHeapSort_exact_state_correct, and CLRS.Chapter06.arrayHeapSort_correct. Costed-execution results (erasure): CLRS.Chapter06.maxHeapifyFuelWithCost_result, CLRS.Chapter06.arrayBuildMaxHeapWithCost_correct, CLRS.Chapter06.arrayHeapSortInPlaceWithCost_correct_and_cost, CLRS.Chapter06.maxHeapifyControlBound_isBigO_n, CLRS.Chapter06.buildMaxHeapControlBound_isBigO_nsq, and CLRS.Chapter06.heapSortControlBound_isBigO_nsq. Tight algorithm-level bounds: CLRS.Chapter06.maxHeapifyFuelWithCost_cost_le_height, CLRS.Chapter06.maxHeapifyFuelWithCost_cost_le_log, CLRS.Chapter06.sum_heapHeight_le, CLRS.Chapter06.buildMaxHeapLoopWithCost_cost_le_linear, CLRS.Chapter06.arrayHeapSortStepWithCost_cost_le_log, CLRS.Chapter06.arrayHeapSortInPlaceLoopWithCost_cost_le_log, CLRS.Chapter06.arrayHeapSortInPlaceWithCost_cost_le_log, and CLRS.Chapter06.arrayHeapSortInPlaceWithCost_correct_and_log_cost; asymptotic wrappers CLRS.Chapter06.maxHeapifyLogBound_isBigO_log, CLRS.Chapter06.buildMaxHeapLinearBound_isBigO_n, and CLRS.Chapter06.heapSortNLogNBound_isBigO_nlogn.

• 6.5 Priority queues: proved for the functional heap interface, with array-level HEAP-MAXIMUM, full fuelled HEAP-INCREASE-KEY, HEAP-EXTRACT-MAX, and HEAP-DELETE state theorems. Main results: CLRS.Chapter06.heapInsert_orderedDesc, CLRS.Chapter06.heapInsert_perm, CLRS.Chapter06.heapIncreaseKey_orderedDesc, and CLRS.Chapter06.heapDelete_orderedDesc; array result: CLRS.Chapter06.arrayHeapMaximum?_max, CLRS.Chapter06.ArrayMaxHeap.set_increased_except_up, CLRS.Chapter06.ArrayMaxHeapExceptUp.bubble_step, CLRS.Chapter06.ArrayMaxHeapExceptUp.bubbleUpFuel_global, CLRS.Chapter06.arrayHeapIncreaseKey?_state_correct, CLRS.Chapter06.arrayHeapIncreaseKeyNoBubble?_state_correct, CLRS.Chapter06.arrayHeapExtractMax?_state_correct, and CLRS.Chapter06.arrayHeapDelete?_state_correct.

Current Gaps

The proved metric is deliberately coarse: build orchestration is free, while visited heapify frames and nontrivial extraction transitions are charged. The tight textbook O(log n) MAX-HEAPIFY, O(n) BUILD-MAX-HEAP, and O(n log n) HEAPSORT bounds are now proved against this metric. The costs of guards and list operations, and an imperative RAM refinement, remain open.