---
slug: two-symbols-are-enough
passed: 2026-10-14
by: the assay line (research/assay-line/queue-1014c/), Codex fixer directed by claude-assaying-boyle-1014; source record by Codex, checked by Codex
checked: 99
confirmed: 83
wrong: 15
unverifiable: 0
observed: 0
stale: 1
---

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.

## Claims

- WRONG | X1 [unrestricted-squaring] Take any rung, feed it two values, and apply some increasing relabelling f to everything \u2014 squaring, shifting, or the harshest relabelling of all, rounding everything below a threshold to 0 and everything at-or-above to 1. | https://bobson.ludost.net/books/algo/book6/chap28.htm; git show f5e5f84f34:research/sorting-networks/verify.mjs:106; recreated: node audit-page.cjs | CLRS Lemma 28.1 requires a nondecreasing map. For the page comparator and input [-2,-1], squaring gives NET(square(x))=[1,4] but square(NET(x))=[4,1]. Squaring is increasing on nonnegative inputs. The verifier already restricted this test to nonnegative ranks.
- MINOR | X2 [all-checks-recomputed-live] Everything above is recomputed in your browser, now, from the same code that draws it. | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:161; git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:383 | The browser computes network outputs and Batcher sizes/depths. OPT_SIZE and OPT_DEPTH are literal cited tables; the six live checks do not reprove their optimality. The revised sentence names the computed results and distinguishes the broader offline checks.
- WRONG | X3 [lean-no-imports] The file imports nothing \u2014 not even a standard library \u2014 so the only thing trusted is Lean's type checker itself; every order law it uses (reflexivity, transitivity, totality) is proved from scratch inside it. | git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:20; https://raw.githubusercontent.com/leanprover/lean4/v4.30.0/src/Lean/Elab/Import.lean; recreated: lean --deps ZeroOnePrinciple.lean | The proof has no prelude or explicit imports. Lean import processing adds core Init; local lean --deps confirms Init.olean. Ord' declares refl/trans/total as premises, while the Bool instance proves them locally. The five theorem axiom footprints still pass.
- WRONG | X4 [exhaustive-check-called-sampling] The check that certifies is the same check that catches \u2014 exactly the break-a-rung game of panels 1–2, now settled by the kernel rather than by sampling. | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:309; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:227 | runCertificate enumerates binaries(N) for every selected network. The Lean negative theorem uses by decide. These are exhaustive JavaScript evaluation and a kernel proof, respectively; the browser certificate is not a sample of binary inputs.
- WRONG | X5 [network-drift-guarantee] verify.mjs §F recomputes the identical comparator lists (and, if lean is on PATH, typechecks the proof live) so the browser check and the machine proof cannot drift apart. | git show f5e5f84f34:research/sorting-networks/verify.mjs:241; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:207; recreated: node mutation/research/sorting-networks/verify.mjs; mutation-run.txt | Section F uses its own CERT literals. The optional Lean branch typechecks the separate proof and checks axiom output; it never compares the Lean, browser and CERT comparator lists. Current browser and Lean lists match for n=4,5,8, but that equality is not enforced by this verifier.
- WRONG | X6 [live-width-seven] the principle's verdict (binary test) is confirmed to agree with the brute-force permutation test on every random network up to n=7, where n! is still enumerable. | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:409; git show f5e5f84f34:research/sorting-networks/verify.mjs:135 | The live loop uses n=3 through 6, 300 trials each: 1,200 networks. The offline loop uses n=3 through 7, 600 trials each: 3,000. The browser smoke check and offline verifier reproduce those totals. Related comments claiming an offline upper limit of 8 were corrected to 7.
- WRONG | X7 [lean-no-imports] The zero-one principle itself \u2014 the universal statement no finite test above can reach \u2014 is machine-checked in Lean 4 (§6): a kernel-certified proof for every network and every width, importing no library and resting on axioms propext and Quot.sound alone (no sorry, no choice). | git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean; https://raw.githubusercontent.com/leanprover/lean4/v4.30.0/src/Lean/Elab/Import.lean; recreated: lean --deps ZeroOnePrinciple.lean | Lean v4.30.0 import processing and local Lean 4.35.0 dependencies both establish the implicit core Init import. The universal zero_one theorem and its propext/Quot.sound axiom footprint remain valid. This duplicates X3's dependency error.
- WRONG | X8 [n17-optimality-attribution] n=17 by Ehlers & Müller. | https://arxiv.org/abs/1410.2736; https://arxiv.org/abs/1507.01428 | The 2014 Ehlers/Müller abstract describes improved upper bounds. The 2015 Codish/Cruz-Filipe/Ehlers/Müller/Schneider-Kamp paper establishes depth optimality for 17 inputs. The attribution now names those five authors and links arXiv:1507.01428; the earlier construction credit is retained.
- MINOR | X9 [bundala-authors-incomplete] D. Bundala, J. Závodný, "Optimal-Depth Sorting Networks," arXiv:1412.5302 (2014). | https://arxiv.org/abs/1412.5302 | The arXiv:1412.5302 author list contains Daniel Bundala, Michael Codish, Luís Cruz-Filipe, Peter Schneider-Kamp and Jakub Závodný. The citation now lists all five. The earlier two-author historical research attribution remains supported.
- WRONG | X10 [last-verified-date] Last verified 19 June 2026, when it was written. | git show f5e5f84f34:memory/log.d/2026-07-12T1830Z-sorting-network-certified.md; git log f5e5f84f34 -- public/strata/two-symbols-are-enough/index.html | The July 12 log records 41/41 passing checks. Read-only git history shows the June last-verified sentence was introduced on September 27 in d4840e62371, after that run. This record supplies passed: 2026-10-14; assay/lib.mjs uses record.passed for the generated placard date. Per the triage exception, the shared landing step must regenerate the placard, and no separate correction line is added.
- MINOR | X11 [all-checks-recomputed-live] Every claim recomputed live and offline first (research/sorting-networks/verify.mjs, 41/41) | git show f5e5f84f34:research/sorting-networks/verify.mjs:304; git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:161 | The verifier cites optimality results and conditionally invokes Lean. The dek now describes computational checks, with 36 JavaScript checks plus five Lean checks when available, rather than claiming all assertions were recomputed.
- WRONG | X12 [n17-optimality-attribution] what's proved here (a given network sorts; the monotone identity; the principle's verdict matches brute force up to n=7) is kept honestly apart from what's cited (minimality theorems: Codish et al. 2014; Harder 2020; Bundala–Závodný 2014; Ehlers–Müller). | https://arxiv.org/abs/1410.2736; https://arxiv.org/abs/1507.01428; git show f5e5f84f34:research/sorting-networks/verify.mjs | The offline n=7 limit is supported by its loop. The minimality citation to Ehlers/Müller is not: their paper establishes upper bounds, while arXiv:1507.01428 supplies the five-author depth-optimality proof. The dek now credits that proof and makes the live/offline limits explicit.
- MINOR | X13 [all-checks-recomputed-live] Every check recomputed in your browser. | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:396; git show f5e5f84f34:research/sorting-networks/lean/verify.sh | The browser runs six JavaScript checks; the Lean kernel checks run outside the browser. Both the meta description and JSON-LD now describe browser recomputation of network results.
- MINOR | X14 [blanket-truth-verdict] the page is telling the truth. | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:419; recreated: node audit-page.cjs | The success branch depends only on pass===checks.length. It now says All six checks passed, which the live script smoke check reproduces, instead of issuing a verdict on every statement on the page.
- WRONG | X15 [n17-optimality-attribution] minimality theorems: Codish et al. 2014; Harder 2020; Bundala–Závodný 2014; Ehlers–Müller | https://arxiv.org/abs/1410.2736; https://arxiv.org/abs/1507.01428 | This is the same false minimality attribution as X8/X12. The five-author 2015 paper proves the 17-input depth optimum; the two-author 2014 paper supplies the construction. The shared dek occurrence is corrected once.
- STALE | X16 [stale-date-modified] (added) "dateModified":"2026-06-19" | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:84; git show f5e5f84f34:memory/log.d/2026-07-12T1830Z-sorting-network-certified.md | June 19 was the original page date. The July 12 log records the added concrete-network section and changed dek/checks/seams, so dateModified was left behind. It is now 2026-10-14 for this substantive revision; the JSON-LD exception requires no Updated line.

- CONFIRMED | A sorting network is a machine with no branches and no memory \u2014 just a fixed list of compare-and-swap wires. | https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [no-branches] PDF p.1: "the order of these comparisons is predetermined by the number of inputs to sort and does not depend on their concrete values"; "Each comparator takes the two inputs from its two channels, compares them, and outputs them sorted". The statements concern data-oblivious control, not inability to compare. Opened and read the PDF after UNREADABLE.
- CONFIRMED | It must put every possible input in order. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [must-sort] Theorem 28.2: "If a comparison network with n inputs sorts all 2n possible sequences of 0's and 1's correctly, then it sorts all sequences of arbitrary numbers correctly." The converse follows by restricting the input domain. Superscripts are flattened in the source record.
- CONFIRMED | For n things that is n! orderings: for sixteen inputs, twenty trillion of them. | https://oeis.org/A000142/b000142.txt | N2 source reread, retained in this directed pass: [permutation-count] OEIS b-file: "16 20922789888000". Independently multiplied 1 through 16; twenty trillion is a rounded description of 20,922,789,888,000.
- CONFIRMED | Yet you never have to check more than the 2n inputs made only of zeros and ones. Pass those, and you have sorted everything. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [binary-suffices] Theorem 28.2: "If a comparison network with n inputs sorts all 2n possible sequences of 0's and 1's correctly, then it sorts all sequences of arbitrary numbers correctly." The converse follows by restricting the input domain. Superscripts are flattened in the source record.
- CONFIRMED | It sorts numbers, but it cannot look at them. | https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [cannot-look] PDF p.1: "the order of these comparisons is predetermined by the number of inputs to sort and does not depend on their concrete values"; "Each comparator takes the two inputs from its two channels, compares them, and outputs them sorted". The statements concern data-oblivious control, not inability to compare. Opened and read the PDF after UNREADABLE.
- CONFIRMED | A normal sorting program asks questions \u2014 is this bigger than that? \u2014 and decides what to do next based on the answer. | https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [adaptive-sort] PDF p.1: "the order of these comparisons is predetermined by the number of inputs to sort and does not depend on their concrete values"; "Each comparator takes the two inputs from its two channels, compares them, and outputs them sorted". The statements concern data-oblivious control, not inability to compare. Opened and read the PDF after UNREADABLE.
- CONFIRMED | A sorting network asks the same question at the same wires no matter what the answer is. | https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [fixed-questions] PDF p.1: "the order of these comparisons is predetermined by the number of inputs to sort and does not depend on their concrete values"; "Each comparator takes the two inputs from its two channels, compares them, and outputs them sorted". The statements concern data-oblivious control, not inability to compare. Opened and read the PDF after UNREADABLE.
- CONFIRMED | 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. | https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [comparator-definition] PDF p.1: "the order of these comparisons is predetermined by the number of inputs to sort and does not depend on their concrete values"; "Each comparator takes the two inputs from its two channels, compares them, and outputs them sorted". The statements concern data-oblivious control, not inability to compare. Opened and read the PDF after UNREADABLE.
- CONFIRMED | Same gates, same order, every time. | https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [fixed-order] PDF p.1: "the order of these comparisons is predetermined by the number of inputs to sort and does not depend on their concrete values"; "Each comparator takes the two inputs from its two channels, compares them, and outputs them sorted". The statements concern data-oblivious control, not inability to compare. Opened and read the PDF after UNREADABLE.
- CONFIRMED | This obliviousness is exactly why hardware loves them \u2014 a sorting network is a circuit, etched once, that sorts at the speed of its wires. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [hardware-speed] The excerpt alone defines the hardware components. The surrounding chapter supplies the missing timing model: "each comparator operates in O(1) time" and "the depth of the network therefore equals the time for the network to produce values at all of its output wires". Read as a circuit explanation, not a measured physical propagation speed.
- CONFIRMED | A list of comparators that looks plausible can fail on one obscure arrangement out of millions. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [rare-failure] The source defines correctness "for every input sequence"; testing an individual successful run does not imply this universal condition. The million-order illustration follows once n! exceeds a million, not from a measured failure rate. Broken net4 passes 12 of 16 binary tests, exhibiting why one passing example is insufficient.
- CONFIRMED | You could test all n! permutations, but that number runs away from you fast. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [permutations-test] The source defines correctness "for every input sequence"; testing an individual successful run does not imply this universal condition. The million-order illustration follows once n! exceeds a million, not from a measured failure rate. Broken net4 passes 12 of 16 binary tests, exhibiting why one passing example is insufficient.
- CONFIRMED | a classical theorem, developed in Knuth's Art of Computer Programming | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [knuth-development] Chapter notes: "Knuth [123] contains a discussion of sorting networks and charts their history" and "Knuth attributes the zero-one principle to W. G. Bouricius (1954)". The page says developed in Knuth, not invented by Knuth; the theorem is in section 28.2. Bundala p.2 independently identifies TAOCP vol.3 section 5.3.4.
- CONFIRMED | A comparator network sorts every input if and only if it sorts every input made of 0s and 1s. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [zero-one-iff] Theorem 28.2: "If a comparison network with n inputs sorts all 2n possible sequences of 0's and 1's correctly, then it sorts all sequences of arbitrary numbers correctly." The converse follows by restricting the input domain. Superscripts are flattened in the source record.
- CONFIRMED | So to vouch for all n! orderings, test the 2n binary strings. Nothing more. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [binary-test-size] Theorem 28.2: "If a comparison network with n inputs sorts all 2n possible sequences of 0's and 1's correctly, then it sorts all sequences of arbitrary numbers correctly." The converse follows by restricting the input domain. Superscripts are flattened in the source record.
- CONFIRMED | 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. | https://arxiv.org/pdf/2012.04400 | N2 source reread, retained in this directed pass: [drawing-convention] Harder p.3: "n horizontal wires, one for each channel, numbered from top to bottom" and "for each comparator [i, j] we draw a vertical arrow pointing from i to j". The diagram description is a standard convention, not a prohibition on rotated drawings. PDF opened after UNREADABLE.
- CONFIRMED | Each rung compares its two wires and puts the smaller value on the upper wire. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [smaller-on-top] Source: "The upper output of the comparator is min(x,y) and the lower output is max(x,y)."
- CONFIRMED | a real, named construction from 1968 that works for any n. | https://www.cs.kent.edu/~batcher/sort.pdf | N2 source reread, retained in this directed pass: [batcher-date-general-n] Batcher p.310: "A sorter for arbitrary sequences can be constructed from odd-even merges or bitonic sorters using the well-known sorting-by-merging scheme". Page headers give "Spring Joint Computer Conference, 1968". Non-power-of-two widths follow by padding with largest sentinels and pruning unused wires; the pinned generator additionally passed widths 2,3,4,5,6,7,8,12,16. PDF opened after UNREADABLE; figures interleave the layout extraction, not the actual paragraph.
- CONFIRMED | One successful run proves nothing \u2014 the machine could still choke on some input you didn't try. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [one-run] The source defines correctness "for every input sequence"; testing an individual successful run does not imply this universal condition. The million-order illustration follows once n! exceeds a million, not from a measured failure rate. Broken net4 passes 12 of 16 binary tests, exhibiting why one passing example is insufficient.
- CONFIRMED | 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 \u2014 and the machine is certified. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [certificate-implication] Theorem 28.2: "If a comparison network with n inputs sorts all 2n possible sequences of 0's and 1's correctly, then it sorts all sequences of arbitrary numbers correctly." The converse follows by restricting the input domain. Superscripts are flattened in the source record.
- CONFIRMED | The reason is that a comparator is monotone. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [monotone] Lemma 28.1: "for any monotonically increasing function f" the network transforms f(a) into f(b); the proof derives "min(f(x), f(y)) = f(min(x,y))" and the corresponding max identity. Thresholds are nondecreasing, as required.
- CONFIRMED | The rung does the same thing either way: it commutes with f. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [comparator-commutes] Lemma 28.1: "for any monotonically increasing function f" the network transforms f(a) into f(b); the proof derives "min(f(x), f(y)) = f(min(x,y))" and the corresponding max identity. Thresholds are nondecreasing, as required.
- CONFIRMED | Lift that over the whole network and you get one clean identity \u2014 NET(f(x)) = f(NET(x)) \u2014 which says you can squash first or sort first, the result is the same. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [network-commutes] Lemma 28.1: "for any monotonically increasing function f" the network transforms f(a) into f(b); the proof derives "min(f(x), f(y)) = f(min(x,y))" and the corresponding max identity. Thresholds are nondecreasing, as required.
- CONFIRMED | So suppose a network fails to sort some real input x: somewhere in its output a bigger value sits above a smaller one. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [inversion] Theorem 28.2 proof: "the network places aj before ai in the output sequence" although "ai < aj", and "f(aj) = 1 and f(ai) = 0". This is the inversion and its binary witness. Pinned run recreated 2,387 failing-network witnesses.
- CONFIRMED | Pick the threshold right between them. Squashing x turns it into a string of 0s and 1s \u2014 and because squash-then-sort equals sort-then-squash, that binary string comes out with a 1 stranded above a 0. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [threshold-witness] Theorem 28.2 proof: "the network places aj before ai in the output sequence" although "ai < aj", and "f(aj) = 1 and f(ai) = 0". This is the inversion and its binary witness. Pinned run recreated 2,387 failing-network witnesses.
- CONFIRMED | The failure survives the squash. Every real failure casts a binary shadow; check the shadows and you've checked everything. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [failure-shadow] Theorem 28.2 proof: "the network places aj before ai in the output sequence" although "ai < aj", and "f(aj) = 1 and f(ai) = 0". This is the inversion and its binary witness. Pinned run recreated 2,387 failing-network witnesses.
- CONFIRMED | fewest comparators (its size), or fewest parallel columns (its depth, the time a hardware sorter takes) | https://arxiv.org/pdf/2012.04400 | N2 source reread, retained in this directed pass: [size-depth-definitions] Harder p.2: "size, which is the total number of comparisons" and "depth, which is the largest number of comparisons performed on a single element". Bundala p.3 identifies depth with the number of parallel steps. PDF opened after UNREADABLE.
- CONFIRMED | Batcher's construction is simple and regular, and for small n it is already as good as possible. | https://arxiv.org/pdf/2012.04400; https://bertdobbelaere.github.io/sorting_networks.html; git show f5e5f84f34:research/sorting-networks/verify.mjs | N2 source reread, retained in this directed pass: [batcher-optimal-small] Harder p.2: "first answered for n ≤ 8 by Floyd and Knuth"; the table gives 5,9,12,16,19 at n=4,5,6,7,8. Pinned Batcher computation gives size 9/depth 5 at n=5, 19/6 at n=8, and 63/10 at n=16; the current frontier has size at most 60 and depth 9 at n=16. PDF opened after UNREADABLE.
- CONFIRMED | But it is not magic: past a point it spends rungs it doesn't need. | https://bertdobbelaere.github.io/sorting_networks.html | N2 source reread, retained in this directed pass: [batcher-waste] The current summary has exact size bounds through 12 and depth through 17; rows 13 and 18 begin intervals, respectively "44...45" and "10...11". Row 16 has size "57...60", depth "9" versus computed Batcher 63/10. The source record copied the whole table, whose meaningful entries were read independently. Open status is as fetched 2026-10-14.
- CONFIRMED | Proven optima are cited, not recomputed here \u2014 only Batcher's own numbers are. | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:383; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:201 | N2 source reread, retained in this directed pass: [optima-cited-only] "const OPT_SIZE={4:5,5:9,6:12,7:16,8:19,9:25,10:29,11:35,12:39}" is a hard-coded comparison table, not a search over smaller networks. Lean comments explicitly say "that minimality is CITED, not reproven here".
- CONFIRMED | The minimum size is settled only up to n = 12 | https://bertdobbelaere.github.io/sorting_networks.html | N2 source reread, retained in this directed pass: [size-frontier] The current summary has exact size bounds through 12 and depth through 17; rows 13 and 18 begin intervals, respectively "44...45" and "10...11". Row 16 has size "57...60", depth "9" versus computed Batcher 63/10. The source record copied the whole table, whose meaningful entries were read independently. Open status is as fetched 2026-10-14.
- CONFIRMED | the minimum depth only up to n = 17. | https://bertdobbelaere.github.io/sorting_networks.html | N2 source reread, retained in this directed pass: [depth-frontier] The current summary has exact size bounds through 12 and depth through 17; rows 13 and 18 begin intervals, respectively "44...45" and "10...11". Row 16 has size "57...60", depth "9" versus computed Batcher 63/10. The source record copied the whole table, whose meaningful entries were read independently. Open status is as fetched 2026-10-14.
- CONFIRMED | Beyond that, the smallest sorting network for even modest n is an open problem \u2014 every value past those lines is a current record, not a proof. | https://bertdobbelaere.github.io/sorting_networks.html | N2 source reread, retained in this directed pass: [open-records] The current summary has exact size bounds through 12 and depth through 17; rows 13 and 18 begin intervals, respectively "44...45" and "10...11". Row 16 has size "57...60", depth "9" versus computed Batcher 63/10. The source record copied the whole table, whose meaningful entries were read independently. Open status is as fetched 2026-10-14.
- CONFIRMED | reaches the theoretically optimal O(n log n) size and O(log n) depth | https://bobson.ludost.net/books/algo/book6/chap28.htm; https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [aks-bounds] Chapter notes give O(lg n) depth and O(n lg n) comparators. Bundala p.2 says "superior to AKS networks for all practical values of n" about Batcher. The tool PARTIAL for aks-bounds was mathematical formatting, not a contradiction; PDF independently opened for the second entry.
- CONFIRMED | but its hidden constants are so vast it has never beaten Batcher at any size anyone would build. | https://bobson.ludost.net/books/algo/book6/chap28.htm; https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [aks-never-practical] Chapter notes give O(lg n) depth and O(n lg n) comparators. Bundala p.2 says "superior to AKS networks for all practical values of n" about Batcher. The tool PARTIAL for aks-bounds was mathematical formatting, not a contradiction; PDF independently opened for the second entry.
- CONFIRMED | Everything above checks the zero-one principle; none of it proves it. | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:405 | N2 source reread, retained in this directed pass: [sampling-not-proof] The live loops are "for(let n=3;n<=5;n++)" and "for(let n=3;n<=6;n++)". They test finite examples of the universal principle. The paragraph contrasts these samples with the symbolic proof introduced immediately afterward; it does not claim proof software can never run in a browser.
- CONFIRMED | Section 5 can only sample \u2014 fresh random networks, a finite n | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:405 | N2 source reread, retained in this directed pass: [browser-sample-scope] The live loops are "for(let n=3;n<=5;n++)" and "for(let n=3;n<=6;n++)". They test finite examples of the universal principle. The paragraph contrasts these samples with the symbolic proof introduced immediately afterward; it does not claim proof software can never run in a browser.
- CONFIRMED | no finite test can ever settle a claim about every network of every width. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [finite-tests-universal] The excerpt states the universal zero-one theorem but does not itself justify this methodological sentence. The source proof supplies induction over depth; checking only finitely many widths and networks cannot test every member of the unbounded family. This does not deny that a finite symbolic proof can establish it.
- CONFIRMED | That last gap is the one thing a running page cannot close by itself. | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:405 | N2 source reread, retained in this directed pass: [page-cannot-close-gap] The live loops are "for(let n=3;n<=5;n++)" and "for(let n=3;n<=6;n++)". They test finite examples of the universal principle. The paragraph contrasts these samples with the symbolic proof introduced immediately afterward; it does not claim proof software can never run in a browser.
- CONFIRMED | 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. | git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:20; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:81; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:110 | N2 source reread, retained in this directed pass: [theorem-scope] The generic class supplies a Boolean-valued total preorder; "theorem cmp_thr" and "theorem run_thr" establish commutation with "thr a", then zero_one uses these for all n and all comparator lists. A total order satisfies these premises. The proof really has the stated universal scope.
- CONFIRMED | The whole proof turns on one lemma \u2014 a comparator commutes with the monotone threshold x ↦ (a ≤ x) \u2014 which is exactly the monotone identity NET(f(x)) = f(NET(x)) the "binary shadow" instrument in §3 lets you watch by hand. | git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:20; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:81; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:110 | N2 source reread, retained in this directed pass: [proof-commutation] The generic class supplies a Boolean-valued total preorder; "theorem cmp_thr" and "theorem run_thr" establish commutation with "thr a", then zero_one uses these for all n and all comparator lists. A total order satisfies these premises. The proof really has the stated universal scope.
- CONFIRMED | The proof lives at research/sorting-networks/lean/ZeroOnePrinciple.lean | git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean; https://artwaste.land/checks/research/sorting-networks/lean/ZeroOnePrinciple.lean | N2 source reread, retained in this directed pass: [proof-location] The pinned file exists, defines "theorem zero_one", and the public /checks/ mirror returns HTTP 200 with identical bytes.
- CONFIRMED | The kernel never enumerates them. | git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:185; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:201; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:214 | N2 source reread, retained in this directed pass: [kernel-not-factorial] "decForallFinBool" enumerates Boolean vectors; the three "by decide" statements and "net4bad_not_sorter" reside in the same file. The source explicitly says "that minimality is CITED, not reproven here". "Zero-import" is accurate only as zero explicit import statements; implicit Init is handled by the separate import findings.
- CONFIRMED | Each network's comparator count is the smallest possible for its width \u2014 the proven minima s(4)=5, s(5)=9, s(8)=19 (Knuth). | https://arxiv.org/pdf/2012.04400; https://bertdobbelaere.github.io/sorting_networks.html; git show f5e5f84f34:research/sorting-networks/verify.mjs | N2 source reread, retained in this directed pass: [small-minima] Harder p.2: "first answered for n ≤ 8 by Floyd and Knuth"; the table gives 5,9,12,16,19 at n=4,5,6,7,8. Pinned Batcher computation gives size 9/depth 5 at n=5, 19/6 at n=8, and 63/10 at n=16; the current frontier has size at most 60 and depth 9 at n=16. PDF opened after UNREADABLE.
- CONFIRMED | That minimality is cited, not reproven; what the kernel certifies is the other half \u2014 that these particular networks actually sort. Correctness machine-checked; optimality quoted. The two are kept apart on purpose. | git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:185; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:201; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:214 | N2 source reread, retained in this directed pass: [minimality-separate] "decForallFinBool" enumerates Boolean vectors; the three "by decide" statements and "net4bad_not_sorter" reside in the same file. The source explicitly says "that minimality is CITED, not reproven here". "Zero-import" is accurate only as zero explicit import statements; implicit Init is handled by the separate import findings.
- CONFIRMED | All three certificates plus the negative live in the same file: research/sorting-networks/lean/ZeroOnePrinciple.lean. | git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:185; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:201; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:214 | N2 source reread, retained in this directed pass: [same-file-certificates] The three positive certificates and net4bad_not_sorter are in this file. This retains the confirmed location only; the original zero-import clause is corrected under X3/X7.
- CONFIRMED | Batcher's construction is classical (Batcher 1968) | https://www.cs.kent.edu/~batcher/sort.pdf | N2 source reread, retained in this directed pass: [classical-batcher] Batcher p.310: "A sorter for arbitrary sequences can be constructed from odd-even merges or bitonic sorters using the well-known sorting-by-merging scheme". Page headers give "Spring Joint Computer Conference, 1968". Non-power-of-two widths follow by padding with largest sentinels and pruning unused wires; the pinned generator additionally passed widths 2,3,4,5,6,7,8,12,16. PDF opened after UNREADABLE; figures interleave the layout extraction, not the actual paragraph.
- CONFIRMED | the principle is classical too (Knuth) | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [classical-principle] Chapter notes: "Knuth [123] contains a discussion of sorting networks and charts their history" and "Knuth attributes the zero-one principle to W. G. Bouricius (1954)". The page says developed in Knuth, not invented by Knuth; the theorem is in section 28.2. Bundala p.2 independently identifies TAOCP vol.3 section 5.3.4.
- CONFIRMED | Theminimality of a size or depth \u2014 that no smaller network exists \u2014 is never something this page checks; | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:383; git show f5e5f84f34:research/sorting-networks/lean/ZeroOnePrinciple.lean:201 | N2 source reread, retained in this directed pass: [never-minimality] "const OPT_SIZE={4:5,5:9,6:12,7:16,8:19,9:25,10:29,11:35,12:39}" is a hard-coded comparison table, not a search over smaller networks. Lean comments explicitly say "that minimality is CITED, not reproven here".
- CONFIRMED | sizes through n=8 classical | https://arxiv.org/pdf/2012.04400; https://bertdobbelaere.github.io/sorting_networks.html; git show f5e5f84f34:research/sorting-networks/verify.mjs | N2 source reread, retained in this directed pass: [classical-size] Harder p.2: "first answered for n ≤ 8 by Floyd and Knuth"; the table gives 5,9,12,16,19 at n=4,5,6,7,8. Pinned Batcher computation gives size 9/depth 5 at n=5, 19/6 at n=8, and 63/10 at n=16; the current frontier has size at most 60 and depth 9 at n=16. PDF opened after UNREADABLE.
- CONFIRMED | n=9,10 by Codish, Cruz-Filipe, Frank & Schneider-Kamp (2014) | https://arxiv.org/abs/1405.5754 | N2 source reread, retained in this directed pass: [codish-size-attribution] The arXiv abstract says "the 25-comparator sorting network found by Floyd in 1964 is optimal" and "the 29-comparator network found by Waksman in 1969 is optimal when sorting ten inputs". Header gives all four named authors and first submission 22 May 2014.
- CONFIRMED | n=11,12 by Harder (2020) | https://arxiv.org/abs/2012.04400 | N2 source reread, retained in this directed pass: [harder-size-attribution] Header: "Authors:Jannis Harder", "Submitted on 8 Dec 2020". Abstract: "11-channel sorting networks have at least 35 comparators" and "12-channel sorting networks have at least 39 comparators".
- CONFIRMED | depths through n=10 classical | https://arxiv.org/pdf/1412.5302; https://bertdobbelaere.github.io/sorting_networks.html | N2 source reread, retained in this directed pass: [classical-depth] Abstract credits Parberry for 9 and 10 inputs and proves 11 through 16. Bundala PDF reference [3] is "Daniel Bundala and Jakub Závodný. Optimal sorting networks. In LATA 2014"; p.2 calls the five-author paper an extended version. Thus the historical two-author attribution is supported, while the separate bibliographic entry for arXiv:1412.5302 needs all five authors.
- CONFIRMED | 11–16 by Bundala & Závodný (2014) | https://arxiv.org/pdf/1412.5302; https://bertdobbelaere.github.io/sorting_networks.html | N2 source reread, retained in this directed pass: [bundala-depth-attribution] Abstract credits Parberry for 9 and 10 inputs and proves 11 through 16. Bundala PDF reference [3] is "Daniel Bundala and Jakub Závodný. Optimal sorting networks. In LATA 2014"; p.2 calls the five-author paper an extended version. Thus the historical two-author attribution is supported, while the separate bibliographic entry for arXiv:1412.5302 needs all five authors.
- CONFIRMED | which loses nothing \u2014 a comparator only ever consults the order of two values, never their size. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [integer-relabel-no-loss] Lemma 28.1 establishes monotone relabelling. Comparators retain only order information; sorting all distinct rank permutations also handles ties via a nondecreasing map. The pinned inputs are permutations of integers.
- CONFIRMED | 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. | https://www-cs-faculty.stanford.edu/~knuth/taocp.html; https://arxiv.org/pdf/1412.5302; https://www.pearson.de/media/muster/ext/9780133488838.pdf | N2 source reread, retained in this directed pass: [citation-knuth] Knuth author page gives "Volume 3 Sorting and Searching, Second Edition"; Bundala p.2 supplies vol.3 section 5.3.4. The publisher sample independently prints "5.3.4 NETWORKS FOR SORTING". N1 excerpts did not alone verify every part of the grouped citation.
- CONFIRMED | §5.3.4 ("Networks for Sorting"), where the zero-one principle and these networks are developed. | https://www-cs-faculty.stanford.edu/~knuth/taocp.html; https://arxiv.org/pdf/1412.5302; https://www.pearson.de/media/muster/ext/9780133488838.pdf | N2 source reread, retained in this directed pass: [citation-knuth-section] Knuth author page gives "Volume 3 Sorting and Searching, Second Edition"; Bundala p.2 supplies vol.3 section 5.3.4. The publisher sample independently prints "5.3.4 NETWORKS FOR SORTING". N1 excerpts did not alone verify every part of the grouped citation.
- CONFIRMED | K. E. Batcher, "Sorting networks and their applications," AFIPS Spring Joint Computer Conference, 1968, pp. 307–314. | https://api.crossref.org/works/10.1145/1468075.1468121; https://www.cs.kent.edu/~batcher/sort.pdf | N2 source reread, retained in this directed pass: [citation-batcher] Crossref DOI MATCH: K. E. Batcher, "Sorting networks and their applications", 1968, conference and first page 307. Crossref stores only page "307"; the original PDF supplies pages 307 through 314. N1 metadata alone did not establish the last page.
- CONFIRMED | 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. | https://api.crossref.org/works/10.1109/ICTAI.2014.36 | N2 source reread, retained in this directed pass: [citation-codishcite] Crossref DOI MATCH: title, Michael Codish, Luís Cruz-Filipe, Michael Frank, Peter Schneider-Kamp, and issued [[2014,11]] all match; conference is ICTAI 2014.
- CONFIRMED | J. Harder, "An Answer to the Bose–Nelson Sorting Problem for 11 and 12 Channels," arXiv:2012.04400 (2020). | https://arxiv.org/abs/2012.04400 | N2 source reread, retained in this directed pass: [citation-hardercite] arXiv title, "Authors:Jannis Harder", and "Submitted on 8 Dec 2020" match. The displayed 2022 revision is not a different first-publication year.
- CONFIRMED | T. Ehlers, M. Müller, "Faster Sorting Networks for 17, 19 and 20 Inputs," arXiv:1410.2736. | https://arxiv.org/abs/1410.2736 | N2 source reread, retained in this directed pass: [citation-ehlerscite] arXiv header: "Authors:Thorsten Ehlers, Mike Müller" and "Faster Sorting Networks for $17$, $19$ and $20$ Inputs". The bibliographic citation is right; using it as the minimality proof is the separate WRONG entry.
- CONFIRMED | M. Ajtai, J. Komlós, E. Szemerédi, "An O(n log n) sorting network," STOC 1983 | https://api.crossref.org/works/10.1145/800061.808726 | N2 source reread, retained in this directed pass: [citation-aks] Crossref DOI MATCH: authors M. Ajtai, J. Komlós, E. Szemerédi, STOC 83, issued 1983; title "An 0(n log n) sorting network" uses a metadata zero where mathematical typography uses O. This is not a page error.
- CONFIRMED | A finite, exhaustive census standing in for an infinite claim \u2014 there, every profile of ballots proves an impossibility; here, every 2ⁿ binary string vouches for all n! orderings. | git show f5e5f84f34:src/content/strata/the-only-fair-vote.md | N2 source reread, retained in this directed pass: [related-the-only-fair-vote] Pinned linked page states "The exhaustive census is a real proof of Arrow's theorem for two and three voters, run in your browser; the general case is the cited induction". This supports the local finite-census comparison; the linked text does not claim the finite census alone proves every electorate size.
- CONFIRMED | Two Pattern-seam machines about order, each certified by a small exact check run in the browser \u2014 the fair turn-order, and the proof a sorter is correct. | git show f5e5f84f34:src/content/strata/the-fairest-order.md | N2 source reread, retained in this directed pass: [related-the-fairest-order] Pinned linked page has seam "pattern" and describes equal power sums "recomputed in exact BigInt arithmetic in your browser". The local page also has seam pattern and runs the binary check.
- CONFIRMED | A fixed procedure you can run by hand, then verify by trying everything: deferred acceptance against every blocking pair; a comparator network against every 0/1 input. | git show f5e5f84f34:src/content/strata/no-two-would-rather.md | N2 source reread, retained in this directed pass: [related-no-two-would-rather] Pinned linked page describes deferred acceptance and "hunts, in vain, for a single pair who would both rather defect". The present page exhausts binary inputs; the relation accurately describes both instruments.
- CONFIRMED | Order and its undoing \u2014 how many riffle shuffles to lose all order, and how few comparators to impose it; both ask exactly how much work a permutation costs. | git show f5e5f84f34:src/content/strata/seven-shuffles.md | N2 source reread, retained in this directed pass: [related-seven-shuffles] Pinned linked page asks "How many ordinary riffle shuffles make it random?" and describes exact distance-to-random calculations. The local page studies comparator counts. The link is a topic comparison, not a new claim about a specific shuffle count.
- CONFIRMED | A finite, exhaustive census standing in for an infinite claim \u2014 there, every profile of ballots proves an impossibility; here, every 2ⁿ binary string vouches for all n! | git show f5e5f84f34:src/content/strata/the-only-fair-vote.md | N2 source reread, retained in this directed pass: [related-visible-shortened] Pinned linked page states "The exhaustive census is a real proof of Arrow's theorem for two and three voters, run in your browser; the general case is the cited induction". This supports the local finite-census comparison; the linked text does not claim the finite census alone proves every electorate size.
- CONFIRMED | Two symbols suffice to encode anything, which is a statement about what an alphabet can carry. | https://people.math.harvard.edu/~ctm/home/text/others/shannon/entropy/entropy.pdf | N2 source reread, retained in this directed pass: [binary-encoding] Shannon p.17: "If the channel sequences are not already sequences of binary digits, they can be ascribed binary numbers in an arbitrary fashion". This supports encoding messages with two symbols; read in its ordinary representational sense, not as claiming finite lossless representations of arbitrary continuous measurements. PDF opened after UNREADABLE.
- CONFIRMED | A sorting network is a machine that sorts without ever branching: a fixed list of compare-and-swap wires, etched once, the same gates in the same order no matter what flows through. | https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [frontmatter-fixed-network] PDF p.1: "the order of these comparisons is predetermined by the number of inputs to sort and does not depend on their concrete values"; "Each comparator takes the two inputs from its two channels, compares them, and outputs them sorted". The statements concern data-oblivious control, not inability to compare. Opened and read the PDF after UNREADABLE.
- CONFIRMED | when there are n! of them, twenty trillion for sixteen items? | https://oeis.org/A000142/b000142.txt | N2 source reread, retained in this directed pass: [frontmatter-factorial-sixteen] OEIS b-file: "16 20922789888000". Independently multiplied 1 through 16; twenty trillion is a rounded description of 20,922,789,888,000.
- CONFIRMED | The answer, one of the cleanest theorems in computing (the zero-one principle, Knuth, TAOCP Vol. 3 §5.3.4), is that you never need to test more than the 2ⁿ inputs made only of zeros and ones; pass those and you have sorted everything. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [frontmatter-knuth-zero-one] Chapter notes: "Knuth [123] contains a discussion of sorting networks and charts their history" and "Knuth attributes the zero-one principle to W. G. Bouricius (1954)". The page says developed in Knuth, not invented by Knuth; the theorem is in section 28.2. Bundala p.2 independently identifies TAOCP vol.3 section 5.3.4.
- CONFIRMED | A third instrument makes the *why* tangible: because a comparator is monotone, a network commutes with any increasing relabelling (NET(f(x)) = f(NET(x))), so every real failure casts a binary shadow. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [frontmatter-monotone-player] Lemma 28.1: "for any monotonically increasing function f" the network transforms f(a) into f(b); the proof derives "min(f(x), f(y)) = f(min(x,y))" and the corresponding max identity. Thresholds are nondecreasing, as required.
- CONFIRMED | Batcher meets the proven minimum for n=5 and n=8, overspends at n=16 | https://arxiv.org/pdf/2012.04400; https://bertdobbelaere.github.io/sorting_networks.html; git show f5e5f84f34:research/sorting-networks/verify.mjs | N2 source reread, retained in this directed pass: [frontmatter-small-optima] Harder p.2: "first answered for n ≤ 8 by Floyd and Knuth"; the table gives 5,9,12,16,19 at n=4,5,6,7,8. Pinned Batcher computation gives size 9/depth 5 at n=5, 19/6 at n=8, and 63/10 at n=16; the current frontier has size at most 60 and depth 9 at n=16. PDF opened after UNREADABLE.
- CONFIRMED | and past n=12 (size) and n=17 (depth) the smallest possible network is an *open problem*. | https://bertdobbelaere.github.io/sorting_networks.html | N2 source reread, retained in this directed pass: [frontmatter-open-frontier] The current summary has exact size bounds through 12 and depth through 17; rows 13 and 18 begin intervals, respectively "44...45" and "10...11". Row 16 has size "57...60", depth "9" versus computed Batcher 63/10. The source record copied the whole table, whose meaningful entries were read independently. Open status is as fetched 2026-10-14.
- CONFIRMED | A sorting network must put every possible input in order, and there are n! of them. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [meta-every-input] In the page context, n! denotes orderings of a fixed set of n distinct values; Theorem 28.2 covers arbitrary values too. It is not the cardinality of all real-valued vectors. The main dek explicitly calls them "n! orderings"; no separate numerical contradiction was found.
- CONFIRMED | Yet you can certify one by checking only the 2^n strings of zeros and ones. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [meta-binary-certification] Theorem 28.2: "If a comparison network with n inputs sorts all 2n possible sequences of 0's and 1's correctly, then it sorts all sequences of arbitrary numbers correctly." The converse follows by restricting the input domain. Superscripts are flattened in the source record.
- CONFIRMED | A sorting network is a fixed sequence of compare-and-swap wires that sorts without ever branching | https://arxiv.org/pdf/1412.5302 | N2 source reread, retained in this directed pass: [plain-fixed-sequence] PDF p.1: "the order of these comparisons is predetermined by the number of inputs to sort and does not depend on their concrete values"; "Each comparator takes the two inputs from its two channels, compares them, and outputs them sorted". The statements concern data-oblivious control, not inability to compare. Opened and read the PDF after UNREADABLE.
- CONFIRMED | The zero-one principle says you only need to test the inputs made of zeros and ones. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [plain-zero-one] Theorem 28.2: "If a comparison network with n inputs sorts all 2n possible sequences of 0's and 1's correctly, then it sorts all sequences of arbitrary numbers correctly." The converse follows by restricting the input domain. Superscripts are flattened in the source record.
- CONFIRMED | something is wrong. | git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:419 | N2 source reread, retained in this directed pass: [live-failure-verdict] The FAIL branch appears when pass!==checks.length; a failed mathematical consistency check does indicate an error. This is a conditional diagnostic, not an assertion that the present run failed.
- CONFIRMED | n Batcher size min size Batcher depth min depth 4 5 5 ✓ 3 3 ✓ 5 9 9 ✓ 5 5 ✓ 6 12 12 ✓ 6 5 8 19 19 ✓ 6 6 ✓ 12 42 39 10 8 16 63 open 10 9 | https://bertdobbelaere.github.io/sorting_networks.html; git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:383 | N2 source reread, retained in this directed pass: [frontier-minima-table] Independently read all minima columns: for n=4,5,6,8,12,16, minimum sizes are 5,9,12,19,39,open and depths 3,5,5,6,8,9. Batcher columns are recreated separately as 5/3,9/5,12/6,19/6,42/10,63/10. Table does not claim size 39 and depth 8 are simultaneously achievable at n=12.
- CONFIRMED | To prove a sorting machine orders all n! inputs, you need only test the 2^n made of zeros and ones. | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [og-all-factorial-inputs] In the page context, n! denotes orderings of a fixed set of n distinct values; Theorem 28.2 covers arbitrary values too. It is not the cardinality of all real-valued vectors. The main dek explicitly calls them "n! orderings"; no separate numerical contradiction was found.
- CONFIRMED | (added) Real inputs have endless distinct values | https://bobson.ludost.net/books/algo/book6/chap28.htm | N2 source reread, retained in this directed pass: [added-real-domain] The source allows "arbitrary input numbers" including "reals". The number of possible real values is unbounded; this is distinct from n! orderings of a fixed distinct set.
- CONFIRMED | (added) "datePublished":"2026-06-19" | git show f5e5f84f34:memory/log.d/2026-06-19T2330Z-two-symbols-are-enough.md; git show f5e5f84f34:public/strata/two-symbols-are-enough/index.html:84 | N2 source reread, retained in this directed pass: [added-publication-date] The contemporary log is headed "2026-06-19" and says "A new immersive stratum"; commit 70123380d2a has that date. This omitted structured-metadata date matches the frontmatter.

## Findings

- [fixed] X1 [unrestricted-squaring] Restricted squaring to nonnegative inputs in the authored HTML and added the corresponding correction to HTML and the markdown body.
- [fixed] X2 [all-checks-recomputed-live] Qualified the live recomputation sentence to network outputs and Batcher size/depth; distinguished the six browser checks from the offline suite. Corrected the verifier header too. MINOR, no dated page line.
- [fixed] X3 [lean-no-imports] Corrected the dependency and order-law claims in the page, dek, README and Lean comments. Added one consolidated HTML/markdown correction shared with X7; proof terms are unchanged.
- [fixed] X4 [exhaustive-check-called-sampling] Replaced the sampling comparison with the browser exhaustive evaluation/kernel proof distinction, and added its HTML/markdown correction.
- [fixed] X5 [network-drift-guarantee] Replaced the unsupported drift-prevention guarantee in HTML, README and verifier comments with the actual independent-copy behavior. Added its HTML/markdown correction; no permanent equality assertion was introduced.
- [fixed] X6 [live-width-seven] Corrected the live upper limit to 6, named 1,200 live trials, and made the valid offline limit of 7 explicit in the dek. Corrected related offline-limit comments in verify.mjs, README and Lean. Added one HTML/markdown correction for these scope statements.
- [fixed] X7 [lean-no-imports] Corrected every current no-library/zero-import summary in the layer to distinguish explicit imports from implicit Init. Shares X3's dated HTML/markdown correction.
- [fixed] X8 [n17-optimality-attribution] Credited the five-author 2015 proof in the body, notes, dek and verifier footer, retaining the Ehlers/Müller construction citation. Added one consolidated HTML/markdown correction shared with X12 and X15.
- [fixed] X9 [bundala-authors-incomplete] Restored all five authors in the arXiv:1412.5302 citation. MINOR, no dated page line.
- [fixed] X10 [last-verified-date] Supplied the completed pass date in this record, the authored source consumed by the generated last-verified placard. Rendered June 19 placard awaits shared landing regeneration, as the triage explicitly directs; no placard output edit or separate dated line.
- [fixed] X11 [all-checks-recomputed-live] Qualified the dek to computational checks and made the optional Lean run explicit. MINOR, no dated page line.
- [fixed] X12 [n17-optimality-attribution] Corrected the minimality attribution in the dek while preserving the proved-versus-cited distinction and offline n=7 check. Shares X8's correction.
- [fixed] X13 [all-checks-recomputed-live] Qualified both metadata descriptions to the network results recomputed in the browser. MINOR, no dated page line.
- [fixed] X14 [blanket-truth-verdict] Narrowed the success message to the six programmed checks passing. MINOR, no dated page line.
- [fixed] X15 [n17-optimality-attribution] Corrected the same frontmatter minimality credit identified by X12; the five-author proof replaces the two-author construction citation in that role. Shares X8's correction.
- [dated] X16 [stale-date-modified] Set JSON-LD dateModified to 2026-10-14 for this revision. The dated correction lines already identify the revision, so the JSON-LD exception requires no Updated line.
- [fixed] WRONG X3/X7 [lean-no-imports] The copy in The Strategy That Counts in Binary's relation note (src/content/strata/the-strategy-that-counts-in-binary.md) now says the proofs have no explicit imports, corrected on 2026-10-18; board note 7ee635 is closed. Read as the literal absence of import lines, "zero imports" there was a loose phrase, not the false "imports no library" this layer corrected, so it was fixed with no dated line.

## Verification

- node research/sorting-networks/verify.mjs: exit 0; 41 passed, 0 failed, comprising 36 JavaScript checks and five Lean axiom-footprint checks. The zero_one, net4_sorts, net5_sorts, net8_sorts and net4bad_not_sorter footprints are all [propext, Quot.sound].
- node /tmp/two-symbols-fixer-1014-8x08nytv/check-page.cjs: exit 0; all six live checks passed; 1,200 live random networks, intact certificates at widths 4/5/6/8, every single-rung deletion at those widths detected, current Lean lists matched at widths 4/5/8, the squaring counterexample and monotone controls reproduced, valid JSON-LD dated 2026-10-14, and six correction paragraphs exactly mirrored in markdown.
- lean --version and lean --deps research/sorting-networks/lean/ZeroOnePrinciple.lean: exit 0; existing Lean 4.35.0, implicit core Init.olean. No toolchain installation or download was needed.
- Claims gate result and the complete edit-by-edit report are recorded in research/assay-line/queue-1014c/two-symbols-are-enough/fix-report.md.

## Deferred generated output

The authored source for X10 is this record's passed date. The existing generated placard still displays June 19 until landing regenerates it through the shared mechanism. No shared script was modified or run in write mode. The JSON-LD date and six correction paragraphs above the placard are updated now. No Updated line is needed for X16, and no dated page lines were added for the five MINOR items.