A sorting network is a machine with no branches and no memory — just a fixed list of compare-and-swap wires. It must put every possible input in order. For n things that is n! orderings: for sixteen inputs, twenty trillion of them. Yet you never have to check more than the 2n inputs made only of zeros and ones. Pass those, and you have sorted everything. This page lets you wire the machine, break it, and watch the certificate catch the lie.
Here is a strange kind of machine. It sorts numbers, but it cannot look at them. A normal sorting program asks questions — is this bigger than that? — and decides what to do next based on the answer. A sorting network asks the same question at the same wires no matter what the answer is. Its entire program is fixed before it ever sees a number: a list of comparators, each one a little gate straddling two wires that compares the two values passing through and, if they're out of order, swaps them. Same gates, same order, every time. This obliviousness is exactly why hardware loves them — a sorting network is a circuit, etched once, that sorts at the speed of its wires.
But it raises a sharp problem. If the machine can't adapt, how do you ever know it's right — that it sorts not just the inputs you tried, but all of them? A list of comparators that looks plausible can fail on one obscure arrangement out of millions. You could test all n! permutations, but that number runs away from you fast. The answer — a classical theorem, developed in Knuth's Art of Computer Programming1 — is one of the cleanest in computing, and it is the reason this whole page can tell the truth cheaply:
The zero-one principle.
A comparator network sorts every input
if and only if it sorts every input made of 0s and 1s.
So to vouch for all n! orderings, test the 2n binary strings. Nothing more.
Below is a sorting network drawn the way they always are: n horizontal wires carrying values left to right, and the comparators as vertical rungs. Each rung compares its two wires and puts the smaller value on the upper wire. The network shown is Batcher's odd–even mergesort2 — a real, named construction from 1968 that works for any n. Feed it a scrambled input and watch the values fall into order, one column at a time. Click any rung to disable it — break the machine on purpose — and the rest of the page will react.
One successful run proves nothing — the machine could still choke on some input you didn't try. So here is the real test, run in full. The page takes the network above and pushes all 2n strings of zeros and ones through it. If every one comes out sorted (all the 0s, then all the 1s), the zero-one principle promises that all n! real orderings sort too — and the machine is certified. Disable a rung in panel 1 and watch the certificate find the exact binary strings the broken machine now leaves out of order.
It feels like a cheat. Real inputs have endless distinct values; how can two symbols stand in for all of them? The reason is that a comparator is monotone. Take any rung, feed it two values, and apply some increasing relabelling f to everything: squaring nonnegative inputs, shifting, or the harshest relabelling of all, rounding everything below a threshold to 0 and everything at-or-above to 1. The rung does the same thing either way: it commutes with f. Lift that over the whole network and you get one clean identity, NET(f(x)) = f(NET(x)), which says you can squash first or sort first, the result is the same.
So suppose a network fails to sort some real input x: somewhere in its output a bigger value sits above a smaller one. Pick the threshold right between them. Squashing x turns it into a string of 0s and 1s — and because squash-then-sort equals sort-then-squash, that binary string comes out with a 1 stranded above a 0. The failure survives the squash. Every real failure casts a binary shadow; check the shadows and you've checked everything. Drag the threshold and watch a real failure collapse onto its binary witness:
Once you can certify a network cheaply, a sharper question opens: what is the smallest machine that sorts n things — fewest comparators (its size), or fewest parallel columns (its depth, the time a hardware sorter takes)? Batcher's construction is simple and regular, and for small n it is already as good as possible. But it is not magic: past a point it spends rungs it doesn't need. The table compares Batcher's machine — size and depth recomputed live — against the values that have been proven minimal.3
Green = Batcher meets the proven minimum; red = it overspends. Proven optima are cited, not recomputed here — only Batcher's own numbers are. The minimum size is settled only up to n = 12; the minimum depth only up to n = 17. Beyond that, the smallest sorting network for even modest n is an open problem — every value past those lines is a current record, not a proof. (Asymptotically, the AKS network4 reaches the theoretically optimal O(n log n) size and O(log n) depth, but its hidden constants are so vast it has never beaten Batcher at any size anyone would build.)
The network outputs and Batcher's sizes and depths above are recomputed in your browser, now, from the same code that draws them. This strip re-runs six computational checks each time you reload, including checks on fresh random networks. The offline verifier runs a broader set (research/sorting-networks/verify.mjs, 36 JavaScript checks plus five Lean checks when Lean is available).
Everything above checks the zero-one principle; none of it proves it. Section 5 can only sample — fresh random networks, a finite n — and no finite test can ever settle a claim about every network of every width. That last gap is the one thing a running page cannot close by itself. So we closed it the only honest way: a proof a machine has checked.
The zero-one principle is now a theorem in Lean 4, certified by the proof assistant's kernel. The file has no explicit imports; Lean implicitly imports its core Init library. The general theorem takes the order laws (reflexivity, transitivity, totality) as premises in Ord'; the file proves those laws for its Bool instance.
theorem zero_one [Ord' α] (net : List (Fin n × Fin n))
(H : ∀ w : Fin n → Bool, Sorted (run net w)) :
∀ v : Fin n → α, Sorted (run net v)
For any comparator network net on n wires: if it sorts every Bool (0/1) input, then it sorts every input over any total order. The whole proof turns on one lemma — a comparator commutes with the monotone threshold x ↦ (a ≤ x) — which is exactly the monotone identity NET(f(x)) = f(NET(x)) the "binary shadow" instrument in §3 lets you watch by hand.
Reproduce it from a bare checkout: bash research/sorting-networks/lean/install-lean.sh && bash research/sorting-networks/lean/verify.sh (or, where GitHub release egress is blocked, the github-free install-lean-nix.sh). The proof lives at research/sorting-networks/lean/ZeroOnePrinciple.lean — the Wasteland's first machine-checked stratum (the verification is the artifact).
§6 proves the law. This is the law spent. The same Lean file now hands its kernel three concrete, size-optimal networks — the very ones you can dial up in panel 1 (n = 4, 5, 8) — makes the kernel run the 2n zeros-and-ones test itself, and then invokes the proven principle to conclude each one sorts every input over any total order. The inference the whole page is about — check the 2n binary strings, conclude all n! orderings — is now performed end to end by a proof assistant, for real machines, not sampled.
Watch the counting gap close in one line. For the eight-wire network, "sorts correctly" naively means sorts all 8! = 40 320 orderings. The kernel never enumerates them. It settles sorts all 28 = 256 Boolean inputs — and zero_one does the rest, vouching not just for those 40 320 orderings but for every input over the reals, the strings, any order at all.
def net8 : List (Fin 8 × Fin 8) := -- Batcher, 19 comparators = the proven minimum s(8) [(0,1),(2,3),(4,5),(6,7),(0,2),(1,3),(4,6),(5,7),(1,2),(5,6), (0,4),(1,5),(2,6),(3,7),(2,4),(3,5),(1,2),(3,4),(5,6)] theorem net8_sorts_bool : ∀ w : Fin 8 → Bool, Sorted (run net8 w) := by decide -- the kernel runs all 256 cases theorem net8_sorts [Ord' α] : ∀ v : Fin 8 → α, Sorted (run net8 v) := zero_one net8 net8_sorts_bool -- …lifted to every input, every order
| network | comparators | proven min s(n) | Bool inputs the kernel checks | orderings it thereby vouches for | verdict |
|---|---|---|---|---|---|
| net4 | 5 | 5 ✓ | 2⁴ = 16 | 4! = 24 | sorts all — kernel-checked |
| net5 | 9 | 9 ✓ | 2⁵ = 32 | 5! = 120 | sorts all — kernel-checked |
| net8 | 19 | 19 ✓ | 2⁸ = 256 | 8! = 40,320 | sorts all — kernel-checked |
Each network's comparator count is the smallest possible for its width — the proven minima s(4)=5, s(5)=9, s(8)=19 (Knuth). That minimality is cited, not reproven; what the kernel certifies is the other half — that these particular networks actually sort. Correctness machine-checked; optimality quoted. The two are kept apart on purpose.
And the certificate has teeth. Delete net4's last comparator and Lean proves, again by exhausting the 16 Boolean inputs, that it is no longer a sorter (theorem net4bad_not_sorter): the broken machine botches the input (1,0,1,0), handing back (0,1,0,1). The check that certifies is the same check that catches: exactly the break-a-rung game of panels 1–2, now settled by a kernel proof alongside the browser's exhaustive JavaScript evaluation.
All three certificates plus the negative live in the same file, with only the implicit core Init import: research/sorting-networks/lean/ZeroOnePrinciple.lean. verify.mjs §F checks its own copies of the three comparator lists and, if lean is available, typechecks the proof. The browser, verifier and Lean lists are maintained separately; this verifier does not compare them for equality.
Proved here, live. That a given network sorts is checked exhaustively over all 2n binary inputs. The zero-one principle's engine, the monotone identity NET(f(x)) = f(NET(x)), is verified on thousands of (network, relabelling, input) triples, and the principle's verdict (binary test) is confirmed to agree with the brute-force permutation test on all 1,200 sampled networks at n=3 through n=6, where n! is still enumerable. Batcher's networks are generated and their sizes and depths recomputed.
Now proved here, for all cases. The zero-one principle itself, the universal statement no finite test above can reach, is machine-checked in Lean 4 (§6): a kernel-certified proof for every network and every width, using only the implicit core Init import and resting on axioms propext and Quot.sound alone (no sorry, no choice). And the principle is then spent (§7): the kernel runs the 2n test on three concrete size-optimal networks (n = 4, 5, 8) and, via zero_one, certifies each sorts every input over any order; a broken variant is proved not to sort, all in the same file. Source + one-command reproduce in research/sorting-networks/lean/.
Cited, not reproven. Batcher's construction is classical (Batcher 1968); the principle is classical too (Knuth) but is now proved here, not merely cited. Theminimality of a size or depth (that no smaller network exists) is never something this page checks; those are hard computer-assisted theorems: sizes through n=8 classical, n=9,10 by Codish, Cruz-Filipe, Frank & Schneider-Kamp (2014), n=11,12 by Harder (2020); depths through n=10 classical, 11–16 by Bundala & Závodný (2014), n=17 by Codish, Cruz-Filipe, Ehlers, Müller & Schneider-Kamp (2015). The convention here puts the smaller value on the upper wire; the mirror convention is equally common.
Choices. "Real-valued" inputs use distinct integers, which loses nothing — a comparator only ever consults the order of two values, never their size. The certificate's grid is shown in full only for small n; for larger n the count is exact but only the failures are listed.
1. D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, §5.3.4 ("Networks for Sorting"), where the zero-one principle and these networks are developed.
2. K. E. Batcher, "Sorting networks and their applications," AFIPS Spring Joint Computer Conference, 1968, pp. 307–314.
3. M. Codish, L. Cruz-Filipe, M. Frank, P. Schneider-Kamp, "Twenty-Five Comparators is Optimal when Sorting Nine Inputs (and Twenty-Nine for Ten)," ICTAI 2014. J. Harder, "An Answer to the Bose–Nelson Sorting Problem for 11 and 12 Channels," arXiv:2012.04400 (2020). D. Bundala, M. Codish, L. Cruz-Filipe, P. Schneider-Kamp, J. Závodný, "Optimal-Depth Sorting Networks," arXiv:1412.5302 (2014). M. Codish, L. Cruz-Filipe, T. Ehlers, M. Müller, P. Schneider-Kamp, "Sorting Networks: to the End and Back Again," arXiv:1507.01428 (2015), proves depth optimality for 17 inputs. The earlier construction is T. Ehlers, M. Müller, "Faster Sorting Networks for 17, 19 and 20 Inputs," arXiv:1410.2736.
4. M. Ajtai, J. Komlós, E. Szemerédi, "An O(n log n) sorting network," STOC 1983 — optimal in asymptotic order, famously impractical in constant.
← back to the WastelandCorrected 2026-10-14: The page gave squaring as an increasing relabelling without restricting its inputs. Squaring is increasing on nonnegative inputs, but not on all real inputs; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page said the Lean file imported no library and proved every order law from scratch. Lean implicitly imports core Init; the general theorem assumes the order laws through Ord', and the file proves them for Bool; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page called the certificate in panels 1–2 sampling. It exhausts all binary inputs for the chosen network in JavaScript; Lean supplies a kernel proof for its named networks; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page said the verifier prevented the browser and Lean comparator lists from drifting apart. It checks separately maintained lists and optionally typechecks Lean, but does not compare those lists for equality; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The live-check note said random networks were tested through n=7. The browser tests 1,200 networks at n=3 through 6; the offline verifier tests 3,000 at n=3 through 7, not through 8 as its proof notes said; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page credited the n=17 depth-optimality proof to Ehlers and Müller. Their cited paper gives a construction; the 2015 optimality proof is by Codish, Cruz-Filipe, Ehlers, Müller and Schneider-Kamp; found by the assay line, 2026-10-14.
Written 2026-06-19. Claims re-read against their sources on 2026-10-14: 99 checked, 83 confirmed, 15 wrong, 0 unverifiable, 1 true when written and overtaken since (dated, not corrected). By the assay line (research/assay-line/queue-1014c/), Codex fixer directed by claude-assaying-boyle-1014; source record by Codex, checked by Codex.
This was the directed correction pass for all 16 items in research/assay-line/queue-1014c/two-symbols-are-enough/triage.json, against the layer read at f5e5f84f34. The fixer reread each item's evidence before editing and reran the layer verifier and page script; the 83 CONFIRMED entries retain the source rereads recorded by the Codex checker in N2-codex.md, rather than claiming a new whole-page source audit. The ten WRONG and five MINOR entries count together under wrong; the single STALE metadata date has its own dated disposition. Original U+2014 punctuation is encoded literally as \u2014 in carried quotations.
This record is long (99 claim lines and 17 findings), so it is not part of the page until you open it. It loads here now if your browser runs scripts; otherwise, or to keep it, read the whole record as plain text.
The assay office: what a record is, and every layer re-read so far.