Sorting networks on 14 inputs need 50 comparators

Let S(N) be the least number of comparators in a sorting network on N inputs. The values are known for N ≤ 13, and for 14 inputs it was known that 49 ≤ S(14) ≤ 51. We prove S(14) ≥ 50, so S(14) is 50 or 51. Deleting the path of the largest input from a sorting network leaves a sorting network on one input fewer. Since S(13) = 45, every path of the largest or the smallest input in a sorting network on 14 inputs with 49 comparators meets at most four comparators, and by Kraft's equality this almost fixes the two trees formed by these paths. The comparators that build the trees without depending on the other comparators can be moved to the front. Up to permutation and complementation of the channels, the set of 0-1 vectors that they produce is one of 5,271 sets. For each of them, a computer search over the remaining comparators shows that the network cannot be completed. The search discards states in three ways. Once the largest or the smallest value can end on only one channel, it deletes that channel and applies the weighted two-value bound of our proof of S(13) = 45, with bounds on the costs of sets on 10 or 11 channels. While the largest or the smallest value can still end on several channels, it applies Huffman's inequality. A last test combines the two on the whole set. A separately written program replays the certificates of the searches. The lower bounds on the costs of small sets that they use, other than trivial bounds carried over from similar sets, are certified in turn, and a separate checker verifies this certification down to lower bounds on the costs of sets with at most 9 channels. These lower bounds were recomputed with Harder's program or derived from his certificate for S(11) ≥ 35 or from a table proved in Lean. In Lean 4 we proved that S(14) ≥ 50 follows from the certified bounds, using the published Lean proofs of S(13) ≥ 45 and S(11) ≥ 35; part of the checks runs as compiled code. As a consequence, S(16) ≥ 59. The data record, doi:10.5281/zenodo.23624772, contains the list of the 5,271 sets with the comparators that produce them, the certificates of all searches, and the programs that replay the certificates, with their logs. It also contains the programs that certify the bounds on the costs of small sets, together with the lower bounds on 7, 8 and 9 channels on which this certification rests. The Lean proofs, their data and their build records are archived as doi:10.5281/zenodo.23632985. Mathematics Subject Classification (2020): 68P10 (primary); 68Q06, 05C05, 68V05 (secondary).