Chapter 9 - Medians and Order Statistics

Chapter 9 now has four compiler-clean correctness interfaces for selection: a specification selector obtains the zero-based rank by sorting and indexing, a pivot-style quickselect model recursively partitions around the first element, a pivot-parametric deterministic SELECT model abstracts over the pivot rule, and a median-of-medians pivot instance specializes that interface. All public theorem layers prove that any returned value satisfies the usual order-statistic count certificate. Section 9.3 also proves the local five-element median certificate, executable five-element grouping, grouped split-count core, and CLRS-style partition-size bound for the median-of-medians pivot, plus the abstract recurrence induction and concrete linear-bound wrapper used by the textbook linear-time argument.

Sections

• 9.2 Selection by rank: proved for the specification selector and the pivot-style quickselect model. Main results: CLRS.Chapter09.selectByRank?_mem, CLRS.Chapter09.selectByRank?_rankCorrect, and CLRS.Chapter09.selectByRank?_correct; CLRS.Chapter09.quickSelect?_mem, CLRS.Chapter09.quickSelect?_rankCorrect, and CLRS.Chapter09.quickSelect?_correct.

• 9.3 Deterministic selection: proved for a pivot-parametric SELECT interface, a five-element median certificate, executable five-element grouping, grouped split-count bounds, a deterministic median-pivot instance, and a median-of-medians pivot/select wrapper. Main results: CLRS.Chapter09.selectWithPivot?_correct, CLRS.Chapter09.medianOfFive?_certificate, CLRS.Chapter09.fullGroupsOfFive_medianGroupCertificates, CLRS.Chapter09.fullGroupsOfFive_medianPivot_split_counts, CLRS.Chapter09.fullGroupsOfFive_medianPivot_fullInput_split_counts, CLRS.Chapter09.fullGroupsOfFive_medianPivot_partition_size_bound, CLRS.Chapter09.selectRecurrence_linear_step, CLRS.Chapter09.medianOfMediansPivot?_recursive_branch_size_bound, CLRS.Chapter09.medianOfMediansPivot?_low_branch_linear_work_step, CLRS.Chapter09.medianOfMediansPivot?_high_branch_linear_work_step, CLRS.Chapter09.selectRecurrence_linear_induction, CLRS.Chapter09.medianOfMedians_linear_bound, CLRS.Chapter09.clrsSelectRecurrence_linear_bound, CLRS.Chapter09.medianGroupCertificates_selectPivot_split_counts, and CLRS.Chapter09.medianOfMediansPivot?_partition_size_bound, and CLRS.Chapter09.medianOfMediansSelect?_correct.

Current Gaps

• Randomized SELECT and expected running time require a probability model.

• Deterministic linear-time SELECT still needs a concrete executable cost semantics connected to the proved abstract recurrence theorem.