Sorting

Sorting is the rearrangement of numbers (or other orderable objects) in a list into their correct lexicographic order. Alphabetization is therefore a form of sorting. Because of the extreme importance of sorting in almost all computer algorithms and database applications, a great deal of effort has been expended in the creation and analysis of efficient sorting algorithms. A number of common sorting algorithms include heapsort, merge sort, quicksort, selection sort, and shellsort.

The following table summarizes the number of comparisons or elementary operations used by several comparison sorts, which determine order by comparing pairs of items, on items. The bounds suppress constant factors and lower-order terms. The base of the logarithm is immaterial in these big-O bounds because changing the base multiplies the logarithm by a constant. Quicksort's quadratic worst case can be avoided with suitable randomization or pivot safeguards, while shellsort bounds depend on the chosen gap sequence.

algorithm	best case	average case	worst case
heapsort
merge sort
quicksort
selection sort

For distinct keys, a correct comparison sorter must distinguish all possible total orders. The resulting worst-case lower bound on the depth of the binary tree of comparisons is , where denotes the ceiling function (Knuth 1998).

Nash (2026a) reports a deterministic online adversary that is initialized using only and keeps its answers jointly consistent with some total order. It uses a fixed polynomial number of bit operations per query and forces every correct comparison sorter on distinct keys to make comparisons as . Nash attributes the adversary and its analysis to GPT-6 Astra and reports human review of the main text. The appendices are identified as AI-generated and excluded from that review. The continuous-position argument is accompanied by finite checks of selected identities. The Lean development for the earlier integer-color construction verifies the asymptotic guarantee and a polynomial cost bound in an explicit bit-work model (Nash 2026b). The public Lean development now also formalizes the continuous adversary's consistency, asymptotic comparison bound, and polynomial initialization and query costs in an explicit arithmetic cost model (Nash 2026c). Its reported continuous integration checks include a build, kernel replay with leanchecker, and an audit admitting only Lean's standard logical axioms. These are formal cost charges rather than a timing bound for executing the Lean implementation.