Selecting the 7th Smallest of 16 Elements Takes Exactly 28 Comparisons
Jonathan Cremer
cs.DS
Oct 13, 2026 · v1
math.CO
TL;DR
Lean 4 kernel-checks the decision-graph certificates for all seven new selection upper bounds; a separate Mathlib-based development formalizes the partial-order leaf lower bound.
Abstract
Let $V_i(n)$ denote the minimum worst-case number of comparisons needed to find the $i$-th smallest of $n$ distinct elements. We construct algorithms showing $V_7(16)\le28$ and $V_8(16)\le29$, improving the previously reported upper bounds of 30 and 31. Together with known lower bounds, these results establish $V_7(16)=28$ and leave $V_8(16)\in\{28,29\}$. For 17 elements, we establish $V_5(17)=27$ and improve the upper bounds for ranks 6 through 9 to 29, 30, 31, and 31, respectively. Every new upper bound has an explicit decision-graph certificate verified by a static checker developed independently of the search. We also derive a lower bound for selection from a partially ordered state by combining the Fussenegger-Gabow weight with its order-reversed counterpart. All new upper bounds and this lower bound are formally verified in Lean 4. For $V_8(16)$, we show that a lower bound based solely on the total number of decision-tree leaves cannot establish $V_8(16)\ge29$. The algorithms were found using fixed-budget search, information-guided comparison ordering, and proof-number search. Proof-number search was decisive in finding the 28-comparison algorithm; in our experiments, refuting a comparison budget remained substantially more expensive than finding an algorithm within it.
Problem
V_i(n) is the minimum worst-case number of comparisons needed to find the i-th smallest of n elements. The entries V_7(16) and V_8(16) were open, with ranges 28–30 and 28–31, and several 17-element entries had wide gaps.
Approach
Selection algorithms were found as decision-graph certificates (Rust programs) using fixed-budget search, information-guided comparison ordering, and proof-number search. A static checker that shares no code with the search verifies each certificate. Lean 4 proofs using only the core library verify the translated certificates. A second, Mathlib-based Lean development formalizes a new lower bound that combines the Fussenegger–Gabow weight with its order-reversed counterpart, for all finite strict partial orders.
Results
The results establish V_7(16)=28, V_8(16)∈{28,29}, and V_5(17)=27, and lower the upper bounds for ranks 6–9 of 17 elements to 29, 30, 31 and 31. A leaf-count argument alone cannot prove V_8(16)≥29. Proof-number search was decisive in finding the 28-comparison algorithm.
| i | 5 | 6 | 7 | 8 |
|---|
| before | 26 | 27 | 28–30 | 28–31 |
| this paper | 26 | 27 | 28 | 28–29 |
Row n=16 of the selection table (previous vs. new)
