Lead-pattern potentials and exact values of merging networks

Let M(m,n) be the least number of comparators in a network that merges sorted lists of lengths m and n. We prove M(5,7) = 18, M(6,8) = 22, M(6,9) = 25, M(7,9) = 27 and M(5,15) = 35, five values listed as open in 2009, together with M(5,10) = 25, M(5,11) = 27, M(5,12) = 29 and M(6,10) = 27, for which we know of no published determination. In all nine cases Batcher's odd-even merge is optimal. Each lead of a network computes a monotone Boolean function of its input, and a comparator replaces two such functions by their disjunction and conjunction, so a potential on these functions that grows by at most one at each comparator bounds the size of the network from below. The best such bound is the optimum of a linear program. For merging networks its solutions round to exact rational certificates, which two separately written programs check, and the nine values are also proved in Lean 4, partly by compiled code. Closed-form potentials give new proofs of the formulas for M(2,n) and M(3,n), of the odd cases of M(4,n), and of Iwata's linear coefficient. The certificates, the checkers and the logs of all computations are archived as doi:10.5281/zenodo.23719457, and the Lean proofs as doi:10.5281/zenodo.23719459. Mathematics Subject Classification (2020): 68P10 (primary); 68Q06, 90C05 (secondary).