Supplement to "Exact sizes of networks that select the three or four largest of n elements"

This archive holds the programs, data and logs behind the computations in the paper "Exact sizes of networks that select the three or four largest of n elements" (doi:10.5281/zenodo.23801189). It contains the two separately written programs that compute Ût(n), the least number of comparators in a network that moves the t largest of n inputs to t given lines, by exhaustive search, with the logs of the runs cited in the paper, and the parallel driver under which one of them was run for Û4(12). It also contains Yao's networks for three of n inputs, n ≤ 18, and optimal networks for four of n inputs, 8 ≤ n ≤ 12, with checkers that test them on all inputs of 0s and 1s; the certificates of the bounds from lead-pattern potentials, which are exact rational potentials and dual solutions, with two checkers; the two programs for the searches restricted to networks whose minimum paths have length at most 2; the data on inserting a line into optimal networks; and a program, separate from Lean, that checks that the search certificates of the Lean proofs are closed. For each claim of the paper, the file CHECKS.md gives a command and the output it prints when the check passes. It records which checks were re-run and cites the recorded runs for the larger computations. Version 2 adds the folder weights/ for Section 5 of the paper, on the lower bounds at powers of two and their extension to every t. It holds: the working notes of the proofs; programs that check the lemmas and the potential on all moves of small weights and on random and optimal networks; programs that replay the sequences of Section 5, compute the values of LB(k) and search the weight model; further checks of the same claims, each written separately. CHECKS.md lists them in rows of their own. Everything else is unchanged from version 1. All files are in the archive sel_supplement.tar.gz. README.md and SHA256SUMS are copies of the files of the same names in it. The Lean proofs are archived separately as doi:10.5281/zenodo.23801200.