CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 9. Medians and Order Statistics

Chapter 9 — Medians and Order Statistics

CLRS, fourth edition · Lean 4 formalization

The proofs below use the models and assumptions described in the scope and implementation notes.

Imports

import Mathlib

9.1. Minimum and Maximum

This section formalizes the pairwise algorithm for finding both extrema of a nonempty list. Each pair is compared internally, then only its smaller member is compared with the running minimum and only its larger member with the running maximum.

Main results:

Theorem minMax?_correct: a successful run returns input members that bound every input element.
Theorem minMax?_comparisons_le: the run performs at most 3 * floor(n / 2) comparisons, the CLRS Section 9.1 bound.

Current gaps:

None for the mathematical comparison-count model. Machine-level instruction and memory costs are outside the Section 9.1 completion boundary.

namespace CLRSnamespace Chapter09

Executable pairwise algorithm

The two extrema returned by the algorithm together with its comparison count.

structure MinMaxResult where
  minimum : Nat
  maximum : Nat
  comparisons : Nat
deriving Repr, DecidableEq

Correctness certificate for a simultaneous minimum/maximum result: both extrema occur in the input and every input value lies between them.

def MinMaxCertificate (xs : List Nat) (result : MinMaxResult) : Prop :=
  result.minimum ∈ xs ∧
    result.maximum ∈ xs ∧
    ∀ x ∈ xs, result.minimum ≤ x ∧ x ≤ result.maximum

Order two values with one comparison, returning the smaller one first.

def orderedPair (x y : Nat) : Nat × Nat :=
  if x ≤ y then (x, y) else (y, x)

The one-comparison result for an input consisting of exactly one pair.

def pairMinMaxResult (x y : Nat) : MinMaxResult :=
  let ordered := orderedPair x y
  ⟨ordered.1, ordered.2, 1⟩

Merge one ordered pair with the extrema of a nonempty recursive suffix. The merge uses three comparisons: one inside the pair and one against each suffix extremum.

def combineMinMax (x y : Nat) (suffix : MinMaxResult) : MinMaxResult :=
  let ordered := orderedPair x y
  ⟨min ordered.1 suffix.minimum,
    max ordered.2 suffix.maximum,
    suffix.comparisons + 3⟩

CLRS pairwise simultaneous minimum/maximum.

The empty input has no extrema, a singleton needs no comparison, an isolated pair needs one comparison, and every pair merged with a nonempty suffix needs three comparisons.

def minMax? : List Nat → Option MinMaxResult
  | [] => none
  | [x] => some ⟨x, x, 0⟩
  | x :: y :: xs =>
      match minMax? xs with
      | none => some (pairMinMaxResult x y)
      | some suffix => some (combineMinMax x y suffix)

Local correctness lemmas

The ordered pair contains exactly its inputs and bounds both of them.

theorem orderedPair_spec (x y : Nat) :
    let ordered := orderedPair x y
    ordered.1 ∈ [x, y] ∧
      ordered.2 ∈ [x, y] ∧
      ordered.1 ≤ x ∧ ordered.1 ≤ y ∧
      x ≤ ordered.2 ∧ y ≤ ordered.2 := by
  simp only [orderedPair]
  split
  · simp_all
  · simp_all
    omega

The base result for one pair has the full extrema certificate.

theorem pairMinMaxResult_correct (x y : Nat) :
    MinMaxCertificate [x, y] (pairMinMaxResult x y) := by
  rcases orderedPair_spec x y with
    ⟨hsmall_mem, hlarge_mem, hsmall_x, hsmall_y, hx_large, hy_large⟩
  refine ⟨?_, ?_, ?_⟩
  · simpa [pairMinMaxResult] using hsmall_mem
  · simpa [pairMinMaxResult] using hlarge_mem
  · intro z hz
    simp at hz
    rcases hz with rfl | rfl
    · simpa [pairMinMaxResult] using And.intro hsmall_x hx_large
    · simpa [pairMinMaxResult] using And.intro hsmall_y hy_large

Merging a pair with certified suffix extrema preserves the certificate.


theorem combineMinMax_correct {xs : List Nat} {suffix : MinMaxResult}
    (hcert : MinMaxCertificate xs suffix) (x y : Nat) :
    MinMaxCertificate (x :: y :: xs) (combineMinMax x y suffix) := by
  rcases hcert with ⟨hsuffix_min_mem, hsuffix_max_mem, hsuffix_bounds⟩
  rcases orderedPair_spec x y with
    ⟨hsmall_mem, hlarge_mem, hsmall_x, hsmall_y, hx_large, hy_large⟩
  have hsmall_mem' : (orderedPair x y).1 = x ∨ (orderedPair x y).1 = y := by
    simpa using hsmall_mem
  have hlarge_mem' : (orderedPair x y).2 = x ∨ (orderedPair x y).2 = y := by
    simpa using hlarge_mem
  have hminimum_mem :
      min (orderedPair x y).1 suffix.minimum ∈ x :: y :: xs := by
    rcases Nat.le_total (orderedPair x y).1 suffix.minimum with hle | hle
    · rw [min_eq_left hle]
      rcases hsmall_mem' with heq | heq <;> simp [heq]
    · rw [min_eq_right hle]
      simp [hsuffix_min_mem]
  have hmaximum_mem :
      max (orderedPair x y).2 suffix.maximum ∈ x :: y :: xs := by
    rcases Nat.le_total (orderedPair x y).2 suffix.maximum with hle | hle
    · rw [max_eq_right hle]
      simp [hsuffix_max_mem]
    · rw [max_eq_left hle]
      rcases hlarge_mem' with heq | heq <;> simp [heq]
  refine ⟨?_, ?_, ?_⟩
  · simpa [combineMinMax] using hminimum_mem
  · simpa [combineMinMax] using hmaximum_mem
  · intro z hz
    simp only [List.mem_cons] at hz
    rcases hz with hzx | hzy | hz
    · subst z
      constructor
      ·
        simpa [combineMinMax] using
          Nat.le_trans (Nat.min_le_left (orderedPair x y).1 suffix.minimum) hsmall_x
      · simpa [combineMinMax] using
          Nat.le_trans hx_large
            (Nat.le_max_left (orderedPair x y).2 suffix.maximum)
    · subst z
      constructor
      ·
        simpa [combineMinMax] using
          Nat.le_trans (Nat.min_le_left (orderedPair x y).1 suffix.minimum) hsmall_y
      · simpa [combineMinMax] using
          Nat.le_trans hy_large
            (Nat.le_max_left (orderedPair x y).2 suffix.maximum)
    · rcases hsuffix_bounds z hz with ⟨hmin_z, hz_max⟩
      constructor
      · simpa [combineMinMax] using
          Nat.le_trans (Nat.min_le_right (orderedPair x y).1 suffix.minimum) hmin_z
      · simpa [combineMinMax] using
          Nat.le_trans hz_max
            (Nat.le_max_right (orderedPair x y).2 suffix.maximum)

Public specification and comparison bound

The pairwise algorithm fails exactly on the empty input.

theorem minMax?_eq_none_iff (xs : List Nat) :
    minMax? xs = none ↔ xs = [] := by
  cases xs with
  | nil => simp [minMax?]
  | cons x xs =>
      cases xs with
      | nil => simp [minMax?]
      | cons y xs =>
          cases hsuffix : minMax? xs <;> simp [minMax?, hsuffix]

The pairwise algorithm succeeds exactly on nonempty inputs.


theorem minMax?_isSome_iff (xs : List Nat) :
    (minMax? xs).isSome ↔ xs ≠ [] := by
  rw [Option.isSome_iff_ne_none]
  simp [minMax?_eq_none_iff]

A successful pairwise run returns the certified extrema of the input.

theorem minMax?_correct {xs : List Nat} {result : MinMaxResult}
    (hrun : minMax? xs = some result) :
    MinMaxCertificate xs result := by
  cases xs with
  | nil => simp [minMax?] at hrun
  | cons x xs =>
      cases xs with
      | nil =>
          simp [minMax?] at hrun
          subst result
          simp [MinMaxCertificate]
      | cons y xs =>
          cases hsuffix : minMax? xs with
          | none =>
              have hxs : xs = [] := (minMax?_eq_none_iff xs).mp hsuffix
              subst xs
              simp [minMax?] at hrun
              subst result
              exact pairMinMaxResult_correct x y
          | some suffix =>
              have hsuffix_cert : MinMaxCertificate xs suffix :=
                minMax?_correct hsuffix
              have hcombined := combineMinMax_correct hsuffix_cert x y
              simp [minMax?, hsuffix] at hrun
              subst result
              exact hcombined
termination_by xs.length
decreasing_by simp_all

The returned minimum is an element of the input.

theorem minMax?_minimum_mem {xs : List Nat} {result : MinMaxResult}
    (hrun : minMax? xs = some result) :
    result.minimum ∈ xs :=
  (minMax?_correct hrun).1

The returned maximum is an element of the input.

theorem minMax?_maximum_mem {xs : List Nat} {result : MinMaxResult}
    (hrun : minMax? xs = some result) :
    result.maximum ∈ xs :=
  (minMax?_correct hrun).2.1

The returned minimum is at most every input element.

theorem minMax?_minimum_le {xs : List Nat} {result : MinMaxResult}
    (hrun : minMax? xs = some result) {x : Nat} (hx : x ∈ xs) :
    result.minimum ≤ x :=
  (minMax?_correct hrun).2.2 x hx |>.1

Every input element is at most the returned maximum.

theorem minMax?_le_maximum {xs : List Nat} {result : MinMaxResult}
    (hrun : minMax? xs = some result) {x : Nat} (hx : x ∈ xs) :
    x ≤ result.maximum :=
  (minMax?_correct hrun).2.2 x hx |>.2

The pairwise algorithm uses at most three comparisons per input pair: comparisons ≤ 3 * floor(xs.length / 2).

theorem minMax?_comparisons_le {xs : List Nat} {result : MinMaxResult}
    (hrun : minMax? xs = some result) :
    result.comparisons ≤ 3 * (xs.length / 2) := by
  cases xs with
  | nil => simp [minMax?] at hrun
  | cons x xs =>
      cases xs with
      | nil =>
          simp [minMax?] at hrun
          subst result
          simp
      | cons y xs =>
          cases hsuffix : minMax? xs with
          | none =>
              have hxs : xs = [] := (minMax?_eq_none_iff xs).mp hsuffix
              subst xs
              simp [minMax?] at hrun
              subst result
              simp [pairMinMaxResult]
          | some suffix =>
              have ih : suffix.comparisons ≤ 3 * (xs.length / 2) :=
                minMax?_comparisons_le hsuffix
              simp [minMax?, hsuffix] at hrun
              subst result
              simp only [combineMinMax, List.length_cons]
              omega
termination_by xs.length
decreasing_by simp_all

end Chapter09end CLRS

Imports

import Mathlib

9.2. Selection in Expected Linear Time

This file gives the first Chapter 9 correctness interface: a selector returns an element with the requested zero-based order statistic. The implementation is the simple specification program obtained by sorting and indexing. The randomized and deterministic linear-time SELECT developments refine this shared rank-certificate interface.

The public certificate is phrased by counts, so duplicates are handled in the usual order-statistic way: if the selected value is x, then at most k elements are strictly smaller than x, and more than k elements are at most x.

Randomized SELECT theorem page

The uniform-pivot recurrence, fresh per-call stochastic execution, and CLRS Theorem 9.2 expected linear comparison bound are proved on the Section 9.2 support page below. It remains directly available without adding another row to the reader sidebar:

Randomized SELECT Expected Time

namespace CLRSnamespace Chapter09

Specification selector and rank certificate

A sorted copy of the input, used as the executable specification.

def sortedCopy (xs : List Nat) : List Nat :=
  xs.mergeSort (fun x y => decide (x ≤ y))

Number of input elements strictly smaller than x.

def ltCount (x : Nat) (xs : List Nat) : Nat :=
  (xs.filter (fun y => decide (y < x))).length

Number of input elements at most x.

def leCount (x : Nat) (xs : List Nat) : Nat :=
  (xs.filter (fun y => decide (y ≤ x))).length

Number of input elements at least x.

def geCount (x : Nat) (xs : List Nat) : Nat :=
  (xs.filter (fun y => decide (x ≤ y))).length

Number of input elements strictly greater than x.

def gtCount (x : Nat) (xs : List Nat) : Nat :=
  (xs.filter (fun y => decide (x < y))).length

Select the zero-based rank k, if the input has that many elements.

def selectByRank? (k : Nat) (xs : List Nat) : Option Nat :=
  (sortedCopy xs)[k]?

Rank certificate for order statistics with duplicates. The selected value x is present in the input, the number of values below it is at most k, and the number of values at most it is greater than k.

def RankCertificate (xs : List Nat) (k x : Nat) : Prop :=
  x ∈ xs ∧ ltCount x xs ≤ k ∧ k < leCount x xs

theorem sortedCopy_perm (xs : List Nat) :
    (sortedCopy xs).Perm xs := by
  simpa [sortedCopy] using
    List.mergeSort_perm xs (fun x y => decide (x ≤ y))

theorem sortedCopy_pairwise (xs : List Nat) :
    (sortedCopy xs).Pairwise (fun x y => x ≤ y) := by
  simpa [sortedCopy] using
    List.pairwise_mergeSort' (r := fun x y : Nat => x ≤ y) xs

List lemmas for the rank proof

              

theorem getElem?_eq_some_iff_split {α : Type u} :
    ∀ {xs : List α} {k : Nat} {x : α},
      xs[k]? = some x ↔
        ∃ lo hi, xs = lo ++ x :: hi ∧ lo.length = k := by
  intro xs k x
  constructor
  · intro h
    induction k generalizing xs with
    | zero =>
        cases xs with
        | nil =>
            simp at h
        | cons y ys =>
            simp at h
            subst y
            exact ⟨[], ys, by simp, rfl⟩
    | succ k ih =>
        cases xs with
        | nil =>
            simp at h
        | cons y ys =>
            simp at h
            rcases ih h with ⟨lo, hi, hys, hlen⟩
            refine ⟨y :: lo, hi, ?_, ?_⟩
            · simp [hys]
            · simp [hlen]
  · rintro ⟨lo, hi, rfl, hlen⟩
    have hget : (lo ++ x :: hi)[lo.length]? = some x := by
      induction lo with
      | nil =>
          simp
      | cons _ lo ih =>
          simp
    rw [← hlen]
    exact hgettheorem pairwise_split_bounds {lo hi : List Nat} {x : Nat}
    (h : (lo ++ x :: hi).Pairwise (fun x y => x ≤ y)) :
    (∀ y ∈ lo, y ≤ x) ∧ (∀ y ∈ hi, x ≤ y) := by
  rcases (List.pairwise_append.mp h) with ⟨_, hxhi, hcross⟩
  constructor
  · intro y hy
    exact hcross y hy x (by simp)
  · cases hxhi with
    | cons hhead _ =>
        intro y hy
        exact hhead y hytheorem ltCount_eq_of_perm {xs ys : List Nat} {x : Nat}
    (h : xs.Perm ys) :
    ltCount x xs = ltCount x ys := by
  unfold ltCount
  exact (h.filter (fun y => decide (y < x))).length_eqtheorem leCount_eq_of_perm {xs ys : List Nat} {x : Nat}
    (h : xs.Perm ys) :
    leCount x xs = leCount x ys := by
  unfold leCount
  exact (h.filter (fun y => decide (y ≤ x))).length_eqtheorem geCount_eq_length_sub_ltCount (x : Nat) :
    ∀ xs : List Nat, geCount x xs = xs.length - ltCount x xs := by
  intro xs
  induction xs with
  | nil =>
      simp [geCount, ltCount]
  | cons y ys ih =>
      unfold geCount ltCount at *
      by_cases hlt : y < x
      · have hnle : ¬ x ≤ y := Nat.not_le_of_gt hlt
        simp [hlt, hnle, ih]
      · have hge : x ≤ y := Nat.le_of_not_gt hlt
        have hfilter_le :
            (ys.filter (fun y => decide (y < x))).length ≤ ys.length :=
          List.length_filter_le (fun y => decide (y < x)) ys
        simp [hlt, hge, ih]
        omegatheorem gtCount_eq_length_sub_leCount (x : Nat) :
    ∀ xs : List Nat, gtCount x xs = xs.length - leCount x xs := by
  intro xs
  induction xs with
  | nil =>
      simp [gtCount, leCount]
  | cons y ys ih =>
      unfold gtCount leCount at *
      by_cases hgt : x < y
      · have hnle : ¬ y ≤ x := Nat.not_le_of_gt hgt
        have hfilter_le :
            (ys.filter (fun y => decide (y ≤ x))).length ≤ ys.length :=
          List.length_filter_le (fun y => decide (y ≤ x)) ys
        simp [hgt, hnle, ih]
        omega
      · have hle : y ≤ x := Nat.le_of_not_gt hgt
        simp [hgt, hle, ih]

theorem leCount_append (x : Nat) (xs ys : List Nat) :
    leCount x (xs ++ ys) = leCount x xs + leCount x ys := by
  unfold leCount
  rw [List.filter_append, List.length_append]

theorem geCount_append (x : Nat) (xs ys : List Nat) :
    geCount x (xs ++ ys) = geCount x xs + geCount x ys := by
  unfold geCount
  rw [List.filter_append, List.length_append]theorem leCount_le_of_sublist {x : Nat} {xs ys : List Nat}
    (hsub : xs.Sublist ys) :
    leCount x xs ≤ leCount x ys := by
  unfold leCount
  exact (hsub.filter (fun y => decide (y ≤ x))).length_letheorem geCount_le_of_sublist {x : Nat} {xs ys : List Nat}
    (hsub : xs.Sublist ys) :
    geCount x xs ≤ geCount x ys := by
  unfold geCount
  exact (hsub.filter (fun y => decide (x ≤ y))).length_letheorem leCount_cons_of_le {x y : Nat} {ys : List Nat} (h : y ≤ x) :
    leCount x (y :: ys) = leCount x ys + 1 := by
  simp [leCount, h, Nat.add_comm]theorem leCount_cons_of_not_le {x y : Nat} {ys : List Nat} (h : ¬ y ≤ x) :
    leCount x (y :: ys) = leCount x ys := by
  simp [leCount, h]theorem geCount_cons_of_le {x y : Nat} {ys : List Nat} (h : x ≤ y) :
    geCount x (y :: ys) = geCount x ys + 1 := by
  simp [geCount, h, Nat.add_comm]theorem geCount_cons_of_not_le {x y : Nat} {ys : List Nat} (h : ¬ x ≤ y) :
    geCount x (y :: ys) = geCount x ys := by
  simp [geCount, h]theorem leCount_mono_of_le {low high : Nat} (h : low ≤ high) :
    ∀ xs : List Nat, leCount low xs ≤ leCount high xs := by
  intro xs
  induction xs with
  | nil =>
      simp [leCount]
  | cons y ys ih =>
      unfold leCount at *
      by_cases hlow : y ≤ low
      · have hhigh : y ≤ high := Nat.le_trans hlow h
        simp [hlow, hhigh, ih]
      · by_cases hhigh : y ≤ high
        · simp [hlow, hhigh]
          exact Nat.le_succ_of_le ih
        · simp [hlow, hhigh, ih]theorem geCount_anti_mono_of_le {low high : Nat} (h : low ≤ high) :
    ∀ xs : List Nat, geCount high xs ≤ geCount low xs := by
  intro xs
  induction xs with
  | nil =>
      simp [geCount]
  | cons y ys ih =>
      unfold geCount at *
      by_cases hhigh : high ≤ y
      · have hlow : low ≤ y := Nat.le_trans h hhigh
        simp [hhigh, hlow, ih]
      · by_cases hlow : low ≤ y
        · simp [hhigh, hlow]
          exact Nat.le_succ_of_le ih
        · simp [hhigh, hlow, ih]

theorem ltCount_le_of_sorted_split {ys lo hi : List Nat} {x : Nat}
    (hsplit : ys = lo ++ x :: hi)
    (_hlo : ∀ y ∈ lo, y ≤ x)
    (hhi : ∀ y ∈ hi, x ≤ y) :
    ltCount x ys ≤ lo.length := by
  subst ys
  unfold ltCount
  have hhi_empty :
      hi.filter (fun y => decide (y < x)) = [] := by
    rw [List.filter_eq_nil_iff]
    intro y hy
    simp [not_lt_of_ge (hhi y hy)]
  have hfilter :
      (lo ++ x :: hi).filter (fun y => decide (y < x)) =
        lo.filter (fun y => decide (y < x)) := by
    rw [List.filter_append]
    simp [hhi_empty]
  rw [hfilter]
  exact List.length_filter_le (fun y => decide (y < x)) lo

theorem lt_length_leCount_of_sorted_split {ys lo hi : List Nat} {x : Nat}
    (hsplit : ys = lo ++ x :: hi)
    (hlo : ∀ y ∈ lo, y ≤ x)
    (_hhi : ∀ y ∈ hi, x ≤ y) :
    lo.length < leCount x ys := by
  subst ys
  unfold leCount
  have hlo_self :
      lo.filter (fun y => decide (y ≤ x)) = lo := by
    rw [List.filter_eq_self]
    intro y hy
    simp [hlo y hy]
  have hfilter :
      (lo ++ x :: hi).filter (fun y => decide (y ≤ x)) =
        lo ++ x :: hi.filter (fun y => decide (y ≤ x)) := by
    rw [List.filter_append]
    simp [hlo_self]
  rw [hfilter]
  simp

Pivot-style selection

Fuelled quickselect over lists of natural numbers.

The first element is used as the pivot. The recursive calls keep only the values strictly below or strictly above the pivot; the middle pivot block is represented by the count interval ltCount pivot xs ≤ k < leCount pivot xs.

def quickSelectFuel? : Nat → Nat → List Nat → Option Nat
  | 0, _, _ => none
  | _ + 1, _, [] => none
  | fuel + 1, k, pivot :: tail =>
      let xs := pivot :: tail
      if k < ltCount pivot xs then
        quickSelectFuel? fuel k (xs.filter fun y => decide (y < pivot))
      else if k < leCount pivot xs then
        some pivot
      else
        quickSelectFuel? fuel (k - leCount pivot xs)
          (xs.filter fun y => decide (pivot < y))

Public quickselect wrapper with exactly one unit of fuel per input element.

def quickSelect? (k : Nat) (xs : List Nat) : Option Nat :=
  quickSelectFuel? xs.length k xs

              

theorem filter_length_lt_of_mem_false {α : Type u}
    (p : α → Bool) {xs : List α} {x : α}
    (hx : x ∈ xs) (hpx : p x = false) :
    (xs.filter p).length < xs.length := by
  have hle : (xs.filter p).length ≤ xs.length := List.length_filter_le p xs
  have hne : (xs.filter p).length ≠ xs.length := by
    intro heq
    have hall := (List.length_filter_eq_length_iff.mp heq) x hx
    rw [hpx] at hall
    contradiction
  exact Nat.lt_of_le_of_ne hle hne

theorem ltCount_filter_lt_eq (xs : List Nat) {x pivot : Nat}
    (hxp : x < pivot) :
    ltCount x xs = ltCount x (xs.filter fun y => decide (y < pivot)) := by
  unfold ltCount
  congr 1
  rw [List.filter_filter]
  apply List.filter_congr
  intro y _hy
  by_cases hyx : y < x
  · simp [hyx, Nat.lt_trans hyx hxp]
  · simp [hyx]

theorem leCount_filter_lt_eq (xs : List Nat) {x pivot : Nat}
    (hxp : x < pivot) :
    leCount x xs = leCount x (xs.filter fun y => decide (y < pivot)) := by
  unfold leCount
  congr 1
  rw [List.filter_filter]
  apply List.filter_congr
  intro y _hy
  by_cases hyx : y ≤ x
  · simp [hyx, Nat.lt_of_le_of_lt hyx hxp]
  · simp [hyx]

theorem ltCount_high_split (xs : List Nat) {pivot x : Nat}
    (hp : pivot < x) :
    leCount pivot xs + ltCount x (xs.filter fun y => decide (pivot < y)) =
      ltCount x xs := by
  unfold ltCount leCount
  induction xs with
  | nil =>
      simp
  | cons y ys ih =>
      have ih' :
          (ys.filter (fun y => decide (y ≤ pivot))).length +
              (ys.filter (fun a => decide (a < x) && decide (pivot < a))).length =
            (ys.filter (fun y => decide (y < x))).length := by
        simpa [List.filter_filter] using ih
      by_cases hyp : y ≤ pivot
      · have hyx : y < x := Nat.lt_of_le_of_lt hyp hp
        have hynot : ¬ pivot < y := not_lt_of_ge hyp
        simp [hyp, hyx, hynot]
        omega
      · have hpy : pivot < y := Nat.lt_of_not_ge hyp
        by_cases hyx : y < x
        · simp [hyp, hpy, hyx]
          omega
        · simp [hyp, hpy, hyx]
          omega

theorem leCount_high_split (xs : List Nat) {pivot x : Nat}
    (hp : pivot < x) :
    leCount pivot xs + leCount x (xs.filter fun y => decide (pivot < y)) =
      leCount x xs := by
  unfold leCount
  induction xs with
  | nil =>
      simp
  | cons y ys ih =>
      have ih' :
          (ys.filter (fun y => decide (y ≤ pivot))).length +
              (ys.filter (fun a => decide (a ≤ x) && decide (pivot < a))).length =
            (ys.filter (fun y => decide (y ≤ x))).length := by
        simpa [List.filter_filter] using ih
      by_cases hyp : y ≤ pivot
      · have hyx : y ≤ x := Nat.le_trans hyp (Nat.le_of_lt hp)
        have hynot : ¬ pivot < y := not_lt_of_ge hyp
        simp [hyp, hyx, hynot]
        omega
      · have hpy : pivot < y := Nat.lt_of_not_ge hyp
        by_cases hyx : y ≤ x
        · simp [hyp, hpy, hyx]
          omega
        · simp [hyp, hpy, hyx]
          omega

theorem rankCertificate_low_lift {xs : List Nat} {pivot k x : Nat}
    (hrank : RankCertificate (xs.filter fun y => decide (y < pivot)) k x) :
    RankCertificate xs k x := by
  have hxmem_low : x ∈ xs.filter fun y => decide (y < pivot) := hrank.1
  have hxmem : x ∈ xs := (List.mem_filter.mp hxmem_low).1
  have hxp : x < pivot := by
    have hxbool := (List.mem_filter.mp hxmem_low).2
    simpa using hxbool
  refine ⟨hxmem, ?_, ?_⟩
  · rw [ltCount_filter_lt_eq xs hxp]
    exact hrank.2.1
  · rw [leCount_filter_lt_eq xs hxp]
    exact hrank.2.2theorem rankCertificate_pivot {xs : List Nat} {pivot k : Nat}
    (hpivot : pivot ∈ xs)
    (hlo : ¬ k < ltCount pivot xs)
    (hle : k < leCount pivot xs) :
    RankCertificate xs k pivot :=
  ⟨hpivot, Nat.le_of_not_gt hlo, hle⟩

theorem rankCertificate_high_lift {xs : List Nat} {pivot k x : Nat}
    (hge : leCount pivot xs ≤ k)
    (hrank :
      RankCertificate (xs.filter fun y => decide (pivot < y))
        (k - leCount pivot xs) x) :
    RankCertificate xs k x := by
  have hxmem_high : x ∈ xs.filter fun y => decide (pivot < y) := hrank.1
  have hxmem : x ∈ xs := (List.mem_filter.mp hxmem_high).1
  have hpx : pivot < x := by
    have hxbool := (List.mem_filter.mp hxmem_high).2
    simpa using hxbool
  refine ⟨hxmem, ?_, ?_⟩
  · have hsplit := ltCount_high_split xs hpx
    have hbound :
        leCount pivot xs +
            ltCount x (xs.filter fun y => decide (pivot < y)) ≤
          leCount pivot xs + (k - leCount pivot xs) :=
      Nat.add_le_add_left hrank.2.1 (leCount pivot xs)
    have hsum : leCount pivot xs + (k - leCount pivot xs) = k :=
      Nat.add_sub_of_le hge
    rw [hsum] at hbound
    rw [← hsplit]
    exact hbound
  · have hsplit := leCount_high_split xs hpx
    have hbound :
        leCount pivot xs + (k - leCount pivot xs) <
          leCount pivot xs +
            leCount x (xs.filter fun y => decide (pivot < y)) :=
      Nat.add_lt_add_left hrank.2.2 (leCount pivot xs)
    have hsum : leCount pivot xs + (k - leCount pivot xs) = k :=
      Nat.add_sub_of_le hge
    rw [hsum, hsplit] at hbound
    exact hbound

theorem quickSelectFuel?_rankCorrect :
    ∀ (fuel k : Nat) (xs : List Nat) {x : Nat}, xs.length ≤ fuel →
      quickSelectFuel? fuel k xs = some x →
        RankCertificate xs k x := by
  intro fuel
  induction fuel with
  | zero =>
      intro k xs selected _hlen hsel
      simp [quickSelectFuel?] at hsel
  | succ fuel ih =>
      intro k xs selected hlen hsel
      cases xs with
      | nil =>
          simp [quickSelectFuel?] at hsel
      | cons pivot tail =>
          let xs : List Nat := pivot :: tail
          have hlow_len :
              (xs.filter fun y => decide (y < pivot)).length ≤ fuel := by
            have hstrict :
                (xs.filter fun y => decide (y < pivot)).length < xs.length :=
              filter_length_lt_of_mem_false (fun y => decide (y < pivot))
                (xs := xs) (x := pivot) (by simp [xs]) (by simp)
            have hlt_fuel : (xs.filter fun y => decide (y < pivot)).length < fuel + 1 :=
              Nat.lt_of_lt_of_le hstrict (by simpa [xs] using hlen)
            exact Nat.lt_succ_iff.mp hlt_fuel
          have hhigh_len :
              (xs.filter fun y => decide (pivot < y)).length ≤ fuel := by
            have hstrict :
                (xs.filter fun y => decide (pivot < y)).length < xs.length :=
              filter_length_lt_of_mem_false (fun y => decide (pivot < y))
                (xs := xs) (x := pivot) (by simp [xs]) (by simp)
            have hlt_fuel : (xs.filter fun y => decide (pivot < y)).length < fuel + 1 :=
              Nat.lt_of_lt_of_le hstrict (by simpa [xs] using hlen)
            exact Nat.lt_succ_iff.mp hlt_fuel
          by_cases hlo : k < ltCount pivot xs
          · have hsel_low :
                quickSelectFuel? fuel k (xs.filter fun y => decide (y < pivot)) =
                  some selected := by
              simpa [quickSelectFuel?, xs, hlo] using hsel
            exact rankCertificate_low_lift (ih k (xs.filter fun y => decide (y < pivot))
              hlow_len hsel_low)
          · by_cases hle : k < leCount pivot xs
            · have hx : selected = pivot := by
                exact Eq.symm (by simpa [quickSelectFuel?, xs, hlo, hle] using hsel)
              subst selected
              exact rankCertificate_pivot (xs := xs) (pivot := pivot)
                (by simp [xs]) hlo hle
            · have hsel_high :
                  quickSelectFuel? fuel (k - leCount pivot xs)
                      (xs.filter fun y => decide (pivot < y)) =
                    some selected := by
                simpa [quickSelectFuel?, xs, hlo, hle] using hsel
              have hge : leCount pivot xs ≤ k := Nat.le_of_not_gt hle
              exact rankCertificate_high_lift hge
                (ih (k - leCount pivot xs)
                  (xs.filter fun y => decide (pivot < y)) hhigh_len hsel_high)

Selection correctness



theorem selectByRank?_rankCorrect {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : selectByRank? k xs = some x) :
    RankCertificate xs k x := by
  unfold selectByRank? at hsel
  rcases (getElem?_eq_some_iff_split.mp hsel) with
    ⟨lo, hi, hsplit, hlen⟩
  have hpair :
      (lo ++ x :: hi).Pairwise (fun x y => x ≤ y) := by
    rw [← hsplit]
    exact sortedCopy_pairwise xs
  rcases pairwise_split_bounds hpair with ⟨hlo, hhi⟩
  have hxSorted : x ∈ sortedCopy xs := by
    rw [hsplit]
    simp
  have hperm : (sortedCopy xs).Perm xs := sortedCopy_perm xs
  refine ⟨(hperm.mem_iff.mp hxSorted), ?_, ?_⟩
  · have hltSorted :
        ltCount x (sortedCopy xs) ≤ lo.length :=
      ltCount_le_of_sorted_split hsplit hlo hhi
    have hltEq : ltCount x (sortedCopy xs) = ltCount x xs :=
      ltCount_eq_of_perm hperm
    rw [← hltEq, ← hlen]
    exact hltSorted
  · have hleSorted :
        lo.length < leCount x (sortedCopy xs) :=
      lt_length_leCount_of_sorted_split hsplit hlo hhi
    have hleEq : leCount x (sortedCopy xs) = leCount x xs :=
      leCount_eq_of_perm hperm
    rw [← hleEq, ← hlen]
    exact hleSorted

theorem selectByRank?_mem {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : selectByRank? k xs = some x) :
    x ∈ xs :=
  (selectByRank?_rankCorrect hsel).1

The specification selector succeeds whenever the requested rank is in range.


theorem selectByRank?_isSome_of_lt {k : Nat} {xs : List Nat}
    (hk : k < xs.length) :
    ∃ x, selectByRank? k xs = some x := by
  unfold selectByRank?
  have hlen : (sortedCopy xs).length = xs.length :=
    (sortedCopy_perm xs).length_eq
  have hk' : k < (sortedCopy xs).length := by
    simpa [hlen] using hk
  exact ⟨(sortedCopy xs)[k], by simp [List.getElem?_eq_getElem hk']⟩

Reader-facing correctness wrapper for the specification selector.

theorem selectByRank?_correct {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : selectByRank? k xs = some x) :
    RankCertificate xs k x :=
  selectByRank?_rankCorrect hsel

theorem quickSelect?_rankCorrect {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : quickSelect? k xs = some x) :
    RankCertificate xs k x := by
  exact quickSelectFuel?_rankCorrect xs.length k xs (Nat.le_refl xs.length) hsel

theorem quickSelect?_mem {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : quickSelect? k xs = some x) :
    x ∈ xs :=
  (quickSelect?_rankCorrect hsel).1

Reader-facing correctness wrapper for the pivot-style quickselect model.

theorem quickSelect?_correct {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : quickSelect? k xs = some x) :
    RankCertificate xs k x :=
  quickSelect?_rankCorrect hsel

end Chapter09end CLRS

Imports

import CLRSLean.FourthEdition.Chapter_09.Section_09_2_Selection_In_Expected_Linear_Time

9.3. Selection in Worst-Case Linear Time

This file factors the Chapter 9 selection proof through a pivot-parametric interface. The key point is pure correctness rather than running time: any pivot rule that returns an element of the current input list yields a selector whose successful result satisfies the same count-based rank certificate used in Section 9.2.

Main results:

selectWithPivot?_correct proves the pivot-parametric rank interface.
fullGroupsOfFive_medianPivot_partition_size_bound proves the CLRS grouped-pivot branch bound.
recursiveMedianOfMediansSelect?_correct proves total rank correctness for the executable recursive selector.
recursiveMedianOfMediansComparisonCost_linear_bound accounts for grouping, nested pivot selection, partitioning, and recursive selection, with total cost at most 100 * xs.length.

Shared source support

The Section 9.2 randomized analysis is stored below this module path so that it can reuse the pivot-parametric infrastructure. It is a support page for 9.2, not an additional subsection of 9.3, and therefore stays outside the sidebar:

Randomized SELECT Expected Time

Completion boundary: the section proves pure functional correctness and a complete CLRS comparison-cost model. In-place array partitioning and hardware-level RAM accounting are lower-level refinements.

namespace CLRSnamespace Chapter09

Pivot-parametric selection

A pivot function is membership-safe when every pivot it returns is an element of the current input list.

def PivotMembership (choosePivot? : List Nat → Option Nat) : Prop :=
  ∀ {xs : List Nat} {pivot : Nat}, choosePivot? xs = some pivot → pivot ∈ xs

A pivot rule is total when it returns a pivot for every nonempty input.

def PivotTotal (choosePivot? : List Nat → Option Nat) : Prop :=
  ∀ {xs : List Nat}, xs ≠ [] → ∃ pivot, choosePivot? xs = some pivot

Fuelled SELECT with an abstract deterministic pivot rule.

The algorithm mirrors the CLRS three-way partition around the chosen pivot: recurse on elements below the pivot, return the pivot block when the requested rank falls inside it, or recurse on elements above the pivot after shifting the rank by the number of elements at most the pivot.

def selectWithPivotFuel? (choosePivot? : List Nat → Option Nat) :
    Nat → Nat → List Nat → Option Nat
  | 0, _, _ => none
  | fuel + 1, k, xs =>
      match choosePivot? xs with
      | none => none
      | some pivot =>
          if k < ltCount pivot xs then
            selectWithPivotFuel? choosePivot? fuel k
              (xs.filter fun y => decide (y < pivot))
          else if k < leCount pivot xs then
            some pivot
          else
            selectWithPivotFuel? choosePivot? fuel (k - leCount pivot xs)
              (xs.filter fun y => decide (pivot < y))

Public SELECT wrapper using one unit of fuel per input element.

def selectWithPivot? (choosePivot? : List Nat → Option Nat)
    (k : Nat) (xs : List Nat) : Option Nat :=
  selectWithPivotFuel? choosePivot? xs.length k xs

Correctness of the fuelled pivot-parametric SELECT.

If the pivot function is membership-safe and the computation returns x, then x is a valid zero-based order statistic certificate for the original input.


theorem selectWithPivotFuel?_rankCorrect
    (choosePivot? : List Nat → Option Nat)
    (hpivot : PivotMembership choosePivot?) :
    ∀ (fuel k : Nat) (xs : List Nat) {x : Nat}, xs.length ≤ fuel →
      selectWithPivotFuel? choosePivot? fuel k xs = some x →
        RankCertificate xs k x := by
  intro fuel
  induction fuel with
  | zero =>
      intro k xs selected _hlen hsel
      simp [selectWithPivotFuel?] at hsel
  | succ fuel ih =>
      intro k xs selected hlen hsel
      cases hchoose : choosePivot? xs with
      | none =>
          simp [selectWithPivotFuel?, hchoose] at hsel
      | some pivot =>
          have hpivot_mem : pivot ∈ xs := hpivot hchoose
          have hlow_len :
              (xs.filter fun y => decide (y < pivot)).length ≤ fuel := by
            have hstrict :
                (xs.filter fun y => decide (y < pivot)).length < xs.length :=
              filter_length_lt_of_mem_false (fun y => decide (y < pivot))
                (xs := xs) (x := pivot) hpivot_mem (by simp)
            have hlt_fuel :
                (xs.filter fun y => decide (y < pivot)).length < fuel + 1 :=
              Nat.lt_of_lt_of_le hstrict hlen
            exact Nat.lt_succ_iff.mp hlt_fuel
          have hhigh_len :
              (xs.filter fun y => decide (pivot < y)).length ≤ fuel := by
            have hstrict :
                (xs.filter fun y => decide (pivot < y)).length < xs.length :=
              filter_length_lt_of_mem_false (fun y => decide (pivot < y))
                (xs := xs) (x := pivot) hpivot_mem (by simp)
            have hlt_fuel :
                (xs.filter fun y => decide (pivot < y)).length < fuel + 1 :=
              Nat.lt_of_lt_of_le hstrict hlen
            exact Nat.lt_succ_iff.mp hlt_fuel
          by_cases hlo : k < ltCount pivot xs
          · have hsel_low :
                selectWithPivotFuel? choosePivot? fuel k
                    (xs.filter fun y => decide (y < pivot)) =
                  some selected := by
              simpa [selectWithPivotFuel?, hchoose, hlo] using hsel
            exact rankCertificate_low_lift
              (ih k (xs.filter fun y => decide (y < pivot))
                hlow_len hsel_low)
          · by_cases hle : k < leCount pivot xs
            · have hx : selected = pivot := by
                exact Eq.symm
                  (by
                    simpa [selectWithPivotFuel?, hchoose, hlo, hle] using hsel)
              subst selected
              exact rankCertificate_pivot (xs := xs) (pivot := pivot)
                hpivot_mem hlo hle
            · have hsel_high :
                  selectWithPivotFuel? choosePivot? fuel
                      (k - leCount pivot xs)
                      (xs.filter fun y => decide (pivot < y)) =
                    some selected := by
                simpa [selectWithPivotFuel?, hchoose, hlo, hle] using hsel
              have hge : leCount pivot xs ≤ k := Nat.le_of_not_gt hle
              exact rankCertificate_high_lift hge
                (ih (k - leCount pivot xs)
                  (xs.filter fun y => decide (pivot < y))
                  hhigh_len hsel_high)

Rank-correctness theorem for the public pivot-parametric SELECT wrapper.

theorem selectWithPivot?_rankCorrect
    (choosePivot? : List Nat → Option Nat)
    (hpivot : PivotMembership choosePivot?) {k : Nat} {xs : List Nat}
    {x : Nat} (hsel : selectWithPivot? choosePivot? k xs = some x) :
    RankCertificate xs k x := by
  exact selectWithPivotFuel?_rankCorrect choosePivot? hpivot xs.length k xs
    (Nat.le_refl xs.length) hsel

Membership projection for pivot-parametric SELECT.

theorem selectWithPivot?_mem
    (choosePivot? : List Nat → Option Nat)
    (hpivot : PivotMembership choosePivot?) {k : Nat} {xs : List Nat}
    {x : Nat} (hsel : selectWithPivot? choosePivot? k xs = some x) :
    x ∈ xs :=
  (selectWithPivot?_rankCorrect choosePivot? hpivot hsel).1

Reader-facing correctness wrapper for pivot-parametric SELECT.

theorem selectWithPivot?_correct
    (choosePivot? : List Nat → Option Nat)
    (hpivot : PivotMembership choosePivot?) {k : Nat} {xs : List Nat}
    {x : Nat} (hsel : selectWithPivot? choosePivot? k xs = some x) :
    RankCertificate xs k x :=
  selectWithPivot?_rankCorrect choosePivot? hpivot hsel

A membership-safe, total pivot rule makes the fuelled selector succeed for every in-range rank. This is the termination half of total correctness; the returned value's rank certificate is supplied by selectWithPivotFuel?_rankCorrect.


theorem selectWithPivotFuel?_isSome_of_lt
    (choosePivot? : List Nat → Option Nat)
    (hpivot : PivotMembership choosePivot?)
    (htotal : PivotTotal choosePivot?) :
    ∀ (fuel k : Nat) (xs : List Nat), xs.length ≤ fuel → k < xs.length →
      ∃ x, selectWithPivotFuel? choosePivot? fuel k xs = some x := by
  intro fuel
  induction fuel with
  | zero =>
      intro k xs hlen hk
      omega
  | succ fuel ih =>
      intro k xs hlen hk
      have hxs : xs ≠ [] := by
        intro hnil
        subst xs
        simp at hk
      rcases htotal hxs with ⟨pivot, hchoose⟩
      have hpivot_mem : pivot ∈ xs := hpivot hchoose
      have hlow_len :
          (xs.filter fun y => decide (y < pivot)).length ≤ fuel := by
        have hstrict :
            (xs.filter fun y => decide (y < pivot)).length < xs.length :=
          filter_length_lt_of_mem_false (fun y => decide (y < pivot))
            hpivot_mem (by simp)
        exact Nat.lt_succ_iff.mp (Nat.lt_of_lt_of_le hstrict hlen)
      have hhigh_len :
          (xs.filter fun y => decide (pivot < y)).length ≤ fuel := by
        have hstrict :
            (xs.filter fun y => decide (pivot < y)).length < xs.length :=
          filter_length_lt_of_mem_false (fun y => decide (pivot < y))
            hpivot_mem (by simp)
        exact Nat.lt_succ_iff.mp (Nat.lt_of_lt_of_le hstrict hlen)
      by_cases hlo : k < ltCount pivot xs
      · have hk_low :
            k < (xs.filter fun y => decide (y < pivot)).length := by
          simpa [ltCount] using hlo
        rcases ih k (xs.filter fun y => decide (y < pivot)) hlow_len hk_low with
          ⟨x, hrun⟩
        exact ⟨x, by simp [selectWithPivotFuel?, hchoose, hlo, hrun]⟩
      · by_cases hmid : k < leCount pivot xs
        · exact ⟨pivot, by simp [selectWithPivotFuel?, hchoose, hlo, hmid]⟩
        · have hge : leCount pivot xs ≤ k := Nat.le_of_not_gt hmid
          have hk_high :
              k - leCount pivot xs <
                (xs.filter fun y => decide (pivot < y)).length := by
            change k - leCount pivot xs < gtCount pivot xs
            rw [gtCount_eq_length_sub_leCount]
            omega
          rcases ih (k - leCount pivot xs)
              (xs.filter fun y => decide (pivot < y)) hhigh_len hk_high with
            ⟨x, hrun⟩
          exact ⟨x, by simp [selectWithPivotFuel?, hchoose, hlo, hmid, hrun]⟩

A total safe pivot rule makes public SELECT succeed on every valid rank.

theorem selectWithPivot?_isSome_of_lt
    (choosePivot? : List Nat → Option Nat)
    (hpivot : PivotMembership choosePivot?)
    (htotal : PivotTotal choosePivot?) {k : Nat} {xs : List Nat}
    (hk : k < xs.length) :
    ∃ x, selectWithPivot? choosePivot? k xs = some x := by
  exact selectWithPivotFuel?_isSome_of_lt choosePivot? hpivot htotal
    xs.length k xs (Nat.le_refl xs.length) hk

Five-element median certificate

Correctness-oriented median selector for a five-element group.

def medianOfFive? (xs : List Nat) : Option Nat :=
  selectByRank? 2 xs

Local certificate used by the CLRS median-of-medians split argument.

For a five-element group, the selected median is an input member, at least three group elements are at most it, and at least three group elements are at least it.

def MedianFiveCertificate (xs : List Nat) (median : Nat) : Prop :=
  xs.length = 5 ∧ median ∈ xs ∧ 3 ≤ leCount median xs ∧ 3 ≤ geCount median xs

The rank-2 selector on a five-element group supplies the local 3/3 median certificate needed by the deterministic SELECT split-size proof.


theorem medianOfFive?_certificate {xs : List Nat} {median : Nat}
    (hlen : xs.length = 5) (hsel : medianOfFive? xs = some median) :
    MedianFiveCertificate xs median := by
  have hrank : RankCertificate xs 2 median := by
    exact selectByRank?_rankCorrect (by simpa [medianOfFive?] using hsel)
  refine ⟨hlen, hrank.1, ?_, ?_⟩
  · exact Nat.succ_le_of_lt hrank.2.2
  · have hlt : ltCount median xs ≤ 2 := hrank.2.1
    rw [geCount_eq_length_sub_ltCount, hlen]
    omega

The five-element median selector succeeds on any five-element input.

theorem medianOfFive?_isSome_of_length_eq_five {xs : List Nat}
    (hlen : xs.length = 5) :
    ∃ median, medianOfFive? xs = some median := by
  exact selectByRank?_isSome_of_lt (by simp [hlen])

Certificates pairing each full five-element group with its selected median.

The theorem layer below intentionally does not require the groups to be computed by a particular chunking function. That keeps the split-size argument usable for both executable median-of-medians code and later lower-level array refinements.

def MedianGroupCertificates (groups : List (List Nat)) (medians : List Nat) :
    Prop :=
  groups.length = medians.length ∧
    ∀ {group : List Nat} {median : Nat}, (group, median) ∈ groups.zip medians →
      MedianFiveCertificate group median

Executable five-element grouping

Fuelled grouping into full five-element blocks, dropping any trailing block of fewer than five elements.

The fuel is only a termination device; the public wrapper below uses xs.length, so the function is executable while keeping the proof obligations straightforward.

def fullGroupsOfFiveFuel : Nat → List Nat → List (List Nat)
  | 0, _ => []
  | fuel + 1, a :: b :: c :: d :: e :: rest =>
      [a, b, c, d, e] :: fullGroupsOfFiveFuel fuel rest
  | _ + 1, _ => []

Executable full five-element grouping used by the median-of-medians layer.

def fullGroupsOfFive (xs : List Nat) : List (List Nat) :=
  fullGroupsOfFiveFuel xs.length xs

theorem fullGroupsOfFiveFuel_lengths {fuel : Nat} :
    ∀ {xs group : List Nat}, group ∈ fullGroupsOfFiveFuel fuel xs →
      group.length = 5 := by
  induction fuel with
  | zero =>
      intro xs group hmem
      simp [fullGroupsOfFiveFuel] at hmem
  | succ fuel ih =>
      intro xs group hmem
      cases xs with
      | nil =>
          simp [fullGroupsOfFiveFuel] at hmem
      | cons a xs =>
          cases xs with
          | nil =>
              simp [fullGroupsOfFiveFuel] at hmem
          | cons b xs =>
              cases xs with
              | nil =>
                  simp [fullGroupsOfFiveFuel] at hmem
              | cons c xs =>
                  cases xs with
                  | nil =>
                      simp [fullGroupsOfFiveFuel] at hmem
                  | cons d xs =>
                      cases xs with
                      | nil =>
                          simp [fullGroupsOfFiveFuel] at hmem
                      | cons e rest =>
                          simp [fullGroupsOfFiveFuel] at hmem
                          rcases hmem with rfl | htail
                          · simp
                          · exact ih htail

Every executable full group has length five.

theorem fullGroupsOfFive_lengths {xs group : List Nat}
    (hmem : group ∈ fullGroupsOfFive xs) :
    group.length = 5 :=
  fullGroupsOfFiveFuel_lengths hmem

              theorem fullGroupsOfFiveFuel_length_mul_five_le {fuel : Nat} :
    ∀ xs : List Nat, 5 * (fullGroupsOfFiveFuel fuel xs).length ≤ xs.length := by
  induction fuel with
  | zero =>
      intro xs
      simp [fullGroupsOfFiveFuel]
  | succ fuel ih =>
      intro xs
      cases xs with
      | nil =>
          simp [fullGroupsOfFiveFuel]
      | cons a xs =>
          cases xs with
          | nil =>
              simp [fullGroupsOfFiveFuel]
          | cons b xs =>
              cases xs with
              | nil =>
                  simp [fullGroupsOfFiveFuel]
              | cons c xs =>
                  cases xs with
                  | nil =>
                      simp [fullGroupsOfFiveFuel]
                  | cons d xs =>
                      cases xs with
                      | nil =>
                          simp [fullGroupsOfFiveFuel]
                      | cons e rest =>
                          have htail := ih rest
                          simp [fullGroupsOfFiveFuel]
                          omegatheorem fullGroupsOfFive_length_mul_five_le (xs : List Nat) :
    5 * (fullGroupsOfFive xs).length ≤ xs.length :=
  fullGroupsOfFiveFuel_length_mul_five_le xs

theorem fullGroupsOfFiveFuel_length_near {fuel : Nat} :
    ∀ {xs : List Nat}, xs.length ≤ fuel →
      xs.length ≤ 5 * (fullGroupsOfFiveFuel fuel xs).length + 4 := by
  induction fuel with
  | zero =>
      intro xs hlen
      cases xs with
      | nil =>
          simp [fullGroupsOfFiveFuel]
      | cons x xs =>
          simp at hlen
  | succ fuel ih =>
      intro xs hlen
      cases xs with
      | nil =>
          simp
      | cons a xs =>
          cases xs with
          | nil =>
              simp [fullGroupsOfFiveFuel]
          | cons b xs =>
              cases xs with
              | nil =>
                  simp [fullGroupsOfFiveFuel]
              | cons c xs =>
                  cases xs with
                  | nil =>
                      simp [fullGroupsOfFiveFuel]
                  | cons d xs =>
                      cases xs with
                      | nil =>
                          simp [fullGroupsOfFiveFuel]
                      | cons e rest =>
                          have hrest : rest.length ≤ fuel := by
                            simp at hlen
                            omega
                          have htail := ih hrest
                          simp [fullGroupsOfFiveFuel]
                          omegatheorem fullGroupsOfFive_length_near (xs : List Nat) :
    xs.length ≤ 5 * (fullGroupsOfFive xs).length + 4 :=
  fullGroupsOfFiveFuel_length_near (Nat.le_refl xs.length)theorem fullGroupsOfFiveFuel_flatten_sublist {fuel : Nat} :
    ∀ xs : List Nat, (List.flatten (fullGroupsOfFiveFuel fuel xs)).Sublist xs := by
  induction fuel with
  | zero =>
      intro xs
      simp [fullGroupsOfFiveFuel]
  | succ fuel ih =>
      intro xs
      cases xs with
      | nil =>
          simp [fullGroupsOfFiveFuel]
      | cons a xs =>
          cases xs with
          | nil =>
              simp [fullGroupsOfFiveFuel]
          | cons b xs =>
              cases xs with
              | nil =>
                  simp [fullGroupsOfFiveFuel]
              | cons c xs =>
                  cases xs with
                  | nil =>
                      simp [fullGroupsOfFiveFuel]
                  | cons d xs =>
                      cases xs with
                      | nil =>
                          simp [fullGroupsOfFiveFuel]
                      | cons e rest =>
                          have htail := ih rest
                          simpa [fullGroupsOfFiveFuel] using
                            List.Sublist.cons_cons a
                              (List.Sublist.cons_cons b
                                (List.Sublist.cons_cons c
                                  (List.Sublist.cons_cons d
                                    (List.Sublist.cons_cons e htail))))theorem fullGroupsOfFive_flatten_sublist (xs : List Nat) :
    (List.flatten (fullGroupsOfFive xs)).Sublist xs :=
  fullGroupsOfFiveFuel_flatten_sublist xs

Map the five-element median selector across a list of groups, failing if any group is not a valid five-element median input.

def medianOfFiveGroups? : List (List Nat) → Option (List Nat)
  | [] => some []
  | group :: groups =>
      match medianOfFive? group, medianOfFiveGroups? groups with
      | some median, some medians => some (median :: medians)
      | _, _ => none

If every group has length five, then the executable median-map produces exactly the certificate package required by the grouped split-count theorem.


theorem medianOfFiveGroups?_certificates {groups : List (List Nat)}
    {medians : List Nat}
    (hall : ∀ group ∈ groups, group.length = 5)
    (hsel : medianOfFiveGroups? groups = some medians) :
    MedianGroupCertificates groups medians := by
  induction groups generalizing medians with
  | nil =>
      simp [medianOfFiveGroups?] at hsel
      subst medians
      simp [MedianGroupCertificates]
  | cons group groups ih =>
      cases hhead : medianOfFive? group with
      | none =>
          simp [medianOfFiveGroups?, hhead] at hsel
      | some median =>
          cases htail : medianOfFiveGroups? groups with
          | none =>
              simp [medianOfFiveGroups?, hhead, htail] at hsel
          | some tailMedians =>
              simp [medianOfFiveGroups?, hhead, htail] at hsel
              subst medians
              have hhead_len : group.length = 5 := hall group (by simp)
              have hhead_cert : MedianFiveCertificate group median :=
                medianOfFive?_certificate hhead_len hhead
              have htail_all : ∀ tailGroup ∈ groups, tailGroup.length = 5 := by
                intro tailGroup hmem
                exact hall tailGroup (by simp [hmem])
              have htail_cert :
                  MedianGroupCertificates groups tailMedians :=
                ih htail_all htail
              rcases htail_cert with ⟨htail_len, htail_cert⟩
              refine ⟨by simp [htail_len], ?_⟩
              intro certGroup certMedian hmem
              simp at hmem
              rcases hmem with hhead_pair | htail_mem
              · rcases hhead_pair with ⟨rfl, rfl⟩
                exact hhead_cert
              · exact htail_cert htail_mem

Every median returned by the executable median-map comes from the flattened input groups.


theorem medianOfFiveGroups?_mem_flatten {groups : List (List Nat)}
    {medians : List Nat}
    (hsel : medianOfFiveGroups? groups = some medians) {median : Nat}
    (hmem : median ∈ medians) :
    median ∈ List.flatten groups := by
  induction groups generalizing medians with
  | nil =>
      simp [medianOfFiveGroups?] at hsel
      subst medians
      simp at hmem
  | cons group groups ih =>
      cases hhead : medianOfFive? group with
      | none =>
          simp [medianOfFiveGroups?, hhead] at hsel
      | some headMedian =>
          cases htail : medianOfFiveGroups? groups with
          | none =>
              simp [medianOfFiveGroups?, hhead, htail] at hsel
          | some tailMedians =>
              simp [medianOfFiveGroups?, hhead, htail] at hsel
              subst medians
              simp at hmem
              rcases hmem with hhead_mem | htail_mem
              · subst median
                have hrank : RankCertificate group 2 headMedian := by
                  exact selectByRank?_rankCorrect
                    (by simpa [medianOfFive?] using hhead)
                simp [hrank.1]
              · have htail_flat : median ∈ List.flatten groups :=
                  ih htail htail_mem
                simp [htail_flat]

The executable median-map succeeds when every group has length five.


theorem medianOfFiveGroups?_isSome_of_all_lengths {groups : List (List Nat)}
    (hall : ∀ group ∈ groups, group.length = 5) :
    ∃ medians, medianOfFiveGroups? groups = some medians := by
  induction groups with
  | nil =>
      exact ⟨[], by simp [medianOfFiveGroups?]⟩
  | cons group groups ih =>
      rcases medianOfFive?_isSome_of_length_eq_five
          (hall group (by simp)) with
        ⟨median, hmedian⟩
      have htail_all : ∀ tailGroup ∈ groups, tailGroup.length = 5 := by
        intro tailGroup hmem
        exact hall tailGroup (by simp [hmem])
      rcases ih htail_all with ⟨medians, hmedians⟩
      exact ⟨median :: medians,
        by simp [medianOfFiveGroups?, hmedian, hmedians]⟩

The executable full-grouping plus median-map automatically constructs the abstract grouped certificate layer.

theorem fullGroupsOfFive_medianGroupCertificates {xs medians : List Nat}
    (hsel : medianOfFiveGroups? (fullGroupsOfFive xs) = some medians) :
    MedianGroupCertificates (fullGroupsOfFive xs) medians :=
  medianOfFiveGroups?_certificates
    (fun _ hmem => fullGroupsOfFive_lengths hmem) hsel

The executable median-map always succeeds on the executable full groups.

theorem fullGroupsOfFive_medianOfFiveGroups?_isSome (xs : List Nat) :
    ∃ medians, medianOfFiveGroups? (fullGroupsOfFive xs) = some medians :=
  medianOfFiveGroups?_isSome_of_all_lengths
    (fun _ hmem => fullGroupsOfFive_lengths hmem)

Every certified group whose median is at most pivot contributes at least three original group elements at most pivot.


theorem medianGroupCertificates_leCount_lower_bound {groups : List (List Nat)}
    {medians : List Nat} {pivot : Nat}
    (hcerts : MedianGroupCertificates groups medians) :
    3 * leCount pivot medians ≤ leCount pivot (List.flatten groups) := by
  induction groups generalizing medians with
  | nil =>
      rcases hcerts with ⟨hlen, _hcert⟩
      cases medians with
      | nil =>
          simp [leCount]
      | cons median medians =>
          simp at hlen
  | cons group groups ih =>
      cases medians with
      | nil =>
          rcases hcerts with ⟨hlen, _hcert⟩
          simp at hlen
      | cons median medians =>
          rcases hcerts with ⟨hlen, hcert⟩
          have htail_len : groups.length = medians.length := by
            simpa using hlen
          have hhead_cert : MedianFiveCertificate group median := by
            exact hcert (by simp)
          have htail_cert :
              MedianGroupCertificates groups medians := by
            refine ⟨htail_len, ?_⟩
            intro tailGroup tailMedian hmem
            exact hcert (by simp [hmem])
          have htail_bound :
              3 * leCount pivot medians ≤ leCount pivot (List.flatten groups) :=
            ih htail_cert
          by_cases hmedian : median ≤ pivot
          · have hhead_mono :
                leCount median group ≤ leCount pivot group :=
              leCount_mono_of_le hmedian group
            have hhead_bound : 3 ≤ leCount pivot group :=
              le_trans hhead_cert.2.2.1 hhead_mono
            simp [leCount_append, leCount_cons_of_le hmedian]
            omega
          · simp [leCount_append, leCount_cons_of_not_le hmedian]
            omega

Every certified group whose median is at least pivot contributes at least three original group elements at least pivot.


theorem medianGroupCertificates_geCount_lower_bound {groups : List (List Nat)}
    {medians : List Nat} {pivot : Nat}
    (hcerts : MedianGroupCertificates groups medians) :
    3 * geCount pivot medians ≤ geCount pivot (List.flatten groups) := by
  induction groups generalizing medians with
  | nil =>
      rcases hcerts with ⟨hlen, _hcert⟩
      cases medians with
      | nil =>
          simp [geCount]
      | cons median medians =>
          simp at hlen
  | cons group groups ih =>
      cases medians with
      | nil =>
          rcases hcerts with ⟨hlen, _hcert⟩
          simp at hlen
      | cons median medians =>
          rcases hcerts with ⟨hlen, hcert⟩
          have htail_len : groups.length = medians.length := by
            simpa using hlen
          have hhead_cert : MedianFiveCertificate group median := by
            exact hcert (by simp)
          have htail_cert :
              MedianGroupCertificates groups medians := by
            refine ⟨htail_len, ?_⟩
            intro tailGroup tailMedian hmem
            exact hcert (by simp [hmem])
          have htail_bound :
              3 * geCount pivot medians ≤ geCount pivot (List.flatten groups) :=
            ih htail_cert
          by_cases hmedian : pivot ≤ median
          · have hhead_mono :
                geCount median group ≤ geCount pivot group :=
              geCount_anti_mono_of_le hmedian group
            have hhead_bound : 3 ≤ geCount pivot group :=
              le_trans hhead_cert.2.2.2 hhead_mono
            simp [geCount_append, geCount_cons_of_le hmedian]
            omega
          · simp [geCount_append, geCount_cons_of_not_le hmedian]
            omega

If pivot has rank certificate k among the group medians, then the original grouped values have at least 3 * (k + 1) elements at most the pivot and at least 3 * (medians.length - k) elements at least the pivot.

This is the reusable counting core of the CLRS median-of-medians split-size argument; the executable wrappers below convert it to the familiar 7n/10 + O(1) branch-size bound.


theorem medianGroupCertificates_selectPivot_split_counts
    {groups : List (List Nat)} {medians : List Nat} {pivot k : Nat}
    (hcerts : MedianGroupCertificates groups medians)
    (hrank : RankCertificate medians k pivot) :
    3 * (k + 1) ≤ leCount pivot (List.flatten groups) ∧
      3 * (medians.length - k) ≤ geCount pivot (List.flatten groups) := by
  constructor
  · have hmedian_count : k + 1 ≤ leCount pivot medians :=
      Nat.succ_le_of_lt hrank.2.2
    have hscale :
        3 * (k + 1) ≤ 3 * leCount pivot medians :=
      Nat.mul_le_mul_left 3 hmedian_count
    exact le_trans hscale (medianGroupCertificates_leCount_lower_bound hcerts)
  · have hge_medians : medians.length - k ≤ geCount pivot medians := by
      have hlt_bound : ltCount pivot medians ≤ k := hrank.2.1
      rw [geCount_eq_length_sub_ltCount]
      omega
    have hscale :
        3 * (medians.length - k) ≤ 3 * geCount pivot medians :=
      Nat.mul_le_mul_left 3 hge_medians
    exact le_trans hscale (medianGroupCertificates_geCount_lower_bound hcerts)

Executable-grouping version of the median-of-medians split-count core.

theorem fullGroupsOfFive_selectPivot_split_counts
    {xs medians : List Nat} {pivot k : Nat}
    (hmedians : medianOfFiveGroups? (fullGroupsOfFive xs) = some medians)
    (hrank : RankCertificate medians k pivot) :
    3 * (k + 1) ≤ leCount pivot (List.flatten (fullGroupsOfFive xs)) ∧
      3 * (medians.length - k) ≤
        geCount pivot (List.flatten (fullGroupsOfFive xs)) :=
  medianGroupCertificates_selectPivot_split_counts
    (fullGroupsOfFive_medianGroupCertificates hmedians) hrank

When the pivot is selected as the median of the executable group medians, the flattened full groups inherit the standard three-per-median split counts.

theorem fullGroupsOfFive_medianPivot_split_counts
    {xs medians : List Nat} {pivot : Nat}
    (hmedians : medianOfFiveGroups? (fullGroupsOfFive xs) = some medians)
    (hpivot : selectByRank? (medians.length / 2) medians = some pivot) :
    3 * (medians.length / 2 + 1) ≤
        leCount pivot (List.flatten (fullGroupsOfFive xs)) ∧
      3 * (medians.length - medians.length / 2) ≤
        geCount pivot (List.flatten (fullGroupsOfFive xs)) := by
  exact fullGroupsOfFive_selectPivot_split_counts hmedians
    (selectByRank?_rankCorrect hpivot)

Full-input version of the executable median-of-medians split-count theorem.

The counts first proved on the flattened full groups lift to the original input because that flattening is a sublist of the input. The partition-size wrapper below packages these count lower bounds with the group-count arithmetic above.

theorem fullGroupsOfFive_medianPivot_fullInput_split_counts
    {xs medians : List Nat} {pivot : Nat}
    (hmedians : medianOfFiveGroups? (fullGroupsOfFive xs) = some medians)
    (hpivot : selectByRank? (medians.length / 2) medians = some pivot) :
    3 * (medians.length / 2 + 1) ≤ leCount pivot xs ∧
      3 * (medians.length - medians.length / 2) ≤ geCount pivot xs := by
  have hgrouped := fullGroupsOfFive_medianPivot_split_counts hmedians hpivot
  have hsub : (List.flatten (fullGroupsOfFive xs)).Sublist xs :=
    fullGroupsOfFive_flatten_sublist xs
  constructor
  · exact le_trans hgrouped.1 (leCount_le_of_sublist hsub)
  · exact le_trans hgrouped.2 (geCount_le_of_sublist hsub)

The strict recursive branches around a median-of-medians pivot are bounded by the input length minus the certified opposite-side mass.


theorem fullGroupsOfFive_medianPivot_partition_lengths
    {xs medians : List Nat} {pivot : Nat}
    (hmedians : medianOfFiveGroups? (fullGroupsOfFive xs) = some medians)
    (hpivot : selectByRank? (medians.length / 2) medians = some pivot) :
    ltCount pivot xs ≤
        xs.length - 3 * (medians.length - medians.length / 2) ∧
      gtCount pivot xs ≤ xs.length - 3 * (medians.length / 2 + 1) := by
  have hsplit :=
    fullGroupsOfFive_medianPivot_fullInput_split_counts hmedians hpivot
  have hlt_len : ltCount pivot xs ≤ xs.length := by
    unfold ltCount
    exact List.length_filter_le (fun y => decide (y < pivot)) xs
  have hle_len : leCount pivot xs ≤ xs.length := by
    unfold leCount
    exact List.length_filter_le (fun y => decide (y ≤ pivot)) xs
  constructor
  · rw [geCount_eq_length_sub_ltCount] at hsplit
    omega
  · rw [gtCount_eq_length_sub_leCount]
    omega

CLRS-style partition-size packaging for any rank-correct median of the executable group medians.


theorem fullGroupsOfFive_rankPivot_partition_size_bound
    {xs medians : List Nat} {pivot : Nat}
    (hmedians : medianOfFiveGroups? (fullGroupsOfFive xs) = some medians)
    (hrank : RankCertificate medians (medians.length / 2) pivot) :
    10 * ltCount pivot xs ≤ 7 * xs.length + 12 ∧
      10 * gtCount pivot xs ≤ 7 * xs.length + 12 := by
  have hgrouped := fullGroupsOfFive_selectPivot_split_counts hmedians hrank
  have hsub : (List.flatten (fullGroupsOfFive xs)).Sublist xs :=
    fullGroupsOfFive_flatten_sublist xs
  have hsplit :
      3 * (medians.length / 2 + 1) ≤ leCount pivot xs ∧
        3 * (medians.length - medians.length / 2) ≤ geCount pivot xs :=
    ⟨le_trans hgrouped.1 (leCount_le_of_sublist hsub),
      le_trans hgrouped.2 (geCount_le_of_sublist hsub)⟩
  have hlt_len : ltCount pivot xs ≤ xs.length := by
    unfold ltCount
    exact List.length_filter_le (fun y => decide (y < pivot)) xs
  have hle_len : leCount pivot xs ≤ xs.length := by
    unfold leCount
    exact List.length_filter_le (fun y => decide (y ≤ pivot)) xs
  have hparts :
      ltCount pivot xs ≤
          xs.length - 3 * (medians.length - medians.length / 2) ∧
        gtCount pivot xs ≤ xs.length - 3 * (medians.length / 2 + 1) := by
    constructor
    · rw [geCount_eq_length_sub_ltCount] at hsplit
      omega
    · rw [gtCount_eq_length_sub_leCount]
      omega
  have hcert := fullGroupsOfFive_medianGroupCertificates hmedians
  have hnear : xs.length ≤ 5 * medians.length + 4 := by
    have hbase := fullGroupsOfFive_length_near xs
    simpa [hcert.1] using hbase
  constructor
  · omega
  · omega

CLRS-style partition-size packaging for the sorting-backed median wrapper.

Both strict recursive branches have size at most 7n/10 + O(1), stated without division as 10 * branchSize ≤ 7 * n + 12.

theorem fullGroupsOfFive_medianPivot_partition_size_bound
    {xs medians : List Nat} {pivot : Nat}
    (hmedians : medianOfFiveGroups? (fullGroupsOfFive xs) = some medians)
    (hpivot : selectByRank? (medians.length / 2) medians = some pivot) :
    10 * ltCount pivot xs ≤ 7 * xs.length + 12 ∧
      10 * gtCount pivot xs ≤ 7 * xs.length + 12 :=
  fullGroupsOfFive_rankPivot_partition_size_bound hmedians
    (selectByRank?_rankCorrect hpivot)

Deterministic median-pivot instance

Deterministic pivot rule that chooses the median of the current list according to the specification selector.

This is a correctness-oriented pivot rule. It deliberately separates the rank proof from the harder CLRS median-of-medians running-time argument.

def deterministicPivot? (xs : List Nat) : Option Nat :=
  selectByRank? (xs.length / 2) xs

The deterministic median-pivot rule returns only members of its input.

theorem deterministicPivot?_mem :
    PivotMembership deterministicPivot? := by
  intro xs pivot hsel
  exact selectByRank?_mem (by simpa [deterministicPivot?] using hsel)

The specification-median pivot exists on every nonempty input.


theorem deterministicPivot?_isSome_of_ne_nil :
    PivotTotal deterministicPivot? := by
  intro xs hxs
  apply selectByRank?_isSome_of_lt
  have hpos : 0 < xs.length := by
    cases xs with
    | nil => contradiction
    | cons _ _ => simp
  omega

A specification median leaves at most half of the input on either strict side.


theorem deterministicPivot?_half_partition_size_bound {xs : List Nat}
    {pivot : Nat} (hsel : deterministicPivot? xs = some pivot) :
    2 * ltCount pivot xs ≤ xs.length ∧
      2 * gtCount pivot xs ≤ xs.length := by
  have hrank : RankCertificate xs (xs.length / 2) pivot :=
    selectByRank?_rankCorrect (by simpa [deterministicPivot?] using hsel)
  have hlt : ltCount pivot xs ≤ xs.length / 2 := hrank.2.1
  have hle : xs.length / 2 < leCount pivot xs := hrank.2.2
  have hdiv : 2 * (xs.length / 2) ≤ xs.length := by omega
  constructor
  · exact le_trans (Nat.mul_le_mul_left 2 hlt) hdiv
  · rw [gtCount_eq_length_sub_leCount]
    omega

The specification median also satisfies the looser CLRS 7n/10 + O(1) bound.

theorem deterministicPivot?_partition_size_bound {xs : List Nat}
    {pivot : Nat} (hsel : deterministicPivot? xs = some pivot) :
    10 * ltCount pivot xs ≤ 7 * xs.length + 12 ∧
      10 * gtCount pivot xs ≤ 7 * xs.length + 12 := by
  have hhalf := deterministicPivot?_half_partition_size_bound hsel
  constructor <;> omega

Deterministic SELECT using the specification median as its pivot rule.

def deterministicSelect? (k : Nat) (xs : List Nat) : Option Nat :=
  selectWithPivot? deterministicPivot? k xs

Rank-correctness theorem for deterministic median-pivot SELECT.

theorem deterministicSelect?_rankCorrect {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : deterministicSelect? k xs = some x) :
    RankCertificate xs k x := by
  exact selectWithPivot?_rankCorrect deterministicPivot? deterministicPivot?_mem
    (by simpa [deterministicSelect?] using hsel)

Membership projection for deterministic median-pivot SELECT.

theorem deterministicSelect?_mem {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : deterministicSelect? k xs = some x) :
    x ∈ xs :=
  (deterministicSelect?_rankCorrect hsel).1

Reader-facing correctness wrapper for deterministic median-pivot SELECT.

theorem deterministicSelect?_correct {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : deterministicSelect? k xs = some x) :
    RankCertificate xs k x :=
  deterministicSelect?_rankCorrect hsel

Median-of-medians pivot instance

CLRS-style median-of-medians pivot rule.

For inputs with at least one full five-element group, this chooses the median of the executable group medians. For shorter inputs, it falls back to the specification median pivot so that the pivot-parametric SELECT wrapper remains usable on every nonempty input.

def medianOfMediansPivot? (xs : List Nat) : Option Nat :=
  match medianOfFiveGroups? (fullGroupsOfFive xs) with
  | some (median :: medians) =>
      selectByRank? ((median :: medians).length / 2) (median :: medians)
  | _ => deterministicPivot? xs

Every median-of-medians pivot returned by the wrapper belongs to the input.


theorem medianOfMediansPivot?_mem :
    PivotMembership medianOfMediansPivot? := by
  intro xs pivot hsel
  unfold medianOfMediansPivot? at hsel
  cases hgroups : medianOfFiveGroups? (fullGroupsOfFive xs) with
  | none =>
      exact deterministicPivot?_mem (by simpa [hgroups] using hsel)
  | some medians =>
      cases medians with
      | nil =>
          exact deterministicPivot?_mem (by simpa [hgroups] using hsel)
      | cons median medians =>
          have hpivot_medians :
              pivot ∈ median :: medians :=
            selectByRank?_mem (by simpa [hgroups] using hsel)
          have hpivot_flat :
              pivot ∈ List.flatten (fullGroupsOfFive xs) :=
            medianOfFiveGroups?_mem_flatten hgroups hpivot_medians
          exact (fullGroupsOfFive_flatten_sublist xs).subset hpivot_flat

The median-of-medians pivot wrapper succeeds on every nonempty input.


theorem medianOfMediansPivot?_isSome_of_ne_nil :
    PivotTotal medianOfMediansPivot? := by
  intro xs hxs
  unfold medianOfMediansPivot?
  cases hgroups : medianOfFiveGroups? (fullGroupsOfFive xs) with
  | none =>
      rcases fullGroupsOfFive_medianOfFiveGroups?_isSome xs with
        ⟨medians, hmedians⟩
      rw [hgroups] at hmedians
      contradiction
  | some medians =>
      cases medians with
      | nil =>
          exact deterministicPivot?_isSome_of_ne_nil hxs
      | cons median medians =>
          apply selectByRank?_isSome_of_lt
          simp only [List.length_cons]
          omega

Any pivot returned by the median-of-medians pivot rule satisfies the proved CLRS branch-size bound. The fallback branch can only occur when there are no full five-element groups, hence the input has length at most four.


theorem medianOfMediansPivot?_partition_size_bound {xs : List Nat}
    {pivot : Nat} (hsel : medianOfMediansPivot? xs = some pivot) :
    10 * ltCount pivot xs ≤ 7 * xs.length + 12 ∧
      10 * gtCount pivot xs ≤ 7 * xs.length + 12 := by
  unfold medianOfMediansPivot? at hsel
  cases hgroups : medianOfFiveGroups? (fullGroupsOfFive xs) with
  | none =>
      rcases fullGroupsOfFive_medianOfFiveGroups?_isSome xs with
        ⟨medians, hmedians⟩
      rw [hgroups] at hmedians
      contradiction
  | some medians =>
      cases medians with
      | nil =>
          have hcert :
              MedianGroupCertificates (fullGroupsOfFive xs) [] :=
            fullGroupsOfFive_medianGroupCertificates hgroups
          have hgroups_len : (fullGroupsOfFive xs).length = 0 := by
            simpa using hcert.1
          have hxs_small : xs.length ≤ 4 := by
            have hnear := fullGroupsOfFive_length_near xs
            rw [hgroups_len] at hnear
            omega
          have hlt_len : ltCount pivot xs ≤ xs.length := by
            unfold ltCount
            exact List.length_filter_le (fun y => decide (y < pivot)) xs
          have hgt_len : gtCount pivot xs ≤ xs.length := by
            unfold gtCount
            exact List.length_filter_le (fun y => decide (pivot < y)) xs
          constructor <;> omega
      | cons median medians =>
          exact fullGroupsOfFive_medianPivot_partition_size_bound
            (xs := xs) (medians := median :: medians) (pivot := pivot)
            hgroups (by simpa [hgroups] using hsel)

Recursive median-of-medians pivot

Fuelled recursive median-of-medians pivot construction.

For a nonempty list of full-group medians, the pivot is selected by the same pivot-parametric selector using the previous fuel level as its pivot rule. Thus the group-median subproblem is solved recursively instead of by sorting. The specification median is used only when the fuel is exhausted or there is no full group (the input then has fewer than five elements).

def recursiveMedianOfMediansPivotFuel? : Nat → List Nat → Option Nat
  | 0, xs => deterministicPivot? xs
  | fuel + 1, xs =>
      if xs.length < 50 then
        deterministicPivot? xs
      else
        match medianOfFiveGroups? (fullGroupsOfFive xs) with
        | some (median :: medians) =>
            selectWithPivot? (recursiveMedianOfMediansPivotFuel? fuel)
              ((median :: medians).length / 2) (median :: medians)
        | _ => deterministicPivot? xs

Every fuel level of the recursive pivot construction returns an input member.


theorem recursiveMedianOfMediansPivotFuel?_mem (fuel : Nat) :
    PivotMembership (recursiveMedianOfMediansPivotFuel? fuel) := by
  induction fuel with
  | zero =>
      intro xs pivot hsel
      exact deterministicPivot?_mem
        (by simpa [recursiveMedianOfMediansPivotFuel?] using hsel)
  | succ fuel ih =>
      intro xs pivot hsel
      simp only [recursiveMedianOfMediansPivotFuel?] at hsel
      by_cases hsmall : xs.length < 50
      · exact deterministicPivot?_mem (by simpa [hsmall] using hsel)
      · simp only [hsmall, ↓reduceIte] at hsel
        cases hgroups : medianOfFiveGroups? (fullGroupsOfFive xs) with
        | none =>
            exact deterministicPivot?_mem (by simpa [hgroups] using hsel)
        | some medians =>
            cases medians with
            | nil =>
                exact deterministicPivot?_mem (by simpa [hgroups] using hsel)
            | cons median medians =>
                have hpivot_medians : pivot ∈ median :: medians :=
                  selectWithPivot?_mem
                    (recursiveMedianOfMediansPivotFuel? fuel) ih
                    (by simpa [hgroups] using hsel)
                have hpivot_flat : pivot ∈ List.flatten (fullGroupsOfFive xs) :=
                  medianOfFiveGroups?_mem_flatten hgroups hpivot_medians
                exact (fullGroupsOfFive_flatten_sublist xs).subset hpivot_flat

Every fuel level of the recursive pivot construction succeeds on nonempty input.


theorem recursiveMedianOfMediansPivotFuel?_isSome_of_ne_nil (fuel : Nat) :
    PivotTotal (recursiveMedianOfMediansPivotFuel? fuel) := by
  induction fuel with
  | zero =>
      intro xs hxs
      simpa [recursiveMedianOfMediansPivotFuel?] using
        (deterministicPivot?_isSome_of_ne_nil hxs)
  | succ fuel ih =>
      intro xs hxs
      simp only [recursiveMedianOfMediansPivotFuel?]
      by_cases hsmall : xs.length < 50
      · simpa [hsmall] using deterministicPivot?_isSome_of_ne_nil hxs
      · simp only [hsmall, ↓reduceIte]
        cases hgroups : medianOfFiveGroups? (fullGroupsOfFive xs) with
        | none =>
            rcases fullGroupsOfFive_medianOfFiveGroups?_isSome xs with
              ⟨medians, hmedians⟩
            rw [hgroups] at hmedians
            contradiction
        | some medians =>
            cases medians with
            | nil =>
                exact deterministicPivot?_isSome_of_ne_nil hxs
            | cons median medians =>
                apply selectWithPivot?_isSome_of_lt
                  (recursiveMedianOfMediansPivotFuel? fuel)
                  (recursiveMedianOfMediansPivotFuel?_mem fuel) ih
                simp only [List.length_cons]
                omega

Public recursive pivot with enough fuel for every nested median subproblem.

def recursiveMedianOfMediansPivot? (xs : List Nat) : Option Nat :=
  recursiveMedianOfMediansPivotFuel? xs.length xs

The public recursive median-of-medians pivot always belongs to its input.

theorem recursiveMedianOfMediansPivot?_mem :
    PivotMembership recursiveMedianOfMediansPivot? := by
  intro xs pivot hsel
  exact recursiveMedianOfMediansPivotFuel?_mem xs.length
    (by simpa [recursiveMedianOfMediansPivot?] using hsel)

The public recursive median-of-medians pivot succeeds on nonempty input.

theorem recursiveMedianOfMediansPivot?_isSome_of_ne_nil :
    PivotTotal recursiveMedianOfMediansPivot? := by
  intro xs hxs
  simpa [recursiveMedianOfMediansPivot?] using
    (recursiveMedianOfMediansPivotFuel?_isSome_of_ne_nil xs.length hxs)

Every fuel level of the recursive pivot satisfies the CLRS branch bound.


theorem recursiveMedianOfMediansPivotFuel?_partition_size_bound (fuel : Nat)
    {xs : List Nat} {pivot : Nat}
    (hsel : recursiveMedianOfMediansPivotFuel? fuel xs = some pivot) :
    10 * ltCount pivot xs ≤ 7 * xs.length + 12 ∧
      10 * gtCount pivot xs ≤ 7 * xs.length + 12 := by
  induction fuel with
  | zero =>
      exact deterministicPivot?_partition_size_bound
        (by simpa [recursiveMedianOfMediansPivotFuel?] using hsel)
  | succ fuel ih =>
      simp only [recursiveMedianOfMediansPivotFuel?] at hsel
      by_cases hsmall : xs.length < 50
      · exact deterministicPivot?_partition_size_bound
          (by simpa [hsmall] using hsel)
      · simp only [hsmall, ↓reduceIte] at hsel
        cases hgroups : medianOfFiveGroups? (fullGroupsOfFive xs) with
        | none =>
            exact deterministicPivot?_partition_size_bound
              (by simpa [hgroups] using hsel)
        | some medians =>
            cases medians with
            | nil =>
                exact deterministicPivot?_partition_size_bound
                  (by simpa [hgroups] using hsel)
            | cons median medians =>
                have hrank :
                    RankCertificate (median :: medians)
                      ((median :: medians).length / 2) pivot :=
                  selectWithPivot?_rankCorrect
                    (recursiveMedianOfMediansPivotFuel? fuel)
                    (recursiveMedianOfMediansPivotFuel?_mem fuel)
                    (by simpa [hgroups] using hsel)
                exact fullGroupsOfFive_rankPivot_partition_size_bound
                  hgroups hrank

The public recursively computed pivot satisfies the CLRS strict-branch bound.

theorem recursiveMedianOfMediansPivot?_partition_size_bound {xs : List Nat}
    {pivot : Nat} (hsel : recursiveMedianOfMediansPivot? xs = some pivot) :
    10 * ltCount pivot xs ≤ 7 * xs.length + 12 ∧
      10 * gtCount pivot xs ≤ 7 * xs.length + 12 := by
  exact recursiveMedianOfMediansPivotFuel?_partition_size_bound xs.length
    (by simpa [recursiveMedianOfMediansPivot?] using hsel)

Recurrence-size wrappers

Pure arithmetic substitution step for the median-of-medians recurrence.

If the median subproblem has size at most one fifth of the input, the selected strict branch satisfies the proved 7n/10 + O(1) bound, and the local work plus the additive split slack fits in the remaining tenth, then the two recursive calls plus local work are bounded by the same linear envelope.


theorem selectRecurrence_linear_step
    {n medianBranch strictBranch localWork C : Nat}
    (hmedian : 5 * medianBranch ≤ n)
    (hbranch : 10 * strictBranch ≤ 7 * n + 12)
    (hlocal : 10 * localWork + 12 * C ≤ C * n) :
    C * medianBranch + C * strictBranch + localWork ≤ C * n := by
  have hmedian_scaled : C * (5 * medianBranch) ≤ C * n :=
    Nat.mul_le_mul_left C hmedian
  have hmedian_part : 10 * (C * medianBranch) ≤ 2 * (C * n) := by
    nlinarith
  have hbranch_scaled : C * (10 * strictBranch) ≤ C * (7 * n + 12) :=
    Nat.mul_le_mul_left C hbranch
  have hbranch_part : 10 * (C * strictBranch) ≤ 7 * (C * n) + 12 * C := by
    nlinarith
  have htotal :
      10 * (C * medianBranch + C * strictBranch + localWork) ≤
        10 * (C * n) := by
    nlinarith
  exact Nat.le_of_mul_le_mul_left htotal (by decide : 0 < 10)

The actual strict recursive SELECT branch lists have the CLRS bound.

theorem medianOfMediansPivot?_recursive_branch_size_bound {xs : List Nat}
    {pivot : Nat} (hsel : medianOfMediansPivot? xs = some pivot) :
    10 * (xs.filter fun y => decide (y < pivot)).length ≤
        7 * xs.length + 12 ∧
      10 * (xs.filter fun y => decide (pivot < y)).length ≤
        7 * xs.length + 12 := by
  simpa [ltCount, gtCount] using
    (medianOfMediansPivot?_partition_size_bound hsel)

Linear-work recurrence step for the low recursive branch of median-of-medians SELECT.


theorem medianOfMediansPivot?_low_branch_linear_work_step
    {xs medians : List Nat} {pivot localWork C : Nat}
    (hmedians : medianOfFiveGroups? (fullGroupsOfFive xs) = some medians)
    (hsel : medianOfMediansPivot? xs = some pivot)
    (hlocal : 10 * localWork + 12 * C ≤ C * xs.length) :
    C * medians.length +
        C * (xs.filter fun y => decide (y < pivot)).length + localWork ≤
      C * xs.length := by
  have hmedian_size : 5 * medians.length ≤ xs.length := by
    have hgroups_size := fullGroupsOfFive_length_mul_five_le xs
    have hcert := fullGroupsOfFive_medianGroupCertificates hmedians
    simpa [hcert.1] using hgroups_size
  exact selectRecurrence_linear_step hmedian_size
    (medianOfMediansPivot?_recursive_branch_size_bound hsel).1 hlocal

Linear-work recurrence step for the high recursive branch of median-of-medians SELECT.


theorem medianOfMediansPivot?_high_branch_linear_work_step
    {xs medians : List Nat} {pivot localWork C : Nat}
    (hmedians : medianOfFiveGroups? (fullGroupsOfFive xs) = some medians)
    (hsel : medianOfMediansPivot? xs = some pivot)
    (hlocal : 10 * localWork + 12 * C ≤ C * xs.length) :
    C * medians.length +
        C * (xs.filter fun y => decide (pivot < y)).length + localWork ≤
      C * xs.length := by
  have hmedian_size : 5 * medians.length ≤ xs.length := by
    have hgroups_size := fullGroupsOfFive_length_mul_five_le xs
    have hcert := fullGroupsOfFive_medianGroupCertificates hmedians
    simpa [hcert.1] using hgroups_size
  exact selectRecurrence_linear_step hmedian_size
    (medianOfMediansPivot?_recursive_branch_size_bound hsel).2 hlocal

Full recurrence induction

Recurrence induction for median-of-medians cost.

Given a cost function T : Nat → Nat, subproblem-size functions g (median subproblem) and h (strict recursive branch), a local-work function f, and a base threshold t, this theorem proves T n ≤ C * n for all n whenever the following hold for all n ≥ t:

The subproblem sizes satisfy the CLRS partition bounds: 5 * g n ≤ n and 10 * h n ≤ 7 * n + 12;
The local work is small enough: 10 * f n + 12 * C ≤ C * n;
T satisfies the one-level recurrence T n ≤ T (g n) + T (h n) + f n;
Base cases n < t respect the linear bound: T n ≤ C * n.

The proof chains selectRecurrence_linear_step through strong induction to lift the single-level substitution to the full recursion tree.

Corresponds to the substitution-method closure in CLRS Section 9.3.


theorem selectRecurrence_linear_induction
    {C t : Nat}
    (ht_bound : 5 ≤ t)
    (f g h : Nat → Nat)
    (hmedian_size : ∀ n, t ≤ n → 5 * g n ≤ n)
    (hstrict_size : ∀ n, t ≤ n → 10 * h n ≤ 7 * n + 12)
    (hlocal_work : ∀ n, t ≤ n → 10 * f n + 12 * C ≤ C * n)
    (T : Nat → Nat)
    (hT_step : ∀ n, t ≤ n → T n ≤ T (g n) + T (h n) + f n)
    (hT_base : ∀ n, n < t → T n ≤ C * n) :
    ∀ n, T n ≤ C * n := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
    by_cases hnt : n < t
    · exact hT_base n hnt
    · have hnt' : t ≤ n := Nat.le_of_not_gt hnt
      have hpos_n : 0 < n := by omega
      have hg_lt : g n < n := by
        have hg_bound := hmedian_size n hnt'
        by_contra! hge
        -- hge : n ≤ g n, so 5*n ≤ 5*g n ≤ n, impossible for n > 0
        have hmul : 5 * n ≤ 5 * g n := Nat.mul_le_mul_left 5 hge
        have hchain : 5 * n ≤ n := le_trans hmul hg_bound
        omega
      have hh_lt : h n < n := by
        have hh_bound := hstrict_size n hnt'
        by_contra! hge
        -- hge : n ≤ h n, so 10*n ≤ 10*h n ≤ 7*n+12, impossible for n ≥ t > 0
        have hmul : 10 * n ≤ 10 * h n := Nat.mul_le_mul_left 10 hge
        have hchain : 10 * n ≤ 7 * n + 12 := le_trans hmul hh_bound
        omega
      have hTg : T (g n) ≤ C * (g n) := ih (g n) hg_lt
      have hTh : T (h n) ≤ C * (h n) := ih (h n) hh_lt
      have hsubst : C * (g n) + C * (h n) + f n ≤ C * n :=
        selectRecurrence_linear_step (hmedian_size n hnt')
          (hstrict_size n hnt') (hlocal_work n hnt')
      have hstep := hT_step n hnt'
      have hsum : T (g n) + T (h n) ≤ C * (g n) + C * (h n) :=
        add_le_add hTg hTh
      have htotal : T (g n) + T (h n) + f n ≤ C * (g n) + C * (h n) + f n :=
        add_le_add hsum (le_refl (f n))
      calc
        T n ≤ T (g n) + T (h n) + f n := hstep
        _ ≤ C * (g n) + C * (h n) + f n := htotal
        _ ≤ C * n := hsubst

Concrete linear bound for the median-of-medians recurrence.

Corollary of selectRecurrence_linear_induction with the standard CLRS subproblem sizes: the median subproblem is ⌊n/5⌋, the strict branch is ⌊(7n+12)/10⌋, and the local work is bounded by a*n where 20*a ≤ C (so that the one-level algebraic slack closes).

The base threshold is 50, which is large enough to absorb the additive constants from the partition bound.


theorem medianOfMedians_linear_bound
    {C a : Nat}
    (hCpos : 0 < C)
    (ha_bound : 20 * a ≤ C)
    (T : Nat → Nat)
    (hT_step : ∀ n, 50 ≤ n →
      T n ≤ T (n / 5) + T ((7 * n + 12) / 10) + a * n)
    (hT_base : ∀ n, n < 50 → T n ≤ C * n) :
    ∀ n, T n ≤ C * n := by
  set g : Nat → Nat := fun n => n / 5
  set h : Nat → Nat := fun n => (7 * n + 12) / 10
  set f : Nat → Nat := fun n => a * n
  have hmedian_size : ∀ n, 50 ≤ n → 5 * g n ≤ n := by
    intro n hn
    unfold g
    exact Nat.mul_div_le n 5
  have hstrict_size : ∀ n, 50 ≤ n → 10 * h n ≤ 7 * n + 12 := by
    intro n hn
    unfold h
    exact Nat.mul_div_le (7 * n + 12) 10
  have hlocal_work : ∀ n, 50 ≤ n → 10 * f n + 12 * C ≤ C * n := by
    intro n hn50
    unfold f
    -- Goal: 10*(a*n) + 12*C ≤ C*n
    -- Scale by 2 to avoid division, then use Nat.le_of_mul_le_mul_left
    have hscale : (10 * (a * n) + 12 * C) * 2 ≤ (C * n) * 2 := by
      calc
        (10 * (a * n) + 12 * C) * 2 = 20 * a * n + 24 * C := by ring
        _ ≤ C * n + 24 * C := by
          have h : 20 * a ≤ C := ha_bound
          nlinarith
        _ ≤ C * n + C * n := by
          have : 24 ≤ n := by omega
          nlinarith
        _ = (C * n) * 2 := by ring
    -- hscale : (stuff)*2 ≤ (other)*2, use right-multiplied form
    have hgoal : 10 * (a * n) + 12 * C ≤ C * n := by
      apply Nat.le_of_mul_le_mul_right (c := 2) ?_ (by omega)
      -- hscale has the terms commuted relative to what the lemma expects
      simpa [mul_comm, mul_left_comm, mul_assoc] using hscale
    exact hgoal
  have hT_step_wrapped : ∀ n, 50 ≤ n → T n ≤ T (g n) + T (h n) + f n := by
    intro n hn50
    unfold g h f
    exact hT_step n hn50
  exact selectRecurrence_linear_induction (by omega) f g h
    hmedian_size hstrict_size hlocal_work T hT_step_wrapped hT_base

CLRS-facing linear-time SELECT recurrence theorem.

If a cost function satisfies the standard median-of-medians recurrence with subproblem sizes ⌊n/5⌋ and ⌊(7n+12)/10⌋, and if the base cases respect the same linear envelope, then the cost is globally linear.

This theorem is intentionally still an abstract recurrence wrapper: connecting the executable medianOfMediansSelect? implementation to a concrete cost function remains a separate refinement target.

theorem clrsSelectRecurrence_linear_bound
    {C a : Nat}
    (hCpos : 0 < C)
    (ha_bound : 20 * a ≤ C)
    (T : Nat → Nat)
    (hT_step : ∀ n, 50 ≤ n →
      T n ≤ T (n / 5) + T ((7 * n + 12) / 10) + a * n)
    (hT_base : ∀ n, n < 50 → T n ≤ C * n) :
    ∀ n, T n ≤ C * n :=
  medianOfMedians_linear_bound hCpos ha_bound T hT_step hT_base

SELECT specialized to the executable median-of-medians pivot rule.

def medianOfMediansSelect? (k : Nat) (xs : List Nat) : Option Nat :=
  selectWithPivot? medianOfMediansPivot? k xs

Median-of-medians SELECT succeeds whenever the requested rank is valid.

theorem medianOfMediansSelect?_isSome_of_lt {k : Nat} {xs : List Nat}
    (hk : k < xs.length) :
    ∃ x, medianOfMediansSelect? k xs = some x := by
  simpa [medianOfMediansSelect?] using
    (selectWithPivot?_isSome_of_lt medianOfMediansPivot?
      medianOfMediansPivot?_mem medianOfMediansPivot?_isSome_of_ne_nil hk)

Rank-correctness theorem for median-of-medians SELECT.

theorem medianOfMediansSelect?_rankCorrect {k : Nat} {xs : List Nat}
    {x : Nat} (hsel : medianOfMediansSelect? k xs = some x) :
    RankCertificate xs k x := by
  exact selectWithPivot?_rankCorrect medianOfMediansPivot?
    medianOfMediansPivot?_mem
    (by simpa [medianOfMediansSelect?] using hsel)

Membership projection for median-of-medians SELECT.

theorem medianOfMediansSelect?_mem {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : medianOfMediansSelect? k xs = some x) :
    x ∈ xs :=
  (medianOfMediansSelect?_rankCorrect hsel).1

Reader-facing correctness wrapper for median-of-medians SELECT.

theorem medianOfMediansSelect?_correct {k : Nat} {xs : List Nat} {x : Nat}
    (hsel : medianOfMediansSelect? k xs = some x) :
    RankCertificate xs k x :=
  medianOfMediansSelect?_rankCorrect hsel

Recursive median-of-medians selector

Executable SELECT whose pivot construction recursively selects the median of the full-group medians.

def recursiveMedianOfMediansSelect? (k : Nat) (xs : List Nat) : Option Nat :=
  selectWithPivot? recursiveMedianOfMediansPivot? k xs

The recursive median-of-medians selector succeeds for every valid rank.

theorem recursiveMedianOfMediansSelect?_isSome_of_lt {k : Nat} {xs : List Nat}
    (hk : k < xs.length) :
    ∃ x, recursiveMedianOfMediansSelect? k xs = some x := by
  simpa [recursiveMedianOfMediansSelect?] using
    (selectWithPivot?_isSome_of_lt recursiveMedianOfMediansPivot?
      recursiveMedianOfMediansPivot?_mem
      recursiveMedianOfMediansPivot?_isSome_of_ne_nil hk)

Successful recursive median-of-medians SELECT runs are rank-correct.

theorem recursiveMedianOfMediansSelect?_correct {k : Nat} {xs : List Nat}
    {x : Nat} (hsel : recursiveMedianOfMediansSelect? k xs = some x) :
    RankCertificate xs k x := by
  exact selectWithPivot?_correct recursiveMedianOfMediansPivot?
    recursiveMedianOfMediansPivot?_mem
    (by simpa [recursiveMedianOfMediansSelect?] using hsel)

Concrete executable cost semantics

This section supplies an executable Nat-valued cost function for the pivot-parametric selector and a proved explicit bound cost n ≤ 17 * n for its outer partition path.

The cost counter selectCostFuel mirrors the recursion of selectWithPivotFuel? exactly: at every recursion level it charges a local work term stepCost xs (for the deterministic instance this is one comparison per element, i.e. the linear partition scan) and then recurses on the single strict branch that selectWithPivotFuel? actually visits. Because SELECT follows only one partition side, the cost is the sum of the local work along one root-to-leaf path of the recursion tree.

The explicit constant 17 comes from the CLRS branch bound 10 * branch ≤ 7 * n + 12: for the substitution guess cost ≤ 17 a n the one-level slack a n + 17 a b ≤ 17 a n reduces to the pure Nat fact 17 b ≤ 16 n, which omega derives from 10 * b ≤ 7 * n + 12 together with the strict-sublist fact b < n.

The pivot-selection work is excluded from this legacy diagnostic counter. The complete composed counter and its linear theorem are recursiveMedianOfMediansComparisonCost and recursiveMedianOfMediansComparisonCost_linear_bound below.

Pure Nat substitution slack for the concrete cost recurrence.

For the substitution guess cost ≤ 17 a n, one recursion level with local work at most a n and strict branch of size b satisfying the CLRS bound 10 b ≤ 7 n + 12 and b < n fits under the same envelope: a n + 17 a b ≤ 17 a n. The core is the pivot-free arithmetic fact 17 b ≤ 16 n, discharged by omega.


theorem selectCost_linear_step {a n b : Nat}
    (hb : 10 * b ≤ 7 * n + 12) (hlt : b < n) :
    a * n + 17 * a * b ≤ 17 * a * n := by
  have h : n + 17 * b ≤ 17 * n := by omega
  calc a * n + 17 * a * b = a * (n + 17 * b) := by ring
    _ ≤ a * (17 * n) := Nat.mul_le_mul (le_refl a) h
    _ = 17 * a * n := by ring

Fuelled cost counter for the pivot-parametric selector.

The recursion is byte-for-byte parallel to selectWithPivotFuel?: it uses the same pivot rule, the same three-way branch conditions, and recurses on the same strict sublist. At each visited level it charges stepCost xs local work; the pivot-block branch stops (charging only the local work) and the two strict branches recurse with one unit of fuel removed.

def selectCostFuel (choosePivot? : List Nat → Option Nat) (stepCost : List Nat → Nat) :
    Nat → Nat → List Nat → Nat
  | 0, _, _ => 0
  | fuel + 1, k, xs =>
      match choosePivot? xs with
      | none => 0
      | some pivot =>
          stepCost xs +
            (if k < ltCount pivot xs then
              selectCostFuel choosePivot? stepCost fuel k
                (xs.filter fun y => decide (y < pivot))
            else if k < leCount pivot xs then
              0
            else
              selectCostFuel choosePivot? stepCost fuel (k - leCount pivot xs)
                (xs.filter fun y => decide (pivot < y)))

Linear bound for the fuelled cost counter.

If the pivot rule is membership-safe, every chosen pivot satisfies the CLRS strict-branch bound 10 * branch ≤ 7 * n + 12, and the local work is linear (stepCost ys ≤ a * ys.length), then the accumulated cost along the recursion path is linear: selectCostFuel … ≤ 17 * a * xs.length.

The proof is strong induction on the fuel, closing each level with selectCost_linear_step.


theorem selectCostFuel_linear_bound
    (choosePivot? : List Nat → Option Nat) (stepCost : List Nat → Nat) {a : Nat}
    (hpivot : PivotMembership choosePivot?)
    (hbound : ∀ (ys : List Nat) (pivot : Nat), choosePivot? ys = some pivot →
      10 * ltCount pivot ys ≤ 7 * ys.length + 12 ∧
      10 * gtCount pivot ys ≤ 7 * ys.length + 12)
    (hstep : ∀ ys : List Nat, stepCost ys ≤ a * ys.length) :
    ∀ (fuel k : Nat) (xs : List Nat), xs.length ≤ fuel →
      selectCostFuel choosePivot? stepCost fuel k xs ≤ 17 * a * xs.length := by
  intro fuel
  induction fuel with
  | zero =>
      intro k xs _hlen
      simp [selectCostFuel]
  | succ fuel ih =>
      intro k xs hlen
      cases hchoose : choosePivot? xs with
      | none =>
          simp [selectCostFuel, hchoose]
      | some pivot =>
          have hmem : pivot ∈ xs := hpivot hchoose
          have hbnd := hbound xs pivot hchoose
          by_cases hlo : k < ltCount pivot xs
          · have hunfold :
                selectCostFuel choosePivot? stepCost (fuel + 1) k xs =
                  stepCost xs +
                    selectCostFuel choosePivot? stepCost fuel k
                      (xs.filter fun y => decide (y < pivot)) := by
              simp [selectCostFuel, hchoose, hlo]
            have hbranch_len_lt :
                (xs.filter fun y => decide (y < pivot)).length < xs.length :=
              filter_length_lt_of_mem_false (fun y => decide (y < pivot))
                hmem (by simp)
            have hbranch_le_fuel :
                (xs.filter fun y => decide (y < pivot)).length ≤ fuel :=
              Nat.lt_succ_iff.mp (Nat.lt_of_lt_of_le hbranch_len_lt hlen)
            have hih := ih k (xs.filter fun y => decide (y < pivot)) hbranch_le_fuel
            have hkey :
                a * xs.length +
                    17 * a * (xs.filter fun y => decide (y < pivot)).length ≤
                  17 * a * xs.length :=
              selectCost_linear_step hbnd.1 hbranch_len_lt
            rw [hunfold]
            exact le_trans (Nat.add_le_add (hstep xs) hih) hkey
          · by_cases hmid : k < leCount pivot xs
            · have hunfold :
                  selectCostFuel choosePivot? stepCost (fuel + 1) k xs =
                    stepCost xs := by
                simp [selectCostFuel, hchoose, hlo, hmid]
              have hmid_bound : a * xs.length ≤ 17 * a * xs.length := by
                have h17 : a ≤ 17 * a := by omega
                exact Nat.mul_le_mul h17 (le_refl xs.length)
              rw [hunfold]
              exact le_trans (hstep xs) hmid_bound
            · have hunfold :
                  selectCostFuel choosePivot? stepCost (fuel + 1) k xs =
                    stepCost xs +
                      selectCostFuel choosePivot? stepCost fuel
                        (k - leCount pivot xs)
                        (xs.filter fun y => decide (pivot < y)) := by
                simp [selectCostFuel, hchoose, hlo, hmid]
              have hbranch_len_lt :
                  (xs.filter fun y => decide (pivot < y)).length < xs.length :=
                filter_length_lt_of_mem_false (fun y => decide (pivot < y))
                  hmem (by simp)
              have hbranch_le_fuel :
                  (xs.filter fun y => decide (pivot < y)).length ≤ fuel :=
                Nat.lt_succ_iff.mp (Nat.lt_of_lt_of_le hbranch_len_lt hlen)
              have hih := ih (k - leCount pivot xs)
                (xs.filter fun y => decide (pivot < y)) hbranch_le_fuel
              have hkey :
                  a * xs.length +
                      17 * a * (xs.filter fun y => decide (pivot < y)).length ≤
                    17 * a * xs.length :=
                selectCost_linear_step hbnd.2 hbranch_len_lt
              rw [hunfold]
              exact le_trans (Nat.add_le_add (hstep xs) hih) hkey

Public cost wrapper: run the fuelled cost counter with one unit of fuel per input element, matching the selectWithPivot? wrapper.

def selectCost (choosePivot? : List Nat → Option Nat) (stepCost : List Nat → Nat)
    (k : Nat) (xs : List Nat) : Nat :=
  selectCostFuel choosePivot? stepCost xs.length k xs

Linear bound for the public cost wrapper, obtained from selectCostFuel_linear_bound with the canonical fuel xs.length.

theorem selectCost_linear_bound
    (choosePivot? : List Nat → Option Nat) (stepCost : List Nat → Nat) {a : Nat}
    (hpivot : PivotMembership choosePivot?)
    (hbound : ∀ (ys : List Nat) (pivot : Nat), choosePivot? ys = some pivot →
      10 * ltCount pivot ys ≤ 7 * ys.length + 12 ∧
      10 * gtCount pivot ys ≤ 7 * ys.length + 12)
    (hstep : ∀ ys : List Nat, stepCost ys ≤ a * ys.length)
    (k : Nat) (xs : List Nat) :
    selectCost choosePivot? stepCost k xs ≤ 17 * a * xs.length :=
  selectCostFuel_linear_bound choosePivot? stepCost hpivot hbound hstep
    xs.length k xs (Nat.le_refl xs.length)

End-to-end recursive median-of-medians comparison cost

Comparison charge for constructing a recursive median-of-medians pivot.

Below the fixed CLRS base threshold, n² comparisons cover a simple local comparison sort. Above the threshold, 2n covers forming and selecting the medians of the full five-element groups (at most ten comparisons per group), and the remaining term is the complete recursive SELECT cost on the list of group medians. Its step charge contains both the partition scan and the next nested pivot construction, so no recursive pivot work is omitted.

def recursiveMedianOfMediansPivotComparisonCostFuel : Nat → List Nat → Nat
  | 0, xs => xs.length * xs.length
  | fuel + 1, xs =>
      if xs.length < 50 then
        xs.length * xs.length
      else
        match medianOfFiveGroups? (fullGroupsOfFive xs) with
        | some (median :: medians) =>
            2 * xs.length +
              selectCost (recursiveMedianOfMediansPivotFuel? fuel)
                (fun ys => ys.length +
                  recursiveMedianOfMediansPivotComparisonCostFuel fuel ys)
                ((median :: medians).length / 2) (median :: medians)
        | _ => xs.length * xs.length

Public pivot-construction comparison charge, using the pivot's canonical fuel.

def recursiveMedianOfMediansPivotComparisonCost (xs : List Nat) : Nat :=
  recursiveMedianOfMediansPivotComparisonCostFuel xs.length xs

End-to-end comparison cost of the executable recursive median-of-medians selector. Every visited SELECT node charges its partition scan plus the full recursive cost of constructing that node's pivot.

def recursiveMedianOfMediansComparisonCost (k : Nat) (xs : List Nat) : Nat :=
  selectCost recursiveMedianOfMediansPivot?
    (fun ys => ys.length + recursiveMedianOfMediansPivotComparisonCost ys) k xs

Arithmetic closure for a recursive (non-base) SELECT node.


private theorem recursiveMedianOfMediansComparisonCost_large_step
    {n medianBranch strictBranch : Nat}
    (hn : 50 ≤ n) (hmedian : 5 * medianBranch ≤ n)
    (hbranch : 10 * strictBranch ≤ 7 * n + 12) :
    n + (2 * n + 100 * medianBranch) + 100 * strictBranch ≤ 100 * n := by
  have hlocal : 10 * (3 * n) + 12 * 100 ≤ 100 * n := by omega
  have h := selectRecurrence_linear_step (C := 100) hmedian hbranch hlocal
  nlinarith

Arithmetic closure for a base-case median SELECT node.

private theorem recursiveMedianOfMediansComparisonCost_small_step
    {n strictBranch : Nat} (hn : n < 50)
    (hbranch : 2 * strictBranch ≤ n) :
    n + n * n + 100 * strictBranch ≤ 100 * n := by
  nlinarith

Linear bound for SELECT using a fixed recursive-pivot fuel. The hypotheses say that both the input and the SELECT recursion fit in their available fuel. This is the strengthened induction needed by the nested median subproblem.


private theorem recursiveMedianOfMediansFixedComparisonCostFuel_linear_bound :
    ∀ n : Nat, ∀ (xs : List Nat) (pivotFuel selectorFuel k : Nat),
      xs.length = n → xs.length ≤ pivotFuel → xs.length ≤ selectorFuel →
        selectCostFuel (recursiveMedianOfMediansPivotFuel? pivotFuel)
          (fun ys => ys.length +
            recursiveMedianOfMediansPivotComparisonCostFuel pivotFuel ys)
          selectorFuel k xs ≤ 100 * xs.length := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs pivotFuel selectorFuel k hlen hpivotFuel hselectorFuel
      cases selectorFuel with
      | zero =>
          simp [selectCostFuel]
      | succ selectorFuel =>
          cases hchoose : recursiveMedianOfMediansPivotFuel? pivotFuel xs with
          | none =>
              simp [selectCostFuel, hchoose]
          | some pivot =>
              have hpivotMem : pivot ∈ xs :=
                recursiveMedianOfMediansPivotFuel?_mem pivotFuel hchoose
              have hpivotBound :=
                recursiveMedianOfMediansPivotFuel?_partition_size_bound
                  pivotFuel hchoose
              have hselectorSucc : n ≤ selectorFuel + 1 := by
                simpa [hlen] using hselectorFuel
              by_cases hsmall : n < 50
              · have hpivotCost :
                    recursiveMedianOfMediansPivotComparisonCostFuel pivotFuel xs =
                      n * n := by
                  cases pivotFuel with
                  | zero =>
                      simp [recursiveMedianOfMediansPivotComparisonCostFuel, hlen]
                  | succ fuel =>
                      simp [recursiveMedianOfMediansPivotComparisonCostFuel,
                        hlen, hsmall]
                have hdet : deterministicPivot? xs = some pivot := by
                  cases pivotFuel with
                  | zero =>
                      simpa [recursiveMedianOfMediansPivotFuel?] using hchoose
                  | succ fuel =>
                      simpa [recursiveMedianOfMediansPivotFuel?, hlen, hsmall]
                        using hchoose
                have hhalf := deterministicPivot?_half_partition_size_bound hdet
                by_cases hlo : k < ltCount pivot xs
                · let low := xs.filter fun y => decide (y < pivot)
                  have hlowLt : low.length < xs.length :=
                    filter_length_lt_of_mem_false
                      (fun y => decide (y < pivot)) hpivotMem (by simp)
                  have hlowLtN : low.length < n := by simpa [hlen] using hlowLt
                  have hlowPivotFuel : low.length ≤ pivotFuel := by
                    omega
                  have hlowSelectorFuel : low.length ≤ selectorFuel := by
                    omega
                  have hih := ih low.length hlowLtN low pivotFuel selectorFuel k
                    rfl hlowPivotFuel hlowSelectorFuel
                  have hclose :
                      n + n * n + 100 * low.length ≤ 100 * n :=
                    recursiveMedianOfMediansComparisonCost_small_step hsmall
                      (by simpa [hlen, low, ltCount] using hhalf.1)
                  simp only [selectCostFuel, hchoose, hlo, if_pos, hpivotCost]
                  calc
                    xs.length + n * n +
                        selectCostFuel
                          (recursiveMedianOfMediansPivotFuel? pivotFuel)
                          (fun ys => ys.length +
                            recursiveMedianOfMediansPivotComparisonCostFuel
                              pivotFuel ys)
                          selectorFuel k
                          (xs.filter fun y => decide (y < pivot))
                        ≤ n + n * n + 100 * low.length := by
                            simpa [hlen, low] using
                              Nat.add_le_add_left hih (n + n * n)
                    _ ≤ 100 * n := hclose
                    _ = 100 * xs.length := by rw [hlen]
                · by_cases hmid : k < leCount pivot xs
                  · simp only [selectCostFuel, hchoose, hlo, hmid, if_false,
                      if_pos, hpivotCost]
                    have hclose : n + n * n ≤ 100 * n := by
                      have := recursiveMedianOfMediansComparisonCost_small_step
                        (strictBranch := 0) hsmall (by omega)
                      simpa using this
                    simpa [hlen] using hclose
                  · let high := xs.filter fun y => decide (pivot < y)
                    have hhighLt : high.length < xs.length :=
                      filter_length_lt_of_mem_false
                        (fun y => decide (pivot < y)) hpivotMem (by simp)
                    have hhighLtN : high.length < n := by
                      simpa [hlen] using hhighLt
                    have hhighPivotFuel : high.length ≤ pivotFuel := by omega
                    have hhighSelectorFuel : high.length ≤ selectorFuel := by omega
                    have hih := ih high.length hhighLtN high pivotFuel selectorFuel
                      (k - leCount pivot xs) rfl hhighPivotFuel hhighSelectorFuel
                    have hclose :
                        n + n * n + 100 * high.length ≤ 100 * n :=
                      recursiveMedianOfMediansComparisonCost_small_step hsmall
                        (by simpa [hlen, high, gtCount] using hhalf.2)
                    simp only [selectCostFuel, hchoose, hlo, hmid, if_false,
                      hpivotCost]
                    calc
                      xs.length + n * n +
                          selectCostFuel
                            (recursiveMedianOfMediansPivotFuel? pivotFuel)
                            (fun ys => ys.length +
                              recursiveMedianOfMediansPivotComparisonCostFuel
                                pivotFuel ys)
                            selectorFuel (k - leCount pivot xs)
                            (xs.filter fun y => decide (pivot < y))
                          ≤ n + n * n + 100 * high.length := by
                              simpa [hlen, high] using
                                Nat.add_le_add_left hih (n + n * n)
                      _ ≤ 100 * n := hclose
                      _ = 100 * xs.length := by rw [hlen]
              · have hnlarge : 50 ≤ n := Nat.le_of_not_gt hsmall
                cases pivotFuel with
                | zero =>
                    have : n = 0 := by omega
                    omega
                | succ fuel =>
                    cases hgroups : medianOfFiveGroups? (fullGroupsOfFive xs) with
                    | none =>
                        rcases fullGroupsOfFive_medianOfFiveGroups?_isSome xs with
                          ⟨medians, hmedians⟩
                        rw [hgroups] at hmedians
                        contradiction
                    | some medians =>
                        cases medians with
                        | nil =>
                            have hcert :
                                MedianGroupCertificates (fullGroupsOfFive xs) [] :=
                              fullGroupsOfFive_medianGroupCertificates hgroups
                            have hgroupsLen : (fullGroupsOfFive xs).length = 0 := by
                              simpa using hcert.1
                            have hnear := fullGroupsOfFive_length_near xs
                            rw [hgroupsLen] at hnear
                            omega
                        | cons median medians =>
                            let ms := median :: medians
                            have hcert :
                                MedianGroupCertificates (fullGroupsOfFive xs) ms :=
                              fullGroupsOfFive_medianGroupCertificates hgroups
                            have hmedianSizeXs : 5 * ms.length ≤ xs.length := by
                              have hgroupsSize :=
                                fullGroupsOfFive_length_mul_five_le xs
                              simpa [hcert.1] using hgroupsSize
                            have hmedianSize : 5 * ms.length ≤ n := by
                              simpa [hlen] using hmedianSizeXs
                            have hmedianLtN : ms.length < n := by omega
                            have hmedianFuel : ms.length ≤ fuel := by omega
                            have hinner := ih ms.length hmedianLtN ms fuel ms.length
                              (ms.length / 2) rfl hmedianFuel (Nat.le_refl ms.length)
                            have hpivotCost :
                                recursiveMedianOfMediansPivotComparisonCostFuel
                                    (fuel + 1) xs ≤
                                  2 * n + 100 * ms.length := by
                              dsimp [ms] at hinner ⊢
                              simp only [recursiveMedianOfMediansPivotComparisonCostFuel,
                                hlen, hsmall, ↓reduceIte, hgroups]
                              simpa [selectCost] using
                                Nat.add_le_add_left hinner (2 * n)
                            by_cases hlo : k < ltCount pivot xs
                            · let low := xs.filter fun y => decide (y < pivot)
                              have hlowLt : low.length < xs.length :=
                                filter_length_lt_of_mem_false
                                  (fun y => decide (y < pivot)) hpivotMem (by simp)
                              have hlowLtN : low.length < n := by
                                simpa [hlen] using hlowLt
                              have hlowPivotFuel : low.length ≤ fuel + 1 := by omega
                              have hlowSelectorFuel : low.length ≤ selectorFuel := by omega
                              have hih := ih low.length hlowLtN low (fuel + 1)
                                selectorFuel k rfl hlowPivotFuel hlowSelectorFuel
                              have hclose :=
                                recursiveMedianOfMediansComparisonCost_large_step
                                  hnlarge hmedianSize
                                  (by simpa [hlen, low, ltCount] using hpivotBound.1)
                              simp only [selectCostFuel, hchoose, hlo, if_pos]
                              calc
                                xs.length +
                                      recursiveMedianOfMediansPivotComparisonCostFuel
                                        (fuel + 1) xs +
                                    selectCostFuel
                                      (recursiveMedianOfMediansPivotFuel? (fuel + 1))
                                      (fun ys => ys.length +
                                        recursiveMedianOfMediansPivotComparisonCostFuel
                                          (fuel + 1) ys)
                                      selectorFuel k
                                      (xs.filter fun y => decide (y < pivot))
                                    ≤ n + (2 * n + 100 * ms.length) +
                                        100 * low.length := by
                                          exact Nat.add_le_add
                                            (by simpa [hlen] using
                                              Nat.add_le_add_left hpivotCost n) hih
                                _ ≤ 100 * n := hclose
                                _ = 100 * xs.length := by rw [hlen]
                            · by_cases hmid : k < leCount pivot xs
                              · simp only [selectCostFuel, hchoose, hlo, hmid,
                                  if_false, if_pos]
                                have hclose :=
                                  recursiveMedianOfMediansComparisonCost_large_step
                                    hnlarge hmedianSize (strictBranch := 0) (by omega)
                                have hbase :
                                    xs.length +
                                        recursiveMedianOfMediansPivotComparisonCostFuel
                                          (fuel + 1) xs ≤
                                      n + (2 * n + 100 * ms.length) + 100 * 0 := by
                                  simpa [hlen] using
                                    Nat.add_le_add_left hpivotCost xs.length
                                exact le_trans hbase (by simpa [hlen] using hclose)
                              · let high := xs.filter fun y => decide (pivot < y)
                                have hhighLt : high.length < xs.length :=
                                  filter_length_lt_of_mem_false
                                    (fun y => decide (pivot < y)) hpivotMem (by simp)
                                have hhighLtN : high.length < n := by
                                  simpa [hlen] using hhighLt
                                have hhighPivotFuel : high.length ≤ fuel + 1 := by omega
                                have hhighSelectorFuel : high.length ≤ selectorFuel := by
                                  omega
                                have hih := ih high.length hhighLtN high (fuel + 1)
                                  selectorFuel (k - leCount pivot xs) rfl
                                  hhighPivotFuel hhighSelectorFuel
                                have hclose :=
                                  recursiveMedianOfMediansComparisonCost_large_step
                                    hnlarge hmedianSize
                                    (by simpa [hlen, high, gtCount] using hpivotBound.2)
                                simp only [selectCostFuel, hchoose, hlo, hmid]
                                calc
                                  xs.length +
                                        recursiveMedianOfMediansPivotComparisonCostFuel
                                          (fuel + 1) xs +
                                      selectCostFuel
                                        (recursiveMedianOfMediansPivotFuel? (fuel + 1))
                                        (fun ys => ys.length +
                                          recursiveMedianOfMediansPivotComparisonCostFuel
                                            (fuel + 1) ys)
                                        selectorFuel (k - leCount pivot xs)
                                        (xs.filter fun y => decide (pivot < y))
                                      ≤ n + (2 * n + 100 * ms.length) +
                                          100 * high.length := by
                                            exact Nat.add_le_add
                                              (by simpa [hlen] using
                                                Nat.add_le_add_left hpivotCost n) hih
                                  _ ≤ 100 * n := hclose
                                  _ = 100 * xs.length := by rw [hlen]

Strengthened public-cost induction with arbitrary sufficient SELECT fuel.


private theorem recursiveMedianOfMediansComparisonCostFuel_linear_bound :
    ∀ n : Nat, ∀ (xs : List Nat) (selectorFuel k : Nat),
      xs.length = n → xs.length ≤ selectorFuel →
        selectCostFuel recursiveMedianOfMediansPivot?
          (fun ys => ys.length + recursiveMedianOfMediansPivotComparisonCost ys)
          selectorFuel k xs ≤ 100 * xs.length := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      intro xs selectorFuel k hlen hselectorFuel
      cases selectorFuel with
      | zero =>
          simp [selectCostFuel]
      | succ selectorFuel =>
          cases hchoose : recursiveMedianOfMediansPivot? xs with
          | none =>
              simp [selectCostFuel, hchoose]
          | some pivot =>
              have hpivotMem : pivot ∈ xs :=
                recursiveMedianOfMediansPivot?_mem hchoose
              have hpivotBound :=
                recursiveMedianOfMediansPivot?_partition_size_bound hchoose
              have hnpos : 0 < n := by
                have hxsne : xs ≠ [] := by
                  intro hnil
                  subst xs
                  simp at hpivotMem
                have : 0 < xs.length := by
                  rw [List.length_pos_iff_ne_nil]
                  exact hxsne
                simpa [hlen] using this
              have hselectorSucc : n ≤ selectorFuel + 1 := by
                simpa [hlen] using hselectorFuel
              by_cases hsmall : n < 50
              · have hpivotCost :
                    recursiveMedianOfMediansPivotComparisonCost xs = n * n := by
                  unfold recursiveMedianOfMediansPivotComparisonCost
                  rw [hlen]
                  cases n with
                  | zero => omega
                  | succ n =>
                      simp [recursiveMedianOfMediansPivotComparisonCostFuel,
                        hlen, hsmall]
                have hdet : deterministicPivot? xs = some pivot := by
                  unfold recursiveMedianOfMediansPivot? at hchoose
                  rw [hlen] at hchoose
                  cases n with
                  | zero => omega
                  | succ n =>
                      simpa [recursiveMedianOfMediansPivotFuel?, hlen, hsmall]
                        using hchoose
                have hhalf := deterministicPivot?_half_partition_size_bound hdet
                by_cases hlo : k < ltCount pivot xs
                · let low := xs.filter fun y => decide (y < pivot)
                  have hlowLt : low.length < xs.length :=
                    filter_length_lt_of_mem_false
                      (fun y => decide (y < pivot)) hpivotMem (by simp)
                  have hlowLtN : low.length < n := by simpa [hlen] using hlowLt
                  have hlowSelectorFuel : low.length ≤ selectorFuel := by omega
                  have hih := ih low.length hlowLtN low selectorFuel k rfl
                    hlowSelectorFuel
                  have hclose :
                      n + n * n + 100 * low.length ≤ 100 * n :=
                    recursiveMedianOfMediansComparisonCost_small_step hsmall
                      (by simpa [hlen, low, ltCount] using hhalf.1)
                  simp only [selectCostFuel, hchoose, hlo, if_pos, hpivotCost]
                  calc
                    xs.length + n * n +
                        selectCostFuel recursiveMedianOfMediansPivot?
                          (fun ys => ys.length +
                            recursiveMedianOfMediansPivotComparisonCost ys)
                          selectorFuel k
                          (xs.filter fun y => decide (y < pivot))
                        ≤ n + n * n + 100 * low.length := by
                            simpa [hlen, low] using
                              Nat.add_le_add_left hih (n + n * n)
                    _ ≤ 100 * n := hclose
                    _ = 100 * xs.length := by rw [hlen]
                · by_cases hmid : k < leCount pivot xs
                  · simp only [selectCostFuel, hchoose, hlo, hmid, if_false,
                      if_pos, hpivotCost]
                    have hclose : n + n * n ≤ 100 * n := by
                      have := recursiveMedianOfMediansComparisonCost_small_step
                        (strictBranch := 0) hsmall (by omega)
                      simpa using this
                    simpa [hlen] using hclose
                  · let high := xs.filter fun y => decide (pivot < y)
                    have hhighLt : high.length < xs.length :=
                      filter_length_lt_of_mem_false
                        (fun y => decide (pivot < y)) hpivotMem (by simp)
                    have hhighLtN : high.length < n := by
                      simpa [hlen] using hhighLt
                    have hhighSelectorFuel : high.length ≤ selectorFuel := by omega
                    have hih := ih high.length hhighLtN high selectorFuel
                      (k - leCount pivot xs) rfl hhighSelectorFuel
                    have hclose :
                        n + n * n + 100 * high.length ≤ 100 * n :=
                      recursiveMedianOfMediansComparisonCost_small_step hsmall
                        (by simpa [hlen, high, gtCount] using hhalf.2)
                    simp only [selectCostFuel, hchoose, hlo, hmid, if_false,
                      hpivotCost]
                    calc
                      xs.length + n * n +
                          selectCostFuel recursiveMedianOfMediansPivot?
                            (fun ys => ys.length +
                              recursiveMedianOfMediansPivotComparisonCost ys)
                            selectorFuel (k - leCount pivot xs)
                            (xs.filter fun y => decide (pivot < y))
                          ≤ n + n * n + 100 * high.length := by
                              simpa [hlen, high] using
                                Nat.add_le_add_left hih (n + n * n)
                      _ ≤ 100 * n := hclose
                      _ = 100 * xs.length := by rw [hlen]
              · have hnlarge : 50 ≤ n := Nat.le_of_not_gt hsmall
                cases n with
                | zero => omega
                | succ n =>
                    cases hgroups : medianOfFiveGroups? (fullGroupsOfFive xs) with
                    | none =>
                        rcases fullGroupsOfFive_medianOfFiveGroups?_isSome xs with
                          ⟨medians, hmedians⟩
                        rw [hgroups] at hmedians
                        contradiction
                    | some medians =>
                        cases medians with
                        | nil =>
                            have hcert :
                                MedianGroupCertificates (fullGroupsOfFive xs) [] :=
                              fullGroupsOfFive_medianGroupCertificates hgroups
                            have hgroupsLen : (fullGroupsOfFive xs).length = 0 := by
                              simpa using hcert.1
                            have hnear := fullGroupsOfFive_length_near xs
                            rw [hgroupsLen] at hnear
                            omega
                        | cons median medians =>
                            let ms := median :: medians
                            have hcert :
                                MedianGroupCertificates (fullGroupsOfFive xs) ms :=
                              fullGroupsOfFive_medianGroupCertificates hgroups
                            have hmedianSizeXs : 5 * ms.length ≤ xs.length := by
                              have hgroupsSize :=
                                fullGroupsOfFive_length_mul_five_le xs
                              simpa [hcert.1] using hgroupsSize
                            have hmedianSize : 5 * ms.length ≤ n + 1 := by
                              simpa [hlen] using hmedianSizeXs
                            have hmedianLtN : ms.length < n + 1 := by omega
                            have hmedianFuel : ms.length ≤ n := by omega
                            have hinner :=
                              recursiveMedianOfMediansFixedComparisonCostFuel_linear_bound
                                ms.length ms n ms.length (ms.length / 2) rfl
                                hmedianFuel (Nat.le_refl ms.length)
                            have hpivotCost :
                                recursiveMedianOfMediansPivotComparisonCost xs ≤
                                  2 * (n + 1) + 100 * ms.length := by
                              dsimp [ms] at hinner ⊢
                              unfold recursiveMedianOfMediansPivotComparisonCost
                              rw [hlen]
                              simp only [recursiveMedianOfMediansPivotComparisonCostFuel,
                                hlen, hsmall, ↓reduceIte, hgroups]
                              simpa [selectCost] using
                                Nat.add_le_add_left hinner (2 * (n + 1))
                            by_cases hlo : k < ltCount pivot xs
                            · let low := xs.filter fun y => decide (y < pivot)
                              have hlowLt : low.length < xs.length :=
                                filter_length_lt_of_mem_false
                                  (fun y => decide (y < pivot)) hpivotMem (by simp)
                              have hlowLtN : low.length < n + 1 := by
                                simpa [hlen] using hlowLt
                              have hlowSelectorFuel : low.length ≤ selectorFuel := by
                                omega
                              have hih := ih low.length hlowLtN low selectorFuel k
                                rfl hlowSelectorFuel
                              have hclose :=
                                recursiveMedianOfMediansComparisonCost_large_step
                                  hnlarge hmedianSize
                                  (by simpa [hlen, low, ltCount] using hpivotBound.1)
                              simp only [selectCostFuel, hchoose, hlo, if_pos]
                              calc
                                xs.length +
                                      recursiveMedianOfMediansPivotComparisonCost xs +
                                    selectCostFuel recursiveMedianOfMediansPivot?
                                      (fun ys => ys.length +
                                        recursiveMedianOfMediansPivotComparisonCost ys)
                                      selectorFuel k
                                      (xs.filter fun y => decide (y < pivot))
                                    ≤ (n + 1) +
                                        (2 * (n + 1) + 100 * ms.length) +
                                          100 * low.length := by
                                            exact Nat.add_le_add
                                              (by simpa [hlen] using
                                                Nat.add_le_add_left hpivotCost (n + 1)) hih
                                _ ≤ 100 * (n + 1) := hclose
                                _ = 100 * xs.length := by rw [hlen]
                            · by_cases hmid : k < leCount pivot xs
                              · simp only [selectCostFuel, hchoose, hlo, hmid,
                                  if_false, if_pos]
                                have hclose :=
                                  recursiveMedianOfMediansComparisonCost_large_step
                                    hnlarge hmedianSize (strictBranch := 0) (by omega)
                                have hbase :
                                    xs.length +
                                        recursiveMedianOfMediansPivotComparisonCost xs ≤
                                      (n + 1) +
                                        (2 * (n + 1) + 100 * ms.length) + 100 * 0 := by
                                  simpa [hlen] using
                                    Nat.add_le_add_left hpivotCost xs.length
                                exact le_trans hbase (by simpa [hlen] using hclose)
                              · let high := xs.filter fun y => decide (pivot < y)
                                have hhighLt : high.length < xs.length :=
                                  filter_length_lt_of_mem_false
                                    (fun y => decide (pivot < y)) hpivotMem (by simp)
                                have hhighLtN : high.length < n + 1 := by
                                  simpa [hlen] using hhighLt
                                have hhighSelectorFuel : high.length ≤ selectorFuel := by
                                  omega
                                have hih := ih high.length hhighLtN high selectorFuel
                                  (k - leCount pivot xs) rfl hhighSelectorFuel
                                have hclose :=
                                  recursiveMedianOfMediansComparisonCost_large_step
                                    hnlarge hmedianSize
                                    (by simpa [hlen, high, gtCount] using hpivotBound.2)
                                simp only [selectCostFuel, hchoose, hlo, hmid]
                                calc
                                  xs.length +
                                        recursiveMedianOfMediansPivotComparisonCost xs +
                                      selectCostFuel recursiveMedianOfMediansPivot?
                                        (fun ys => ys.length +
                                          recursiveMedianOfMediansPivotComparisonCost ys)
                                        selectorFuel (k - leCount pivot xs)
                                        (xs.filter fun y => decide (pivot < y))
                                      ≤ (n + 1) +
                                          (2 * (n + 1) + 100 * ms.length) +
                                            100 * high.length := by
                                              exact Nat.add_le_add
                                                (by simpa [hlen] using
                                                  Nat.add_le_add_left hpivotCost (n + 1)) hih
                                  _ ≤ 100 * (n + 1) := hclose
                                  _ = 100 * xs.length := by rw [hlen]

The complete comparison charge of recursive median-of-medians SELECT is linear, including every nested pivot-selection subproblem and every selected outer partition branch.

theorem recursiveMedianOfMediansComparisonCost_linear_bound
    (k : Nat) (xs : List Nat) :
    recursiveMedianOfMediansComparisonCost k xs ≤ 100 * xs.length := by
  unfold recursiveMedianOfMediansComparisonCost selectCost
  exact recursiveMedianOfMediansComparisonCostFuel_linear_bound xs.length xs
    xs.length k rfl (Nat.le_refl xs.length)

Partition-path comparison cost of the executable median selector medianOfMediansSelect?.

The local work at each recursion level is xs.length: one comparison per element for the linear partition scan around the median-of-medians pivot. This is a genuine Nat-valued cost on list input, computed by the selector's outer recursion. It deliberately excludes the cost of constructing each pivot.

def medianOfMediansPartitionPathCost (k : Nat) (xs : List Nat) : Nat :=
  selectCost medianOfMediansPivot? (fun ys => ys.length) k xs

Linear bound for the outer partition path.

The partition-comparison cost of medianOfMediansSelect? is linear with the explicit constant 17:

medianOfMediansPartitionPathCost k xs ≤ 17 * xs.length.

This is the concrete counterpart of the abstract recurrence closure medianOfMedians_linear_bound: the CLRS branch bound medianOfMediansPivot?_partition_size_bound supplies the 10 * branch ≤ 7 * n + 12 hypothesis at every recursion level, and selectCost_linear_bound sums the linear local work into the closed form ≤ 17 n.


theorem medianOfMediansPartitionPathCost_linear_bound (k : Nat) (xs : List Nat) :
    medianOfMediansPartitionPathCost k xs ≤ 17 * xs.length := by
  have hbound : ∀ (ys : List Nat) (pivot : Nat),
      medianOfMediansPivot? ys = some pivot →
        10 * ltCount pivot ys ≤ 7 * ys.length + 12 ∧
        10 * gtCount pivot ys ≤ 7 * ys.length + 12 :=
    fun _ys _pivot hsel => medianOfMediansPivot?_partition_size_bound hsel
  have hstep : ∀ ys : List Nat, (fun zs => zs.length) ys ≤ 1 * ys.length :=
    fun ys => by simp
  have h := selectCost_linear_bound (a := 1) medianOfMediansPivot?
    (fun ys => ys.length) medianOfMediansPivot?_mem hbound hstep k xs
  simpa [medianOfMediansPartitionPathCost] using h

Outer partition-path cost for the recursive median-of-medians selector.

def recursiveMedianOfMediansPartitionPathCost (k : Nat) (xs : List Nat) : Nat :=
  selectCost recursiveMedianOfMediansPivot? (fun ys => ys.length) k xs

The outer partition path of the recursive selector is linear. This diagnostic bound intentionally omits nested pivot construction; the end-to-end theorem recursiveMedianOfMediansComparisonCost_linear_bound includes it.


theorem recursiveMedianOfMediansPartitionPathCost_linear_bound
    (k : Nat) (xs : List Nat) :
    recursiveMedianOfMediansPartitionPathCost k xs ≤ 17 * xs.length := by
  have hstep : ∀ ys : List Nat, (fun zs => zs.length) ys ≤ 1 * ys.length :=
    fun ys => by simp
  have h := selectCost_linear_bound (a := 1) recursiveMedianOfMediansPivot?
    (fun ys => ys.length) recursiveMedianOfMediansPivot?_mem
    (fun _ys _pivot hsel =>
      recursiveMedianOfMediansPivot?_partition_size_bound hsel)
    hstep k xs
  simpa [recursiveMedianOfMediansPartitionPathCost] using h

end Chapter09end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_09.Section_09_3_Selection_In_Worst_Case_Linear_Time.Randomized_Select

CLRS Section 9.2 - Randomized SELECT expected running time

This support page formalizes the standard majorizing recurrence used in the analysis of RANDOMIZED-SELECT and proves that this recurrence is linear.

The model is built directly on the shared finite-expectation toolkit CLRS.Probability.expect / CLRS.Probability.fintypeExpect. One recurrence step averages uniformly over the pivot rank Fin n and charges the larger of the two partition sides. The section also defines the actual state-dependent stochastic execution: every recursive call takes a fresh uniform pivot-rank choice, follows the branch selected by the requested rank, and charges its partition comparisons. That continuation is bounded pointwise by the larger-side recurrence, yielding expected cost at most 4n.

Main results:

Definition CLRS.Chapter09.subproblemSize: the larger partition side max i (n-1-i) when the (0-indexed) pivot rank is i.
Definition CLRS.Chapter09.randSelectExpectedCost: the expected-cost recurrence, defined by the uniform pivot average.
Theorem CLRS.Chapter09.randSelectExpectedCost_recurrence: the derived expected-comparison recurrence E[T(n+1)] = c(n+1) + expect (n+1) (fun i => E[T(max i (n-i))]) (CLRS equation for RANDOMIZED-SELECT), phrased with the toolkit CLRS.Probability.expect.
Theorem CLRS.Chapter09.randSelectExpectedCost_recurrence_fintype: the same recurrence phrased with CLRS.Probability.fintypeExpect over the per-step sample space Fin (n+1).
Theorem CLRS.Chapter09.randSelectExpectedCost_le: the substitution-method solution E[T(n)] ≤ 4·c·n.
Theorem CLRS.Chapter09.randomizedSelectMajorizer_bigO_linear: the asymptotic bound for the majorizing recurrence isBigO (fun n => E[T n]) (fun n => (n : ℝ)).
Definition CLRS.Chapter09.freshRandomizedSelectExpectedComparisons and theorem CLRS.Chapter09.freshRandomizedSelectExpectedComparisons_linear_bound: fresh per-call pivot choices for the actual selected continuation have expected comparison cost at most 4n.
Definition CLRS.Chapter09.randomizedSelectCostWithSchedule: an executable fresh-rank path cost that rejects exhausted or invalid schedules; theorem CLRS.Chapter09.randomizedSelectCostWithSchedule_rankCorrect erases successful cost runs to rank-correct SELECT results.
Definition CLRS.Chapter09.randomizedSelectExpectedCostFuel and theorem CLRS.Chapter09.randomizedSelectExpectedCostFuel_succ: the exact nested conditional-uniform expectation with local charge c * currentLength.
Theorems CLRS.Chapter09.randomizedSelectExpectedCost_le_randSelectExpectedCost and CLRS.Chapter09.randomizedSelectExpectedCost_linear_bound: every concrete state-dependent expected cost is bounded by the CLRS majorizer and hence by 4 * c * n.
Theorem CLRS.Chapter09.freshRandomizedSelectWithRanks?_correct: every executable finite sample path driven by successive pivot ranks is rank-correct.
Theorem CLRS.Chapter09.freshRandomizedSelectContinuationSize_le_subproblemSize: the actual selected continuation is pointwise bounded by the larger-side recurrence argument.
Theorem CLRS.Chapter09.randomizedSelectAtIndex?_rankCorrect: the randomized selector reuses the pivot-parametric SELECT skeleton, so rank correctness is inherited.

Notation conventions used in this section:

c : the per-element local-work constant (partition comparison cost)
n : current subproblem size
i : the 0-indexed pivot rank (number of elements below the pivot)

              namespace CLRSnamespace Chapter09open scoped BigOperatorsopen CLRS.Probability

Subproblem size and the expected-cost model

Size of the larger partition side when RANDOMIZED-SELECT picks the (0-indexed) pivot rank i from n elements: i elements fall below the pivot and n - 1 - i above it, so the recursion continues on the larger side max i (n - 1 - i).

This corresponds to the max(k-1, n-k) term of the CLRS expected-comparison recurrence (with k = i + 1 the 1-indexed rank).

def subproblemSize (n i : ℕ) : ℕ := max i (n - 1 - i)

Expected comparison count of RANDOMIZED-SELECT on n elements, defined as the CLRS majorizing recurrence.

At each step the pivot rank is uniform over Fin n; the local partition work is c · n; and the recursion charges the larger partition side. The average over the pivot rank is expressed as the uniform sum divided by n, i.e. the toolkit average CLRS.Probability.expect (see CLRS.Chapter09.randSelectExpectedCost_recurrence).

The sum is taken over (Finset.range (n+1)).attach purely so the well-founded recursion can see that every recursive argument max i (n - i) is < n + 1.

noncomputable def randSelectExpectedCost (c : ℝ) : ℕ → ℝ
  | 0 => 0
  | (n + 1) =>
      c * ((n : ℝ) + 1) +
        (∑ i ∈ (Finset.range (n + 1)).attach,
            randSelectExpectedCost c (max i.1 (n - i.1))) / ((n : ℝ) + 1)
  decreasing_by
    have hi : i.1 < n + 1 := Finset.mem_range.mp i.2
    omega



@[simp]
theorem randSelectExpectedCost_zero (c : ℝ) : randSelectExpectedCost c 0 = 0 := by
  rw [randSelectExpectedCost]

One-step unfolding of CLRS.Chapter09.randSelectExpectedCost, converting the termination-friendly attach sum into an ordinary sum over Finset.range (n + 1).


theorem randSelectExpectedCost_succ (c : ℝ) (n : ℕ) :
    randSelectExpectedCost c (n + 1) =
      c * ((n : ℝ) + 1) +
        (∑ i ∈ Finset.range (n + 1),
            randSelectExpectedCost c (max i (n - i))) / ((n : ℝ) + 1) := by
  conv_lhs => rw [randSelectExpectedCost]
  rw [Finset.sum_attach (Finset.range (n + 1))
        (fun i => randSelectExpectedCost c (max i (n - i)))]

The expected-comparison recurrence (derived from the model)

Expected-comparison recurrence for RANDOMIZED-SELECT.

The expected cost satisfies

E[T(n+1)] = c·(n+1) + expect (n+1) (fun i => E[T(max i (n-i))]),

where CLRS.Probability.expect is the uniform average over the pivot rank i ∈ {0, …, n}. Writing k = i + 1 for the 1-indexed rank, the averaged term is E[T(max (k-1) ((n+1)-k))], exactly the CLRS recurrence E[T(n)] = (1/n) Σ_k E[T(max(k-1, n-k))] + c·n.

This is an equality derived from the definition of the model (it is not an assumed recurrence), and in particular implies the acceptance-criterion upper bound.


theorem randSelectExpectedCost_recurrence (c : ℝ) (n : ℕ) :
    randSelectExpectedCost c (n + 1) =
      c * ((n : ℝ) + 1) +
        Probability.expect (n + 1)
          (fun i => randSelectExpectedCost c (max i (n - i))) := by
  rw [randSelectExpectedCost_succ]
  simp only [Probability.expect, Nat.cast_add, Nat.cast_one]

The uniform pivot average CLRS.Probability.expect equals the finite-type expectation CLRS.Probability.fintypeExpect over the per-step sample space Fin m. This makes the "uniform independent pivot rank over Fin n" reading of the model explicit.


theorem expect_eq_fintypeExpect (m : ℕ) (X : ℕ → ℝ) :
    Probability.expect m X
      = Probability.fintypeExpect (fun j : Fin m => X j.1) := by
  unfold Probability.expect Probability.fintypeExpect
  rw [Fintype.card_fin, Fin.sum_univ_eq_sum_range X m]

The expected-comparison recurrence phrased with CLRS.Probability.fintypeExpect over the explicit per-step pivot-rank sample space Fin (n + 1).


theorem randSelectExpectedCost_recurrence_fintype (c : ℝ) (n : ℕ) :
    randSelectExpectedCost c (n + 1) =
      c * ((n : ℝ) + 1) +
        Probability.fintypeExpect
          (fun j : Fin (n + 1) => randSelectExpectedCost c (max j.1 (n - j.1))) := by
  rw [randSelectExpectedCost_recurrence, expect_eq_fintypeExpect]

Nonnegativity

The expected cost is nonnegative whenever the work constant is nonnegative.


theorem randSelectExpectedCost_nonneg (c : ℝ) (hc : 0 ≤ c) :
    ∀ n, 0 ≤ randSelectExpectedCost c n := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
    rcases n with _ | m
    · simp
    · rw [randSelectExpectedCost_succ]
      have hsum :
          0 ≤ ∑ i ∈ Finset.range (m + 1),
              randSelectExpectedCost c (max i (m - i)) := by
        apply Finset.sum_nonneg
        intro i hi
        have hlt : max i (m - i) < m + 1 := by
          have := Finset.mem_range.mp hi; omega
        exact ih _ hlt
      have h1 : 0 ≤ c * ((m : ℝ) + 1) := mul_nonneg hc (by positivity)
      have h2 :
          0 ≤ (∑ i ∈ Finset.range (m + 1),
              randSelectExpectedCost c (max i (m - i))) / ((m : ℝ) + 1) :=
        div_nonneg hsum (by positivity)
      linarith

The max-side sum and its `3n²/4` bound

Sum of the larger partition sides over all pivot ranks: ∑_{i<n} max i (n - 1 - i). This is the combinatorial core of the substitution method: the substitution guess T(k) ≤ K·k turns the averaged recursive term into K · maxSideSum n / n.

def maxSideSum (n : ℕ) : ℕ := ∑ i ∈ Finset.range n, max i (n - 1 - i)

Two-step recurrence for the max-side sum: maxSideSum (n+2) = maxSideSum n + 3n + 2.

Peeling the extremal pivot ranks 0 and n+1 (each contributing n+1) and reindexing the interior leaves ∑_{i<n} (max i (n-1-i) + 1) = maxSideSum n + n.


theorem maxSideSum_add_two (n : ℕ) :
    maxSideSum (n + 2) = maxSideSum n + 3 * n + 2 := by
  unfold maxSideSum
  rw [Finset.sum_range_succ', Finset.sum_range_succ]
  have hmid : ∀ i ∈ Finset.range n,
      max (i + 1) (n + 2 - 1 - (i + 1)) = max i (n - 1 - i) + 1 := by
    intro i hi
    have := Finset.mem_range.mp hi
    omega
  rw [Finset.sum_congr rfl hmid, Finset.sum_add_distrib, Finset.sum_const,
      Finset.card_range, smul_eq_mul, mul_one]
  omega

The max-side sum is at most three quarters of n²: 4 · maxSideSum n ≤ 3 · n².

Proved by two-step strong induction using CLRS.Chapter09.maxSideSum_add_two. This is the constant < 1 that the substitution method needs (a bound like maxSideSum n ≤ n² would not close).


theorem four_mul_maxSideSum_le (n : ℕ) : 4 * maxSideSum n ≤ 3 * n ^ 2 := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
    rcases n with _ | _ | m
    · simp [maxSideSum]
    · norm_num [maxSideSum, Finset.sum_range_one]
    · have hm : 4 * maxSideSum m ≤ 3 * m ^ 2 := ih m (by omega)
      rw [maxSideSum_add_two]
      nlinarith [hm]

Real-valued form of the max-side bound specialized to the recursion: 4 · Σ_{i≤m} (max i (m-i) : ℝ) ≤ 3 · (m+1)².


theorem sum_maxSide_real_bound (m : ℕ) :
    4 * (∑ i ∈ Finset.range (m + 1), ((max i (m - i) : ℕ) : ℝ))
      ≤ 3 * ((m : ℝ) + 1) ^ 2 := by
  have hdef : maxSideSum (m + 1) = ∑ i ∈ Finset.range (m + 1), max i (m - i) := by
    unfold maxSideSum
    simp only [Nat.add_sub_cancel]
  have hN : 4 * (∑ i ∈ Finset.range (m + 1), max i (m - i)) ≤ 3 * (m + 1) ^ 2 := by
    rw [← hdef]; exact four_mul_maxSideSum_le (m + 1)
  calc
    (4 : ℝ) * (∑ i ∈ Finset.range (m + 1), ((max i (m - i) : ℕ) : ℝ))
        = ((4 * (∑ i ∈ Finset.range (m + 1), max i (m - i)) : ℕ) : ℝ) := by
          push_cast; ring
    _ ≤ ((3 * (m + 1) ^ 2 : ℕ) : ℝ) := by exact_mod_cast hN
    _ = 3 * ((m : ℝ) + 1) ^ 2 := by push_cast; ring

The linear expected-time bound (CLRS Theorem 9.2)

Substitution-method solution of the expected-comparison recurrence.

For a nonnegative work constant c, the expected cost is linear: E[T(n)] ≤ 4·c·n.

The proof is the CLRS substitution method: guess T(k) ≤ 4c·k, bound the averaged recursive term by 4c · maxSideSum n / n ≤ 3c·n using CLRS.Chapter09.four_mul_maxSideSum_le, and close with the local work c·n.


theorem randSelectExpectedCost_le (c : ℝ) (hc : 0 ≤ c) :
    ∀ n, randSelectExpectedCost c n ≤ 4 * c * (n : ℝ) := by
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
    rcases n with _ | m
    · simp
    · rw [randSelectExpectedCost_succ]
      set S := ∑ i ∈ Finset.range (m + 1),
          randSelectExpectedCost c (max i (m - i)) with hSdef
      -- Bound each recursive term by the substitution guess.
      have hterm : ∀ i ∈ Finset.range (m + 1),
          randSelectExpectedCost c (max i (m - i))
            ≤ 4 * c * ((max i (m - i) : ℕ) : ℝ) := by
        intro i hi
        have hlt : max i (m - i) < m + 1 := by
          have := Finset.mem_range.mp hi; omega
        exact ih _ hlt
      have hS1 : S ≤ ∑ i ∈ Finset.range (m + 1), 4 * c * ((max i (m - i) : ℕ) : ℝ) :=
        Finset.sum_le_sum hterm
      have hS2 :
          (∑ i ∈ Finset.range (m + 1), 4 * c * ((max i (m - i) : ℕ) : ℝ))
            = 4 * c * (∑ i ∈ Finset.range (m + 1), ((max i (m - i) : ℕ) : ℝ)) := by
        rw [Finset.mul_sum]
      have hpos : 0 ≤ ∑ i ∈ Finset.range (m + 1), ((max i (m - i) : ℕ) : ℝ) := by
        apply Finset.sum_nonneg; intro i _; positivity
      have hbound := sum_maxSide_real_bound m
      -- S ≤ 3c(m+1)²
      have hSle : S ≤ 3 * c * ((m : ℝ) + 1) ^ 2 := by
        rw [hS2] at hS1
        nlinarith [hS1, hbound, hc, hpos]
      have hmpos : (0 : ℝ) < (m : ℝ) + 1 := by positivity
      have hne : ((m : ℝ) + 1) ≠ 0 := ne_of_gt hmpos
      have hsimp :
          (3 * c * ((m : ℝ) + 1) ^ 2) / ((m : ℝ) + 1) = 3 * c * ((m : ℝ) + 1) := by
        rw [div_eq_iff hne]; ring
      have hfrac : S / ((m : ℝ) + 1) ≤ 3 * c * ((m : ℝ) + 1) := by
        have h1 := div_le_div_of_nonneg_right hSle hmpos.le
        rwa [hsimp] at h1
      have hcm : c * ((m : ℝ) + 1) + 3 * c * ((m : ℝ) + 1) = 4 * c * ((m : ℝ) + 1) := by
        ring
      push_cast
      linarith [hfrac, hcm]

The CLRS majorizing expected-comparison recurrence with unit local-work constant (n comparisons per partition, i.e. c = 1).

noncomputable def randomizedSelectMajorizingExpectedComparisons (n : ℕ) : ℝ :=
  randSelectExpectedCost 1 n

The expected cost is O(n) for every nonnegative work constant, via the CLRS-compatible CLRS.Chapter03.isBigO wrapper.


theorem randSelectExpectedCost_bigO_linear (c : ℝ) (hc : 0 ≤ c) :
    CLRS.Chapter03.isBigO (fun n => randSelectExpectedCost c n) (fun n => (n : ℝ)) := by
  rw [CLRS.Chapter03.isBigO_iff]
  refine ⟨4 * c + 1, by linarith, 0, ?_⟩
  intro n _
  have hnn : 0 ≤ randSelectExpectedCost c n := randSelectExpectedCost_nonneg c hc n
  have hle : randSelectExpectedCost c n ≤ 4 * c * (n : ℝ) := randSelectExpectedCost_le c hc n
  have hcast : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n
  rw [abs_of_nonneg hnn, abs_of_nonneg hcast]
  nlinarith [hle, hcast]

The majorizing recurrence used in the proof of CLRS Theorem 9.2 is O(n). The fresh-choice state-dependent execution and its coupling to the same larger-side argument are proved separately below.

theorem randomizedSelectMajorizer_bigO_linear :
    CLRS.Chapter03.isBigO
      (fun n => randomizedSelectMajorizingExpectedComparisons n) (fun n => (n : ℝ)) :=
  randSelectExpectedCost_bigO_linear 1 (by norm_num)

Fresh-choice RANDOMIZED-SELECT semantics

Fuelled RANDOMIZED-SELECT path interpreter driven by a sequence of pivot ranks. Each recursive call consumes one new rank. A stochastic implementation obtains that next rank from the current Fin xs.length; keeping the choices explicit here makes every finite sample path executable and independently testable.

def freshRandomizedSelectWithRanksFuel? :
    Nat → List Nat → Nat → List Nat → Option Nat
  | 0, _, _, _ => none
  | _ + 1, [], _, _ => none
  | fuel + 1, i :: choices, k, xs =>
      match selectByRank? i xs with
      | none => none
      | some pivot =>
          if k < ltCount pivot xs then
            freshRandomizedSelectWithRanksFuel? fuel choices k
              (xs.filter fun y => decide (y < pivot))
          else if k < leCount pivot xs then
            some pivot
          else
            freshRandomizedSelectWithRanksFuel? fuel choices
              (k - leCount pivot xs)
              (xs.filter fun y => decide (pivot < y))

Public rank-choice path interpreter with enough fuel for strict recursion.

def freshRandomizedSelectWithRanks? (choices : List Nat)
    (k : Nat) (xs : List Nat) : Option Nat :=
  freshRandomizedSelectWithRanksFuel? xs.length choices k xs

Schedule-driven concrete cost semantics

Cost of one concrete fresh-rank execution path. Every visited nonempty state charges c * length and consumes exactly one rank from choices. Running out of fuel or choices, or presenting a rank outside the current subproblem, rejects the path instead of silently assigning zero cost.

This partition-work metric does not charge the specification implementation of selectByRank?, random-number generation, list primitives, or RAM operations.

def randomizedSelectCostWithScheduleFuel :
    Nat → Nat → Nat → List Nat → List Nat → Option Nat
  | 0, _, _, _, _ => none
  | _ + 1, _, _, [], _ => none
  | _ + 1, _, _, _, [] => none
  | fuel + 1, c, k, x :: xs, i :: choices =>
      match selectByRank? i (x :: xs) with
      | none => none
      | some pivot =>
          let here := c * (x :: xs).length
          if k < ltCount pivot (x :: xs) then
            Option.map (here + ·)
              (randomizedSelectCostWithScheduleFuel fuel c k
                ((x :: xs).filter fun y => decide (y < pivot)) choices)
          else if k < leCount pivot (x :: xs) then
            some here
          else
            Option.map (here + ·)
              (randomizedSelectCostWithScheduleFuel fuel c
                (k - leCount pivot (x :: xs))
                ((x :: xs).filter fun y => decide (pivot < y)) choices)

Public schedule cost with one fuel unit for every input occurrence.

def randomizedSelectCostWithSchedule
    (c k : Nat) (xs choices : List Nat) : Option Nat :=
  randomizedSelectCostWithScheduleFuel xs.length c k xs choices

Every successful fresh-rank sample path returns the requested order statistic.


theorem freshRandomizedSelectWithRanksFuel?_correct :
    ∀ (fuel : Nat) (choices : List Nat) (k : Nat) (xs : List Nat) {x : Nat},
      freshRandomizedSelectWithRanksFuel? fuel choices k xs = some x →
        RankCertificate xs k x := by
  intro fuel
  induction fuel with
  | zero =>
      intro choices k xs x hrun
      simp [freshRandomizedSelectWithRanksFuel?] at hrun
  | succ fuel ih =>
      intro choices k xs selected hrun
      cases choices with
      | nil =>
          simp [freshRandomizedSelectWithRanksFuel?] at hrun
      | cons i choices =>
          cases hpivot : selectByRank? i xs with
          | none =>
              simp [freshRandomizedSelectWithRanksFuel?, hpivot] at hrun
          | some pivot =>
              have hpivotMem : pivot ∈ xs := selectByRank?_mem hpivot
              by_cases hlo : k < ltCount pivot xs
              · have hlow :
                    freshRandomizedSelectWithRanksFuel? fuel choices k
                        (xs.filter fun y => decide (y < pivot)) =
                      some selected := by
                  simpa [freshRandomizedSelectWithRanksFuel?, hpivot, hlo]
                    using hrun
                exact rankCertificate_low_lift (ih choices k _ hlow)
              · by_cases hmid : k < leCount pivot xs
                · have hselected : selected = pivot := by
                    exact Eq.symm (by
                      simpa [freshRandomizedSelectWithRanksFuel?, hpivot, hlo,
                        hmid] using hrun)
                  subst selected
                  exact rankCertificate_pivot hpivotMem hlo hmid
                · have hhigh :
                      freshRandomizedSelectWithRanksFuel? fuel choices
                          (k - leCount pivot xs)
                          (xs.filter fun y => decide (pivot < y)) =
                        some selected := by
                    simpa [freshRandomizedSelectWithRanksFuel?, hpivot, hlo,
                      hmid] using hrun
                  exact rankCertificate_high_lift (Nat.le_of_not_gt hmid)
                    (ih choices (k - leCount pivot xs) _ hhigh)

Correctness of the public fresh-rank path interpreter.

theorem freshRandomizedSelectWithRanks?_correct {choices : List Nat}
    {k : Nat} {xs : List Nat} {x : Nat}
    (hrun : freshRandomizedSelectWithRanks? choices k xs = some x) :
    RankCertificate xs k x := by
  exact freshRandomizedSelectWithRanksFuel?_correct xs.length choices k xs
    (by simpa [freshRandomizedSelectWithRanks?] using hrun)

A successful costed path erases to a successful fresh-rank SELECT path.

theorem randomizedSelectCostWithScheduleFuel_result :
    ∀ {fuel c k : Nat} {xs choices : List Nat} {cost : Nat},
      randomizedSelectCostWithScheduleFuel fuel c k xs choices = some cost →
        ∃ x, freshRandomizedSelectWithRanksFuel? fuel choices k xs = some x := by
  intro fuel
  induction fuel with
  | zero =>
      intro c k xs choices cost hcost
      simp [randomizedSelectCostWithScheduleFuel] at hcost
  | succ fuel ih =>
      intro c k xs choices cost hcost
      cases xs with
      | nil =>
          simp [randomizedSelectCostWithScheduleFuel] at hcost
      | cons x xs =>
          cases choices with
          | nil =>
              simp [randomizedSelectCostWithScheduleFuel] at hcost
          | cons i choices =>
              cases hpivot : selectByRank? i (x :: xs) with
              | none =>
                  simp [randomizedSelectCostWithScheduleFuel, hpivot] at hcost
              | some pivot =>
                  by_cases hlo : k < ltCount pivot (x :: xs)
                  · cases hrec : randomizedSelectCostWithScheduleFuel fuel c k
                        ((x :: xs).filter fun y => decide (y < pivot)) choices with
                    | none =>
                        simp [randomizedSelectCostWithScheduleFuel, hpivot, hlo,
                          hrec] at hcost
                    | some subcost =>
                        rcases ih hrec with ⟨selected, hselected⟩
                        exact ⟨selected, by
                          simpa [freshRandomizedSelectWithRanksFuel?, hpivot, hlo]
                            using hselected⟩
                  · by_cases hmid : k < leCount pivot (x :: xs)
                    · exact ⟨pivot, by
                        simp [freshRandomizedSelectWithRanksFuel?, hpivot, hlo,
                          hmid]⟩
                    · cases hrec : randomizedSelectCostWithScheduleFuel fuel c
                          (k - leCount pivot (x :: xs))
                          ((x :: xs).filter fun y => decide (pivot < y)) choices with
                      | none =>
                          simp [randomizedSelectCostWithScheduleFuel, hpivot, hlo,
                            hmid, hrec] at hcost
                      | some subcost =>
                          rcases ih hrec with ⟨selected, hselected⟩
                          exact ⟨selected, by
                            simpa [freshRandomizedSelectWithRanksFuel?, hpivot, hlo,
                              hmid] using hselected⟩

A successful public cost execution erases to the public fresh-rank path.

theorem randomizedSelectCostWithSchedule_result
    {c k : Nat} {xs choices : List Nat} {cost : Nat}
    (hcost : randomizedSelectCostWithSchedule c k xs choices = some cost) :
    ∃ x, freshRandomizedSelectWithRanks? choices k xs = some x := by
  exact randomizedSelectCostWithScheduleFuel_result
    (by simpa [randomizedSelectCostWithSchedule,
      freshRandomizedSelectWithRanks?] using hcost)

Every successful costed schedule returns a rank-correct SELECT result.

theorem randomizedSelectCostWithSchedule_rankCorrect
    {c k : Nat} {xs choices : List Nat} {cost : Nat}
    (hcost : randomizedSelectCostWithSchedule c k xs choices = some cost) :
    ∃ x, RankCertificate xs k x := by
  rcases randomizedSelectCostWithSchedule_result hcost with ⟨x, hx⟩
  exact ⟨x, freshRandomizedSelectWithRanks?_correct hx⟩

Size of the continuation actually selected by one pivot-rank choice.

def freshRandomizedSelectContinuationSize (k i : Nat) (xs : List Nat) : Nat :=
  match selectByRank? i xs with
  | none => 0
  | some pivot =>
      if k < ltCount pivot xs then ltCount pivot xs
      else if k < leCount pivot xs then 0
      else gtCount pivot xs

Pointwise coupling to the CLRS larger-side recurrence: for every valid sampled pivot rank, the continuation actually chosen by the requested order statistic is no larger than max i (n - 1 - i).


theorem freshRandomizedSelectContinuationSize_le_subproblemSize
    {k i : Nat} {xs : List Nat} (hi : i < xs.length) :
    freshRandomizedSelectContinuationSize k i xs ≤
      subproblemSize xs.length i := by
  rcases selectByRank?_isSome_of_lt hi with ⟨pivot, hpivot⟩
  have hrank : RankCertificate xs i pivot :=
    selectByRank?_rankCorrect hpivot
  by_cases hlo : k < ltCount pivot xs
  · simp only [freshRandomizedSelectContinuationSize, hpivot, hlo, if_pos,
      subproblemSize]
    exact le_trans hrank.2.1 (Nat.le_max_left _ _)
  · by_cases hmid : k < leCount pivot xs
    · simp [freshRandomizedSelectContinuationSize, hpivot, hlo, hmid]
    · simp only [freshRandomizedSelectContinuationSize, hpivot, hlo, hmid,
        if_false, subproblemSize]
      have hhigh : gtCount pivot xs ≤ xs.length - 1 - i := by
        rw [gtCount_eq_length_sub_leCount]
        have hirank : i + 1 ≤ leCount pivot xs :=
          Nat.succ_le_of_lt hrank.2.2
        have hsub := Nat.sub_le_sub_left hirank xs.length
        simpa [Nat.sub_sub, Nat.add_comm] using hsub
      exact le_trans hhigh (Nat.le_max_right _ _)

Expected comparisons of RANDOMIZED-SELECT with an explicit fresh uniform pivot-rank choice at every recursive call.

The sampled rank i ranges uniformly over the current Fin xs.length; the value selectByRank? i xs is the corresponding uniformly sampled occurrence written in rank coordinates. This is an analysis reindexing of choosing a uniform input position, not an extra order-statistic computation charged to the algorithm. After the partition scan, the expectation recursively averages again on the selected strict subproblem, so choices at different levels are fresh rather than a single fixed index reused throughout the run.

noncomputable def freshRandomizedSelectExpectedComparisonsFuel :
    Nat → Nat → List Nat → ℝ
  | 0, _, _ => 0
  | _ + 1, _, [] => 0
  | fuel + 1, k, (x :: xs) =>
      ((x :: xs).length : ℝ) +
        Probability.expect (x :: xs).length (fun i =>
          match selectByRank? i (x :: xs) with
          | none => 0
          | some pivot =>
              if k < ltCount pivot (x :: xs) then
                freshRandomizedSelectExpectedComparisonsFuel fuel k
                  ((x :: xs).filter fun y => decide (y < pivot))
              else if k < leCount pivot (x :: xs) then
                0
              else
                freshRandomizedSelectExpectedComparisonsFuel fuel
                  (k - leCount pivot (x :: xs))
                  ((x :: xs).filter fun y => decide (pivot < y)))

Public fresh-choice expectation, with one unit of fuel per input element.

noncomputable def freshRandomizedSelectExpectedComparisons
    (k : Nat) (xs : List Nat) : ℝ :=
  freshRandomizedSelectExpectedComparisonsFuel xs.length k xs

Nested expected cost of fresh-rank RANDOMIZED-SELECT with local charge c * length. The expectation is taken anew over the current subproblem at every recursive level; invalid ranks are absent because the sample space has cardinality equal to the current list length. This is a recursively nested conditional-uniform semantics, not a flat uniform distribution over variable-length schedules, and it carries the same partition-work boundary as randomizedSelectCostWithSchedule.

noncomputable def randomizedSelectExpectedCostFuel :
    Nat → Nat → Nat → List Nat → Real
  | 0, _, _, _ => 0
  | _ + 1, _, _, [] => 0
  | fuel + 1, c, k, x :: xs =>
      c * ((x :: xs).length : Real) +
        Probability.expect (x :: xs).length fun i =>
          match selectByRank? i (x :: xs) with
          | none => 0
          | some pivot =>
              if k < ltCount pivot (x :: xs) then
                randomizedSelectExpectedCostFuel fuel c k
                  ((x :: xs).filter fun y => decide (y < pivot))
              else if k < leCount pivot (x :: xs) then
                0
              else
                randomizedSelectExpectedCostFuel fuel c
                  (k - leCount pivot (x :: xs))
                  ((x :: xs).filter fun y => decide (pivot < y))

Public expected cost with one fuel unit for every input occurrence.

noncomputable def randomizedSelectExpectedCost
    (c k : Nat) (xs : List Nat) : Real :=
  randomizedSelectExpectedCostFuel xs.length c k xs

Exact one-step unfolding of the state-dependent nested expectation.


theorem randomizedSelectExpectedCostFuel_succ
    (fuel c k x : Nat) (xs : List Nat) :
    randomizedSelectExpectedCostFuel (fuel + 1) c k (x :: xs) =
      c * ((x :: xs).length : Real) +
        Probability.expect (x :: xs).length (fun i =>
          match selectByRank? i (x :: xs) with
          | none => 0
          | some pivot =>
              if k < ltCount pivot (x :: xs) then
                randomizedSelectExpectedCostFuel fuel c k
                  ((x :: xs).filter fun y => decide (y < pivot))
              else if k < leCount pivot (x :: xs) then
                0
              else
                randomizedSelectExpectedCostFuel fuel c
                  (k - leCount pivot (x :: xs))
                  ((x :: xs).filter fun y => decide (pivot < y))) := by
  rw [randomizedSelectExpectedCostFuel]

Unit local charge recovers the existing fresh-comparison expectation.


theorem randomizedSelectExpectedCost_one
    (fuel k : Nat) (xs : List Nat) :
    randomizedSelectExpectedCostFuel fuel 1 k xs =
      freshRandomizedSelectExpectedComparisonsFuel fuel k xs := by
  induction fuel generalizing k xs with
  | zero =>
      simp [randomizedSelectExpectedCostFuel,
        freshRandomizedSelectExpectedComparisonsFuel]
  | succ fuel ih =>
      cases xs with
      | nil =>
          simp [randomizedSelectExpectedCostFuel,
            freshRandomizedSelectExpectedComparisonsFuel]
      | cons x xs =>
          rw [randomizedSelectExpectedCostFuel,
            freshRandomizedSelectExpectedComparisonsFuel]
          simp only [Nat.cast_one, one_mul]
          congr 1
          apply congrArg (Probability.expect (x :: xs).length)
          funext i
          cases hpivot : selectByRank? i (x :: xs) with
          | none =>
              simp
          | some pivot =>
              by_cases hlo : k < ltCount pivot (x :: xs)
              · simp [hlo, ih]
              · by_cases hmid : k < leCount pivot (x :: xs)
                · simp [hlo, hmid]
                · simp [hlo, hmid, ih]

The nested fresh-choice expected cost is nonnegative.


theorem randomizedSelectExpectedCost_nonneg
    (fuel c k : Nat) (xs : List Nat) :
    0 ≤ randomizedSelectExpectedCostFuel fuel c k xs := by
  induction fuel generalizing c k xs with
  | zero =>
      simp [randomizedSelectExpectedCostFuel]
  | succ fuel ih =>
      cases xs with
      | nil =>
          simp [randomizedSelectExpectedCostFuel]
      | cons x xs =>
          rw [randomizedSelectExpectedCostFuel]
          apply add_nonneg (by positivity)
          apply Probability.expect_nonneg
          intro i
          cases selectByRank? i (x :: xs) with
          | none =>
              simp
          | some pivot =>
              by_cases hlo : k < ltCount pivot (x :: xs)
              · simpa [hlo] using ih c k
                  ((x :: xs).filter fun y => decide (y < pivot))
              · by_cases hmid : k < leCount pivot (x :: xs)
                · simp [hlo, hmid]
                · simpa [hlo, hmid] using ih c
                    (k - leCount pivot (x :: xs))
                    ((x :: xs).filter fun y => decide (pivot < y))

The size-only RANDOMIZED-SELECT majorizer is monotone in input size.


private theorem randSelectExpectedCost_monotone (c : Real) (hc : 0 ≤ c) :
    Monotone (randSelectExpectedCost c) := by
  apply monotone_nat_of_le_succ
  intro n
  induction n using Nat.strong_induction_on with
  | h n ih =>
      rcases n with _ | m
      · rw [randSelectExpectedCost_zero, randSelectExpectedCost_succ]
        simp
        exact hc
      · have hmonoBelow : ∀ {a b : Nat}, a ≤ b → b ≤ m + 1 →
            randSelectExpectedCost c a ≤ randSelectExpectedCost c b := by
          intro a b hab hb
          refine Nat.le_induction (m := a)
            (P := fun j _ => j ≤ m + 1 →
              randSelectExpectedCost c a ≤ randSelectExpectedCost c j)
            (fun _ => le_rfl)
            (fun j _ hchain hj =>
              le_trans (hchain (by omega)) (ih j (by omega)))
            b hab hb
        let A : Nat → Real := fun i =>
          randSelectExpectedCost c (max i (m - i))
        let B : Nat → Real := fun i =>
          randSelectExpectedCost c (max i (m + 1 - i))
        let SA : Real := ∑ i ∈ Finset.range (m + 1), A i
        let SB : Real := ∑ i ∈ Finset.range (m + 1), B i
        have hAB : SA ≤ SB := by
          apply Finset.sum_le_sum
          intro i hi
          have hiLt : i < m + 1 := Finset.mem_range.mp hi
          apply hmonoBelow
          · omega
          · omega
        have hAT :
            SA ≤ (m + 1 : Real) * randSelectExpectedCost c (m + 1) := by
          calc
            SA ≤ ∑ _i ∈ Finset.range (m + 1),
                randSelectExpectedCost c (m + 1) := by
              apply Finset.sum_le_sum
              intro i hi
              apply hmonoBelow
              · have hiLt : i < m + 1 := Finset.mem_range.mp hi
                omega
              · exact le_rfl
            _ = (m + 1 : Real) * randSelectExpectedCost c (m + 1) := by
              simp
        have hn : (0 : Real) < m + 1 := by positivity
        have hnp : (0 : Real) < m + 2 := by positivity
        have hmulAB : (m + 1 : Real) * SA ≤ (m + 1 : Real) * SB :=
          mul_le_mul_of_nonneg_left hAB hn.le
        have hnum : SA * (m + 2 : Real) ≤
            (SB + randSelectExpectedCost c (m + 1)) * (m + 1 : Real) := by
          nlinarith [hAT, hmulAB]
        have hAvg : SA / (m + 1 : Real) ≤
            (SB + randSelectExpectedCost c (m + 1)) / (m + 2 : Real) := by
          exact (div_le_div_iff₀ hn hnp).2 hnum
        have hSBsucc :
            (∑ i ∈ Finset.range (m + 1 + 1),
                randSelectExpectedCost c (max i (m + 1 - i))) =
              SB + randSelectExpectedCost c (m + 1) := by
          rw [Finset.sum_range_succ]
          simp [SB, B]
        rw [randSelectExpectedCost_succ, randSelectExpectedCost_succ, hSBsucc]
        have hlocal : c * (m + 1 : Real) ≤ c * (m + 2 : Real) := by
          nlinarith
        dsimp [SA, A] at hAvg
        convert add_le_add hlocal hAvg using 1
        · push_cast
          ring

The state-dependent nested expected cost is bounded by the CLRS larger-side majorizer on every input, rank, fuel amount, and nonnegative natural local-work constant.


theorem randomizedSelectExpectedCost_le_randSelectExpectedCost :
    ∀ (fuel c k : Nat) (xs : List Nat),
      randomizedSelectExpectedCostFuel fuel c k xs ≤
        randSelectExpectedCost c xs.length := by
  intro fuel
  induction fuel with
  | zero =>
      intro c k xs
      rw [randomizedSelectExpectedCostFuel]
      exact randSelectExpectedCost_nonneg c (by positivity) xs.length
  | succ fuel ih =>
      intro c k xs
      cases xs with
      | nil =>
          simp [randomizedSelectExpectedCostFuel, randSelectExpectedCost_zero]
      | cons x xs =>
          let ys := x :: xs
          let X : Nat → Real := fun i =>
            match selectByRank? i ys with
            | none => 0
            | some pivot =>
                if k < ltCount pivot ys then
                  randomizedSelectExpectedCostFuel fuel c k
                    (ys.filter fun y => decide (y < pivot))
                else if k < leCount pivot ys then
                  0
                else
                  randomizedSelectExpectedCostFuel fuel c
                    (k - leCount pivot ys)
                    (ys.filter fun y => decide (pivot < y))
          let Y : Nat → Real := fun i =>
            randSelectExpectedCost c (max i (xs.length - i))
          have hterm : ∀ i ∈ Finset.range ys.length, X i ≤ Y i := by
            intro i hi
            have hiLt : i < ys.length := Finset.mem_range.mp hi
            rcases selectByRank?_isSome_of_lt hiLt with ⟨pivot, hpivot⟩
            simp only [X, hpivot]
            by_cases hlo : k < ltCount pivot ys
            · simp only [hlo, if_pos]
              have hsize :=
                freshRandomizedSelectContinuationSize_le_subproblemSize
                  (k := k) (i := i) (xs := ys) hiLt
              have hlen :
                  (ys.filter fun y => decide (y < pivot)).length ≤
                    max i (xs.length - i) := by
                change ltCount pivot ys ≤ max i (xs.length - i)
                simpa [freshRandomizedSelectContinuationSize, hpivot, hlo,
                  subproblemSize, ys] using hsize
              exact le_trans (ih c k _)
                (randSelectExpectedCost_monotone c (by positivity) hlen)
            · by_cases hmid : k < leCount pivot ys
              · simp only [hlo, hmid, if_false, if_true]
                exact randSelectExpectedCost_nonneg c (by positivity) _
              · simp only [hlo, hmid, if_false]
                have hsize :=
                  freshRandomizedSelectContinuationSize_le_subproblemSize
                    (k := k) (i := i) (xs := ys) hiLt
                have hlen :
                    (ys.filter fun y => decide (pivot < y)).length ≤
                      max i (xs.length - i) := by
                  change gtCount pivot ys ≤ max i (xs.length - i)
                  simpa [freshRandomizedSelectContinuationSize, hpivot, hlo,
                    hmid, subproblemSize, ys] using hsize
                exact le_trans (ih c (k - leCount pivot ys) _)
                  (randSelectExpectedCost_monotone c (by positivity) hlen)
          have hExpect :
              Probability.expect ys.length X ≤
                Probability.expect ys.length Y := by
            unfold Probability.expect
            apply div_le_div_of_nonneg_right
            · exact Finset.sum_le_sum hterm
            · positivity
          rw [randomizedSelectExpectedCostFuel]
          change (c : Real) * (ys.length : Real) +
              Probability.expect ys.length X ≤
            randSelectExpectedCost c (xs.length + 1)
          rw [randSelectExpectedCost_recurrence]
          have hadd := add_le_add_left hExpect ((c : Real) * (ys.length : Real))
          simpa [Y, ys, Nat.cast_add, Nat.cast_one] using hadd

Fresh per-recursion RANDOMIZED-SELECT has expected cost at most 4 * c * n under the explicit local charge c * currentLength.

theorem randomizedSelectExpectedCost_linear_bound
    (c k : Nat) (xs : List Nat) :
    randomizedSelectExpectedCost c k xs ≤
      4 * c * (xs.length : Real) := by
  unfold randomizedSelectExpectedCost
  exact le_trans
    (randomizedSelectExpectedCost_le_randSelectExpectedCost xs.length c k xs)
    (randSelectExpectedCost_le c (by positivity) xs.length)

The actual recursive continuation selected at pivot rank i is bounded by the larger-side term max i (n-1-i) used in the CLRS majorizing recurrence. Consequently the fresh-choice stochastic execution has expected comparison cost at most 4n.


theorem freshRandomizedSelectExpectedComparisonsFuel_linear_bound :
    ∀ (fuel k : Nat) (xs : List Nat),
      freshRandomizedSelectExpectedComparisonsFuel fuel k xs ≤
        4 * (xs.length : ℝ) := by
  intro fuel
  induction fuel with
  | zero =>
      intro k xs
      simp [freshRandomizedSelectExpectedComparisonsFuel]
  | succ fuel ih =>
      intro k xs
      cases xs with
      | nil =>
          simp [freshRandomizedSelectExpectedComparisonsFuel]
      | cons x xs =>
          let ys := x :: xs
          let X : Nat → ℝ := fun i =>
            match selectByRank? i ys with
            | none => 0
            | some pivot =>
                if k < ltCount pivot ys then
                  freshRandomizedSelectExpectedComparisonsFuel fuel k
                    (ys.filter fun y => decide (y < pivot))
                else if k < leCount pivot ys then
                  0
                else
                  freshRandomizedSelectExpectedComparisonsFuel fuel
                    (k - leCount pivot ys)
                    (ys.filter fun y => decide (pivot < y))
          have hterm : ∀ i ∈ Finset.range ys.length,
              X i ≤ 4 * ((max i (xs.length - i) : Nat) : ℝ) := by
            intro i hi
            have hiLt : i < ys.length := Finset.mem_range.mp hi
            rcases selectByRank?_isSome_of_lt hiLt with ⟨pivot, hpivot⟩
            have hrank : RankCertificate ys i pivot :=
              selectByRank?_rankCorrect hpivot
            simp only [X, hpivot]
            by_cases hlo : k < ltCount pivot ys
            · simp only [hlo, if_pos]
              have hrec := ih k (ys.filter fun y => decide (y < pivot))
              have hsize :
                  (ys.filter fun y => decide (y < pivot)).length ≤
                    max i (xs.length - i) := by
                exact le_trans hrank.2.1 (Nat.le_max_left _ _)
              have hcast :
                  4 * ((ys.filter fun y => decide (y < pivot)).length : ℝ) ≤
                    4 * ((max i (xs.length - i) : Nat) : ℝ) := by
                exact_mod_cast Nat.mul_le_mul_left 4 hsize
              exact le_trans hrec hcast
            · by_cases hmid : k < leCount pivot ys
              · simp [hlo, hmid]
              · simp only [hlo, hmid, if_false]
                have hrec := ih (k - leCount pivot ys)
                  (ys.filter fun y => decide (pivot < y))
                have hhigh : gtCount pivot ys ≤ xs.length - i := by
                  rw [gtCount_eq_length_sub_leCount]
                  have hirank : i < leCount pivot ys := hrank.2.2
                  have hlenys : ys.length = xs.length + 1 := by simp [ys]
                  omega
                have hsize :
                    (ys.filter fun y => decide (pivot < y)).length ≤
                      max i (xs.length - i) := by
                  exact le_trans hhigh (Nat.le_max_right _ _)
                have hcast :
                    4 * ((ys.filter fun y => decide (pivot < y)).length : ℝ) ≤
                      4 * ((max i (xs.length - i) : Nat) : ℝ) := by
                  exact_mod_cast Nat.mul_le_mul_left 4 hsize
                exact le_trans hrec hcast
          have hsum :
              (∑ i ∈ Finset.range ys.length, X i) ≤
                4 * (∑ i ∈ Finset.range ys.length,
                  ((max i (xs.length - i) : Nat) : ℝ)) := by
            calc
              (∑ i ∈ Finset.range ys.length, X i) ≤
                  ∑ i ∈ Finset.range ys.length,
                    4 * ((max i (xs.length - i) : Nat) : ℝ) :=
                Finset.sum_le_sum hterm
              _ = 4 * (∑ i ∈ Finset.range ys.length,
                    ((max i (xs.length - i) : Nat) : ℝ)) := by
                rw [Finset.mul_sum]
          have hmax :
              4 * (∑ i ∈ Finset.range ys.length,
                  ((max i (xs.length - i) : Nat) : ℝ)) ≤
                3 * (ys.length : ℝ) ^ 2 := by
            simpa [ys, Nat.cast_add, Nat.cast_one] using
              sum_maxSide_real_bound xs.length
          have hsumBound :
              (∑ i ∈ Finset.range ys.length, X i) ≤
                3 * (ys.length : ℝ) ^ 2 := le_trans hsum hmax
          have hlenPos : (0 : ℝ) < (ys.length : ℝ) := by
            have hnat : 0 < ys.length := by simp [ys]
            exact_mod_cast hnat
          have hfrac :
              (∑ i ∈ Finset.range ys.length, X i) / (ys.length : ℝ) ≤
                3 * (ys.length : ℝ) := by
            apply (div_le_iff₀ hlenPos).2
            nlinarith
          change (ys.length : ℝ) + Probability.expect ys.length X ≤
            4 * (ys.length : ℝ)
          unfold Probability.expect
          linarith

Fresh-choice RANDOMIZED-SELECT has expected linear comparison cost on every input and requested rank: E[C] ≤ 4n.

theorem freshRandomizedSelectExpectedComparisons_linear_bound
    (k : Nat) (xs : List Nat) :
    freshRandomizedSelectExpectedComparisons k xs ≤ 4 * (xs.length : ℝ) := by
  exact freshRandomizedSelectExpectedComparisonsFuel_linear_bound xs.length k xs

Rank correctness via a randomized pivot oracle

Pivot oracle that selects the element at a designated index, reusing the pivot-parametric SELECT skeleton of Section 9.3. Fixing one index does not by itself model fresh random choices across recursive calls.

def pivotAtIndex? (i : ℕ) (xs : List ℕ) : Option ℕ := xs[i]?

The index pivot oracle only ever returns members of its input list.

theorem pivotAtIndex?_mem (i : ℕ) : PivotMembership (pivotAtIndex? i) := by
  intro xs pivot hsel
  rcases getElem?_eq_some_iff_split.mp hsel with ⟨lo, hi, rfl, _hlen⟩
  simp

SELECT with the pivot chosen at a fixed index i, obtained by instantiating the pivot-parametric selector CLRS.Chapter09.selectWithPivot?. This is a deterministic specialization used only for conditional rank correctness; it does not model the fresh per-call choices of RANDOMIZED-SELECT.

def randomizedSelectAtIndex? (i k : ℕ) (xs : List ℕ) : Option ℕ :=
  selectWithPivot? (pivotAtIndex? i) k xs

Rank correctness of the fixed-index specialization is inherited from the pivot-parametric skeleton: any successful result is a valid zero-based order statistic.

theorem randomizedSelectAtIndex?_rankCorrect {i k : ℕ} {xs : List ℕ} {x : ℕ}
    (hsel : randomizedSelectAtIndex? i k xs = some x) :
    RankCertificate xs k x :=
  selectWithPivot?_rankCorrect (pivotAtIndex? i) (pivotAtIndex?_mem i)
    (by simpa [randomizedSelectAtIndex?] using hsel)

Membership projection for the randomized selector.

theorem randomizedSelectAtIndex?_mem {i k : ℕ} {xs : List ℕ} {x : ℕ}
    (hsel : randomizedSelectAtIndex? i k xs = some x) :
    x ∈ xs :=
  (randomizedSelectAtIndex?_rankCorrect hsel).1

end Chapter09end CLRS

Scope and implementation notes

Imports

import CLRSLean.FourthEdition.Chapter_09.Section_09_1_Minimum_And_Maximum
import CLRSLean.FourthEdition.Chapter_09.Section_09_2_Selection_In_Expected_Linear_Time
import CLRSLean.FourthEdition.Chapter_09.Section_09_3_Selection_In_Worst_Case_Linear_Time
import CLRSLean.FourthEdition.Chapter_09.Section_09_3_Selection_In_Worst_Case_Linear_Time.Randomized_Select

Native fourth-edition chapter guide.

Current source

This guide sources fourth-edition §9.1–§9.3 from the native section modules under CLRSLean.FourthEdition.Chapter_09. Declarations retain the CLRS.Chapter09 namespace; the legacy import CLRSLean.Chapter_09 and its Section_09_* modules forward to these sources during the compatibility period.

Chapter 9 is structurally represented by Sections 9.1--9.3. Section 9.1 is complete for the simultaneous pairwise minimum/maximum algorithm and the CLRS 3 * floor(n / 2) comparison bound. Sections 9.2 and 9.3 are complete for the advertised functional and comparison-cost models: RANDOMIZED-SELECT has a schedule-driven path cost, fresh per-call uniform choices, a bridge to the CLRS larger-side majorizer, and expected partition-work cost at most 4 * c * n; recursive median-of-medians SELECT has an end-to-end cost at most 100n.

Sections

9.1 proves simultaneous minimum/maximum correctness and the pairwise comparison bound.
9.2 proves duplicate-aware rank selection, pivot-style SELECT correctness, schedule-cost erasure, and the fresh-choice randomized expected-cost bridge.
9.3 proves recursive median-of-medians SELECT correctness and its complete worst-case comparison bound.

Closure interface

The chapter's main public results are CLRS.Chapter09.minMax?_correct, CLRS.Chapter09.minMax?_comparisons_le, CLRS.Chapter09.randomizedSelectCostWithSchedule_rankCorrect, CLRS.Chapter09.randomizedSelectExpectedCostFuel_succ, CLRS.Chapter09.randomizedSelectExpectedCost_le_randSelectExpectedCost, CLRS.Chapter09.randomizedSelectExpectedCost_linear_bound, CLRS.Chapter09.recursiveMedianOfMediansSelect?_correct, and CLRS.Chapter09.recursiveMedianOfMediansComparisonCost_linear_bound. The proof map records the supporting theorem inventory.

Completion boundary

The chapter is complete for pure functional correctness and CLRS comparison costs. The RANDOMIZED-SELECT metric charges only c * currentLength; it does not charge the internal specification implementation of selectByRank?, random-number generation, list primitives, or RAM operations, and it does not identify the nested process with a flat distribution on variable-length schedules. Mutable arrays, in-place partitioning, a concrete RNG, and hardware-level accounting are later implementation refinements and do not reopen this theorem boundary.

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

CLRS, fourth edition · Chapter 9 of 35

9.1. Minimum and Maximum

Executable pairwise algorithm

Local correctness lemmas

Public specification and comparison bound

9.2. Selection in Expected Linear Time

Randomized SELECT theorem page

Specification selector and rank certificate

List lemmas for the rank proof

Pivot-style selection

Selection correctness

9.3. Selection in Worst-Case Linear Time

Shared source support

Pivot-parametric selection

Five-element median certificate

Executable five-element grouping

Deterministic median-pivot instance

Median-of-medians pivot instance

Recursive median-of-medians pivot

Recurrence-size wrappers

Full recurrence induction

Recursive median-of-medians selector

Concrete executable cost semantics

End-to-end recursive median-of-medians comparison cost

Definitions and proofs

CLRSLean.FourthEdition.Chapter_09.Section_09_3_Selection_In_Worst_Case_Linear_Time.Randomized_Select

CLRS Section 9.2 - Randomized SELECT expected running time

Subproblem size and the expected-cost model

The expected-comparison recurrence (derived from the model)

Nonnegativity

The max-side sum and its 3n²/4 bound

The linear expected-time bound (CLRS Theorem 9.2)

Fresh-choice RANDOMIZED-SELECT semantics

Schedule-driven concrete cost semantics

Rank correctness via a randomized pivot oracle

Scope and implementation notes

Current source

Sections

Closure interface

Completion boundary

The max-side sum and its `3n²/4` bound