Sorting networks on 13 inputs need 45 comparators

Let S(N) be the least number of comparators in a sorting network on N inputs. The values are known for N ≤ 12. For 13 inputs the smallest known sorting network, found by Juillé, has 45 comparators, and the best proved lower bound has been 44. We prove S(13) ≥ 45, so S(13) = 45. The proof extends a two-value bound to partial sorting. If a network with L comparators sorts a set X of 0-1 vectors, then for suitable pairs of inputs the largest and the second largest value meet at most L − c comparators, where c is the cost of sorting the residual set left when their paths are deleted. Whether a single network stays within all these budgets is decided by a finite search over the tree of paths of the largest value, the comparators on these paths, and a forest of comparators that carries the second largest value. A breadth-first search over the sets produced by prefixes of a hypothetical sorting network with 44 comparators discards each set that fails this test. The costs of the residual sets are bounded below using S(11) = 35 and exact costs of 9- and 7-channel sets. No set survives at depth 25. A separate verifier, with its own implementation of the test, checks the certificate written by the search. It trusts Harder's program for the exact 9- and 7-channel costs, the bound S(11) = 35, and this implementation of the test. A second proof, in Lean 4, checks the same certificate with another implementation of the test, which it proves sound, and proves the 9- and 7-channel bounds that it uses; its large computations run as compiled code. The certificate, the verifier, the Lean proof and the verification logs are archived as doi:10.5281/zenodo.23504361. Mathematics Subject Classification (2020): 68P10 (primary); 68Q06, 05C05, 68V05 (secondary).