Supplement to "Lead-pattern potentials and exact values of merging networks"

This archive holds the programs, data and logs behind the computations in the paper "Lead-pattern potentials and exact values of merging networks" (doi:10.5281/zenodo.23749963). It contains the certificates for the lower bounds of the paper (each an integer weight for every up-set of the merging grid, together with a denominator) and two separately written checkers that verify them in integer arithmetic. It also contains the scripts and weight tables behind the closed-form potentials, with the programs that list or check all configurations for the potentials of m = 5 and m = 6, the logs of the linear programs, and the patches and logs of the exact search with Harder's program, which recomputes M(m,n) for all pairs with m + n ≤ 14 and for two pairs with m + n = 15. For each certificate and closed-form statement of the paper, the file CHECKS.md gives one command and the output it prints when the check passes, and for the exact search and the largest certificates it cites the recorded runs. CHECKS.md also records which checks were re-run for this archive, and the outputs of those runs are included. This version adds the files and checks for the potentials of m = 5 with residues modulo 4, which complete the formula for M(5,n), together with the logs of the original runs and of an independent check, and a certificate showing that every sorting network on six channels has at least 12 comparators, with the programs that generate and check it. All files are in the archive ltp_merging_supplement.tar.gz. README.md and SHA256SUMS are copies of the files of the same names in it. The Lean proofs of the values are archived separately as doi:10.5281/zenodo.23749966.