Twelve prรฉcis covering the 0-1 principle, forced partial orders, comparability monoid, twist freedom, orbit of optima, and complexity hedging. Includes program listings (order_only.py verifier) and example network JSON files.
Machine-checked (Isabelle/HOL) treatment of the Boolean function family computed by comparator networks. Traces the path from the zero-one principle through cofactor structure to the complexity boundary of verification.
A sorting primitive below the comparator. Given x โค z, the two comparators (x,y) and (y,z) are mutually exclusive and can share a single swap unit. Trades comparisons for swap hardware. Exhaustively verified over all n^n tuples and n! permutations.
Dobbelaere's 185/14 network in coordinates where the hypercube prefix, twist, and closure are visible. Shows that planes {5,10,15} and {6,9,15} are the same twist under a GF(2)โต automorphism.
Sorting networks verified on a Tang Nano 20K FPGA (Gowin GW2AR-18C) at frequencies up to 594 MHz. Both Network 01 (braid_60) and Dobbelaere's optimal pass at all tested frequencies.
Sometimes, we use a USB digital microscope to look at the LEDs on the Dev Board. This works without disturbing the device-under-test.
