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

Let Ût(n) be the least number of comparators in a network that moves the t largest of n inputs to t given lines, in any order. In 1975 Yao proved 2n − 6 + ⌈lg⌈n/3⌉⌉ ≤ Û3(n) ≤ 2n − 5 + ⌊lg(n − 3)⌋ and asked for the exact value. We prove that his upper bound is exact for 4 ≤ n ≤ 18, so that Û3(n) = 2n − 2 for 11 ≤ n ≤ 18, and that Û3(n) ≥ 2n − 2 for all n ≥ 11, which improves his lower bound for 11 ≤ n ≤ 24. We also prove Û4(n) = 3n − 10 for 6 ≤ n ≤ 12. Knuth posed Û4(n) ≤ 3n − 10 as an exercise, credited its solution to a construction of M. W. Green, and expected equality; for n = 8 the result also settles a conjecture of Qu, Tasbihi and Kschischang. The lower bounds come from exhaustive searches by two separately written programs at a few sizes, and from the inequality Ût(n) ≥ Ût(n − 1) + 2 for t ≥ 2 and n ≥ t + 1. With it, Yao's question reduces to the sizes n = 2j + 3, where his upper bound grows by three, and the paper gives an exact criterion for each of them in terms of the optimal networks on 2j + 2 inputs. Lead-pattern potentials on the inputs of weights 2 and 3 give Û3(n) exactly for n ≤ 6, but at most 10 < Û3(7) for n = 7. The inequality, the two results on Û3 and the values of Û4(n) for 6 ≤ n ≤ 10 are also proved in Lean 4, partly through compiled checks. The programs, certificates and logs are archived as doi:10.5281/zenodo.23783470, and the Lean proofs as doi:10.5281/zenodo.23783476. Mathematics Subject Classification (2020): 68P10 (primary); 68Q06 (secondary).