Chapter 7 — Quicksort

Native fourth-edition chapter guide.

Current source

This guide sources fourth-edition §7.1–§7.4 from the native section modules under CLRSLean.FourthEdition.Chapter_07. Declarations retain the CLRS.Chapter07 namespace; the legacy import CLRSLean.Chapter_07 and its Section_07_* modules forward to these sources during the compatibility period.

Chapter 7 now has three compiler-clean proof layers: the functional quicksort correctness spine, a deterministic comparison-count upper bound, and the expected-comparison recurrence with a named closed form and harmonic bounds for the current randomized-quicksort model. The remaining gap is not the recurrence algebra itself, but the lower-level CLRS array refinement and an explicit probability space for random pivot choices.

Sections

• 7.1 Description of quicksort: proved for the current functional-list model, scan-state partition loop, and returned pivot-index wrapper with an explicit adjacent-swap trace. Main results: CLRS.Chapter07.partitionAround_left_eq_filter, CLRS.Chapter07.partitionAround_right_eq_filter, CLRS.Chapter07.partitionAround_correct, CLRS.Chapter07.partitionAround_perm, CLRS.Chapter07.partitionLoop_invariant, CLRS.Chapter07.partitionLoop_correct, CLRS.Chapter07.clrsPartition_correct, CLRS.Chapter07.clrsPartitionArray_correct, CLRS.Chapter07.clrsPartitionArray_correct_with_trace, CLRS.Chapter07.quickSort_perm, CLRS.Chapter07.quickSort_ordered, and CLRS.Chapter07.quickSort_correct.

• 7.2 Performance of quicksort: proved for a deterministic comparison-count quadratic upper bound. Main results: CLRS.Chapter07.partitionAround_length_add, CLRS.Chapter07.quickSortComparisons_quadratic.

• 7.3 Randomized quicksort: proved for the expected-comparison closed form and Θ(n log n) asymptotic bound, including the bridge between the random-permutation probability model and the algebraic closed form. Main results: CLRS.Chapter07.harmonic_succ, CLRS.Chapter07.sum_mul_harmonic_eq, CLRS.Chapter07.sum_expectedComparisons_eq, CLRS.Chapter07.expectedComparisons_closed_form, CLRS.Chapter07.expectedComparisons_recurrence, CLRS.Chapter07.expectedComparisons_telescope, CLRS.Chapter07.expectedComparisons_clrs_harmonic_bound, CLRS.Chapter07.expectedComparisons_harmonic_bound, CLRS.Chapter07.expectedComparisons_quadratic, CLRS.Chapter07.expectedComparisons_monotone, CLRS.Chapter07.expectedComparisons_isBigTheta_nlogn, CLRS.Chapter07.expectedComparisons_succ_add_two, and CLRS.Chapter07.sum_compared_prob_eq_expectedComparisons.

• 7.4 Analysis of quicksort: proved for the expected running time. The section identifies the expected running time with the expected number of comparisons E[X] (each comparison performs O(1) work and dominates all other operations), proves the indicator decomposition E[X] = Σ_{i<j} P[z_i and z_j are compared] = Σ_{i<j} 2/(j-i+1) through CLRS.Chapter07.expectedRunningTime_eq_sum_compared_prob, and closes with CLRS Theorem 7.1: the expected running time is Θ(n log n) (CLRS.Chapter07.expectedRunningTime_isBigTheta_nlogn), with the explicit harmonic upper bound CLRS.Chapter07.expectedRunningTime_le_two_mul.

Current Gaps

• Index-level mutable-array PARTITION loop refinement and RAM cost model.

• Sharp n log n tail bound (Chernoff/Hoeffding) and lower bound (Omega(n log n) for comparison sorting).

The expected-comparison closed form, the Θ(n log n) asymptotic, and the bridge between the random-permutation probability model and the algebraic formula (sum_compared_prob_eq_expectedComparisons) are now proved. The remaining random pivot-choice independence assertion and expectation-of-sum theorem are deferred refinements.

See docs/clrs-fourth-edition-map.csv for the section-level mapping and docs/migrations/clrs4.md for compatibility and deprecation policy.