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.23756850). 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. The scripts and weight tables behind the closed-form potentials are included too, with the programs that list or check all configurations for the potentials of m = 5, 6 and 7. So are 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 potential of m = 7 with even n, which gives M(7,16) and M(7,24), together with the logs of the original runs and of an independent check. It also adds the dual certificates that limit what potentials of the parity type can prove; they come with an explicit pair of up-sets for each of their constraints and with two checkers. 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.23756852.