\documentclass[11pt]{amsart} \pdfsuppressptexinfo=-1 \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage[margin=1.1in]{geometry} \usepackage{amssymb,mathtools} \usepackage{booktabs} \usepackage{array} \usepackage{enumitem} \usepackage{alltt} \usepackage{microtype} \usepackage[hidelinks]{hyperref} \input{ids.tex} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\cl}[1]{\lceil #1\rceil} \renewcommand{\lg}{\log_2} \newcommand{\hi}{\mathrm{hi}} \newcommand{\lo}{\mathrm{lo}} \newcommand{\seg}{\mathrm{seg}} \newcommand{\pre}{\mathrm{pre}} \newcommand{\lca}{\mathrm{lca}} \newcommand{\cb}{\mathrm{cl}} \newcommand{\oM}{o_{M}} \newcommand{\om}{o_{m}} \newcommand{\B}{\{0,1\}} \newcommand{\dg}{\ensuremath{^{\dagger}}} \newcommand{\dead}{\textsf{dead}} \hypersetup{pdftitle={Sorting networks on 13 inputs need 45 comparators}, pdfauthor={Tejasvi Singh Tomar}} \title{Sorting networks on 13 inputs need 45 comparators} \author{Tejasvi Singh Tomar} \renewcommand{\urladdrname}{{\itshape ORCID}} \urladdr{\href{https://orcid.org/0000-0003-4668-3639}{https://orcid.org/0000-0003-4668-3639}} \date{\pubdate} \subjclass[2020]{Primary 68P10; Secondary 68Q06, 05C05, 68V05} \keywords{Sorting networks, Bose--Nelson problem, comparator networks, lower bounds, computer-assisted proof} \setlength{\emergencystretch}{1.5em} \begin{document} \begin{abstract} Let $S(N)$ be the least number of comparators in a sorting network on $N$ inputs (the Bose--Nelson problem). The values are known for $N\le12$, and for $13$ inputs the smallest known sorting network, found by Juill\'e, has $45$ comparators. We prove $S(13)\ge45$, so $S(13)=45$. Deleting the comparators met by the largest and the second largest input leaves a sorting network on $N-2$ inputs, so $S(N)\ge S(N-2)+P(2,N)$, where $P(2,N)$ is the least possible worst-case number of comparators met by these two values. Van Voorhis stated $P(2,N)\ge\cl{\lg F(N)}$ for an explicit function $F$, but Mericanii showed that his proof is invalid. We prove $P(2,N)=\cl{\lg F(N)}$ for $3\le N\le32$ by a finite search, which rests on the structure of the tree of paths of the largest value, the comparators on these paths, and a forest of comparators that carries the second largest value. With $S(11)=35$ this bound gives only $S(13)\ge44$. For $45$ we apply it to the suffix of a network: if a network with $L$ comparators sorts a set $X$ of $0$-$1$ vectors, then for suitable pairs of inputs the two values meet at most $L-c$ comparators, where $c$ is the cost of sorting the residual set left when their paths are deleted. A breadth-first search over the sets produced by prefixes of a hypothetical sorting network with $44$ comparators discards each set for which no single network stays within all these budgets, and no set survives at depth $25$. A separate verifier checks the certificate written by the search. Two proofs in Lean~4 check the same certificate, and in one of them Lean's kernel checks every computation, with only the standard axioms. Juill\'e's network is checked in the kernel as well. As a consequence, each of the twenty lower bounds on $S(N)$ for $13\le N\le32$ that rested on Van Voorhis's inequality is proved and raised by one. \end{abstract} \maketitle \section{Introduction}\label{sec:intro} A comparator network on $N$ inputs is a circuit of comparators, each of which outputs the larger and the smaller of its two input values on two separate leads. A sorting network delivers every input sequence in sorted order. The Bose--Nelson problem~\cite{BN62} asks for $S(N)$, the least number of comparators in a sorting network on $N$ inputs. Floyd and Knuth determined $S(N)$ for $N\le8$~\cite{FK73}, Codish, Cruz-Filipe, Frank and Schneider-Kamp proved $S(9)=25$ and $S(10)=29$~\cite{CCFS16}, and Harder proved $S(11)=35$ and $S(12)=39$~\cite{Har22}. Harder's bound $S(11)\ge35$ is backed by a certificate, which is checked by a program verified in Isabelle/HOL~\cite{Har19}. For $13$ inputs the smallest known sorting network, found by Juill\'e~\cite{Jui95}, has $45$ comparators, and Van Voorhis's one-value bound $S(N)\ge S(N-1)+\cl{\lg N}$~\cite{VV72a} gives $S(13)\ge43$. We close this gap. Throughout, a dagger ($\dagger$) marks a statement whose proof includes a computation. \begin{theorem}\label{thm:main} $S(13)=45$.\dg \end{theorem} The upper bound is Juill\'e's network. Both bounds are also proved in Lean~4 (Section~\ref{sec:lean}). \subsection*{Two values} In a chapter published the same year as the one-value bound~\cite{VV72b}, Van Voorhis followed the two largest inputs instead of one. Put the largest value on input $x$ and the second largest on input $y$. The comparators that these two values meet can be deleted, and the rest of the network sorts the other $N-2$ inputs. This gives \begin{equation}\label{eq:two} S(N)\ \ge\ S(N-2)+P(2,N), \end{equation} where $P(2,N)$ is the least possible worst-case number of comparators met by the two values, over all networks that deliver them to fixed outputs (Section~\ref{sec:defs}). Van Voorhis stated that $P(2,N)\ge\cl{\lg F(N)}$ for an explicit function $F$ (Section~\ref{ssec:F}). With $F(13)=392$ and $S(11)=35$ this gives $S(13)\ge 35+9=44$. Dobbelaere's table of sorting networks~\cite{Dob} has listed $44$ as the lower bound for $13$ inputs since 21 April 2025 (consulted on 18 October 2026), together with lower bounds for $14\le N\le32$, with the note ``on suggestion from Jelmer Firet and based on principles in'' Van Voorhis's chapter. In an audit of the chapter~\cite{Mer26}, however, Mericanii showed that its proof of $P(2,N)\ge\cl{\lg F(N)}$ is invalid. The proof identifies the comparators on the paths of the maximum with the $N-1$ comparators at which two such paths merge. This fails when a path of the maximum passes a comparator whose other input never carries the maximum, a \emph{pass-through}, and pass-throughs occur already in a size-optimal network on $3$ inputs. Mericanii proves the inequality for two classes of networks and leaves it open in general. The same work derives the tabulated lower bounds for $13\le N\le32$ from~\eqref{eq:two}, the one-value bound and $P(2,N)\ge\cl{\lg F(N)}$, and finds that each of them exceeds what the one-value bound alone gives. Each of these twenty values therefore depends on the disputed inequality. We do not repair Van Voorhis's argument. Instead, we compute $P(2,N)$ for $N\le32$. \begin{theorem}\label{thm:P} $P(2,N)=\cl{\lg F(N)}$ for $3\le N\le32$.\dg \end{theorem} The upper bound comes from an explicit network for each $N$ (Proposition~\ref{prop:upper}). The lower bound rests on a computation, which two observations keep small. First, after the second maximum meets the maximum, it travels through comparators that the maximum never visits, and it can re-enter the tree of paths of the maximum only through pass-throughs. Once we delete each pass-through whose other input never carries the second maximum, and each comparator off the tree with an input that never carries it (Lemma~\ref{lem:reduce}), the costs of all $N(N-1)$ runs are determined by the tree, the number of pass-throughs on each of its edges, and, for each place where the second maximum leaves the tree, the root and the depth at which it joins the forest that carries it on (Theorem~\ref{thm:config}). Kraft's equality characterizes the possible depths. Second, the paths of the maximum are short in any network with small cost (Lemma~\ref{lem:fixedx}), which bounds the height of the tree. At $N=13$ and $L=8$, for instance, only $4$ tree shapes and $25$ choices of the pass-through numbers remain, and the depth-first search over the forests rejects each of them. At $N=28$ and $L=11$ the search is far larger. For its hardest tree shapes we also discard partial assignments that a symmetry of the tree and its pass-throughs makes lexicographically smaller; at least one member of each class of assignments survives (Lemma~\ref{lem:sym}). \subsection*{Two values in the suffix} With $P(2,13)=9$ and $S(11)=35$, inequality~\eqref{eq:two} gives $S(13)\ge44$, and since $P(2,13)=9$ is exact it gives no more. It treats the comparators that the two values do not meet only through the single number $S(11)$. To reach $45$ we apply the two-value argument not to a whole network but to its suffix. Let $T$ be a sorting network with at most $44$ comparators, and let $X$ be the set of $0$-$1$ vectors produced by its first $k$ comparators. The remaining comparators sort $X$, and there are at most $44-k$ of them. Suppose that $X$ contains the vector with a single $1$ on a channel $x$ and the vector with $1$s on $x$ and on another channel $y$ (Definition~\ref{def:scen} gives the precise condition). Run the suffix with the largest value on $x$ and the second largest on $y$. Deleting the comparators that these two values meet leaves a network that sorts a set $Y_{xy}$ on $11$ channels, the \emph{core} of the pair. The suffix therefore meets the two values at most $44-k-s(Y_{xy})$ times in the run from $(x,y)$, where $s(Y)$ denotes the least size of a network that sorts $Y$. Different pairs now have different budgets. We call the resulting condition, that a single network stays within all these budgets, a \emph{weighted top-two instance}. If no network meets it, the prefix cannot be completed within $44$ comparators. Deciding a weighted instance is a finite problem. Section~\ref{sec:model} extends the structure theory of Section~\ref{sec:structure} from all pairs of inputs to an arbitrary set of pairs, and we decide such instances by a computer search over the possible configurations, whose tests Section~\ref{sec:checker} proves valid. The costs of the cores are bounded below in two ways. Deleting the comparators that the two values meet in the prefix leaves a network on $11$ channels whose outputs lie in the core, so $s(Y_{xy})\ge S(11)-(k-w)$ when the two values meet $w$ of the first $k$ comparators. Sharper bounds come from the same test one level down: a core $Y$ on $11$ channels has cores on $9$ channels, and if the weighted instance of $Y$ with budget $\theta-1$ is infeasible, then $s(Y)\ge\theta$. Its weights are exact costs of sets on $9$ channels, computed by Harder's program~\cite{HarRepo}, or bounds obtained from the instance on $9$ channels with exact costs of sets on $7$ channels. The search runs over prefixes, one layer per comparator, with each set taken up to permutation and complementation of the channels. Each comparator that is useful for the set of a prefix (Section~\ref{sec:sets}) gives a child, and a child of depth $k$ is discarded when its weighted instance with budget $44-k$ is infeasible for one of the two polarities of Definition~\ref{def:prune}. The surviving sets form the next layer. The layers grow to $142{,}881$ sets at depth $14$ and then shrink, and layer $25$ is empty. The search writes a certificate: a record for each child, which states whether the child survives, repeats an earlier child, or is discarded together with the weights that make its instance infeasible, and a record for each bound on a core that these weights use. A verifier, written from the format of the certificate and the mathematical description without the search code, checks all of them. The verifier and the search share only Harder's program for exact values. The verification relies on three components that it does not check: Harder's program for the exact costs of the $\nineexact$ sets on $9$ channels and the $\sevenexact$ sets on $7$ channels that the certificate uses, the bound $S(11)=35$, and the program that decides weighted instances. Section~\ref{sec:trust} states what each of them is trusted for and how it was tested. Section~\ref{sec:lean} gives two proofs of the lower bound in Lean~4, which check the same certificate without the verifier and without the program that decides weighted instances. Both derive $S(11)\ge35$ from Harder's certificate~\cite{Har19} and prove every bound on $9$ and $7$ channels that they need. In the first, the large computations run as compiled code. In the second, Lean's kernel checks every computation itself, and the proof uses only the standard axioms of Lean's logic. A short proof, also checked by the kernel, shows that Juill\'e's network sorts. \subsection*{Larger networks} Theorems~\ref{thm:main} and~\ref{thm:P} give lower bounds for larger $N$ as well. \begin{corollary}\label{cor:table} For $13\le N\le32$, $S(N)\ge\Lambda(N)+1$, where $\Lambda(N)$ is the value in Table~\ref{tab:chain}.\dg \end{corollary} The values $\Lambda(N)$ are the twenty tabulated lower bounds discussed above, so each of them is proved and raised by one. No step of this paper uses Van Voorhis's inequality $P(2,N)\ge\cl{\lg F(N)}$ or the argument of~\cite{VV72b}. \subsection*{Organization} Section~\ref{sec:defs} defines the model and $P(2,N)$, and proves~\eqref{eq:two}, the monotonicity of $P(2,N)$ and the upper bound in Theorem~\ref{thm:P}. Section~\ref{sec:structure} describes networks that deliver the two largest values to fixed outputs, and Section~\ref{sec:tsearch} gives the search for $P(2,N)$, its results and their independent checks, which prove Theorem~\ref{thm:P}. Section~\ref{sec:sets} recalls partial sorting networks and defines cores. Section~\ref{sec:bound} states the weighted two-value bound, Section~\ref{sec:model} reduces it to configurations, and Section~\ref{sec:checker} describes the search over configurations. Section~\ref{sec:cores} gives the bounds on cores, Section~\ref{sec:search} the search over prefixes and the proof of Theorem~\ref{thm:main}, Section~\ref{sec:cert} the certificate and its verification, and Section~\ref{sec:results} the results. Section~\ref{sec:trust} lists the trusted components and the cross-checks, Section~\ref{sec:lean} describes the proofs in Lean, and Section~\ref{sec:cons} proves Corollary~\ref{cor:table}. The programs, the certificates, the logs and the native Lean proofs are in the supplements~\cite{Supp,SuppTwo}. The kernel-checked proofs of both bounds are in~\cite{LeanKernel}, and that of $P(2,13)\ge9$ is in~\cite{SuppTwo}. \section{Comparator networks and the two-value bound}\label{sec:defs} In this section we fix the model, prove the two-value bound $S(N)\ge S(N-2)+P(2,N)$ and the monotonicity of $P(2,N)$, and construct the networks that give the upper bound in Theorem~\ref{thm:P}. \subsection{Comparator networks}\label{ssec:circuit} A \emph{comparator network} $T$ on a finite set $A$ of channels is a finite acyclic circuit made of input leads, one for each channel, and of comparators. A comparator $g$ has two input leads and two output leads, $\hi(g)$ and $\lo(g)$. Each lead is either an input lead of $T$ or an output lead of exactly one comparator, and it enters at most one comparator. The leads that enter no comparator are the \emph{outputs} of $T$, and there are $|A|$ of them. Given values on the input leads, each comparator puts the larger of its two input values on $\hi(g)$ and the smaller on $\lo(g)$. The size $|T|$ is the number of comparators. We write $[n]=\{0,\dots,n-1\}$ and speak of a network on $n$ inputs when $|A|=n$; renaming the channels then gives $A=[n]$. Such a network is a \emph{sorting network} if its outputs can be listed as $o_0,\dots,o_{n-1}$ so that, for all distinct input values, $o_i$ carries the value of rank $i$, counted from $0$. Drawing $T$ on channels along a topological order of its comparators gives a sequence of standard comparators, defined below, followed by a permutation of the channels~\cite[Section~2]{Har22}. Conversely, a sequence of comparators on channels is a network: the comparator $(i,j)$, for channels $i\ne j$, puts the maximum on channel $i$ and the minimum on channel $j$, and the outputs are identified with the channels. The comparator $(i,j)$ is \emph{standard} if $i>j$. A sorting network in the circuit model can be untangled into a standard sorting network with the same number of comparators~\cite[Exercise~5.3.4--16]{Knu98}, so $S(N)$ is the same in both models. \subsection{Runs and deleted paths}\label{ssec:runs} For distinct channels $x$ and $y$, the \emph{run} $(x,y)$ puts the largest value $M$ on $x$, the second largest value $m$ on $y$, and smaller distinct values on the other inputs. The value $M$ leaves every comparator it enters on $\hi$. The value $m$ leaves a comparator on $\lo$ if $M$ is on the other input lead, and on $\hi$ otherwise. Hence the leads that carry $M$ and $m$ depend only on $(x,y)$. We write $\Pi_x$ for the set of leads that carry $M$, which depends only on $x$, $\delta(x)$ for the number of comparators that $M$ enters, and $W(x,y)$ for the set of comparators with $M$ or $m$ on an input lead. A comparator that $m$ enters while $M$ is on its other input lead is a \emph{meeting}. Deleting a path is the operation of~\cite[Definition~13]{Har22}. For a channel $x$, the network $T/x$ on $A\setminus\{x\}$ is obtained from $T$ by deleting the leads of $\Pi_x$ and the comparators that they enter, and joining the other input lead of each such comparator to its $\lo$ output lead. The input lead $x$ and the output lead at the end of $\Pi_x$ disappear. \begin{lemma}\label{lem:twodel} Let $x\ne y$. In the run $(x,y)$ the value $m$ never occupies a lead of $\Pi_x$. The comparators of $W(x,y)$ are the $\delta(x)$ comparators that $M$ enters and the comparators of $T/x$ on the path that the maximum of $T/x$ takes from $y$, which are the comparators that $m$ enters and that are not meetings. Deleting this path from $T/x$ gives the network $(T/x)/y$, which has $|T|-|W(x,y)|$ comparators. \end{lemma} \begin{proof} Since $M$ occupies every lead of $\Pi_x$ in the run $(x,y)$, the value $m$ occupies none of them. When $m$ enters a comparator $g$ of $\Pi_x$, the value $M$ is on the other input lead, and $m$ leaves on $\lo(g)$, which is where the join of $T/x$ leads. At any other comparator $m$ leaves on $\hi$, as the maximum of $T/x$ does. Thus the leads of $m$ are those of the path of the maximum of $T/x$ from $y$, with the joins expanded, and the comparators that $m$ enters outside $\Pi_x$ are the comparators of $T/x$ on that path. \end{proof} \subsection{The quantity \texorpdfstring{$P(2,N)$}{P(2,N)} and the two-value bound}\label{ssec:P} \begin{definition}\label{def:P} A comparator network on $N\ge2$ inputs is \emph{top-two correct} if it has outputs $\oM\ne\om$ such that in each run $(x,y)$ the value $M$ ends on $\oM$ and $m$ ends on $\om$. For such a network $T$ let $p_2(T)=\max_{x\ne y}|W(x,y)|$. Let $P(2,N)$ be the least value of $p_2(T)$ over all top-two correct networks $T$ on $N$ inputs. \end{definition} A sorting network is top-two correct, with $\oM=o_{N-1}$ and $\om=o_{N-2}$. The next lemma is the two-value bound. Mericanii~\cite{Mer26} identifies it as equation~(2) of~\cite{VV72b} and does not dispute it. Its proof extends Harder's argument for one value~\cite[Lemma~16]{Har22} to two values. \begin{lemma}[two-value pruning]\label{lem:prune} Let $T$ be a sorting network on $N\ge3$ inputs. Then $|T|\ge S(N-2)+p_2(T)$. Hence $S(N)\ge S(N-2)+P(2,N)$. \end{lemma} \begin{proof} We fix $x\ne y$ and call a lead \emph{special} if it carries $M$ or $m$ in the run $(x,y)$. A comparator with two special input leads has two special output leads. A comparator with exactly one special input lead sends the special value to one output lead and the value of its other input lead to the other output lead, which is not special. We delete the comparators of $W(x,y)$ and the special leads, and for each deleted comparator with one special input lead we join its other input lead to its output lead that is not special. The result $T'$ is a comparator network with $|T|-|W(x,y)|$ comparators whose inputs are the $N-2$ inputs of $T$ other than $x$ and $y$. Let $z$ be distinct values on these inputs, and run $T$ on $z$ together with $M$ on $x$ and $m$ on $y$, where $M>m>\max z$. Induction along a topological order shows that each lead of $T'$ carries the same value in $T'$ as in $T$. Since $T$ sorts, $M$ and $m$ end on $o_{N-1}$ and $o_{N-2}$, and $o_0,\dots,o_{N-3}$ carry $z$ in increasing order. Therefore $T'$ is a sorting network on $N-2$ inputs, and $|T|-|W(x,y)|\ge S(N-2)$. Taking $(x,y)$ with $|W(x,y)|=p_2(T)$ gives the first inequality, and applying it to a sorting network with $S(N)$ comparators gives the second. \end{proof} \begin{lemma}[monotonicity]\label{lem:mono} $P(2,N)\le P(2,N+1)$ for $N\ge2$. \end{lemma} \begin{proof} Let $T$ be a top-two correct network on $N+1$ inputs with $p_2(T)=P(2,N+1)$, and fix an input $w$. A value below all others on $w$ leaves every comparator it enters on $\lo$, so it follows a fixed path. Delete each comparator on this path and join its other input lead to its $\hi$ output lead. The result $T'$ is a comparator network on the $N$ inputs other than $w$. In a run $(x,y)$ of $T'$, the values $M$ and $m$ follow the same leads as in the run $(x,y)$ of $T$ with the smallest value on $w$, except that they skip the deleted comparators, which they would have left on $\hi$ in $T$ as well. Hence $M$ and $m$ end on $\oM$ and $\om$, the network $T'$ is top-two correct, and each of its runs meets at most as many comparators as the same run in $T$. This gives $P(2,N)\le p_2(T')\le p_2(T)$. \end{proof} \begin{lemma}[Kraft]\label{lem:kraft} Consider rooted trees in which each vertex has zero or two children. \begin{enumerate}[label=(\alph*)] \item If the leaves of such a tree have depths $d_1,\dots,d_k$, then $\sum_i2^{-d_i}=1$. \item If integers $d_1,\dots,d_k\ge0$ satisfy $\sum_i2^{-d_i}=1$, some such tree has leaves at depths $d_1,\dots,d_k$. \item If $k\ge1$ and integers $\ell_1,\dots,\ell_k\ge0$ satisfy $\sum_i2^{-\ell_i}\le1$, some such tree has $k$ leaves at depths $d_i\le\ell_i$. \end{enumerate} \end{lemma} \begin{proof} (a) Replacing two sibling leaves at depth $d$ by their parent at depth $d-1$ preserves the sum, so induction on the number of vertices applies. (b) If $k=1$ then $d_1=0$. Otherwise let $D=\max_id_i\ge1$. Multiplying the equation by $2^D$ shows that the number of indices with $d_i=D$ is even, so we may replace two of them by one index with value $D-1$, build a tree by induction, and give that leaf two children. (c) While the sum is below $1$, decrease a largest $\ell_i$ by one. The sum is a multiple of $2^{-\max\ell_i}$, so it stays at most $1$. When it reaches $1$, apply (b). \end{proof} \subsection{Van Voorhis's function and the upper bound}\label{ssec:F} Let $B$ be a rooted tree with $N\ge2$ leaves in which each vertex has zero or two children. We call such a tree a \emph{binary tree}. For a vertex $u$ of $B$ let $D(u)$ be its depth, the root having depth $0$, and for an internal vertex $c$ let $h_1(c)$ and $h_2(c)$ be the heights of the subtrees at its two children, a leaf having height $0$. Put \[ a(c)=D(c)+1+h_1(c)+h_2(c),\qquad f(B)=\sum_c2^{a(c)},\qquad F(N)=\min_Bf(B), \] where $c$ ranges over the internal vertices of $B$ and $B$ over the binary trees with $N$ leaves. Van Voorhis introduced the function $F$~\cite{VV72b}. As checked in~\cite[Section~2]{Mer26}, $f$ satisfies the recursion of~\cite[Theorem~1]{VV72b}, and $\min_Bf(B)$ reproduces Van Voorhis's table of $F(N)$ for $N\le16$. We use the definition above for all $N$, as~\cite{Mer26} does. Table~\ref{tab:F} lists $F(N)$ for $N\le32$. We computed it by a dynamic program over the pairs (height, $f$), and the values for $13\le N\le32$ agree with~\cite[Section~4.2]{Mer26}. \begin{table}[ht] \centering\small \setlength{\tabcolsep}{3.2pt} \begin{tabular}{@{}l*{15}{r}@{}} \toprule $N$ & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 & 11 & 12 & 13 & 14 & 15 & 16 & 17\\ $F(N)$ & 8 & 16 & 36 & 52 & 80 & 96 & 168 & 200 & 256 & 288 & 392 & 424 & 480 & 512 & 784\\ $\cl{\lg F(N)}$ & 3 & 4 & 6 & 6 & 7 & 7 & 8 & 8 & 8 & 9 & 9 & 9 & 9 & 9 & 10\\ $\nu(N)$ & 3 & 4 & 5 & 6 & 6 & 6 & 7 & 8 & 8 & 8 & 8 & 8 & 8 & 8 & 9\\ \midrule $N$ & 18 & 19 & 20 & 21 & 22 & 23 & 24 & 25 & 26 & 27 & 28 & 29 & 30 & 31 & 32\\ $F(N)$ & 848 & 960 & 1024 & 1232 & 1296 & 1408 & 1472 & 1872 & 1936 & 2048 & 2112 & 2320 & 2384 & 2496 & 2560\\ $\cl{\lg F(N)}$ & 10 & 10 & 10 & 11 & 11 & 11 & 11 & 11 & 11 & 11 & 12 & 12 & 12 & 12 & 12\\ $\nu(N)$ & 10 & 10 & 10 & 10 & 10 & 10 & 10 & 10 & 10 & 10 & 10 & 10 & 10 & 10 & 10\\ \bottomrule \end{tabular} \caption{Van Voorhis's function $F(N)$, the value $\cl{\lg F(N)}$, and the bound $\nu(N)=\cl{\lg N}+\cl{\lg(N-1)}$ of Corollary~\ref{cor:nu}.}\label{tab:F} \end{table} \begin{proposition}\label{prop:upper} For each $N\ge2$ there is a top-two correct network on $N$ inputs with $2N-3$ comparators and $p_2\le\cl{\lg F(N)}$. Hence $P(2,N)\le\cl{\lg F(N)}$. \end{proposition} \begin{proof} Let $B$ be a binary tree with $f(B)=F(N)$, and let $K=\cl{\lg F(N)}$. The leaves of $B$ are the inputs, and each internal vertex $c$ of $B$ is a comparator whose input leads are the input leads or the $\hi$ outputs at its two children. The $\hi$ output of the root is $\oM$. In the run $(x,y)$ the value $M$ passes the $D(x)$ comparators above $x$. The value $m$ passes the comparators above $y$ up to $c=\lca_B(x,y)$, meets $M$ at $c$ and leaves on $\lo(c)$. These two paths contain at most $a(c)$ comparators, because $x$ and $y$ lie below different children of $c$. Each $a(c)$ is at most $K$, and $\sum_c2^{-(K-a(c))}=2^{-K}f(B)\le1$. By Lemma~\ref{lem:kraft}(c) there is a binary tree $R$ whose leaves are the $N-1$ leads $\lo(c)$, at depths at most $K-a(c)$. Each internal vertex of $R$ is a comparator whose input leads are the leads at its children, and the lead at the root of $R$ is $\om$. The value $M$ never enters $R$, so $m$ leaves each comparator of $R$ on $\hi$ and reaches $\om$ after at most $K-a(c)$ of them. So $|W(x,y)|\le K$. The network has $(N-1)+(N-2)$ comparators. \end{proof} \section{The structure of top-two correct networks}\label{sec:structure} In this section we show that the costs of all runs of a top-two correct network are determined by a small amount of data, which the search of Section~\ref{sec:tsearch} enumerates. Section~\ref{sec:model} extends the argument from all pairs of inputs to the pairs of a weighted instance. \subsection{The tree of maximum paths}\label{ssec:tree} A lead is \emph{red} if it lies in $\Pi_x$ for some input $x$, and \emph{blue} otherwise. The first lemma uses only the behaviour of $M$, so we state it for networks in which the maximum alone is delivered to a fixed output. It is also applied to pruned networks in Lemma~\ref{lem:fixedx}. \begin{lemma}[the tree of maximum paths]\label{lem:tred} Let $T$ be a comparator network on $n\ge2$ inputs in which the largest value ends on the same output $\oM$ whichever input carries it. \begin{enumerate}[label=(\alph*)] \item Input leads are red, each $\lo$ output is blue, and $\hi(g)$ is red if and only if $g$ has a red input lead. \item Join each red lead $\ell\ne\oM$ to $\hi(g)$, where $g$ is the comparator that $\ell$ enters. Then the red leads form a rooted tree with root $\oM$ whose leaves are the $n$ input leads. \item Call a comparator a \emph{branch node} if both of its input leads are red, a \emph{pass-through} if exactly one is, and \emph{blue} if neither is. There are exactly $n-1$ branch nodes. Contracting the vertices with one child in the tree of~\textup{(b)} gives a binary tree $B$ whose leaves are the inputs and whose internal vertices are the branch nodes, and each pass-through lies on an edge of $B$ or on the edge from the root of $B$ to $\oM$. \end{enumerate} \end{lemma} \begin{proof} (a) The input lead $x$ lies in $\Pi_x$. The maximum leaves each comparator on $\hi$, so no $\lo$ output is red. If an input lead of $g$ lies in $\Pi_x$, the maximum enters $g$ on it and leaves on $\hi(g)$, so $\hi(g)\in\Pi_x$. Conversely, if $\hi(g)\in\Pi_x$, the maximum entered $g$ on an input lead, which lies in $\Pi_x$. (b) Let $\ell\in\Pi_x$. If $\ell$ enters a comparator $g$, then $\hi(g)$ is the next lead of $\Pi_x$. Otherwise $\ell$ is an output that carries the maximum, so $\ell=\oM$. Since each lead enters at most one comparator, each red lead other than $\oM$ has exactly one successor, and since the circuit is acyclic, following successors from any red lead ends at $\oM$. A red lead that is not an input lead is $\hi(g)$ for a comparator $g$ with a red input lead, by~(a), and that input lead is a predecessor. An input lead is the output of no comparator, so it has no predecessor. Thus the leaves are the $n$ input leads. (c) A vertex $\hi(g)$ of the tree has one child for each red input lead of $g$, so it has one or two. A rooted tree with $n$ leaves in which each vertex other than a leaf has one or two children has exactly $n-1$ vertices with two children. Contracting the vertices with one child gives $B$. A pass-through $g$ gives the vertex $\hi(g)$, which has one child, so it lies on an edge of $B$ or above the root of $B$. \end{proof} From now on in this section, $T$ is a top-two correct network on $N\ge3$ inputs and $B$ is its tree. For a vertex $u$ of $B$ (an input or a branch node), $\seg(u)$ denotes the edge from $u$ to its parent, or from $u$ to $\oM$ if $u$ is the root, and $k(u)$ denotes the number of pass-throughs on $\seg(u)$. We number them $(u,1),\dots,(u,k(u))$ from below. The branch nodes and the pass-throughs are the \emph{red comparators}. For a red comparator $v$, let $u(v)=v$ if $v$ is a branch node and $u(v)=u$ if $v=(u,i)$, and let $A(v)$ be the set of red comparators above $v$ on the path to $\oM$, with $v$ excluded. For an input $x$, the comparators on the path from $x$ to $\oM$ are those that $M$ passes when it starts on $x$, so \[ \delta(x)=k(x)+\sum_{u}\bigl(1+k(u)\bigr), \] where $u$ runs over the proper ancestors of $x$ in $B$. For a branch node $c$ and an input $y$ below $c$, let $\pre(y,c)=k(y)+\sum_u(1+k(u))$ over the vertices $u$ strictly between $y$ and $c$, the number of comparators on the path from $y$ up to $c$, with $c$ excluded. For a pass-through $q=(w,i)$ and a branch node $e$ that is a proper ancestor of $w$, let \[ \cb(q,e)=1+\bigl(k(w)-i\bigr)+\sum_{z}\bigl(1+k(z)\bigr), \] where $z$ runs over the vertices strictly between $w$ and $e$. This is the number of red comparators from $q$ up to $e$, with $e$ excluded. A pass-through $q=(w,i)$ lies on the path from an input $x$ to $\oM$ exactly when $w$ is $x$ or an ancestor of $x$. \begin{remark}\label{rem:onevalue} The depth of $x$ in $B$ is at most $\delta(x)$, and some leaf of $B$ has depth at least $\cl{\lg N}$, by Lemma~\ref{lem:kraft}(a). Together with the pruning of one path~\cite[Lemma~16]{Har22} this gives the one-value bound $S(N)\ge S(N-1)+\cl{\lg N}$ of Van Voorhis~\cite{VV72a}. Mericanii~\cite[Section~6.1]{Mer26} reads Harder's proof of this bound~\cite[Lemma~17]{Har22} as identifying the comparators on the paths of the maximum with the branch nodes, and observes that this does not affect the bound. The argument above does not need the identification. \end{remark} \subsection{The runs}\label{ssec:truns} \begin{lemma}[the second maximum before the meeting]\label{lem:trun} Let $x\ne y$ and $c=\lca_B(x,y)$. \begin{enumerate}[label=(\alph*)] \item In the run $(x,y)$, the value $m$ passes the comparators on the path from $y$ up to $c$ without meeting $M$, meets $M$ at $c$ and leaves $c$ on $\lo(c)$. \item After $c$, $m$ can meet $M$ only at comparators of $A(c)$, and the leads of $m$ after $c$ depend only on $c$. \item $|W(x,y)|=\delta(x)+\pre(y,c)+\tau(c)$, where $\tau(c)$ is the number of comparators that $m$ enters after leaving $c$ and that do not belong to $A(c)$. \end{enumerate} \end{lemma} \begin{proof} In the run $(x,y)$ the leads that carry $M$ are those of $\Pi_x$. When $m$ enters a comparator $g$, the lead that carries $m$ is not in $\Pi_x$, so $m$ leaves on $\lo(g)$ exactly when the other input lead of $g$ lies in $\Pi_x$, that is, when $g$ is on the path from $x$ to $\oM$. (a) In the tree of Lemma~\ref{lem:tred}(b) the paths from $x$ and $y$ to $\oM$ meet at $c$ and coincide above it. While $m$ is on the path from $y$ below $c$, it enters either $c$ or a comparator below $c$ on the side of $y$. Such a comparator is not on the path from $x$, so $m$ leaves it on $\hi$, which is the next lead on the path from $y$. The other input lead of $c$ lies on the path from $x$, so $m$ leaves $c$ on $\lo(c)$. (b) After $c$ the value $m$ is on leads that come after $c$ in the circuit. The comparators on the path from $x$ below $c$ come before $c$, so $m$ does not enter them. Hence the only comparators where $m$ can meet $M$ are those of $A(c)$, and by the first paragraph the leads of $m$ after $c$ are determined by $\lo(c)$ and $A(c)$. (c) The run meets the $\delta(x)$ comparators on the path from $x$, the $\pre(y,c)$ comparators on the path from $y$ below $c$, which are not on the path from $x$, and the comparators that $m$ enters after $c$. By~(b), those of the latter that lie on the path from $x$ belong to $A(c)$. Since the circuit is acyclic, $m$ enters no comparator twice. \end{proof} The same argument applies to every meeting. If $m$ leaves a red comparator $v$ on $\lo(v)$ in some run, then $M$ was at $v$, the comparators that $M$ passes after $v$ are those of $A(v)$, and the leads of $m$ after $v$ depend only on $v$. We write $\tau(v)$ for the number of comparators that $m$ enters after leaving $v$ and that do not belong to $A(v)$. The \emph{walk} from $\lo(v)$ starts at $\lo(v)$ and, while the current lead enters a blue comparator $g$, moves to $\hi(g)$. It stops at a lead $\rho(v)$ that is an output or enters a comparator that is not blue, and $d(v)$ denotes the number of blue comparators it passes. For a pass-through $q$ and a red comparator $v$ such that $u(q)$ and $u(v)$ are incomparable in $B$, let $e(q,v)=\lca_B(u(q),u(v))$. \begin{lemma}[after a meeting]\label{lem:after} Let $v$ be a red comparator, and suppose that $m$ leaves $v$ on $\lo(v)$ in some run. In that run $m$ follows the walk from $\lo(v)$ and passes its $d(v)$ blue comparators, and one of the following holds. \begin{enumerate}[label=(\roman*)] \item $\rho(v)$ is an output. Then $\rho(v)=\om$ and $\tau(v)=d(v)$. \item $\rho(v)$ is the blue input lead of a pass-through $q\in A(v)$. Then $m$ meets $M$ at $q$, leaves on $\lo(q)$, and $\tau(v)=d(v)+\tau(q)$. \item $\rho(v)$ is the blue input lead of a pass-through $q\notin A(v)$. Then $u(q)$ and $u(v)$ are incomparable in $B$, the vertex $e=e(q,v)$ lies in $A(v)$, the value $m$ passes the $\cb(q,e)$ red comparators from $q$ up to $e$, none of which lies in $A(v)$, meets $M$ at $e$ and leaves on $\lo(e)$, and $\tau(v)=d(v)+\cb(q,e)+\tau(e)$. \end{enumerate} \end{lemma} \begin{proof} The leads of the walk are blue. The other input lead of a blue comparator is blue, so it does not carry $M$, and $m$ leaves on $\hi$, which is blue by Lemma~\ref{lem:tred}(a). Therefore $m$ follows the walk. If $\rho(v)$ is an output, $m$ ends on it, so $\rho(v)=\om$ because $T$ is top-two correct, and $\tau(v)=d(v)$. Otherwise $\rho(v)$ enters a comparator $q$ that is not blue and has the blue input lead $\rho(v)$, so $q$ is a pass-through. Since $q$ comes after $v$ in the circuit, $M$ is at $q$ exactly when $q\in A(v)$. In case~(ii), $M$ is on the red input lead of $q$, so $m$ leaves on $\lo(q)$, and $q$ itself is not counted in $\tau(v)$. This gives $\tau(v)=d(v)+\tau(q)$. In case~(iii), $m$ leaves $q$ on the red lead $\hi(q)$. If $u(q)$ were an ancestor of $u(v)$, or equal to $u(v)$ with $q$ above $v$, then $q$ would lie in $A(v)$. If $u(q)$ were a proper descendant of $u(v)$, or equal to $u(v)$ with $q$ below $v$, then $q$ would come before $v$ in the circuit. Hence $u(q)$ and $u(v)$ are incomparable, and $e$ is a proper ancestor of $u(v)$, hence $e\in A(v)$. At each pass-through above $q$ on $\seg(u(q))$, the value $m$ is on the red input lead and the other input lead is blue, so $m$ leaves on $\hi$. A branch node $z$ strictly between $u(q)$ and $e$ is not an ancestor of $u(v)$, so $z\notin A(v)$. It comes after $v$ in the circuit, so it is not on the path of $M$, and $m$ leaves it on $\hi$ and continues up $\seg(z)$, whose pass-throughs are not in $A(v)$ either. At $e$ the value $M$ arrives on the input lead on the side of $u(v)$ and $m$ on the other one, so $m$ leaves on $\lo(e)$. The comparators passed from $q$ up to $e$, with $e$ excluded, are the $\cb(q,e)$ red comparators counted above, and none of them is in $A(v)$, which gives the formula for $\tau(v)$. \end{proof} Each step of this recursion moves to a comparator of $A(v)$, so it ends, in case~(i). \subsection{Reduced networks and the forest of the second maximum}\label{ssec:reduce} The blue input lead of a pass-through is its \emph{port}. A blue lead is \emph{relevant} if it carries $m$ in some run. We call $T$ \emph{reduced} if \begin{enumerate}[label=(R\arabic*)] \item the port of each pass-through is relevant, and \item both input leads of each blue comparator are relevant. \end{enumerate} \begin{lemma}[reduction]\label{lem:reduce} For each top-two correct network $T$ there is a reduced top-two correct network $T^*$ on the same inputs such that each run meets at most as many comparators in $T^*$ as in $T$. \end{lemma} \begin{proof} Suppose a pass-through $q$ violates~(R1). Delete $q$, and join its red input lead to $\hi(q)$ and its port to $\lo(q)$. The port carries neither $M$, being blue, nor $m$, and $\lo(q)$ carries neither: it would carry $m$ only if $m$ entered on the port. A value $M$ or $m$ on the red input lead leaves $q$ on $\hi(q)$, because the port does not carry $M$. Thus in each run $M$ and $m$ follow the same leads as before, with $q$ skipped. Suppose a blue comparator $g$ has an input lead that is not relevant. Delete $g$, and join its other input lead to $\hi(g)$ and that input lead to $\lo(g)$. The value $M$ never enters $g$, and $m$ leaves $g$ on $\hi(g)$ whenever it enters, so again $M$ and $m$ follow the same leads, with $g$ skipped. Each deletion keeps the network top-two correct, increases no $|W(x,y)|$, and does not change which leads carry $m$, up to the joins. Repeat while~(R1) or~(R2) fails. This ends because each step removes a comparator. \end{proof} \begin{lemma}[the forest of the second maximum]\label{lem:forest} Let $T$ be reduced. \begin{enumerate}[label=(\alph*)] \item A relevant lead enters a blue comparator, or is the port of a pass-through, or is $\om$. \item Join each relevant lead that enters a blue comparator $g$ to $\hi(g)$. Then the relevant leads form a forest in which each vertex has zero or two children. Its roots are $\om$ and the ports. Its leaves are the leads $\lo(c)$ of all branch nodes $c$ and the leads $\lo(q)$ of those pass-throughs $q$ for which $\lo(q)$ is relevant. \item A blue lead that is not relevant enters no comparator. \item If $\lo(v)$ is relevant for a red comparator $v$, then $\rho(v)$ is the root of the tree that contains $\lo(v)$, and $d(v)$ is the depth of $\lo(v)$ in that tree. \end{enumerate} \end{lemma} \begin{proof} (a) A relevant lead is blue, so it does not enter a branch node. If it enters a pass-through, it is the port. If it enters no comparator, it is an output that carries $m$ in some run, so it is $\om$. (b) If a relevant lead enters a blue comparator $g$, then $\hi(g)$ carries $m$ whenever that lead does, so $\hi(g)$ is relevant. Each lead enters at most one comparator and the circuit is acyclic, so the joins form a forest. Its roots are the relevant leads that enter no blue comparator, which by~(a) and~(R1) are $\om$ and all ports. The lead $\om$ is relevant because $m$ ends there. The children of a vertex $\hi(g)$ are the two input leads of $g$, both relevant by~(R2). A relevant lead that is not $\hi(g)$ for a blue comparator $g$ is neither an input lead nor the $\hi$ output of a red comparator, since those are red. It is therefore $\lo(g)$ for a comparator $g$, which is not blue because $m$ leaves blue comparators on $\hi$. Each lead $\lo(c)$ of a branch node $c$ is relevant, since $m$ leaves $c$ on $\lo(c)$ in the runs $(x,y)$ with $\lca_B(x,y)=c$. (c) A blue lead does not enter a branch node. By~(R2) an irrelevant one enters no blue comparator, and by~(R1) it is the port of no pass-through. (d) The walk from $\lo(v)$ follows the joins of~(b). \end{proof} \subsection{Configurations}\label{ssec:tconfig} \begin{definition}\label{def:tconfig} A \emph{configuration} $\Gamma$ on $N$ inputs consists of \begin{enumerate}[label=(\roman*)] \item a binary tree $B$ whose leaves are the $N$ inputs, together with an edge from its root to $\oM$; \item a number $k(u)\ge0$ of pass-throughs $(u,1),\dots,(u,k(u))$ on each edge $\seg(u)$, numbered from below; the \emph{red nodes} are the internal vertices of $B$, called branch nodes, and the pass-throughs; \item for each red node $v$, either the mark \dead, allowed for pass-throughs only, or a \emph{source} $(\rho(v),d(v))$ consisting of a \emph{root} $\rho(v)$, which is $\om$ or a pass-through, and a \emph{depth} $d(v)\ge0$; the red nodes that are not \dead\ are \emph{live}; \end{enumerate} subject to two conditions: \begin{enumerate} \item[(K)] for each $r\in\{\om\}\cup\{\text{pass-throughs}\}$, the live red nodes with root $r$ form a nonempty set whose depths satisfy $\sum2^{-d}=1$; \item[(G)] the directed graph $G(\Gamma)$ on the red nodes, with an arc from each red node to the next red node above it and an arc from each live red node $v$ to its root whenever that root is a pass-through, is acyclic. \end{enumerate} A root that is a pass-through $q$ stands for the port of $q$. We call the pair $(B,k)$ of (i) and (ii) the \emph{skeleton} of $\Gamma$. The quantities $\delta$, $\pre$, $u(\cdot)$, $A(\cdot)$, $\cb$ and $e(\cdot,\cdot)$ are defined from the skeleton as in Sections~\ref{ssec:tree} and~\ref{ssec:truns}. For each live red node $v$, define $\tau_\Gamma(v)$ by the recursion of Lemma~\ref{lem:after}, \[ \tau_\Gamma(v)=\begin{cases} d(v) & \text{if }\rho(v)=\om,\\ d(v)+\tau_\Gamma(q) & \text{if }\rho(v)=q\in A(v),\\ d(v)+\cb(q,e(q,v))+\tau_\Gamma(e(q,v)) & \text{if }\rho(v)=q\notin A(v), \end{cases} \] and put $\tau_\Gamma(v)=\infty$ if the recursion reaches a \dead\ node. The \emph{cost} of the run $(x,y)$ is $\mathrm{cost}_\Gamma(x,y)=\delta(x)+\pre(y,c)+\tau_\Gamma(c)$ with $c=\lca_B(x,y)$, and $\Gamma$ is \emph{feasible at level $L$} if $\mathrm{cost}_\Gamma(x,y)\le L$ for all $x\ne y$. For an internal vertex $c$ of $B$ with children $c_1$ and $c_2$ and an input $x$ below $c_1$, put $\sigma(c,x)=L-\delta(x)-\max_{y\text{ below }c_2}\pre(y,c)$. \end{definition} In the third case of the recursion, $u(q)$ and $u(v)$ are incomparable by~(G). Otherwise $q$ would lie at or below $v$ on the path to $\oM$, as in the proof of Lemma~\ref{lem:after}, and the path from $q$ to $v$ in $G(\Gamma)$ together with the arc from $v$ to $q$ would form a cycle. Each step of the recursion moves strictly up, so $\tau_\Gamma$ is well defined. \begin{theorem}[reduction to configurations]\label{thm:config} Let $N\ge3$ and $L\ge0$. \begin{enumerate}[label=(\alph*)] \item If some top-two correct network on $N$ inputs has $p_2\le L$, then so does a reduced one, $T^*$, and the configuration of $T^*$ given by Lemmas~\ref{lem:tred} and~\ref{lem:forest} is feasible at level $L$ and gives each live red node a depth at most $L$. \item Conversely, each configuration $\Gamma$ feasible at level $L$ is realized by a top-two correct network in which the run $(x,y)$ meets exactly $\mathrm{cost}_\Gamma(x,y)$ comparators, for all $x\ne y$. \end{enumerate} \end{theorem} \begin{proof} (a) By Lemma~\ref{lem:reduce} we may assume that the network $T$ is reduced. Lemma~\ref{lem:tred} gives $B$ and the numbers $k(u)$. By Lemma~\ref{lem:forest}, give each branch node $c$, and each pass-through $q$ for which $\lo(q)$ is relevant, the source formed by the root and the depth of its $\lo$ output in the forest, and mark the other pass-throughs \dead. Condition~(K) holds by Lemma~\ref{lem:kraft}(a); each root is the root of some live red node, since the tree of the forest at that root has a leaf. An arc of $G(\Gamma)$ is a directed path in the circuit: from a red comparator up to the next one, or from a live red node $v$ through $\lo(v)$ and the blue comparators of its tree into the pass-through that is its root. Consequently, a cycle in $G(\Gamma)$ would give a cycle in the circuit, and~(G) holds. By Lemmas~\ref{lem:trun}, \ref{lem:after} and~\ref{lem:forest}(d), $|W(x,y)|=\mathrm{cost}_\Gamma(x,y)$ for all $x\ne y$. No recursion reaches a \dead\ node, because $m$ leaves each node that the recursion reaches on its $\lo$ output in the run. Hence $\Gamma$ is feasible at level $L$. For a live red node $v$, the value $m$ is on $\lo(v)$ in some run $(x,y)$, and that run passes the $d(v)$ blue comparators below $\rho(v)$ after $\lo(v)$, so $d(v)\le|W(x,y)|\le L$. (b) Build the circuit as follows. The red part is the tree $B$ with $k(u)$ comparators on each edge $\seg(u)$, each branch node taking the leads from its two children and each pass-through taking the lead from below on one input lead. Its top lead is $\oM$. For each root $r$, take a binary tree of blue comparators whose leaves are the $\lo$ outputs of the live red nodes with root $r$, at the prescribed depths (Lemma~\ref{lem:kraft}(b)). Each internal vertex of this tree is a comparator with the leads at its children as input leads. The lead at its root is the port of $r$, or the output $\om$ if $r=\om$. The $\lo$ outputs of \dead\ nodes and of blue comparators are outputs. A directed cycle in this circuit would give a cycle in $G(\Gamma)$, after each tree of blue comparators is contracted, so by~(G) the circuit is acyclic. The maximum, from each input, stays in the red part and ends on $\oM$, so the red comparators of this network are those of $\Gamma$. The proofs of Lemmas~\ref{lem:trun} and~\ref{lem:after} use top-two correctness only to identify the output in case~(i), and here each walk from a red node ends at its root by construction. Since $\Gamma$ is feasible, the recursion from each $\lo(c)$ avoids \dead\ nodes and ends at $\om$. Thus $m$ always ends on $\om$, the network is top-two correct, and $|W(x,y)|=\mathrm{cost}_\Gamma(x,y)$. \end{proof} \subsection{Isomorphic configurations}\label{ssec:iso} An \emph{isomorphism} from a binary tree $B$ onto a binary tree $B'$ is a bijection $h$ between their vertices that preserves the parent relation; it maps the root to the root and inputs to inputs. If $B'=B$, it is an \emph{automorphism} of $B$. The isomorphism classes of binary trees are the \emph{tree shapes}. For a configuration $\Gamma$ with skeleton $(B,k)$, let $h\Gamma$ denote the data consisting of the skeleton $(B',k\circ h^{-1})$, in which the pass-through $(h(u),i)$ is the image of the pass-through $(u,i)$, and of the assignment that gives the red node $h(v)$ the root $h(\rho(v))$ and the depth $d(v)$ if $v$ is live, and the mark \dead\ otherwise. Here $h(\om)=\om$. An automorphism $h$ of $B$ with $k\circ h^{-1}=k$ is an automorphism of the skeleton $(B,k)$. \begin{lemma}\label{lem:symcost} Let $\Gamma$ be a configuration with skeleton $(B,k)$, and let $h$ be an isomorphism from $B$ onto a binary tree $B'$. Then $h\Gamma$ is a configuration, $h$ carries $\delta$, $\pre$ and $\sigma$ of $\Gamma$ to those of $h\Gamma$, and $\mathrm{cost}_{h\Gamma}(h(x),h(y))=\mathrm{cost}_\Gamma(x,y)$ for all inputs $x\ne y$. In particular, $h\Gamma$ is feasible at level $L$ if and only if $\Gamma$ is. \end{lemma} \begin{proof} The quantities $\delta$, $\pre$, $\sigma$, $\lca_B$, $A(\cdot)$, $\cb$ and $e(\cdot,\cdot)$ are defined from the parent relation, the numbers $k$ and the positions of the pass-throughs on their edges, and $h$ carries each of them for $\Gamma$ to the same quantity for $h\Gamma$. For instance, $\delta$ takes the same value at $x$ for $\Gamma$ as at $h(x)$ for $h\Gamma$, and $e(h(q),h(v))=h(e(q,v))$. The red nodes with root $h(r)$ in $h\Gamma$ are the images of those with root $r$ in $\Gamma$, with the same depths, so~(K) holds for $h\Gamma$. The graph $G(h\Gamma)$ is the image of $G(\Gamma)$ under $h$, so~(G) holds. Induction along the recursion of Definition~\ref{def:tconfig} gives $\tau_{h\Gamma}(h(v))=\tau_\Gamma(v)$ for every live red node $v$, and the costs follow. \end{proof} The \emph{decorated canonical string} of the subtree at a vertex $u$ is $k(u)\mathtt{L}$ if $u$ is an input, and $k(u)\mathtt{(}s\mathtt{,}t\mathtt{)}$ otherwise, where $s$ and $t$ are the decorated canonical strings of the two children of $u$, with $s$ preceding or equal to $t$ lexicographically. Two subtrees have the same decorated canonical string if and only if some bijection between them preserves the parent relation and the numbers $k$. \subsection{Bounds for the search}\label{ssec:tbounds} \begin{lemma}[fixed-input bound]\label{lem:fixedx} Let $T$ be top-two correct on $N\ge3$ inputs, and let $x$ be an input. Then $\max_{y\ne x}|W(x,y)|\ge\delta(x)+\cl{\lg(N-1)}$. In particular, if $p_2(T)\le L$, then $\delta(x)\le H_L$ for each input $x$, where $H_L=L-\cl{\lg(N-1)}$, and $B$ has height at most $H_L$. \end{lemma} \begin{proof} We delete the comparators on the path from $x$ to $\oM$, join the other input lead of each to its $\lo$ output, and call the result $T_x$. It is the network $T/x$ of Section~\ref{ssec:runs}, on the $N-1$ inputs other than $x$. In the run $(x,y)$ of $T$, the value $m$ is never on a lead of $\Pi_x$. At a comparator on the path from $x$ it leaves on $\lo$, where the join takes it, and at every other comparator it leaves on $\hi$, as the maximum of $T_x$ does. Hence the leads of $m$ in the run $(x,y)$ are the leads of the path of the maximum of $T_x$ from $y$, up to the joins, and this path ends on $\om$ for every $y\ne x$. By Lemma~\ref{lem:tred}(c) applied to $T_x$, the tree of $T_x$ has $N-1$ leaves, so by Lemma~\ref{lem:kraft}(a) some leaf $y$ has depth at least $\cl{\lg(N-1)}$ in it. The path of $y$ in $T_x$ then passes at least $\cl{\lg(N-1)}$ comparators of $T_x$. In the run $(x,y)$ the value $m$ enters them, and they are not on the path from $x$. Therefore $|W(x,y)|\ge\delta(x)+\cl{\lg(N-1)}$. The depth of $x$ in $B$ is at most $\delta(x)$. \end{proof} \begin{corollary}\label{cor:nu} $P(2,N)\ge\nu(N):=\cl{\lg N}+\cl{\lg(N-1)}$ for $N\ge3$. \end{corollary} \begin{proof} Some leaf $x$ of $B$ has depth at least $\cl{\lg N}$ by Lemma~\ref{lem:kraft}(a), so $\delta(x)\ge\cl{\lg N}$, and Lemma~\ref{lem:fixedx} applies. \end{proof} Corollary~\ref{cor:nu} amounts to applying the one-value bound twice. For $3\le N\le32$ it equals $\cl{\lg F(N)}$ when $N\in\{3,4,6,10,11,18,19,20\}$, and it is smaller by one or two otherwise (Table~\ref{tab:F}). \begin{lemma}[budgets]\label{lem:budget} Let $\Gamma$ be a configuration feasible at level $L$, let $c$ be an internal vertex of $B$ with children $c_1$ and $c_2$, and let $x$ lie below $c_1$. Then \[ d(c)+\chi(c)\ \le\ \tau_\Gamma(c)\ \le\ \sigma(c,x), \] where $\chi(c)=\cb(\rho(c),e(\rho(c),c))$ if $\rho(c)$ is a pass-through outside $A(c)$, and $\chi(c)=0$ otherwise. \end{lemma} \begin{proof} The upper bound is $\mathrm{cost}_\Gamma(x,y)\le L$ for a $y$ below $c_2$ that maximizes $\pre(y,c)$. The lower bound follows from the recursion, since $\tau_\Gamma\ge0$. \end{proof} \section{Determining \texorpdfstring{$P(2,N)$}{P(2,N)}}\label{sec:tsearch} We now describe the search for a configuration feasible at level $L$, for given $N\ge3$ and $L$, prove that each of its tests is valid, and report the searches and their independent checks. Put $H_L=L-\cl{\lg(N-1)}$. \subsection{The basic search}\label{ssec:basic} \begin{enumerate}[label=(S\arabic*)] \item Enumerate the binary trees $B$ with $N$ leaves and height at most $H_L$, up to isomorphism. A tree is encoded by a canonical string: \texttt{L} for a leaf, and \texttt{(}$st$\texttt{)} for a tree with subtrees encoded by $s$ and $t$, where $s$ precedes or equals $t$ lexicographically. \item For each $B$, enumerate the numbers $k(u)\in\{0,\dots,H_L\}$ with $\delta(x)\le H_L$ for all inputs $x$, and keep one skeleton $(B,k)$ from each class under the automorphisms of $B$, using the decorated canonical string of Section~\ref{ssec:iso}. \item Compute $\sigma(c,x)$ for each internal vertex $c$ and each input $x$ below $c$, and discard the skeleton if some $\sigma(c,x)$ is negative. \item Search depth first over the red nodes: the internal vertices of $B$ in increasing order of $\min_x\sigma(c,x)$, then the pass-throughs. An internal vertex receives a root and a depth in $\{0,\dots,L\}$, and a pass-through receives the mark \dead\ or a root and a depth in $\{0,\dots,L\}$. A partial assignment is extended only if \begin{enumerate}[label=(\alph*)] \item at each root, the depths assigned so far satisfy $\sum2^{-d}\le1$, a depth $0$ occurs only as the only member, and a root whose sum has reached $1$ receives no further member; \item an arc from a red node $v$ to a pass-through $q$ is added only if the graph formed by the arcs from each red node to the next red node above it and the arcs to roots present so far has no path from $q$ to $v$; \item each internal vertex $c$ satisfies $d(c)+\chi(c)\le\sigma(c,x)$ for each input $x$ below $c$. \end{enumerate} \item At a complete assignment, check~(K) and evaluate $\mathrm{cost}_\Gamma(x,y)$ for all $x\ne y$. The configuration is feasible if no recursion reaches a \dead\ node and all costs are at most $L$. \item Build the network of each feasible configuration as in Theorem~\ref{thm:config}(b), simulate all $N(N-1)$ runs, and compare the largest simulated cost with the largest value of $\mathrm{cost}_\Gamma$. \end{enumerate} \begin{proposition}\label{prop:valid} If the search \textup{(S1)--(S5)} finds no feasible configuration for $(N,L)$, then $P(2,N)>L$. \end{proposition} \begin{proof} Suppose a top-two correct network on $N$ inputs has $p_2\le L$. Theorem~\ref{thm:config}(a) gives a reduced network $T^*$ with $p_2(T^*)\le L$ whose configuration $\Gamma$ is feasible at level $L$ and has depths at most $L$. Lemma~\ref{lem:fixedx}, applied to $T^*$, shows that the tree of $\Gamma$ has height at most $H_L$ and that $\delta(x)\le H_L$ for each $x$; in particular $k(u)\le\delta(x)\le H_L$ for each input $x$ below $u$. Let $B'$ be the tree listed by (S1) with the shape of the tree of $\Gamma$, and let $h_0$ be an isomorphism onto it. By Lemma~\ref{lem:symcost}, $h_0$ carries $\delta$, so (S2) enumerates the skeleton of $h_0\Gamma$ and keeps the skeleton of $h\Gamma$, where $h=\alpha h_0$ for some automorphism $\alpha$ of $B'$. By the same lemma, $h\Gamma$ is feasible at level $L$, has depths at most $L$ and satisfies $\delta(x)\le H_L$. Replace $\Gamma$ by $h\Gamma$. Each $\sigma(c,x)$ is at least $\tau_\Gamma(c)\ge0$ by Lemma~\ref{lem:budget}, so (S3) keeps the skeleton. Condition~(K) implies~(a) for each partial assignment, (G) implies~(b), and Lemma~\ref{lem:budget} gives~(c). So the search reaches the assignment of $\Gamma$, and (S5) reports it feasible. \end{proof} The programs decide whether a pass-through $q$ lies in $A(v)$, for a red node $v$, by testing whether $u(q)$ is equal to or an ancestor of the input $x$ at hand, for $x$ below $v$. For assignments that pass~(b) this gives the right answer for all such $x$, because a pass-through at or below $v$ on the side of $x$ would close a cycle with the arc from $v$ to $q$. \subsection{Three further tests}\label{ssec:extra} The program \texttt{abs9} adds the following three tests to (S1)--(S5). Each discards only partial data that admit no configuration feasible at level $L$, so Proposition~\ref{prop:valid} holds with them. \begin{enumerate}[label=(P\arabic*)] \item \emph{Path test.} After (S3), discard the skeleton if, for some input $x$ such that each pass-through lies on the path from $x$ to $\oM$, the internal vertices $c$ above $x$ satisfy $\sum_c2^{-\sigma(c,x)}>1$. \item \emph{Capacity test.} During (S4), let $U$ be the set of internal vertices not yet assigned. Call a root open if its sum is below $1$ and it has no member of depth $0$. For $c\in U$ and an open root $r$ that $c$ may join under~(b), let $\mu(c,r)$ be $\min_x\sigma(c,x)$ minus the value that $\chi(c)$ would take if $\rho(c)=r$, capped at $L$. The programs also evaluate a value of $\mu$ for roots that (b) forbids, and including such roots in the conditions below can only weaken the test. Prune if some $c\in U$ has $\mu(c,r)<0$ for each open root $r$, or if \[ \sum_{c\in U}2^{-\max_r\mu(c,r)}\ >\ \sum_{r\text{ open}}\Bigl(1-\sum_{v\text{ assigned to }r} 2^{-d(v)}\Bigr). \] \item \emph{Partial costs.} During (S4), define $\tau^-(v)$ by the recursion of Definition~\ref{def:tconfig} with $\tau^-(v)=0$ for red nodes that are not yet assigned or are \dead. Prune if $\delta(x)+\pre(y,c)+\tau^-(c)>L$ for some $x\ne y$ with $c=\lca_B(x,y)$. \end{enumerate} \begin{lemma}\label{lem:antichain} Let $\Gamma$ be feasible at level $L$, and let $x$ be an input such that each pass-through of $\Gamma$ lies on the path from $x$ to $\oM$. Then $\sum_c2^{-\tau_\Gamma(c)}\le1$ over the internal vertices $c$ above $x$, so the path test~\textup{(P1)} is valid. \end{lemma} \begin{proof} Let $T$ be the network of $\Gamma$ given by Theorem~\ref{thm:config}(b), let $T_x$ be as in the proof of Lemma~\ref{lem:fixedx}, and let $R_x$ be the tree of maximum paths of $T_x$ given by Lemma~\ref{lem:tred}(b), with root $\om$. For an internal vertex $c$ above $x$, the lead $\lo(c)$ lies in $R_x$, since it carries the maximum of $T_x$ when that maximum starts on an input $y$ with $\lca_B(x,y)=c$. The comparators of $T_x$ on the path in $R_x$ from $\lo(c)$ to $\om$ are the comparators that $m$ enters after leaving $c$ and that are not on the path from $x$, so there are $\tau_\Gamma(c)$ of them. We claim that no lead $\lo(c)$ lies on the path in $R_x$ from another lead $\lo(c')$ to $\om$. Suppose it did. Then in some run $m$ leaves $c'$, later enters $c$, and leaves $c$ on $\lo(c)$, so $c$ lies above $c'$ and $m$ arrives at $c$ on the input lead that is not on the path from $x$. That lead is red. By Lemma~\ref{lem:after}, $m$ is on a red lead only while it climbs from a pass-through $q$ to the vertex $e(q,v)$, where $v$ is the comparator of the previous meeting. Here $e(q,v)=c$, and $v$ lies on the path from $x$ below $c$, so $u(q)$ lies below the child of $c$ that is not on the path from $x$. Then $q$ is not on the path from $x$, contrary to the hypothesis. So the leads $\lo(c)$ form an antichain in $R_x$. Give the root of $R_x$ weight $1$, and let each vertex pass its weight to its child or split it equally between its two children. The leaves below a vertex then carry total weight equal to its weight, so the weights of an antichain sum to at most $1$. The weight of $\lo(c)$ is $2^{-j}$, where $j$ is the number of vertices with two children strictly above $\lo(c)$. Such a vertex is $\hi(g)$ for a comparator $g$ of $T_x$ on the path from $\lo(c)$, so $j\le \tau_\Gamma(c)$. Hence $\sum_c2^{-\tau_\Gamma(c)}\le1$. Since $\tau_\Gamma(c)\le\sigma(c,x)$ by Lemma~\ref{lem:budget}, a configuration with $\sum_c2^{-\sigma(c,x)}>1$ is not feasible. \end{proof} The hypothesis of Lemma~\ref{lem:antichain} cannot be dropped, however. Take the sorting network $(1,0),(2,0),(2,1)$ on $3$ inputs, written with the conventions of Section~\ref{ssec:circuit}; it is the network of~\cite[Proposition~3]{Mer26}. Its branch nodes are $c_1=(1,0)$ and $c_2=(2,1)$, and $(2,0)$ is a pass-through on the edge of input~$2$. For $x=0$ the value $m$ leaves $c_1$, enters $(2,0)$ through its port, climbs to $c_2$ and meets $M$ again there. So $\tau(c_1)=1$ and $\tau(c_2)=0$, and $\sum_c2^{-\tau(c)}=3/2$. At $L=3$ the path test would discard this skeleton, although the network has $p_2=3$. A missing antichain step of this kind is what~\cite{Mer26} found in Van Voorhis's argument. \begin{lemma}\label{lem:tcapacity} The tests \textup{(P2)} and \textup{(P3)} are valid. \end{lemma} \begin{proof} (P2) In a feasible completion each $c\in U$ is assigned to a root that is open at this node, since by~(K) a root whose sum has reached $1$ takes no further member, and by Lemma~\ref{lem:budget} its depth is at most $\mu(c,r)$ for its root $r$. It therefore adds at least $2^{-\max_r\mu(c,r)}$ to the sum at its root. By~(K) the total added at the open roots equals their remaining capacity, and the pass-throughs add nonnegative amounts. (P3) In a completion the terms fixed by the assigned red nodes do not change, and the other terms are nonnegative or infinite. Induction along the recursion gives $\tau^-(v)\le \tau_\Gamma(v)$ for every live red node $v$. \end{proof} \subsection{A symmetry reduction}\label{ssec:tsym} Let $v$ be an internal vertex of $B$ whose children $u_1$ and $u_2$ have the same decorated canonical string (Section~\ref{ssec:iso}). Then some bijection from the subtree at $u_1$ onto the subtree at $u_2$ preserves the parent relation and the numbers $k$. Let $g_v$ exchange the two subtrees by such a bijection and fix every other vertex. Then $g_v$ is an automorphism of the skeleton $(B,k)$, and $g_v^{-1}=g_v$. In~(S4) the red nodes are visited in a fixed order $s_1,\dots,s_n$. We order the possible values of a red node as follows: the mark \dead\ comes first, then the root $\om$, then the pass-throughs in a fixed order, and values with the same root are ordered by depth. Assignments are compared lexicographically through $(a(s_1),\dots,a(s_n))$. For an automorphism $g$ of the skeleton and a partial assignment $a$, $ga$ is defined as for configurations in Section~\ref{ssec:iso}, and a \emph{class} of assignments is an orbit of the group generated by the automorphisms $g_v$. \emph{Symmetry test.} Let $a$ be a partial assignment of $s_1,\dots,s_t$, and let $g=g_v$ for some $v$ as above. Since $g^{-1}=g$, the value $(ga)(s_j)$ is the value $a(g(s_j))$ with its root mapped by $g$, and it is defined when $g(s_j)$ is among $s_1,\dots,s_t$. Prune $a$ if for some such $g$ and some $j\le t$ the values $(ga)(s_i)$ with $i\le j$ are defined, $(ga)(s_i)=a(s_i)$ for $i{\raggedright\arraybackslash}p{0.275\textwidth}>{\raggedright\arraybackslash}p{0.41\textwidth}>{\raggedright\arraybackslash}p{0.27\textwidth}@{}} \toprule check & scope & outcome\\ \midrule \texttt{abs9} against \texttt{abs5} & all runs of Table~\ref{tab:runs} with $N\le17$, and $L=\cl{\lg F(N)}$ for $N\le8$ and $N=11$ & same verdicts and same numbers of feasible configurations\\ simulation (S6) of feasible configurations & $L=\cl{\lg F(N)}$: \texttt{abs5} for $N\le8$ and $N=11$, \texttt{abs9} also for $N=9,10$ & $1{,}258$ and $118{,}825$ configurations, no mismatch\\ networks of Proposition~\ref{prop:upper} & all $N(N-1)$ runs, $2\le N\le32$ & $p_2=\cl{\lg F(N)}$\\ method A: search over networks with exact state compression, isomorphism rejection and a Kraft prune & $3\le N\le13$ at $L=\cl{\lg F(N)}-1$, and witnesses at $L=\cl{\lg F(N)}$ for $N\le12$ & $P(2,N)$ as in Theorem~\ref{thm:P}, witnesses simulated\\ method A without the Kraft prune & $N=9$, $L=7$ & infeasible, $4{,}619{,}670$ states\\ methods B and C: search over the relaxed tree model, with and without a height bound & $3\le N\le13$, $L=\cl{\lg F(N)}-1$ and $\cl{\lg F(N)}$ & $P(2,N)$ as in Theorem~\ref{thm:P}\\ test of the prunes of method A & all $15{,}113{,}524$ states reachable with costs at most $L$, for $N=8$ and $L=6,7,8$ & the prunes remove no state from which a goal is reachable\\ tests of the relaxed tree model & $3{,}420$ random top-two correct networks with $3\le N\le8$ & no failure\\ one integer program per skeleton (HiGHS~\cite{HH18}) & $15$ pairs $(N,L)$ with $N\le13$, among them $(12,8)$ and $(13,8)$ & the same skeletons admit a feasible configuration as in \texttt{abs5}. At $(13,8)$ none of $508$ skeletons on ordered trees does\\ networks mapped into the model & $4{,}464{,}896$ top-two correct networks with $4\le N\le11$, among them all $3{,}972{,}276$ on $4$ inputs with at most $9$ comparators. Each is reduced, mapped to a configuration and run through the code of \texttt{abs5} & costs equal to simulation, each accepted at its own $p_2$, no failure\\ search over standard networks without the model & $(N,L)=(12,8),(13,8),(12,9),(13,9)$ & infeasible, infeasible, feasible ($21$ comparators), feasible ($23$)\\ tests of the two lower bounds and the symmetry reduction of that search & \lemmaprefixes\ prefixes of \lemmanets\ networks, $4\le N\le13$ & no violation\\ \texttt{abs9f} against \texttt{abs9} & all $22$ runs of \texttt{abs9} & same numbers of skeletons and feasible configurations for each shape\\ \texttt{abs9g} against \texttt{abs9f} & the same $22$ runs & feasible configurations in the same shapes; the same classes of feasible assignments with and without the test ($53{,}578$ at $(9,8)$)\\ split runs against unsplit runs & \splitcheckscope & skeletons, feasible configurations and complete assignments add up\\ the revisions of \texttt{abs9g} used at $N=28$ & $53$ small runs, and $42$ shares at $N=28$ & identical output\\ separate run at $N=28$ (\texttt{abs9} and two variants) & $62{,}522$ shapes & no feasible configuration; same numbers of skeletons as \texttt{abs9f} for each shape\\ \bottomrule \end{tabular} \caption{Independent checks of the computation of $P(2,N)$, and in the last five rows consistency checks of the programs used at $N=28$. The supplement~\cite{SuppTwo} lists the programs and logs for each row.}\label{tab:verify} \end{table} \section{Partial sorting networks and cores}\label{sec:sets} For $N=13$, Lemma~\ref{lem:prune} gives only $S(13)\ge44$ (Section~\ref{sec:intro}). From now on we apply the two-value argument to the suffix of a network instead. This section introduces the sets of $0$-$1$ vectors that prefixes of a network produce, the networks that sort them, and the cores of pairs of channels. \subsection{Partial sorting networks} For a set of channels $A$, a vector is an element $v\in\B^A$, $e_c$ denotes the vector with a single $1$ on channel $c$, and $\mathbf 1$ the vector of all $1$s. A network $T$ on $A$ \emph{sorts} a set $X\subseteq\B^A$ if its outputs can be listed as $o_0,\dots,o_{|A|-1}$ so that, for each input vector in $X$, the output values read in this order are nondecreasing. Let $s(X)$ be the least size of a network that sorts $X$. These are Harder's partial sorting networks~\cite[Definition~1]{Har22}: his networks may contain exchanges of channels, which the circuit model absorbs into the wiring. A permutation $\pi$ of the channels acts on vectors by moving coordinates, and $\bar X=\{\mathbf 1-v:v\in X\}$ is the complement of $X$. Sets related by a permutation of the channels, possibly combined with complementation, are \emph{similar}. \begin{lemma}\label{lem:sfacts} \begin{enumerate}[label=(\alph*)] \item $s(\B^n)=S(n)$. \item If $X\subseteq X'$ then $s(X)\le s(X')$. \item Similar sets have the same value of $s$. \end{enumerate} \end{lemma} \begin{proof} (a) A network sorts every input sequence if and only if it sorts all $0$-$1$ sequences~\cite[Section~5.3.4]{Knu98}, and a network in the circuit model that sorts can be untangled into a standard sorting network of the same size~\cite[Exercise~5.3.4--16]{Knu98}. (b) and (c) are Lemma~2 and Corollary~6 of~\cite{Har22}. \end{proof} A standard comparator $(i,j)$ maps a set $X$ to the set $X(i,j)$ of its images. It is \emph{useful} for $X$ if $X$ contains a vector $v$ with $(v_i,v_j)=(0,1)$ and a vector with $(v_i,v_j)=(1,0)$. If no vector of $X$ has $(v_i,v_j)=(0,1)$, the comparator leaves $X$ unchanged. If some vector does but none has $(1,0)$, it acts on $X$ as the exchange of channels $i$ and $j$. \subsection{Pruning and cores} \begin{definition}\label{def:prune} Let $X\subseteq\B^A$ and $\epsilon\in\{0,1\}$, the \emph{polarity}. A channel $c\in A$ is \emph{extremal} in $X$ for polarity $0$ if $e_c\in X$, and for polarity $1$ if $\mathbf 1-e_c\in X$. For polarity $0$ and an extremal channel $c$, let $R$ be the set of vectors $u\in X$ that can be reached from $e_c$ by a sequence of vectors of $X$ in which each vector arises from the previous one by changing one coordinate from $0$ to $1$. The \emph{pruned set} $X/c\subseteq\B^{A\setminus\{c\}}$ consists of the restrictions of the vectors of $R$ to $A\setminus\{c\}$. For polarity $1$, $X/c$ is the complement of $\bar X/c$, the latter taken for polarity $0$. \end{definition} The vectors of $R$ have a $1$ on channel $c$, so $X/c$ is contained in Harder's pruned set $\{u|_{A\setminus\{c\}}:u\in X,\ u_c=1\}$~\cite[Definition~18]{Har22}. \begin{lemma}[pruning a channel]\label{lem:prune1} Let $T$ sort $X\subseteq\B^A$ with outputs $o_0,\dots,o_{|A|-1}$, and let $c$ be extremal in $X$ for polarity $0$. Then $\Pi_c$ ends on $o_{|A|-1}$, and $T/c$ sorts $X/c$ with its outputs listed as $o_0,\dots,o_{|A|-2}$. \end{lemma} \begin{proof} On input $e_c$ the single $1$ follows $\Pi_c$, and since the output is sorted, $\Pi_c$ ends on $o_{|A|-1}$. Harder proves that $T/c$ sorts his pruned set~\cite[Lemma~20]{Har22}, which contains $X/c$. \end{proof} A \emph{maximal chain} of $\B^A$ is a sequence $u_0,\dots,u_{|A|}$ that starts at the zero vector and in which each vector arises from the previous one by changing one coordinate from $0$ to $1$. Harder calls a set \emph{well-behaved} if it is a union of maximal chains~\cite[Definitions~27 and~28]{Har22}. His program computes $s(X)$ for well-behaved sets~\cite[Corollary~56]{Har22}. \begin{lemma}[well-behaved sets]\label{lem:wb} Let $X\subseteq\B^A$ be well-behaved and let $c$ be extremal in $X$ for polarity $0$. Then $X/c$ is the union of the maximal chains of $\B^{A\setminus\{c\}}$ that are contained in Harder's pruned set. In particular, $X/c$ is well-behaved. For polarity $1$, too, $X/c$ is well-behaved. Consequently, the well-behaved sets are closed under comparators, similarity and pruning an extremal channel of either polarity, and every set obtained from $\B^n$ by these operations is well-behaved. \end{lemma} \begin{proof} Let $u\in X/c$ be the restriction of $\bar u\in R$. Some maximal chain of $\B^A$ inside $X$ passes through $\bar u$. Its part above $\bar u$, preceded by a sequence from $e_c$ to $\bar u$ as in Definition~\ref{def:prune}, runs from $e_c$ to $\mathbf 1$ inside $X$, and its restriction to $A\setminus\{c\}$ is a maximal chain through $u$ inside Harder's pruned set. Conversely, setting coordinate $c$ to $1$ in the vectors of a maximal chain of $\B^{A\setminus\{c\}}$ inside Harder's pruned set gives a sequence in $X$ from $e_c$ as in Definition~\ref{def:prune}, so the chain lies in $X/c$. Polarity $1$ follows by complementation. The set $\B^n$ is well-behaved, and comparators, permutations of the channels and complementation map well-behaved sets to well-behaved sets~\cite[Lemma~35 and Corollary~36]{Har22}. \end{proof} \begin{definition}\label{def:scen} Let $X\subseteq\B^n$ and let $\epsilon$ be a polarity. A \emph{scenario} of $(X,\epsilon)$ is a pair $(x,y)$ of channels such that $x$ is extremal in $X$ and $y$ is extremal in $X/x$, both for polarity $\epsilon$. Its \emph{core} is the set $Y_{xy}=(X/x)/y\subseteq\B^{[n]\setminus\{x,y\}}$, where $[n]=\{0,\dots,n-1\}$. \end{definition} \begin{remark}\label{rem:pol} A channel is extremal in $X$ for polarity $1$ exactly when it is extremal in $\bar X$ for polarity $0$, and $X/c$ for polarity $1$ is the complement of $\bar X/c$ for polarity $0$. Hence the scenarios of $(X,1)$ are those of $(\bar X,0)$, and their cores are the complements of the cores of $(\bar X,0)$. By Lemma~\ref{lem:sfacts}(c) they have the same values of $s$. \end{remark} \begin{lemma}[two values]\label{lem:twoval} Let $T$ sort $X\subseteq\B^n$ with outputs $o_0,\dots,o_{n-1}$, and let $(x,y)$ be a scenario of $(X,0)$. In the run $(x,y)$ of $T$, the value $M$ ends on $o_{n-1}$ and $m$ ends on $o_{n-2}$, and $|T|-|W(x,y)|\ge s(Y_{xy})$. \end{lemma} \begin{proof} By Lemma~\ref{lem:prune1}, $\Pi_x$ ends on $o_{n-1}$ and $T/x$ sorts $X/x$ with outputs $o_0,\dots,o_{n-2}$. Since $y$ is extremal in $X/x$, the same lemma applied to $T/x$ shows that the path of the maximum of $T/x$ from $y$ ends on $o_{n-2}$ and that $(T/x)/y$ sorts $Y_{xy}$. By Lemma~\ref{lem:twodel} this path is the path of $m$, and $(T/x)/y$ has $|T|-|W(x,y)|$ comparators. \end{proof} \subsection{The trivial bound}\label{ssec:trivial} The bound of the next lemma uses only the comparators that produce $X$. \begin{lemma}[trivial bound]\label{lem:trivial} Let $P$ be a sequence of $k$ comparators on $n$ channels, and let $X$ be the set of outputs of $P$ on $\B^n$. For channels $i\ne j$, let $x$ and $y$ be the channels on which $M$ and $m$ end in the run $(i,j)$ of $P$, and let $w=|W(i,j)|$. Then $(x,y)$ is a scenario of $(X,0)$, and \[ s(Y_{xy})\ \ge\ S(n-2)-(k-w). \] The same holds for polarity $1$ with the run that has the smallest value on $i$ and the second smallest on $j$. \end{lemma} \begin{proof} Let $P_{ij}=(P/i)/j$. By Lemma~\ref{lem:twodel} it has $k-w$ comparators. Its input channels are $[n]\setminus\{i,j\}$, and its outputs are the channels other than $x$ and $y$. On an input vector with a $1$ on channel $i$, the leads of $\Pi_i$ carry $1$, because comparator networks are monotone. Hence $P$ and $P/i$ agree on the remaining leads~\cite[proof of Lemma~16]{Har22}. Applying the same argument to $P/i$ and channel $j$ shows, for every $z\in\B^{[n]\setminus\{i,j\}}$, that $P(e_i+e_j+z)$ has $1$s on $x$ and $y$ and agrees with $P_{ij}(z)$ on the other channels. Since the map $P$ is monotone and preserves the number of $1$s, a vector $u'$ that arises from $u$ by changing one coordinate from $0$ to $1$ is mapped to a vector that arises from $P(u)$ in the same way. Starting from $e_i$, adding the $1$ on $j$ and then the $1$s of $z$ one at a time gives vectors whose images form a sequence in $X$ from $P(e_i)=e_x$ through $P(e_i+e_j)=e_x+e_y$ to $P(e_i+e_j+z)$, each arising from the previous one by changing one coordinate from $0$ to $1$. Hence $x$ is extremal in $X$, $y$ is extremal in $X/x$, and $P_{ij}(z)\in Y_{xy}$ for all $z$. If a network $U$ sorts $Y_{xy}$, then $P_{ij}$ followed by $U$ sorts $\B^{[n]\setminus\{i,j\}}$, so $s(Y_{xy})+k-w\ge S(n-2)$ by Lemma~\ref{lem:sfacts}(a). For polarity $1$, apply this to the sequence $\bar P$ obtained from $P$ by replacing each comparator $(a,b)$ with $(b,a)$. Since it maps $\mathbf 1-u$ to $\mathbf 1-P(u)$, its set of outputs is $\bar X$, and its run with the largest values on $i$ and $j$ is the run of $P$ with the smallest values there. By Remark~\ref{rem:pol}, the scenarios and cores of $(\bar X,0)$ give those of $(X,1)$. \end{proof} \section{The weighted two-value bound}\label{sec:bound} \begin{definition}\label{def:inst} A \emph{weighted instance} $I$ on a set of $n$ channels consists of a budget $L\ge0$ and a finite list of \emph{scenarios} $(x,y,v)$, where $x\ne y$ are channels and $v\ge0$ is an integer, the \emph{weight}. Let $E$ be the set of pairs $(x,y)$ that occur in scenarios, and for $(x,y)\in E$ let $V(x,y)$ be the largest weight of a scenario on $(x,y)$ and $b(x,y)=L-V(x,y)$. The instance is \emph{feasible} if there are a comparator network $T$ on the $n$ channels and two distinct outputs $\oM$ and $\om$ of $T$ such that, for each $(x,y)\in E$, the run $(x,y)$ of $T$ ends with $M$ on $\oM$ and $m$ on $\om$, and $|W(x,y)|\le b(x,y)$. \end{definition} For a set $X\subseteq\B^n$, a polarity $\epsilon$, integers $v_t$ indexed by the scenarios $(x_t,y_t)$ of $(X,\epsilon)$, and a budget $L$, let $I(X,\epsilon;v;L)$ denote the weighted instance with budget $L$ and scenarios $(x_t,y_t,v_t)$. \begin{proposition}[weighted two-value bound]\label{prop:bound} Let $X\subseteq\B^n$, let $\epsilon$ be a polarity, and let $v_t$ be integers with $0\le v_t\le s(Y_t)$ for each scenario $(x_t,y_t)$ of $(X,\epsilon)$ with core $Y_t$. If $s(X)\le L$, then $I(X,\epsilon;v;L)$ is feasible. Hence, if $I(X,\epsilon;v;L)$ is infeasible, then $s(X)\ge L+1$. \end{proposition} \begin{proof} For polarity $0$, let $T$ sort $X$ with $s(X)$ comparators and outputs $o_0,\dots,o_{n-1}$. By Lemma~\ref{lem:twoval}, each run $(x_t,y_t)$ ends with $M$ on $o_{n-1}$ and $m$ on $o_{n-2}$, and $|W(x_t,y_t)|\le s(X)-s(Y_t)\le L-v_t$. With $\oM=o_{n-1}$ and $\om=o_{n-2}$, the network $T$ shows that the instance is feasible. For polarity $1$, Remark~\ref{rem:pol} shows that $I(X,1;v;L)=I(\bar X,0;v;L)$ and that the cores of $(\bar X,0)$ have the same values of $s$, and $s(\bar X)=s(X)$. \end{proof} For $X=\B^n$ and polarity $0$, every pair of distinct channels is a scenario, and every core is the full set on the other $n-2$ channels. With all weights equal to $S(n-2)$, the instance with budget $L$ is feasible exactly when some top-two correct network has $p_2\le L-S(n-2)$ (Definition~\ref{def:P}). The weighted bound thus generalizes the two-value bound $S(n)\ge S(n-2)+P(2,n)$ of Lemma~\ref{lem:prune}. In our application $X$ is the set produced by a prefix of a network, the weights are lower bounds on the costs of the cores (Section~\ref{sec:cores}), and different scenarios have different budgets. \section{From feasible networks to configurations}\label{sec:model} In this section we show that a feasible weighted instance has a \emph{valid configuration}, a finite object that the search of Section~\ref{sec:checker} enumerates. The argument extends Section~\ref{sec:structure}, where every pair of inputs is a scenario, to an arbitrary set of scenarios. Throughout, $I$ is a weighted instance with $E\ne\emptyset$, and $T$ with outputs $\oM$ and $\om$ shows that $I$ is feasible. Let $P'=\{x:(x,y)\in E\}$. The channels $y\notin P'$ with $(x,y)\in E$ for some $x$ are the \emph{blue starts}. For a channel $y$ let $E^y=\{x:(x,y)\in E\}$, and for $x\in P'$ let $E_x=\{y:(x,y)\in E\}$. \subsection{The tree of maximum paths} A lead of $T$ is \emph{red} if it lies in $\Pi_x$ for some $x\in P'$, and \emph{blue} otherwise. With this meaning of red, branch nodes, pass-throughs, blue comparators and ports are defined as in Sections~\ref{ssec:tree} and~\ref{ssec:reduce}. \begin{lemma}\label{lem:red} \begin{enumerate}[label=(\alph*)] \item The input lead of a channel $x$ is red exactly when $x\in P'$. Each $\lo$ output is blue, and $\hi(g)$ is red if and only if $g$ has a red input lead. \item Join each red lead $\ell\ne\oM$ to $\hi(g)$, where $g$ is the comparator that $\ell$ enters. Then the red leads form a rooted tree with root $\oM$ whose leaves are the input leads of the channels in $P'$. \item There are exactly $|P'|-1$ branch nodes. Contracting the vertices with one child in the tree of~\textup{(b)} gives a binary tree $B$ whose leaves are the channels of $P'$ and whose internal vertices are the branch nodes. Each pass-through lies on an edge of $B$ or on the edge from the root of $B$ to $\oM$. \end{enumerate} \end{lemma} \begin{proof} The proof of Lemma~\ref{lem:tred} applies to the paths $\Pi_x$ with $x\in P'$. Each of them ends on $\oM$, because some scenario has $M$ on $x$. The input lead of a channel outside $P'$ lies on none of them, since a path $\Pi_x$ starts at the input lead of $x$ and input leads are outputs of no comparator. \end{proof} For this tree we use the notation of Section~\ref{ssec:tree}: the segments $\seg(u)$, the numbers $k(u)$, the pass-throughs $(u,1),\dots,(u,k(u))$, the red comparators, $u(v)$, $A(v)$ and $\cb(q,e)$, and, for channels $x,y\in P'$, the numbers $\delta(x)$ and $\pre(y,c)$, given by the same formulas. The red comparators on the path from $x\in P'$ to $\oM$ are the comparators that $M$ enters in the runs from $x$, and a pass-through $q=(w,i)$ lies on this path exactly when $w$ is $x$ or an ancestor of $x$. \subsection{The runs} For a blue lead $\ell$, the \emph{walk} from $\ell$ is defined as in Section~\ref{ssec:truns}: it starts at $\ell$ and, while the current lead enters a blue comparator $g$, moves to $\hi(g)$. It stops at a lead $\rho(\ell)$ that is an output or enters a comparator that is not blue, and $d(\ell)$ denotes the number of blue comparators that it passes. Since a blue lead does not enter a branch node, $\rho(\ell)$ is the port of a pass-through whenever it is not an output. \begin{lemma}\label{lem:walk} Suppose that $m$ is on a blue lead $\ell$ in the run $(x,y)$, where $(x,y)\in E$. Then $m$ follows the walk from $\ell$, none of the $d(\ell)$ blue comparators on it is a meeting, and one of the following holds. \begin{enumerate}[label=(\roman*)] \item $\rho(\ell)$ is an output. Then $\rho(\ell)=\om$, and $m$ ends there. \item $\rho(\ell)$ is the port of a pass-through $q$ that lies on $\Pi_x$. Then $q$ is a meeting, and $m$ leaves $q$ on $\lo(q)$. \item $\rho(\ell)$ is the port of a pass-through $q=(w,i)$ that does not lie on $\Pi_x$. Then $e=\lca_B(w,x)$ is a proper ancestor of $w$, $m$ passes the $\cb(q,e)$ red comparators from $q$ up to $e$, none of which is a meeting, meets $M$ at $e$, and leaves $e$ on $\lo(e)$. \end{enumerate} \end{lemma} \begin{proof} The other input lead of a blue comparator is blue and does not carry $M$. The value $m$ therefore leaves on $\hi$, which is blue by Lemma~\ref{lem:red}(a), and it follows the walk. In case (i), $m$ ends on $\rho(\ell)$, which is $\om$ because $(x,y)\in E$. In case (ii), $M$ is on the red input lead of $q$. In case (iii), $M$ is not at $q$. Then $m$ leaves on the red lead $\hi(q)$, and $w$ is neither $x$ nor an ancestor of $x$. From then on $m$ climbs the tree of Lemma~\ref{lem:red}(b). At a pass-through on the way, the other input lead is the port, which never carries $M$. At a branch node $z$ strictly between $w$ and $e$, the other input lead comes from the subtree of $z$ that does not contain $w$. Since $z$ is not an ancestor of $x$, that subtree does not contain $x$, and the lead does not carry $M$. Hence $m$ leaves each of these comparators on $\hi$. At $e$ the value $M$ arrives from the side of $x$ and $m$ from the side of $w$, and $m$ leaves on $\lo(e)$. \end{proof} \begin{lemma}\label{lem:runs} Let $(x,y)\in E$. \begin{enumerate}[label=(\alph*)] \item If $y\in P'$ and $c=\lca_B(x,y)$, then $m$ passes the $\pre(y,c)$ red comparators below $c$ on the path from $y$, none of which is a meeting, meets $M$ at $c$ and leaves $c$ on $\lo(c)$. \item If $m$ leaves a red comparator $v$ on $\lo(v)$, then from there on, the comparators that $m$ enters, and which of them are meetings, depend only on $v$. We write $\tau(v)$ for the number of those comparators that are not meetings. \item $|W(x,y)|=\delta(x)+\pre(y,c)+\tau(c)$ if $y\in P'$ and $c=\lca_B(x,y)$, and $|W(x,y)|=\delta(x)+r_x(y)$ if $y$ is a blue start, where $r_x(y)$ is the number of comparators that $m$ enters in the run $(x,y)$ and that are not meetings. \end{enumerate} \end{lemma} \begin{proof} (a) The proof of Lemma~\ref{lem:trun}(a) applies. (b) After $v$ the value $M$ passes the comparators of $A(v)$. The comparators of $\Pi_x$ below $v$ come before $v$ in the circuit, and $m$ enters only comparators after $v$. Whether $m$ leaves a comparator on $\lo$ therefore depends only on its current lead and on $A(v)$. (c) follows from (a), (b) and Lemma~\ref{lem:twodel}. \end{proof} For a red comparator $v$ that $m$ leaves on $\lo(v)$ in some run of a scenario, we call $v$ \emph{live}. Then $\lo(v)$ is blue, and Lemma~\ref{lem:walk} applies to it. If $\rho(\lo(v))$ is the port of a pass-through $q$, then $q$ comes after $v$ in the circuit. The comparators of $\Pi_x$ that come after $v$ are those of $A(v)$, so $q$ lies on $\Pi_x$ exactly when $q\in A(v)$. If $q\notin A(v)$, then $u(q)$ is not $u(v)$ or a descendant of $u(v)$: otherwise $q$ would lie in $A(v)$, be $v$ or come before $v$. As $x$ is $u(v)$ or lies below it, the vertex $\lca_B(u(q),x)$ of Lemma~\ref{lem:walk}(iii) is then $\lca_B(u(q),u(v))$, a proper ancestor of $u(v)$. This gives the recursion \begin{equation}\label{eq:tau} \tau(v)=\begin{cases} d(v) & \text{if }\rho(v)=\om,\\ d(v)+\tau(q) & \text{if }\rho(v)\text{ is the port of }q\in A(v),\\ d(v)+\cb(q,e)+\tau(e) & \text{if }\rho(v)\text{ is the port of }q\notin A(v)\text{, with }e=\lca_B(u(q),u(v)), \end{cases} \end{equation} where $\rho(v)=\rho(\lo(v))$ and $d(v)=d(\lo(v))$. For a blue start $y$ and $x\in E^y$, Lemma~\ref{lem:walk} applied to the input lead $y$ gives $r_x(y)=d(y)$ if $\rho(y)=\om$; $r_x(y)=d(y)+\tau(q)$ if $\rho(y)$ is the port of $q=(w,i)$ and $x$ lies below $w$ or equals it; and $r_x(y)=d(y)+\cb(q,e)+\tau(e)$ with $e=\lca_B(w,x)$ otherwise. Here $\rho(y)=\rho(\ell)$ and $d(y)=d(\ell)$ for the input lead $\ell$ of $y$. \subsection{Three properties of feasible networks} A pass-through $q$ has a \emph{climbing run} if, in the run of some scenario, $m$ enters the port of $q$ while $M$ is not at $q$. \begin{lemma}\label{lem:climbing} If $I$ is feasible, then some network $T$ with outputs $\oM$ and $\om$ shows this and has a climbing run for each of its pass-throughs. In such a network no pass-through lies on $\seg(\text{root of }B)$. \end{lemma} \begin{proof} Let $q$ be a pass-through without a climbing run, with red input lead $a$ and port $b$. Delete $q$, and join $a$ to $\hi(q)$ and $b$ to $\lo(q)$. In the run of a scenario, if $M$ is at $q$ then it is on $a$ and leaves on $\hi(q)$. If $m$ enters $q$ through $b$, then $M$ is at $q$, because there is no climbing run, and $m$ leaves on $\lo(q)$. If $m$ enters on $a$, then $M$ is not at $q$, since $M$ is not on $a$ and never on the blue lead $b$, and $m$ leaves on $\hi(q)$. In every scenario run, $M$ and $m$ therefore follow the same leads as before, with $q$ skipped, and the new network shows that $I$ is feasible. Since the runs are the same, the other comparators keep their kinds and the remaining pass-throughs keep their climbing runs. Repeating this ends, since each step removes a comparator. A pass-through on the segment of the root has no climbing run, because every path $\Pi_x$ with $x\in P'$ passes it. \end{proof} The \emph{source leads} are the leads $\lo(v)$ of the live red comparators $v$ and the input leads of the blue starts. \begin{lemma}[Kraft sums at a lead]\label{lem:kraftnet} For each lead $r$, the source leads $s$ with $\rho(s)=r$ satisfy $\sum_s2^{-d(s)}\le1$. \end{lemma} \begin{proof} Each lead on a walk, except its first lead, is $\hi(g)$ for a blue comparator $g$. A source lead is the $\lo$ output of a red comparator or an input lead, so it lies on no walk except its own, as the first lead. The walks to $r$ form a tree with root $r$ whose leaves are the source leads $s$ with $\rho(s)=r$, and the depth of $s$ in it is $d(s)$. A vertex $\hi(g)$ of this tree has at most two children, the input leads of $g$. Give the root weight $1$, and let each vertex pass its weight to its child or split it equally between its two children. The weight of a leaf is $2^{-j}\ge2^{-d(s)}$, where $j$ is the number of vertices with two children above it, and the weights of the leaves sum to $1$. \end{proof} \begin{lemma}\label{lem:ports} If each pass-through has a climbing run, then each port is $\rho(s)$ for some source lead $s$. \end{lemma} \begin{proof} Let $q$ be a pass-through and consider a climbing run of $q$. Before $m$ enters the port of $q$, it is on blue leads. Let $s$ be the last lead before the port at which $m$ either started or arrived from a red comparator $v$ on $\lo(v)$. In the first case $s$ is the input lead of a blue start, because input leads of $P'$ are red. In the second case $v$ is live. In both cases $s$ is a source lead. After $s$, the value $m$ passes only blue comparators until it reaches the port: it never enters a pass-through through its port on the way, since a meeting there would give a later $\lo$ output, and so would the meeting that ends a climb (Lemma~\ref{lem:walk}). The walk from $s$ thus ends at the port of $q$. \end{proof} \begin{lemma}[cap]\label{lem:cap} For each $x\in P'$, $\;2^{\delta(x)}\sum_{y\in E_x}2^{-b(x,y)}\le1$. \end{lemma} \begin{proof} Fix $x$. In the runs $(x,y)$ with $y\in E_x$ the value $M$ follows $\Pi_x$, and the next lead of $m$ depends only on its current lead. The leads of $m$ in these runs therefore form a tree with root $\om$ whose leaves are the input leads of the channels in $E_x$, since an input lead is the output of no comparator. Call a comparator \emph{binary} if both of its input leads lie in this tree. A binary comparator does not lie on $\Pi_x$, since one of its input leads would then carry $M$ in all these runs. In particular, it is not a meeting. With weights passed down from the root as in the proof of Lemma~\ref{lem:kraftnet}, the leaf $y$ receives $2^{-j_y}$, where $j_y$ is the number of binary comparators that $m$ enters in the run $(x,y)$, and these weights sum to $1$. By Lemma~\ref{lem:twodel}, $j_y\le|W(x,y)|-\delta(x)\le b(x,y)-\delta(x)$. Hence $\sum_y2^{-(b(x,y)-\delta(x))}\le1$. \end{proof} \subsection{Configurations}\label{ssec:config} The following definition adapts Definition~\ref{def:tconfig} to weighted instances. Besides adding the blue starts, it excludes pass-throughs on $\seg(\text{root})$, as Lemma~\ref{lem:climbing} permits, lets branch nodes be \dead, and replaces the equality~(K) by the inequality~(V1), which suffices by Lemma~\ref{lem:kraft}(c), together with~(V2). Below, a source also stands for the live red node or blue start that carries it. \begin{definition}\label{def:config} A \emph{configuration} $\Gamma$ for $I$ consists of \begin{enumerate}[label=(\roman*)] \item a binary tree $B$ whose leaves are the channels of $P'$, each once, with an edge $\seg(\text{root})$ from its root to $\oM$; \item numbers $k(u)\ge0$ for the vertices $u$ of $B$, with $k(\text{root})=0$, which give the pass-throughs $(u,i)$ with $1\le i\le k(u)$ and the red nodes as in Definition~\ref{def:tconfig}; \item for each red node $v$, either the mark \dead\ or a source $(\rho(v),d(v))$ as in Definition~\ref{def:tconfig}, where branch nodes may now be \dead\ as well; the red nodes that are not \dead\ are live; \item for each blue start $y$, a source $(\rho(y),d(y))$. \end{enumerate} \end{definition} The quantities $\delta$, $\pre$, $\cb$, $u(\cdot)$ and $A(\cdot)$ are defined from $(B,k)$ as above. A root that is a pass-through $q$ stands for the port of $q$. For a live red node $v$ whose root is a pass-through $q$, the \emph{successor} of $v$ is $q$ if $q\in A(v)$, and $\lca_B(u(q),u(v))$ otherwise. For a blue start $y$ whose root is a pass-through $q=(w,i)$ and for $x\in E^y$, the successor of $y$ for $x$ is $q$ if $x$ is $w$ or lies below $w$, and $\lca_B(w,x)$ otherwise. The values $\tau(v)$ of the live red nodes are defined by the recursion~\eqref{eq:tau}, and the values $r_x(y)$ of the blue starts by the formulas that follow it; a value is $\infty$ if the recursion reaches a \dead\ node. The \emph{LCA nodes} are the branch nodes $\lca_B(x,y)$ with $(x,y)\in E$ and $y\in P'$. For an LCA node $c$ let \[ \beta(c)=\min\bigl\{b(x,y)-\delta(x)-\pre(y,c):\ (x,y)\in E,\ y\in P',\ \lca_B(x,y)=c\bigr\}. \] \begin{definition}\label{def:valid} A configuration is \emph{valid} if it satisfies the following conditions. \begin{enumerate}[label=(V\arabic*)] \item For each root $r$, the sources with root $r$, of live red nodes and of blue starts, satisfy $\sum2^{-d}\le1$. \item Each pass-through is the root of some source. \item The directed graph on the red nodes with an arc from each red node to the next red node above it, and an arc from each live red node $v$ to its root whenever that root is a pass-through, is acyclic. \item Each LCA node is live, the successor of each live red node is live, and the successor of each blue start for each $x\in E^y$ is live. \item $\tau(c)\le\beta(c)$ for each LCA node $c$, and $\delta(x)+r_x(y)\le b(x,y)$ for each blue start $y$ and each $x\in E^y$. \item $2^{\delta(x)}\sum_{y\in E_x}2^{-b(x,y)}\le1$ for each $x\in P'$. \end{enumerate} \end{definition} By~(V3) the successor of a live red node $v$ lies in $A(v)$. If the root $q$ of $v$ is not in $A(v)$, then $q$ is neither $v$ nor below $v$, since the arc from $v$ to $q$ would close a cycle with the path from $q$ up to $v$. As in the paragraph before~\eqref{eq:tau}, $u(q)$ is then not $u(v)$ or a descendant of $u(v)$, so $\lca_B(u(q),u(v))$ is a proper ancestor of $u(v)$. Each step of the recursion therefore moves strictly up, and $\tau$ is well defined. For $(x,y)\in E$ the \emph{cost} is $\delta(x)+\pre(y,c)+\tau(c)$ with $c=\lca_B(x,y)$ if $y\in P'$, and $\delta(x)+r_x(y)$ if $y$ is a blue start. Condition~(V5) says that every cost is at most $b(x,y)$. \begin{theorem}[soundness]\label{thm:sound} If $I$ is feasible and $E\ne\emptyset$, then $I$ has a valid configuration. \end{theorem} \begin{proof} By Lemma~\ref{lem:climbing} we may assume that every pass-through of $T$ has a climbing run, and then $k(\text{root})=0$. Lemma~\ref{lem:red} gives $B$ and the numbers $k(u)$. Give each live red comparator $v$ the source $(\rho(\lo(v)),d(\lo(v)))$, mark the other red comparators \dead, and give each blue start $y$ the source $(\rho(\ell),d(\ell))$ of its input lead $\ell$. By Lemma~\ref{lem:walk}(i) and the discussion before~\eqref{eq:tau}, each root is $\om$ or the port of a pass-through, and the successors in the configuration are the comparators at which $m$ meets $M$ next in the network. These are live, which gives~(V4) together with Lemma~\ref{lem:runs}(a). The values $\tau$ and $r_x$ of the configuration are those of the network, by~\eqref{eq:tau}. By Lemma~\ref{lem:runs}(c) the costs are then the numbers $|W(x,y)|$, and~(V5) holds because $T$ shows that $I$ is feasible. (V1), (V2) and~(V6) are Lemmas~\ref{lem:kraftnet}, \ref{lem:ports} and~\ref{lem:cap}. Each arc of the graph of~(V3) is a directed path in the circuit: from a red comparator to the next one above it, or from $v$ through $\lo(v)$ and the blue comparators of its walk into the pass-through. A cycle in this graph would give a cycle in the circuit. \end{proof} \begin{remark}\label{rem:realize} Conversely, every valid configuration is realized by a network whose runs cost at most the costs of the configuration: build the red tree with its pass-throughs, and for each root a tree of blue comparators on the $\lo$ outputs of its live red nodes and the input leads of its blue starts, at depths at most the given ones, by Lemma~\ref{lem:kraft}(c). For budgets at most $56$, the program of Section~\ref{sec:checker} uses this construction to confirm each feasible answer by simulating every run. No part of the proof of Theorem~\ref{thm:main} uses this converse. \end{remark} \section{Deciding weighted instances}\label{sec:checker} The program \texttt{lb2cr} decides a weighted instance by searching for a valid configuration. If $E=\emptyset$ it answers that the instance is feasible, and if some $b(x,y)$ is negative it answers that it is infeasible. Otherwise it searches the configurations in a normal form, discards partial data that violate necessary conditions, and answers \emph{infeasible} only if the search finishes without finding one. By Theorem~\ref{thm:sound}, the instance is then infeasible. A third answer, \emph{unknown}, is given when a limit on the work is reached; the verification of Section~\ref{sec:cert} treats it as a failure. This section states the normal form and the necessary conditions, proves each of them, and describes the search. We fix an instance $I$ with $E\ne\emptyset$ and $b(x,y)\ge0$ for all $(x,y)\in E$. \subsection{Normal forms}\label{ssec:normal} A pass-through $q=(w,i)$ is \emph{readable} if some red node lies below it on the path to $\oM$, or some blue start $y$ has an $x\in E^y$ that is $w$ or lies below $w$. A branch node $e$ is readable if some pass-through lies on the segment of a proper descendant of $e$. By the recursion~\eqref{eq:tau} and the formulas for $r_x(y)$, the value $\tau(q)$ of a pass-through enters only the values of sources that meet at $q$, which lie below $q$, and of blue starts with $x$ equal to $w$ or below $w$, while $\tau(e)$ of a branch node enters only the values of sources whose root is a pass-through on the segment of a proper descendant of $e$. Only readable nodes can thus be successors. For a source $s$ whose successor is $s'$, we call $s$ a \emph{predecessor} of $s'$; a blue start $y$ is a predecessor of each of its successors for the $x\in E^y$. Let \[ B_{\max}=\max\Bigl(\{\beta(c):c\text{ an LCA node}\}\cup\{b(x,y)-\delta(x):y\text{ a blue start},\ x\in E^y\}\Bigr). \] A configuration is in \emph{normal form} if, besides being valid, it satisfies: \begin{enumerate}[label=(N\arabic*)] \setcounter{enumi}{2} \item each live red node that is not readable is an LCA node, and an LCA node $c$ that is not readable has the largest depth for which $\tau(c)\le\beta(c)$, given its root; \item $\tau(v)\le B_{\max}$ for each live red node $v$ that is not an LCA node; \item each blue start $y$ has the largest depth for which $\delta(x)+r_x(y)\le b(x,y)$ for all $x\in E^y$, given its root. \end{enumerate} The numbering follows~(N1), $k(\text{root})=0$, and~(N2), which is~(V2). \begin{lemma}[deletion]\label{lem:delete} Let $\Gamma$ be a configuration that satisfies all conditions of validity except possibly~(V2). Then deleting, one at a time, pass-throughs that are the root of no source gives a valid configuration. If $\Gamma$ violates~(V2), the result has fewer pass-throughs than $\Gamma$. \end{lemma} \begin{proof} Let $q=(w,i)$ be the root of no source, and delete it: $k(w)$ drops by one and the pass-throughs above $q$ on $\seg(w)$ move down one place. No successor is $q$, since a pass-through is a successor only of sources whose root it is. Since membership in $A(\cdot)$ is unchanged for the other red nodes and $B$ is unchanged, every other successor stays the same. The numbers $\delta$, $\pre$ and $\cb$ count red nodes on paths and do not increase. By induction along the recursion, no value $\tau$ or $r_x$ increases, and no $\beta(c)$ decreases. Conditions~(V4), (V5) and~(V6) therefore still hold. The source of $q$, if any, leaves the sum at its root, so~(V1) holds. A path in the new graph of~(V3) comes from a path in the old one, so~(V3) holds. Only~(V2) can fail, at the root of $q$, and then we repeat. This ends, since each step removes a pass-through. \end{proof} The formal configurations of the native Lean proof (Section~\ref{ssec:leannative}) also have a \emph{reachability condition}: every live red node can be reached from an LCA node or a blue start by a chain of successors. Deletions keep this condition: the deleted pass-through is the successor of no source, so it is not reached and hence \dead, and no other successor changes. \begin{lemma}[normal form]\label{lem:normal} Let $\Gamma$ be a valid configuration whose number of pass-throughs is the least among all valid configurations for $I$. Then some configuration with the same $B$ and $k$ is in normal form. \end{lemma} \begin{proof} Each step below keeps $(B,k)$, only marks nodes \dead\ or increases depths, and changes the values $\tau$ and $r_x$ only where stated. This keeps~(V1), (V3) and~(V6). If it left a pass-through that is the root of no source, Lemma~\ref{lem:delete} would give a valid configuration with fewer pass-throughs, contrary to the choice of $\Gamma$. Condition~(V2) is kept as well, and we check~(V4) and~(V5) at each step. (N4) Let $Z$ be the set of live red nodes $v$ that are not LCA nodes and have $\tau(v)>B_{\max}$. A predecessor $s$ of a node $v\in Z$ has $\tau(s)\ge\tau(v)$, or $r_x(s)\ge\tau(v)$ if $s$ is a blue start. It is not an LCA node, since those have $\tau\le\beta\le B_{\max}$, and not a blue start, since $r_x(y)\le b(x,y)-\delta(x)\le B_{\max}$. Thus $Z$ contains every predecessor of its members. Mark the nodes of $Z$ \dead. No live node outside $Z$ has its successor in $Z$, so~(V4) holds, and no value outside $Z$ changes, so~(V5) holds. (N3) A live red node $v$ that is not readable is the successor of no source. If it is not an LCA node, mark it \dead: no other value changes, and~(V4) holds. If it is an LCA node, its value $\tau(v)$ enters only the condition $\tau(v)\le\beta(v)$ of~(V5), and we raise its depth as far as that condition allows. This changes no other value. These changes do not affect~(N4). (N5) Since no source has a blue start as its successor, raising the depth of a blue start changes only its own values $r_x(y)$. We raise each depth as far as~(V5) allows. \end{proof} \begin{lemma}\label{lem:n9} Let $\Gamma$ be as in Lemma~\ref{lem:normal}. Then each pass-through $q=(w,i)$ of $\Gamma$ has an \emph{affordable climber}: an LCA node $c$ such that $q$ neither lies on the path from $c$ to $\oM$ nor below $c$, and $\beta(c)\ge\cb(q,\lca_B(w,c))$; or a blue start $y$ and an $x\in E^y$ that is not $w$ and not below $w$, with $b(x,y)-\delta(x)\ge\cb(q,\lca_B(w,x))$. \end{lemma} \begin{proof} A source with root $q$ \emph{climbs} through $q$ if its successor is not $q$; for a blue start this means that its successor for some $x\in E^y$ is a branch node. First, some source climbs through $q$. Otherwise every source $s$ with root $q$ has successor $q$, and $q$ is live by~(V4). Give each such $s$ the root $\rho(q)$ and the depth $d(s)+d(q)$. If $\rho(q)$ is $\om$ or a pass-through above $q$, then $s$ meets there as $q$ did. If $\rho(q)$ is a pass-through $q'$ not above $q$, then $q$ climbs to $e=\lca_B(u(q'),w)$, and since $s$ lies below $q$, or $x$ lies below $w$ for a blue start, the climb from $q'$ also ends at $e$ for $s$. In each case the value of $s$ is unchanged. The sum at $\rho(q)$ changes by $2^{-d(q)}(\mu-1)\le0$, where $\mu\le1$ is the sum at $q$. Each new arc of~(V3) replaces a path through $q$. Then mark $q$ \dead. Now $q$ is the root of no source, and Lemma~\ref{lem:delete} gives a valid configuration with fewer pass-throughs, a contradiction. Let $U$ be the set of sources that climb through $q$, and let $Z$ be the set of sources from which a chain of successors reaches a member of $U$. Suppose that $Z$ contains an LCA node or a blue start $c$, whose chain reaches $t\in U$. If $t$ is a red node, then $u(q)=w$ is not $u(t)$ or a descendant of $u(t)$ (see the remarks after Definition~\ref{def:valid}). If $c$ is an LCA node, then $c$ is $t$ or lies below $t$, so the climb from $q$ ends at the same branch node $e$ for $c$ as for $t$. Moreover $q$ does not lie on the path from $c$ to $\oM$: it would then lie above $t$, so that $t$ meets at $q$, or at or below $t$, which~(V3) excludes. Nor does $q$ lie below $c$, since it would then lie below $t$. If $c=y$ is a blue start, choose $x\in E^y$ as follows: if $t=y$, an $x$ for which the successor of $y$ is a branch node; otherwise an $x$ to which the chain from $y$ to $t$ belongs. In the second case every node of the chain lies on the path from $x$ to $\oM$, so $x$ lies in the subtree of $u(t)$, and $w$ is not $x$ and not an ancestor of $x$, since $q$ would otherwise lie in $A(t)$. In both cases $x$ is not $w$ and does not lie below $w$, and the climb from $q$ ends at the same branch node $e$ for $c$ as for $t$. In all cases the value of $c$ is at least that of $t$, which is at least $\cb(q,e)$, and the budget of $c$ is at least its value. Hence $c$ is an affordable climber. Otherwise $Z$ contains no LCA node and no blue start. Mark the nodes of $Z$ \dead. No live node outside $Z$ has its successor in $Z$, so~(V4) holds, and no value outside $Z$ changes. If a pass-through became the root of no source, Lemma~\ref{lem:delete} would contradict the choice of $\Gamma$. The result is therefore valid, with the same $(B,k)$, and no source climbs through $q$, which the first part excludes. \end{proof} \subsection{Necessary conditions on the tree and the pass-throughs}\label{ssec:treeconds} For $x\in P'$ let $\eta_x$ be the largest integer $a$ with $2^a\sum_{y\in E_x}2^{-b(x,y)}\le1$. As in Section~\ref{ssec:F}, $D(u)$ denotes the depth of a vertex $u$ of $B$, the root having depth $0$. \begin{lemma}\label{lem:treeconds} Every valid configuration satisfies the following. \begin{enumerate}[label=(\alph*)] \item $D(x)\le\delta(x)\le \eta_x$ for each $x\in P'$. Moreover, if numbers $c(x)\ge D(x)$ are given for the leaves $x$ of a subtree of $B$ whose root has depth $t$, then $\sum_x2^{-(c(x)-t)}\le1$ over these leaves, and $c(x)-t\ge1$ if the subtree has at least two leaves. \item $\delta(x)+\pre(y,c)\le b(x,y)$ for each $(x,y)\in E$ with $y\in P'$ and $c=\lca_B(x,y)$. In particular $D(x)+D(y)\le b(x,y)+D(c)+1$. \item $\beta(c)\ge0$ for each LCA node $c$, and $\delta(x)\le b(x,y)$ for each blue start $y$ and $x\in E^y$. \end{enumerate} \end{lemma} \begin{proof} (a) Each proper ancestor of $x$ contributes at least $1$ to $\delta(x)$, and~(V6) gives $\delta(x)\le \eta_x$. The leaves of a subtree satisfy Kraft's equality $\sum2^{-(D(x)-t)}=1$ (Lemma~\ref{lem:kraft}(a)), and $D(x)-t\ge1$ if there are at least two of them. (b) and (c) follow from~(V5), since $\tau$ and $r_x$ are nonnegative, and from $\pre(y,c)\ge D(y)-D(c)-1$. \end{proof} Since $\delta(x)=D(x)+\sum_uk(u)$ over $x$ and its proper ancestors, the conditions of~(b) and~(c), and those of~(a) other than the subtree condition, are linear inequalities in the numbers $k(u)$, with coefficients $0$ and $1$. For a segment $w$, let $k_{\max}(w)$ be the least right-hand side among the inequalities of~(a) and~(b) that contain $k(w)$. \subsection{Credit bounds}\label{ssec:credit} The following bounds compare the budgets with what the forest of sources can carry. Fix a valid configuration. Give each live red node $v$ the \emph{credit} $\kappa(v)=2^{-\tau(v)}$. For a blue start $y$ fix $x^*(y)\in E^y$ with the least value of $b(x,y)-\delta(x)$, put $\beta(y)=b(x^*(y),y)-\delta(x^*(y))$, and let $\kappa(y)=2^{-r_{x^*(y)}(y)}$. The \emph{parent} of a live red node is $\om$ if its root is $\om$, and its successor otherwise. The parent of a blue start $y$ is defined in the same way, with its successor for $x^*(y)$. Parents are live by~(V4), and they lie above their children on the path to $\oM$, so the parents form a tree with root $\om$, the \emph{flow tree}. Put $\kappa(\om)=1$. By~\eqref{eq:tau}, each child $s$ of a node $p$ satisfies \begin{equation}\label{eq:flow} \kappa(s)=\kappa(p)\,2^{-d(s)-\gamma(s)}, \end{equation} where $\gamma(s)=\cb(q,p)$ if $s$ climbs to $p$ through its root $q$, and $\gamma(s)=0$ otherwise. The LCA nodes and the blue starts are \emph{required}. The LCA nodes are live by~(V4), and the total credit $R^*$ of the required nodes satisfies \begin{equation}\label{eq:lhs} R^*\ \ge\ \Omega:=\sum_{c}2^{-\beta(c)}+\sum_y2^{-\beta(y)} \end{equation} by~(V5), where $c$ runs over the LCA nodes and $y$ over the blue starts. \begin{lemma}[gain bound]\label{lem:gain} $R^*\le1+\sum_w\bigl(1-2^{-k(w)}\bigr)$, where $w$ runs over the vertices of $B$. \end{lemma} \begin{proof} Sum~\eqref{eq:flow} over all nodes of the flow tree other than $\om$, and group the terms by the parent. The children of $\om$ contribute at most $1$, by~(V1). The children of a live pass-through $q$ meet at $q$ and contribute $\kappa(q)\mu_q$, where $\mu_q\le1$ is their part of the sum at $q$. The nodes that climb contribute a total $C$. Since every live pass-through is a node of the flow tree that is not required, \[ R^*\ \le\ 1+\sum_q\kappa(q)\mu_q+C-\sum_q\kappa(q)\ \le\ 1+C. \] A source that climbs through $q=(w,i)$ to $p$ has $\gamma=\cb(q,p)\ge1+k(w)-i$ and $\kappa(p)\le1$, and the sources with root $q$ have total sum at most $1$. Hence $C\le\sum_{(w,i)}2^{-(1+k(w)-i)}=\sum_w(1-2^{-k(w)})$. \end{proof} The search fixes the numbers $k(w)$ one segment at a time. Suppose some segments are \emph{fixed} and the others are \emph{free}, with value $0$ for now; a completion gives the free segments values $k'(w)\le k_{\max}(w)$. For each required node $o$ let $\lambda_o$ be the inequality of Lemma~\ref{lem:treeconds}(b) or~(c) for a pair that attains the minimum in the definition of $\beta(o)$, so that its right-hand side minus its left-hand side at the current $k$ equals $\beta(o)$, and let $\Delta_w=\sum2^{-\beta(o)}$ over the $o$ whose $\lambda_o$ contains $k(w)$. Write $\Omega(k)$ for the value of~\eqref{eq:lhs} at the current $k$. \begin{lemma}[lifted gain bound]\label{lem:liftgain} If some completion has a valid configuration, then \[ 1-\Omega(k)+\sum_{w\text{ fixed}}\bigl(1-2^{-k(w)}\bigr)+\sum_{w\text{ free}}\max_{0\le k'\le k_{\max}(w)} \Bigl(\bigl(1-2^{-k'}\bigr)-\Delta_w\bigl(2^{k'}-1\bigr)\Bigr)\ \ge\ 0. \] \end{lemma} \begin{proof} In a completion $k'$, each $\beta(o)$ is at most the value of $\lambda_o$ (its right-hand side minus its left-hand side), which is $\beta(o)$ at $k$ minus the sum of $k'(w)$ over the free segments in $\lambda_o$; if the completion has a valid configuration, these values are nonnegative by Lemma~\ref{lem:treeconds}. Since $2^{a+b}-1\ge(2^a-1)+(2^b-1)$ for $a,b\ge0$, this gives $\Omega(k')\ge\Omega(k)+\sum_{w\text{ free}}\Delta_w(2^{k'(w)}-1)$. Combine with~\eqref{eq:lhs} and Lemma~\ref{lem:gain} at $k'$. \end{proof} For a vertex $u$ of $B$, the \emph{region} of $u$ is the set of red nodes $v$ with $u(v)$ in the subtree of $u$. Define $\Psi$ on the vertices of $B$ from the leaves up: $\Psi(u)=1$ for a leaf, and for an internal vertex $e$ with children $a$ and $b$, \[ \Phi_e=[e\text{ is an LCA node}]+\Psi(b)S_a(e)+\Psi(a)S_b(e),\qquad\Psi(e)=\max\bigl(\Psi(a),\Psi(b),\Phi_e\bigr), \] where $S_a(e)=\sum2^{-\cb(q,e)}$ over the pass-throughs $q$ in the region of $a$, and similarly $S_b(e)$. \begin{lemma}[amplification bound]\label{lem:amp} $R^*\le\Psi(\text{root})$. If the root $\varrho$ of $B$ is an LCA node, put $\omega_{\min}=2^{-\beta(\varrho)}$ and $\Psi'=\max(\Psi(a),\Psi(b))$ for the children $a,b$ of $\varrho$. Then $R^*\le\Phi_\varrho$ if $\Phi_\varrho\ge\Psi'$, and $R^*\le \omega_{\min}\Phi_\varrho+(1-\omega_{\min})\Psi'$ otherwise. \end{lemma} \begin{proof} For a node $s$ of the flow tree other than $\om$, let $\phi(s)$ be the total credit of the required nodes in the subtree of $s$, divided by $\kappa(s)$. We show $\phi(v)\le\Psi(u(v))$ for each live red node $v$, by induction from the bottom of the flow tree; note that $\Psi$ does not decrease towards the root and that $\Psi\ge1$. A blue start has no children and has $\phi=1$. A live pass-through $q$ is not required, and its children meet at $q$. They lie below $q$ in the region of $u(q)$, and their part of the sum at $q$ is at most $1$, so $\phi(q)$ is at most the largest $\phi$ of a child, hence at most $\Psi(u(q))$. A live branch node $e$ with children $a$ and $b$ has as its children in the flow tree the sources that climb to $e$. Such a source $s$ climbs through a pass-through $q$ in the region of one child, say $a$. Its successor $e$ is $\lca_B(u(q),u(s))$, and $u(q)$ is not $u(s)$ or a descendant of $u(s)$ (see the remarks after Definition~\ref{def:valid}), so $s$ lies in the region of $b$; or $s$ is a blue start. Its value of $\phi$ is then at most $\Psi(b)$. Since the sources with root $q$ have total sum at most $1$, \[ \phi(e)\ \le\ [e\text{ is an LCA node}]+\Psi(b)S_a(e)+\Psi(a)S_b(e)=\Phi_e\le\Psi(e). \] Now $R^*=\sum_s\kappa(s)\phi(s)=\sum_s2^{-d(s)}\phi(s)$ over the children $s$ of $\om$. By~(V1) this is at most the largest $\phi(s)$, hence at most $\Psi(\text{root})$. If the root $\varrho$ of $B$ is an LCA node, its root is $\om$: since $k(\varrho)=0$, no pass-through lies above it, and a pass-through below it cannot be its root (remarks after Definition~\ref{def:valid}). So $\varrho$ does not climb. Its term is $\omega\phi(\varrho)$ with $\omega=2^{-d(\varrho)}\ge2^{-\tau(\varrho)}\ge \omega_{\min}$ and $\phi(\varrho)\le\Phi_\varrho$. The other children of $\om$ lie in the regions of $a$ and $b$ or are blue starts, so their terms total at most $(1-\omega)\Psi'$. Being linear in $\omega\in[\omega_{\min},1]$, the bound $\omega\Phi_\varrho+(1-\omega)\Psi'$ is largest at an endpoint. \end{proof} With $H(e)=\sum_z(1+k(z))$ over the internal vertices $z$ from $e$ up to the root, the pass-throughs on the segment of a vertex $w$ in the region of $a$ contribute $(1-2^{-k(w)})2^{-(H(\mathrm{par}\,w)-H(e))}$ to $S_a(e)$, where $\mathrm{par}\,w$ is the parent of $w$. For a partial assignment of the numbers $k(w)$, the search evaluates the \emph{lifted form} of this bound, the bound with $k_{\max}(w)$ pass-throughs on each free segment, with $H$ and $\beta(\varrho)$ at the current $k$. In every completion, $\Omega$ is at least its current value and $R^*$ is at most this bound: more pass-throughs give more terms, the current $H$ gives the shortest climbs, and the current $\beta(\varrho)$ gives the smallest $\omega_{\min}$. During the search over sources, the red nodes are assigned in an order in which each node comes after the nodes above it. At a given point, let $\mathrm{free}(r)$ be $1$ minus the sum of $2^{-d}$ over the sources already assigned to the root $r$. For a pass-through $q=(w,i)$ put $F_q=2^{-(1+k(w)-i)}$, or $F_q=\max(\kappa(q), 2^{-(1+k(w)-i)})$ if $q$ is assigned and live. \begin{lemma}[credit capacity]\label{lem:capacity} Every valid completion of the current partial assignment satisfies \[ \sum_s2^{-\beta(s)}\ \le\ \mathrm{free}(\om)+\sum_q\mathrm{free}(q)\,F_q, \] where $s$ runs over the required nodes not yet assigned. \end{lemma} \begin{proof} For an unassigned required node $s$, follow the parents in the flow tree as long as the step goes from a child that meets at a pass-through not yet assigned. Let $p$ be the node where this stops. Then $p$ is unassigned, and either its parent is $\om$, or it meets at an assigned pass-through $q$, which is live by~(V4), or it climbs through some pass-through $q$. By \eqref{eq:flow}, $\kappa(p)$ is at most $2^{-d(p)}$, $2^{-d(p)}\kappa(q)$ or $2^{-d(p)}2^{-(1+k(w)-i)}$ in these three cases. Group the required nodes by this node $p$. In the subtree of $p$ formed by the steps that meet at unassigned pass-throughs, the required nodes are leaves, since sources meet only at pass-throughs, while the required nodes are branch nodes or blue starts. The sums at the pass-throughs are at most $1$, so the required nodes in this subtree have total credit at most $\kappa(p)$. Since the nodes $p$ are unassigned, their sums $2^{-d(p)}$ at a root $r$ total at most $\mathrm{free}(r)$. Finally $2^{-\beta(s)}\le\kappa(s)$ by~(V5). \end{proof} \subsection{Symmetry}\label{ssec:sym} Two channels are \emph{interchangeable} if exchanging them maps the function $V$ on $E$ to itself. This is an equivalence relation, and the product $G$ of the symmetric groups of its classes consists of automorphisms of $I$. A class that meets $P'$ lies inside $P'$, and $V(gx,gy)=V(x,y)$ for $g\in G$. Relabelling a valid configuration by an element of $G$ gives a valid configuration, with the same number of pass-throughs, whose tree is the image of $B$, and the conditions~(N3)--(N5) and the conclusion of Lemma~\ref{lem:n9} are preserved. Two trees whose leaves are labelled by the channels of $P'$ lie in one $G$-orbit exactly when they are isomorphic as trees with leaves coloured by the classes. It therefore suffices to examine one labelled tree for each coloured isomorphism class. Blue starts in one class have the same sets $E^y$ and the same budgets. Exchanging their sources therefore keeps a configuration valid and in normal form, and we may assume: \begin{enumerate}[label=(N\arabic*)] \setcounter{enumi}{5} \item within each maximal run of consecutive blue starts of one class, in the order of the search, the roots do not decrease in a fixed order of the roots. \end{enumerate} The program computes the classes from the scenarios themselves. \subsection{The search}\label{ssec:search} The program proceeds as follows. \begin{enumerate}[label=(\arabic*)] \item Compute the numbers $\eta_x$. Answer infeasible if some $\eta_x<0$ or $\sum_x2^{-\eta_x}>1$ (Lemma~\ref{lem:treeconds}(a)). \item Enumerate the coloured binary trees on $P'$, one for each isomorphism class, from the root down. Each leaf $x$ has a cap on its depth, at first $\eta_x$. When the second subtree of a vertex $c$ is enumerated, the depths of the leaves of the first subtree are known, and the cap of each leaf $y$ of the second subtree is lowered to the least value of $b+D(c)+1-D(x)$, where $x$ runs over the leaves of the first subtree and $b$ over the budgets $b(x,y)$ and $b(y,x)$ of the pairs in $E$ (Lemma~\ref{lem:treeconds}(b), whose left side is symmetric in $x$ and $y$). Because $V$ is invariant under $G$, these budgets depend only on the classes of $x$ and $y$, and the program uses the deepest leaf of each class. The subtree condition of Lemma~\ref{lem:treeconds}(a) is applied with the current caps. \item For each tree, enumerate the numbers $k(w)$ on the segments other than that of the root, from the top down, under the linear inequalities of Lemma~\ref{lem:treeconds}. At each node of this enumeration, including the first, discard the partial assignment if Lemma~\ref{lem:liftgain} or the lifted form of Lemma~\ref{lem:amp} fails. \item For each $(B,k)$, compute $\delta$, $\pre$, $\beta$ and the budgets of the blue starts, and discard $(B,k)$ if one of them is negative, if some pass-through has no affordable climber (Lemma~\ref{lem:n9}), or if Lemma~\ref{lem:gain} fails with $R^*$ replaced by $\Omega$. Then search the red nodes depth first, in an order in which each node comes after the nodes above it. A node that is not an LCA node may be \dead. Otherwise it receives a root, $\om$ or a pass-through allowed by~(V3), whose successor is live, and a depth. Its value $\tau$ is then determined, and it must satisfy $\tau\le\beta$ for an LCA node and $\tau\le B_{\max}$ otherwise. A node that is not readable receives only the choices allowed by~(N3). Depths are tried from the largest allowed value down, and the loop stops when the sum at the root would exceed $1$. The condition of Lemma~\ref{lem:capacity} is tested whenever some red node is still unassigned. Condition~(V3) is enforced in part during the search, by excluding roots at or below the node, and in full in step~(6). \item Then search the blue starts depth first. Each receives a root whose successors are live and the largest depth allowed by~(V5), subject to~(N6) and to~(V1). \item At a complete assignment, check~(V2) and~(V3), evaluate every cost again with a separate implementation of the recursion, build the network of Remark~\ref{rem:realize}, and simulate the run of every scenario. Answer feasible. If the two evaluations disagree or a simulated run fails, the program stops with an error. \end{enumerate} If the search ends without a complete assignment that passes step~(6), the answer is infeasible. \begin{proposition}\label{prop:checker} If \texttt{lb2cr} answers infeasible for an instance whose budgets are all at most $56$, then the instance is infeasible. \end{proposition} \begin{proof} Suppose the instance is feasible. Then $E\ne\emptyset$, since \texttt{lb2cr} answers feasible when $E=\emptyset$, and all $b(x,y)\ge0$, since $|W(x,y)|\ge0$. By Theorem~\ref{thm:sound} there is a valid configuration. Take one with the fewest pass-throughs, put it in normal form by Lemma~\ref{lem:normal}, and relabel it by an element of $G$ so that its tree is the one listed in step~(2), then apply~(N6). By Lemmas~\ref{lem:n9} to~\ref{lem:capacity}, no test of steps~(1)--(5) discards it or one of its partial assignments, and each choice it makes is offered. The search then reaches it in step~(6). \end{proof} The bound $56$ comes from the arithmetic. Kraft sums are computed exactly as integers in units of $2^{-56}$, and a depth above $56$ gets weight $0$, which only weakens each test. The credit bounds use exact $128$-bit integers, except the amplification bound. That bound is computed in floating point from nonnegative dyadic terms, and the program prunes only if $\Omega$ exceeds it by a relative $10^{-9}$ plus $10^{-12}$, far more than the rounding error. Rounding is toward the weaker test except in four places: the lifted gain bound maximizes over $k'\le56$ only, the amplification bound would overflow once $H$ exceeds about $1000$ and caps $\beta(\varrho)$ at $60$, and the number $2^{28}$ marks the absence of a budget. None of them matters when every budget is at most $56$, because $k_{\max}(w)$, $H$ and $\beta(\varrho)$ are at most $\max b(x,y)$. With such budgets every depth in the search is at most $56$ as well, so step~(6) builds and simulates a network for every feasible answer. The program also answers unknown for malformed input. Every instance that the verification passes to it has budgets at most $\maxbudget$ (Section~\ref{sec:results}). \section{Lower bounds for cores}\label{sec:cores} As weights of the instances in the search we use lower bounds on the costs of cores. We obtain them in three ways. \emph{The trivial bound.} Let $X$ be produced by a prefix $P$ of $k$ standard comparators on $13$ channels, and let $(x,y)$ be a scenario of $(X,\epsilon)$. By Lemma~\ref{lem:trivial} and $S(11)=35$~\cite{Har22}, its core satisfies \[ s(Y_{xy})\ \ge\ 35-(k-w_\epsilon(x,y)), \] where $w_\epsilon(x,y)$ is the largest value of $|W(i,j)|$ over the runs $(i,j)$ of polarity $\epsilon$ of $P$ that end on $(x,y)$. If no such run ends on $(x,y)$, the trivial bound is $0$. Since $k\le25$ in the search, the trivial bound is $0$ or at least $10$. \emph{Instances on $11$ channels.} A core $Y$ on $11$ channels has scenarios of its own, whose cores lie on $9$ channels. Proposition~\ref{prop:bound} applied to $Y$ gives: if $u_t\le s(Z_t)$ for the cores $Z_t$ of the scenarios of $(Y,\epsilon')$, and the instance $I(Y,\epsilon';u;\theta-1)$ is infeasible, then $s(Y)\ge\theta$. Each weight $u_t$ is justified in one of two ways. \begin{enumerate}[label=(\Alph*)] \setcounter{enumi}{4} \item $u_t$ is at most the exact value $s(Z_t)$, computed by Harder's program. \end{enumerate} \begin{enumerate}[label=(\Alph*)] \setcounter{enumi}{1} \item For some polarity $\epsilon''$, the instance $I(Z_t,\epsilon'';z;u_t-1)$ on $9$ channels is infeasible, where $z$ consists of the exact values of the $7$-channel cores of $(Z_t,\epsilon'')$, computed by Harder's program. Then $s(Z_t)\ge u_t$ by Proposition~\ref{prop:bound}. \end{enumerate} \emph{Sharing.} By Lemma~\ref{lem:sfacts}(c), a bound on $s(Y)$ holds for every set similar to $Y$. A bound proved for the core of one scenario of one prefix thus serves every scenario, of any prefix, whose core is similar to it. In particular, a trivial bound found for one prefix can be larger than the trivial bound of another prefix with a similar core. Harder's program computes $s(Z)$ for a well-behaved set $Z$ by the recursion $s(Z)=1+\min s(Z')$ over the successors $Z'$ of $Z$, taken up to similarity, with lower bounds from his Huffman bound~\cite[Lemma~12, Theorem~26, Corollary~56]{Har22}. By Lemma~\ref{lem:wb} all sets on $9$ and $7$ channels that we pass to it are well-behaved. We use his program with our changes, which let it handle sets on up to $13$ channels, and add a command-line front end that prints $s(Z)$ for a set given as a bitmap. Further changes, such as query servers, options for seeding bounds and upper bounds for $12$ and $13$ channels, are not used in the computation of the tables. In that computation, the changed program runs his search unchanged, except that a state that is stored again keeps the larger of its two lower bounds and the smaller of its two upper bounds. The values are not certified, so this program is one of the trusted components listed in Section~\ref{sec:trust}. The search computes these bounds as needed. For a child at depth $k$ it first uses the trivial bounds and the bounds already proved for similar cores. If the instance on $13$ channels is still feasible, the instance solver of the search returns a configuration, and for the scenarios whose costs in it reach their budgets, the search tries to raise the bounds on their cores through instances on $11$ channels. For the weights on $9$ channels it uses the exact values already known, including a table loaded at the start, and bounds of type~(B) otherwise, and it computes exact values for the scenarios on $9$ channels whose costs reach their budgets. \section{The search over prefixes}\label{sec:search} A \emph{state} of depth $k$ is a set $X\subseteq\B^{13}$ produced by a prefix of $k$ standard comparators, stored together with that prefix. The search produces \emph{layers} $L_0,L_1,\dots$, which are finite lists of states, the states of $L_k$ having depth $k$, with $L_0=\{\B^{13}\}$. For a state $R\in L_{k-1}$ and a standard comparator $(i,j)$ that is useful for $R$, the \emph{child} $R(i,j)$ has depth $k$, the prefix of $R$ followed by $(i,j)$, and the budget $44-k$. Given the layers, a \emph{record} of a child is \emph{valid} if it is one of the following: \begin{itemize} \item \emph{cut}: for some polarity $\epsilon$ and weights $v$ that are lower bounds on the costs of the cores (Section~\ref{sec:cores}), the instance $I(R(i,j),\epsilon;v;44-k)$ is infeasible, so $s(R(i,j))\ge45-k$ by Proposition~\ref{prop:bound}; \item \emph{alive}: a set similar to the child lies in $L_k$; \item \emph{duplicate}: the record names another child. Each duplicate record on the way names a child that is similar to its own child and has at most its depth, and after finitely many steps one reaches a valid cut or alive record. \end{itemize} The search builds $L_k$ from the alive children of depth $k$, one for each canonical form up to similarity (Section~\ref{ssec:producer}), and stops at the first empty layer. \begin{theorem}\label{thm:bfs} Suppose that every child of every state in $L_0,\dots,L_{24}$ has a valid record, that no state in these layers has $14$ or fewer vectors, and that $L_{25}$ is empty. Then $S(13)\ge45$. \end{theorem} \begin{proof} Suppose $S(13)=s\le44$, and let $g_1,\dots,g_s$ be a standard sorting network on $13$ channels with $s$ comparators (Lemma~\ref{lem:sfacts}(a)). Let $X_j$ be the set produced by $g_1,\dots,g_j$. Then $s(X_j)=s-j$: the remaining comparators sort $X_j$, and a shorter network sorting $X_j$, preceded by $g_1,\dots,g_j$, would sort $\B^{13}$ with fewer than $s$ comparators. Each $g_{j+1}$ is useful for $X_j$: otherwise $X_{j+1}$ equals $X_j$ or arises from it by exchanging two channels, and $s(X_{j+1})=s(X_j)$ by Lemma~\ref{lem:sfacts}(c). We show by induction on $j\le s$ that some layer $L_d$ with $d\le\min(j,24)$ contains a state similar to $X_j$. For $j=0$ this is $L_0$. Let $R\in L_d$, $d\le j$, be the image of $X_j$ under a permutation of the channels possibly combined with complementation, and let $g_{j+1}=(a,b)$. The same map takes $X_{j+1}$ to the image of $R$ under a comparator $(a',b')$, where $\{a',b'\}$ is the image of $\{a,b\}$. If $a'q$, that is similar to $X_{j+1}$. The comparator $(p,q)$ is useful for $R$, because $g_{j+1}$ is useful for $X_j$ and the map preserves this property. The child $C$ has depth $d+1\le j+1$, and $s(C)=s(X_{j+1})=s-j-1\le44-(d+1)$. Hence its record is not a cut. If it is alive, $L_{d+1}$ contains a set similar to $C$. If it is a duplicate, the names lead to a child $C'$ of depth $d'\le d+1$ that is similar to $C$ and has a valid cut or alive record. Since $s(C')=s(C)\le44-d'$, that record is not a cut but alive, and $L_{d'}$ contains a set similar to $C$. In both cases this layer has depth at most $d+1\le25$ and is not empty, so its depth is at most $24$. For $j=s$ the set $X_s$ consists of the $14$ sorted vectors, so some layer $L_d$ with $d\le24$ contains a state with $14$ vectors. This contradicts the hypothesis. \end{proof} \begin{proof}[Proof of Theorem~\ref{thm:main}] Juill\'e's network~\cite{Jui95} gives $S(13)\le45$, and we check this in Lean (Section~\ref{ssec:upper}). The certificate (Section~\ref{sec:cert}) records the layers $L_0,\dots,L_{25}$ and a record for every child of every state in $L_0,\dots,L_{24}$, and its verification confirms the hypotheses of Theorem~\ref{thm:bfs}, using the components listed in Section~\ref{sec:trust}. Hence $S(13)\ge45$. \end{proof} \subsection{The program}\label{ssec:producer} Our search program, \texttt{lb2w}, builds on Harder's library for sets of vectors~\cite{HarRepo}: his representation of sets as bitmaps, his canonical form of a set up to similarity, and his search for exact values. It decides the instances with a solver of its own, which the verification does not use. When that solver reaches a limit on its work, the child is kept. For each child it builds the two instances on $13$ channels, one for each polarity, first with the trivial bounds and the bounds already known for similar cores, and then with bounds raised by instances on $11$ channels, as described at the end of Section~\ref{sec:cores}. Each process keeps a table of the best bound known for each core in canonical form, so that a bound found once serves all later scenarios of the same process with a similar core. Duplicates are detected within one process: the canonical form of each child is looked up among those of the children already generated by the same process, at any depth, and a repeated child refers to the first one. We computed layers $1$ to $12$ with one process, which used only the trivial bounds and their sharing and needed no exact values. From depth $13$ on, we dealt out the states of each layer in turn to several servers, each running one process at a time, which kept its tables from layer to layer until the process was restarted. A coordinator merged the alive children of each layer, kept one state for each canonical form, and dealt the result out as the next layer. When a server failed, fresh processes computed its share of a layer again, split into up to eight parts (Section~\ref{sec:cert}). \section{The certificate and its verification}\label{sec:cert} \subsection{The records} Each process of the search writes, for each layer, one record for each child that it generates, and a file of bounds on cores, the \emph{claims}. A set is written as a bitmap. A map between similar sets is written as a flag for complementation followed by a permutation of the channels. The records are of four kinds. \begin{itemize} \item[\texttt{A}] The child is alive. The record gives a map that takes the child to a set listed in the merged set of its layer. \item[\texttt{D}] The child is a duplicate. The record names a child of the same process, by layer, parent and comparator, and gives two maps that take the two children to the same set. \item[\texttt{T}, \texttt{C}] The child is cut. The record gives the polarity $\epsilon$ and the weights $v_t$ of the infeasible instance, and for each scenario whose weight exceeds its trivial bound, a claim whose bound is at least $v_t$ and a map that takes the core of the scenario to the core of the claim. The letter \texttt{T} marks cuts that use trivial bounds and shared bounds only, and \texttt{C} the cuts found after bounds were raised by instances on $11$ channels. \end{itemize} The claims are of three kinds. \begin{itemize} \item[\texttt{Q}] A core on $11$ channels, with an identifier. \item[\texttt{K\,T}] A bound $s(Y)\ge\theta$ for a core $Y$, justified by the trivial bound of a scenario of a child of the same process: the claim names the child, the polarity, the scenario and a map that takes its core to $Y$. \item[\texttt{K\,L}] A bound $s(Y)\ge\theta$ justified by an instance on $11$ channels: the claim gives the polarity $\epsilon'$ and the weights $u_t$ of the scenarios of $(Y,\epsilon')$, each with a tag \texttt{E} or \texttt{B} for the justifications (E) and (B) in Section~\ref{sec:cores}. \end{itemize} Each process also writes a manifest, which identifies the input of each of its layers by its length and a $64$-bit hash. The coordinator writes the list of states of each layer, the share of each server, the merged set of each layer, and its log. The merged set lists the states of the layer, each with its canonical form, which is the state's image under the map given in the alive record that produced it. Layers $1$ to $12$ consist of the alive children of the one process that computed them. The format is specified in full in the supplement~\cite{Supp}, so that a verifier needs nothing from the search code. \subsection{The verifier} The verifier consists of a program \texttt{cv}, which checks the records and claims of the processes, and a script \texttt{gv}, which checks the layers as a whole. We wrote both from the format specification and the mathematics in Sections~\ref{sec:sets} to~\ref{sec:cores}, without the search code. They decide every instance with \texttt{lb2cr}, which we wrote from a separate derivation of the mathematics in Sections~\ref{sec:model} and~\ref{sec:checker}, without the code of the search's instance solver, and they ask Harder's program for exact values. For each layer of each process, \texttt{cv} checks the following. \begin{enumerate}[label=(\roman*)] \item In layers $2$ to $12$ the input of the layer is the list of alive children of the previous layer of the same process. In the other layers it has the length and hash that the manifest records, and \texttt{gv} matches it with the share named in the coordinator's files: it compares the SHA-256 digest of the share with the digest that \texttt{cv} recorded for the input of the process that used the share. Each state of the input is the set produced by its prefix, which consists of standard comparators and has the length of the depth. The only state of depth $0$ is the full set. \item Each standard comparator that is useful for a state gives exactly one record, and no record names a comparator that is not useful. \item For a cut, it computes the trivial bounds of all scenarios of the given polarity from the prefix, checks that each weight above its trivial bound is covered by the named claim and map, and checks that \texttt{lb2cr} answers infeasible for the instance. The program computes the symmetries of each instance itself and ignores any hint in the record. \item For an alive child, it checks that the child has more than $14$ vectors and that its image under the map is listed in the merged set of its layer. \item For a duplicate, it checks that the two maps give the same set, that the named child has a depth at most that of the duplicate, and that following the names ends at a verified alive or cut record. \end{enumerate} For each claim that a record uses, \texttt{cv} checks the following. \begin{enumerate}[label=(\roman*),resume] \item For \texttt{K\,T}, it recomputes the trivial bound of the named scenario and applies the map. \item For \texttt{K\,L}, it checks that \texttt{lb2cr} answers infeasible for the instance on $11$ channels with budget $\theta-1$. For a weight tagged \texttt{E}, it checks that the weight is at most the exact value of the core on $9$ channels, or at most a bound of type~(B) for it. For a weight tagged \texttt{B}, it checks (B) for one of the two polarities on a set similar to the core, with exact values of the cores on $7$ channels. \end{enumerate} In all of these, maps must be permutations of the channels, with or without complementation, and the identifiers of claims must be unique. \budgetcheck{} The script \texttt{gv} checks that the shares of each layer split it as the coordinator's files say; that for each share exactly one output is used, as named in the log; that every state of a layer is covered; that layers $1$ to $12$ end in the states of depth $12$ from which layers $13$ on start; that every line of a merged set comes from an alive record of a used output, and that the images of these alive records are exactly the listed canonical forms; that each layer is the merged set of the previous one; and that layer $25$ is empty. \invocation We computed nine shares of layers $14$ to $17$ again after a server failed, and for each of them the output used is the one named in the last line of the log that concerns the share. For two of these shares, both of layer $14$, the processes whose outputs were replaced went on to later layers, and the duplicate records that they wrote there may name children of the replaced outputs. Those children are checked like all others, but an alive child among them can end a chain of duplicates only if its image is listed in the merged set of layer $14$. In the replaced outputs, $37$ alive records and $8$ duplicate records do not satisfy the conditions above. The verifier reports them, but no record of a used output depends on them. \subsection{Exact values} We computed the exact values in advance for the cores on $9$ and $7$ channels whose values the verifier needs, and stored them in two tables with $\nineexact$ and $\sevenexact$ entries. Each entry gives the value for one image of the core under a map of the kind above, which the verifier computes before the look-up. This image is not always a canonical form, but by Lemma~\ref{lem:sfacts}(c) any image will do. Of the $\ninecores$ cores on $9$ channels that the claims use, counted up to the verifier's representatives, $\nineexact$ needed exact values. For the others, bounds of type~(B) cover every weight of the claims that use them. \crosscheckninesentence \section{Results}\label{sec:results} We list the layers in Table~\ref{tab:layers}. The search went extinct at depth $25$, which gives the last hypothesis of Theorem~\ref{thm:bfs}: the three states of depth $24$ have $134$ children, all of them cut. In total the outputs used contain $41{,}142{,}659$ records of children, of which $31{,}899{,}147$ are cuts, $2{,}120{,}883$ alive and $7{,}122{,}629$ duplicates. The two replaced outputs of layer~$14$ add $369{,}927$ records. The layers $L_1,\dots,L_{24}$ contain $662{,}820$ states. The cuts use $\claimsKT$ bounds of kind \texttt{K\,T} and $\claimsKL$ of kind \texttt{K\,L}. The claims of kind \texttt{K\,L} have $\tagsE$ weights tagged \texttt{E} and $\tagsB$ tagged \texttt{B}. The verifier covered $\tagsEbyB$ of the weights tagged \texttt{E} by bounds of type~(B), and looked up the other $\tagsEbyOracle$ in the table of exact values. \begin{table}[ht] \centering\small \begin{tabular}{@{}rrrrrrrr@{}} \toprule $k$ & $|L_{k-1}|$ & children & alive & duplicate & cut \texttt{T} & cut \texttt{C} & $|L_k|$\\ \midrule 1 & 1 & 78 & 1 & 77 & 0 & 0 & 1\\ 2 & 1 & 77 & 2 & 75 & 0 & 0 & 2\\ 3 & 2 & 152 & 5 & 146 & 1 & 0 & 5\\ 4 & 5 & 375 & 13 & 358 & 4 & 0 & 13\\ 5 & 13 & 961 & 36 & 902 & 23 & 0 & 36\\ 6 & 36 & 2{,}624 & 106 & 2{,}389 & 129 & 0 & 106\\ 7 & 106 & 7{,}617 & 300 & 6{,}616 & 701 & 0 & 300\\ 8 & 300 & 21{,}234 & 823 & 17{,}186 & 3{,}225 & 0 & 823\\ 9 & 823 & 57{,}392 & 2{,}398 & 42{,}095 & 12{,}899 & 0 & 2{,}398\\ 10 & 2{,}398 & 164{,}723 & 7{,}311 & 107{,}586 & 49{,}826 & 0 & 7{,}311\\ 11 & 7{,}311 & 494{,}205 & 21{,}956 & 282{,}325 & 189{,}924 & 0 & 21{,}956\\ 12 & 21{,}956 & 1{,}459{,}781 & 65{,}659 & 717{,}716 & 676{,}406 & 0 & 65{,}659\\ \midrule 13 & 65{,}659 & 4{,}292{,}552 & 318{,}344 & 1{,}163{,}812 & 2{,}544{,}340 & 266{,}056 & 100{,}762\\ 14 & 100{,}762 & 6{,}475{,}632 & 490{,}716 & 1{,}138{,}486 & 4{,}241{,}800 & 604{,}630 & 142{,}881\\ 15 & 142{,}881 & 9{,}006{,}443 & 489{,}270 & 1{,}243{,}569 & 5{,}938{,}250 & 1{,}335{,}354 & 133{,}426\\ 16 & 133{,}426 & 8{,}213{,}431 & 358{,}766 & 1{,}072{,}034 & 5{,}263{,}682 & 1{,}518{,}949 & 94{,}630\\ 17 & 94{,}630 & 5{,}667{,}481 & 212{,}574 & 719{,}135 & 3{,}513{,}826 & 1{,}221{,}946 & 54{,}471\\ 18 & 54{,}471 & 3{,}167{,}491 & 99{,}158 & 374{,}536 & 1{,}942{,}775 & 751{,}022 & 24{,}920\\ 19 & 24{,}920 & 1{,}405{,}142 & 37{,}391 & 156{,}818 & 859{,}050 & 351{,}883 & 9{,}250\\ 20 & 9{,}250 & 504{,}626 & 11{,}567 & 53{,}685 & 312{,}013 & 127{,}361 & 2{,}812\\ 21 & 2{,}812 & 147{,}750 & 3{,}403 & 16{,}976 & 92{,}216 & 35{,}155 & 807\\ 22 & 807 & 40{,}768 & 892 & 4{,}743 & 25{,}922 & 9{,}211 & 208\\ 23 & 208 & 10{,}114 & 174 & 1{,}132 & 6{,}635 & 2{,}173 & 40\\ 24 & 40 & 1{,}876 & 18 & 232 & 1{,}232 & 394 & 3\\ 25 & 3 & 134 & 0 & 0 & 103 & 31 & 0\\ \bottomrule \end{tabular} \caption{The layers of the search. Row $k$ counts the children of the states of $L_{k-1}$ by the kind of their record. One process computed layers $1$ to $12$. From layer $13$ on, alive children of different processes can be similar, and $|L_k|$ counts their similarity classes. Duplicates are found within one process.}\label{tab:layers} \end{table} Deeper in the search, more of the cuts were found only after bounds were raised by instances on $11$ channels: the cuts of kind \texttt{C} make up $9\%$ of the cuts at depth $13$ but between $22\%$ and $30\%$ from depth $16$ on. The verifier decided with \texttt{lb2cr} $\insttt$ instances on $13$ channels, $\insteleven$ on $11$ channels and $\nineinst$ on $9$ channels for the bounds of type~(B), and $\crossninecalls$ more on $9$ channels for the test at the exact values. The largest budgets were $\maxbudgett$, $\maxbudgete$ and $\maxbudgetn$ on $13$, $11$ and $9$ channels, so all of them lie within the range of Proposition~\ref{prop:checker}. These counts, and those of claims and weights above, include the records of the two replaced outputs of layer~$14$ (Section~\ref{sec:cert}). \emph{Computation.} \computeparagraph \section{Trusted components and cross-checks}\label{sec:trust} The proof of the lower bound in Theorem~\ref{thm:main} rests on Sections~\ref{sec:defs} and~\ref{sec:structure}, Sections~\ref{sec:sets} to~\ref{sec:search} and the verification of Section~\ref{sec:cert}. The verification checks every record and every claim that a record uses. It does not check the following three components. \begin{enumerate}[label=(\arabic*)] \item \emph{Harder's program}, with the changes described in Section~\ref{sec:cores}, for the exact values of the $\nineexact$ sets on $9$ channels and the $\sevenexact$ sets on $7$ channels in the two tables. These sets are well-behaved (Lemma~\ref{lem:wb}), as Harder's proof of correctness of his algorithm requires. The same search computes $S(11)=35$ in~\cite{Har22}, where its results are backed by certificates; the values in our tables have no certificates. \item \emph{The bound $S(11)=35$}, used by every trivial bound. Harder's certificate for $S(11)\ge35$ is checked by a program verified in Isabelle/HOL~\cite{Har19}, and again by the two checkers in Lean, whose soundness is proved (Section~\ref{ssec:harderlean}). \item \emph{The program \texttt{lb2cr}}, for the answer infeasible on each instance that the verifier passes to it. Its correctness for budgets at most $56$ is the content of Sections~\ref{sec:model} and~\ref{sec:checker} (Proposition~\ref{prop:checker}). \end{enumerate} We trust the verifier itself, the compilers and the hardware in the usual way, but not the search, its instance solver or its bookkeeping. Table~\ref{tab:checks} lists the tests of these components. Section~\ref{ssec:leantrust} states what the native proof in Lean trusts, and Section~\ref{ssec:kerneltrust} what the kernel-checked proof relies on. \begin{table}[ht] \centering\footnotesize \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.33\textwidth}>{\raggedright\arraybackslash}p{0.36\textwidth}>{\raggedright\arraybackslash}p{0.25\textwidth}@{}} \toprule check & scope & outcome\\ \midrule \texttt{lb2cr} at budget equal to the exact value, on the instances on $9$ channels with the exact values on $7$ channels as weights & all $\nineexact$ cores with exact values, both polarities & \crossninerow\\ an exact solver written separately, by search over sets up to similarity, against the $7$-channel table & every $200$th entry, $\exsevensample$ in all & all agree\\ values of the $9$-channel table computed twice & $\nineoverlap$ cores, $\nineoverlapdiff$ of them on two different machines, among them $\ninerecovered$ computed again after a machine went down & no conflict\\ \texttt{lb2cr} against an exhaustive search over networks, which gives the least feasible budget $L^*$ & $\bfinst$ random instances with $4$ to $8$ channels, $\bfanswers$ answers at budgets from $L^*-2$ to $L^*+1$ & no disagreement\\ feasible answers of \texttt{lb2cr} & every feasible answer, for budgets at most $56$ & network built and every run simulated\\ prefixes of Juill\'e's network~\cite{Jui95} and of its mirror image, at budget $45-k$ & $\juilleinst$ instances of both polarities, from $\juilleorders$ orders of the comparators of each & none infeasible\\ Theorem~\ref{thm:sound} & formal proof in Lean~4 & standard axioms only\\ the native proof in Lean & the records of the outputs used and the claims that they use, with its own search & all checks pass\\ the kernel-checked proof in Lean & the same records, with every computation checked by Lean's kernel & all checks pass, standard axioms only\\ the verifier on a small certificate with single corruptions & $\mutations$ corruptions, $19$ of the certificate and one of its table of exact values & each detected by the expected check\\ \bottomrule \end{tabular} \caption{Tests of the trusted components. The supplement~\cite{Supp} contains the programs and logs for each row except the third, which its README describes, and the kernel-checked proof, which is archived with its build log in~\cite{LeanKernel}.}\label{tab:checks} \end{table} \section{Proofs in Lean}\label{sec:lean} We formalized both bounds of Theorem~\ref{thm:main} in Lean~4~\cite{Lean4} with Mathlib~\cite{Mathlib}. Two proofs of the lower bound check the certificate (Section~\ref{sec:cert}) without the verifier and without the program \texttt{lb2cr}. In the first, the large computations run as compiled code (Section~\ref{ssec:leannative}); in the second, Lean's kernel checks every computation itself (Section~\ref{ssec:leankernel}). A short proof checks the upper bound in the kernel (Section~\ref{ssec:upper}). Two further proofs, in the supplement~\cite{SuppTwo}, check the bound $P(2,13)\ge9$ of Theorem~\ref{thm:P} (Section~\ref{ssec:p213lean}). All of them use the same definitions of networks and of sorting, and the bound $S(11)\ge35$ enters each proof of a lower bound through one of the two checkers of Harder's certificates (Section~\ref{ssec:harderlean}). \subsection{The statements}\label{ssec:leanstatement} The definitions behind the statements use only Lean's core library. A comparator on $n$ channels is a pair $i if k = c.i then min (v c.i) (v c.j) else if k = c.j then max (v c.i) (v c.j) else v k abbrev Network (n : Nat) := List (Comparator n) def Network.eval (net : Network n) (v : Fin n \(\to\) Nat) : Fin n \(\to\) Nat := net.foldl (fun w c => c.apply w) v def Network.Sorts (net : Network n) : Prop := \(\forall\) v : Fin n \(\to\) Nat, \(\forall\) a b : Fin n, a \(\le\) b \(\to\) net.eval v a \(\le\) net.eval v b theorem S13_ge_45 : \(\forall\) net : Network 13, net.Sorts \(\to\) 45 \(\le\) net.length theorem S13_le_45 : \(\exists\) net : Network 13, net.Sorts \(\land\) net.length = 45 \end{alltt} Both theorems are in the namespace \texttt{Sortnet}. Since the file of these definitions, \texttt{S13/Defs.lean}, is byte-identical in every Lean project of the three records~\cite{Supp,LeanKernel,SuppTwo}, and all these projects use the same versions of Lean and Mathlib, \texttt{Network} and \texttt{Network.Sorts} mean the same in every statement. Together, therefore, the two theorems state $S(13)=45$ for these definitions. No single Lean theorem states $S(13)=45$; it would need the proof of Section~\ref{ssec:upper} and one of the large builds of Sections~\ref{ssec:leannative} and~\ref{ssec:leankernel} in one project. The native proof, the proof of the upper bound and the projects of~\cite{SuppTwo} also prove the $0$-$1$ principle (\texttt{Network.sorts\_iff\_sorts01}), over the same definitions, so the theorems hold equally with sorting defined on inputs in $\B$. \subsection{Harder's certificates in Lean}\label{ssec:harderlean} The proofs follow the proof system of Harder's certificates~\cite{Har22}. A network \emph{works} on a set $V$ of vectors in $\B^n$ if any two members of $V$ whose outputs have the same weight have the same output; a sorting network works on every set, and its comparators may here be any pairs of channels. A lower bound $b$ for a set means that every network that works on the set has at least $b$ comparators. Each step of the certificate claims such a bound for its set $V$, and the rules that the steps use are proved in Lean: a claim for a set gives the same claim for every larger set, for every relabeling of the channels and for the set with all values inverted; if the empty network does not work on $V$, and every comparator maps $V$ to $V$, to the image of $V$ under the transposition of its two channels, or to a set that needs at least $b-1$ comparators, then $V$ needs $b$ (the \emph{successor rule}); and, for the channels $i$ at which $V$ contains the vector with a single $1$ (or a single $0$), bounds $b_i$ for the vectors of $V$ with that value at $i$ show that $V$ needs $\cl{\lg\sum_i2^{b_i}}$ comparators. The proof of the last rule is a potential argument: one comparator reduces $\sum_i2^{b_i}$ by at most a factor of two. A checking function verifies each step of the certificate from earlier steps, and a proof in Lean by induction over the steps shows that a successful check makes every claim true. The certificate is Harder's published file \texttt{proof\_cert\_11.bin.zst}~\cite{Har19} (Zenodo record 4108365, SHA-256 \hardersha). It decompresses to a file of $3{,}068{,}651{,}498$ bytes (SHA-256 \hardershaU) with $\hardersteps$ steps. Its last step claims the bound $35$ for all vectors of width~$11$, which gives $S(11)\ge35$ for sorting networks in the form above. There are two checkers. The \emph{kernel checker} represents a set of vectors of width $w$ by a number whose bit $x$ is set if and only if the vector with code $x$ is in the set. The image under a comparator, a transposition of two channels, the inversion of all vectors and the deletion of a channel are then a few operations on such numbers. We prove each of these operations correct in Lean bit by bit and lift the results to sets of vectors. An untrusted program converts Harder's file, checks every step again, and writes $4.5$~GB of packed data (claims and steps) and the Lean modules that read them: a table of the claims in $194$ modules, and the steps in $1{,}266$ modules of up to $10{,}000$ steps. These step modules contain $620{,}675$ theorems, each stating that a range of steps passes the check and proved by \texttt{Eq.refl true}, so that the kernel evaluates the check itself. A tree of theorems then combines the ranges, and finally the claim of the last step is checked by \texttt{decide +kernel}. The \emph{native checker} is a checking function of about $200$ lines. An untrusted program re-encodes the certificate as text, which Lean reads at build time as string constants, and Lean compiles the check and runs it (the mechanism \texttt{native\_decide}, described in Section~\ref{ssec:leandata}). In the native proofs of~\cite{Supp,SuppTwo} the text has $2.2$~GB in $33$ string constants. We tested both checkers on certificates produced by Harder's program~\cite{HarRepo}. Through the kernel checker they give $S(9)\ge25$ and $S(10)\ge29$, and through the native checker $S(5)\ge9$, $S(6)\ge12$, $S(7)\ge16$, $S(8)\ge19$, $S(9)\ge25$ and $S(10)\ge29$. Both checkers also fail on corrupted versions of the $11$-channel certificate: the kernel checker rejects each of five corruptions of steps or claims, and the native checker each of $32$ corruptions of single steps. \subsection{The native proof of the lower bound}\label{ssec:leannative} In this proof we check the certificate with our own search over configurations and our own checks of the records, and we prove in Lean that the instances this search rejects are infeasible. The Lean project is part of the supplement~\cite{Supp}. Its main theorem is \texttt{Sortnet.S13\_ge\_45} (Section~\ref{ssec:leanstatement}). \subsubsection{What is proved} We prove the following results in Lean from the three standard axioms of its logic, together with the computations described in Section~\ref{ssec:leandata} where stated. \begin{enumerate}[label=(\roman*)] \item \emph{Theorem~\ref{thm:sound}.} The formal instance is a budget and a list of scenarios $(x,y,v)$ on channels \texttt{Fin n}. A network is a list of pairs of distinct channels, and the run of a scenario is computed by a function that moves $M$ and $m$ as in Section~\ref{ssec:runs} and counts the comparators that it touches: \begin{alltt}\footnotesize def Feasible \{n : Nat\} (I : Inst n) : Prop := \(\exists\) net : List (Fin n \(\times\) Fin n), Proper net \(\land\) \(\exists\) oM om : Fin n, oM \(\ne\) om \(\land\) \(\forall\) s \(\in\) I.sc, (tokRun net s.x s.y).M = oM \(\land\) (tokRun net s.x s.y).m = om \(\land\) (tokRun net s.x s.y).w + s.v \(\le\) I.L theorem feasible_valid \{n : \(\mathbb{N}\)\} (I : Inst n) (hwf : I.WF) (hne : I.sc \(\ne\) []) (hF : Feasible I) : HasValid I \end{alltt} Here \texttt{I.WF} says that each scenario has $x\ne y$, and \texttt{HasValid I} says that some configuration satisfies a structure \texttt{Valid}. Its fields are the requirements of Definition~\ref{def:config} on the tree, the numbers $k$ and the roots, the conditions~(V1)--(V6), the recursion~\eqref{eq:tau} for the values $\tau$, which the formal configuration carries as data, and the reachability condition of Section~\ref{ssec:normal}: every live red node can be reached from an LCA node or a blue start by a chain of successors. The checker \texttt{lb2cr} does not use the reachability condition. \texttt{Comp.solve}, the search of~(ii), derives from it~(N4) and the part of~(N3) that marks nodes \dead, in place of the deletion argument of Lemma~\ref{lem:normal}. \item \emph{A search over configurations.} A function \texttt{Comp.solve} performs the search of Section~\ref{ssec:search} without the tests of Lemmas~\ref{lem:n9} and~\ref{lem:gain} to~\ref{lem:capacity} and without the conditions~(N5) and~(N6), and in step~(6) it only checks~(V2) and~(V3). Leaving out a test can only make the search accept more instances. The theorem \texttt{solve\_complete} states that \texttt{Comp.solve} accepts every instance on at most $13$ channels that has $x\ne y$ in each scenario and a valid configuration. With~(i), an instance on at most $13$ channels that \texttt{Comp.solve} rejects is infeasible. Kraft sums are exact integers in units of $2^{-56}$, with weight $0$ for a depth above $56$. All other arithmetic is exact. \item \emph{The weighted two-value bound} for the sets of the search. If the instance of a state for one polarity, with weights that are lower bounds for the cores of its scenarios, is infeasible with budget $L$, then every network that works on the state has at least $L+1$ comparators. \item \emph{The trivial bound} (Section~\ref{sec:cores}), from $S(11)\ge35$. The bound $S(11)\ge35$ comes from a computation that checks Harder's certificate~\cite{Har19}, which has $\hardersteps$ steps. The computation uses the native checker (Section~\ref{ssec:harderlean}). \item \emph{The induction over the layers.} Suppose that the empty network works on no listed state, and that for each listed state $X$ of depth $d$ and each standard comparator $c$, the set $c(X)$ is $X$, or the image of $X$ under the exchange of the two channels of $c$, or similar to a listed state of depth at most $d+1$, or needs at least $44-d$ comparators. Then each listed state of depth $d$ needs at least $45-d$ comparators, and in particular every sorting network on $13$ channels has at least $45$ comparators. A reference to a state of depth $d+1$ uses the bound for a shorter network, so cycles among the references are harmless. \item \emph{The bounds on cores.} A claim \texttt{K\,L} holds if \texttt{Comp.solve} rejects its instance on $11$ channels and each weight is a lower bound for its core on $9$ channels. Such a bound comes from route~(B) (Section~\ref{sec:cores}), by a rejected instance on $9$ channels whose weights are proved bounds on $7$ channels, or from the table of values on $9$ channels, whose entries are proved in~(vii).\ We prove all $\sevenexact$ values on $7$ channels as lower bounds, in computations by a checker whose soundness is proved in Lean. Each value follows from the bounds for the successors of the set, by the successor rule (Section~\ref{ssec:harderlean}), down to sets for which route~(B) applies one level lower, with an instance on $7$ channels and values on $5$ channels that the checker computes. \item \emph{The bounds on $9$ channels.} We prove each of the $\nineexact$ values on $9$ channels in the table as a lower bound, in computations by checkers whose soundness is proved in Lean. Here a set $X$ contains a set $Z$ if $X$ contains an image of $Z$ under a permutation of the channels, possibly combined with complementation. If $X$ contains $Z$, a lower bound for $Z$ is one for $X$, and if $X$ contains $c(Z)$ for a comparator $c$, a lower bound $b$ for $Z$ gives the bound $b-1$ for $X$. Of the entries, $\leanderived$ follow in this way, directly or through one or two comparators, from a step on $9$ channels of Harder's certificate~\cite{Har19} or from other entries, and a rank in each record excludes cycles. The other $\leanroots$ are proved by the successor rule, down to sets for which route~(B) applies, as for the values on $7$ channels in~(vi). \end{enumerate} \subsubsection{Data and computations}\label{ssec:leandata} An untrusted program converts the released certificate files into one stream of $\leanstream$ bytes, which the proof reads at build time as $16$ string constants. It keeps the records of the outputs used by the coordinator and the $\leanclaims$ claims \texttt{K\,L} used by these records. Chains of duplicates are replaced by their final targets. The checking functions recompute from the prefixes the states, the useful comparators, the children, the scenarios, the cores and the trivial bounds. The data supply the rest: for each listed state its parent and comparator, and for each child a listed state with a map, a cut child with a map, or a cut with its claims. The tables of values on $9$ and $7$ channels and Harder's certificate are read in the same way. Each constant is pinned by a $64$-bit hash, and the build script compares the regenerated data with their SHA-256 digests. An error of the converter can make a check fail, but the soundness theorems hold for any data. The checks run by the tactic \texttt{native\_decide}, which compiles a Boolean computation, runs it, and records its result as an axiom. The proof uses $\leannativea$ of them: $\leanbfs$ for the listed states, $\leankl$ for the claims \texttt{K\,L}, $\leanhint$ for the values on $7$ channels, $\leanrootchunks$ for the entries of~(vii) proved by the successor rule, one that checks the records of the other entries, two for the header of the stream and the table of listed states, and one for Harder's certificate. The records of~(vii), one of $15$ characters for each entry, and the list of the entries proved by the successor rule are read in the same way as the other data. They form a separate file of the supplement~\cite{Supp}. We found these records with programs that are not part of the release, and the proof checks every one of them. \texttt{\#print axioms} lists these and the three standard axioms, and nothing else. No definition of the project is marked \texttt{implemented\_by} or \texttt{extern}, so each computation runs code compiled from the definitions about which the soundness theorems are proved; the only overrides are those of Lean's core and standard libraries. A few short functions outside the precompiled libraries, in one chunk theorem of~(vii) and in the check of the records of~(vii), run in Lean's interpreter; they call the compiled checking functions. \subsubsection{Trust and tests}\label{ssec:leantrust} Besides Lean's kernel, the proof relies, for its $\leannativea$\ computations, on the Lean compiler and its interpreter, the C compiler and the runtime. It reads the same certificate files and tables as the verifier, but it trusts none of the three components listed at the start of Section~\ref{sec:trust}. We compared \texttt{Comp.solve} with \texttt{lb2cr} with the same tests switched off, on $\leandiff$ instances ($\leandiffdistinct$ distinct) on $13$, $11$, $9$ and at most $8$ channels, most of them instances of cuts. The two programs gave the same answer on every instance, and on the $35{,}344$ instances on at most $8$ channels \texttt{Comp.solve} also agreed with an exhaustive search over networks. In $\leanneg$ tests, run with the same checking functions on a different ordering of the same data, we made one field or one record of the converted data wrong, and each change made the check of the affected part fail. After the build scripts have regenerated and compared the data (Section~\ref{ssec:leandata}), the commands in the build instructions, which also give the SHA-256 digest of Harder's certificate, build the proof. We built the proof on $17$ servers with $192$ hardware threads each. Sixteen of them proved the entries of~(vii) that need the successor rule, in $86$ to $147$ minutes each and about $1{,}120$ hours of processor time in all, and the seventeenth built the rest. The builds took $2$ hours and $33$ minutes from their start to the output of \texttt{\#print axioms}. \subsection{The kernel-checked proof of the lower bound}\label{ssec:leankernel} The computations of the native proof (Section~\ref{ssec:leannative}) run as compiled code, so that proof also relies on Lean's compiler. In the proof of this section, Lean's kernel checks every computation itself. It follows the same certificate, but we wrote its checking functions and its data so that the kernel can evaluate them, and it uses neither \texttt{native\_decide} nor any other way of running compiled code. The Lean project, its data and the record of its build are archived on Zenodo~\cite{LeanKernel}. \subsubsection{The statement} The theorem has the same name and the same statement as in the native proof: \begin{alltt}\small theorem Sortnet.S13_ge_45 : \(\forall\) net : Network 13, net.Sorts \(\to\) 45 \(\le\) net.length \end{alltt} The final module checks that its type is the same Lean expression as the statement of the native proof, not only equal up to unfolding of definitions. That statement is copied verbatim and elaborated over the same file of definitions, which is byte-identical to the one of the native proof. \texttt{\#print axioms} lists \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}, and nothing else. \subsubsection{How the kernel checks the computations} Each check is a Boolean function applied to data. It is stated as \texttt{f a = true}, or as \texttt{f a = false} for the refutations, and proved by \texttt{Eq.refl} or by \texttt{decide +kernel}. The kernel accepts such a proof only after it has evaluated \texttt{f a} itself. To make this feasible, we write the checking functions without strings, arrays and hash maps, using natural numbers, Booleans, lists and small inductive types. Sets of $0$-$1$ vectors are natural numbers read as bitmaps, and the data are tables of numerals inside the declarations. The kernel reads the string constants of the native proof far too slowly: a string of one kilobyte takes it about $20$ seconds. This proof therefore has its own table of the values on $9$ channels, written as numerals from the same released file, and it proves that every entry of this table is a lower bound; the final theorem does not mention the table. Every data file is pinned by its SHA-256 digest. As in the native proof, the soundness theorems of the checking functions hold for any data, so wrong data can only make a check fail. \subsubsection{The parts of the proof} The proof has five parts, which discharge the hypotheses of a theorem that assembles them. \begin{enumerate}[label=(\alph*)] \item $S(11)\ge35$, from a check of each of the $\hardersteps$ steps of Harder's certificate~\cite{Har19} by the kernel checker (Section~\ref{ssec:harderlean}). \item The table of values on $9$ channels. Of its $\nineexact$ entries, $\leanderived$ follow from steps of Harder's certificate or from other entries, as in item~(vii) of the native proof. Each of the other $\leanroots$ entries has a certificate: either Harder's Huffman bound for the entry's set, or a set of nodes, each the image of the entry's set under a path of comparators. The set of every node has two different vectors of the same weight, so that some comparator is still needed, and the set that each useful comparator reaches from it is bounded through a step of Harder's certificate, an entry of lower level, Harder's Huffman bound, another node of the certificate, or the set that another comparator reaches from the same node. \item A second table of values on $9$ channels, which the claims \texttt{K\,L} use besides the table of~(b). Its $8{,}977{,}498$ entries follow from steps of Harder's certificate, from entries of the table of~(b) and from certificates of the same kind. \item The $\leanclaims$ claims \texttt{K\,L}, grouped into $6{,}139{,}636$ classes. Their instances on $11$ channels, $2{,}249{,}283$ in all, are refuted. \item The induction over the layers. Its $31{,}899{,}147$ cuts use $5{,}290{,}420$ distinct instances on $13$ channels, and each of them is refuted in its own declaration. \end{enumerate} We refute the instances by a search over configurations written for the kernel, with a proof that every instance it rejects is infeasible. For the instances on $11$ channels it also rejects, once all numbers $k(w)$ are fixed, the choices of $k$ for which $\Omega$ exceeds the bound of Lemma~\ref{lem:gain} or of Lemma~\ref{lem:amp}. We prove these two lemmas in Lean as part of the project. We also prove Lemmas~\ref{lem:n9}, \ref{lem:liftgain} and~\ref{lem:capacity} in Lean, although the search does not use them. \subsubsection{Build and trust}\label{ssec:kerneltrust} We ran the build, which comprises $102{,}624$ Lean modules, on $40$ machines, starting from a frozen source archive and $22$ data archives. From the first module to the last it took $6$ hours and $35$ minutes, with a pause of about an hour before the largest part, and about $8{,}800$ hours of processor time. Checks after the build found no module out of date, but they import the compiled files of all modules, which Lean does not check again, and we ran no independent replay of the declarations. The proof relies on Lean's kernel, as run on each module by the machine that built it, on the definitions of networks and sorting, which use only Lean's core library, and on the three standard axioms. It does not rely on Lean's compiler, on the data or on the programs that produced them. Since the build takes the compiled files of Mathlib from its official cache, we compared them with a rebuild of Mathlib and its dependencies from source, done as Mathlib's continuous integration builds it: they are identical, except for one module whose compiled output varies from run to run, and repeated runs reproduce the cached version of that module as well. \subsection{The upper bound}\label{ssec:upper} We prove the theorem \texttt{Sortnet.S13\_le\_45} with the network \texttt{Sortnet.juille}, the list of the $45$ comparators of Juill\'e's network~\cite{Jui95} in $10$ layers (Table~\ref{tab:juille}). The theorem \texttt{juille\_length} states that it has $45$ comparators, and \texttt{juille\_sorts} that it sorts. The proof is part of~\cite{LeanKernel}, as the archive \texttt{lean\_s13\_upper.tar.gz}. \begin{table}[ht] \centering\small \begin{tabular}{@{}rl@{}} \toprule layer & comparators\\ \midrule 1 & $(12,0)$ $(10,1)$ $(9,2)$ $(7,3)$ $(11,5)$ $(8,6)$\\ 2 & $(6,1)$ $(3,2)$ $(11,4)$ $(9,7)$ $(10,8)$\\ 3 & $(4,0)$ $(2,1)$ $(6,3)$ $(8,7)$ $(10,9)$ $(12,11)$\\ 4 & $(6,4)$ $(9,5)$ $(11,8)$ $(12,10)$\\ 5 & $(5,0)$ $(8,3)$ $(7,4)$ $(11,6)$ $(10,9)$\\ 6 & $(1,0)$ $(5,2)$ $(9,6)$ $(8,7)$ $(11,10)$\\ 7 & $(3,1)$ $(4,2)$ $(6,5)$ $(10,9)$\\ 8 & $(2,1)$ $(4,3)$ $(7,5)$ $(8,6)$\\ 9 & $(3,2)$ $(5,4)$ $(7,6)$ $(9,8)$\\ 10 & $(4,3)$ $(6,5)$\\ \bottomrule \end{tabular} \caption{Juill\'e's network on $13$ channels, as standard comparators (Section~\ref{ssec:circuit}), applied layer by layer and from left to right within a layer.}\label{tab:juille} \end{table} By the $0$-$1$ principle, which the formalization proves, a network sorts if it sorts the $2^{13}=8{,}192$ inputs with entries in $\B$. These inputs run through the network together. Channel $k$ carries one number with $8{,}192$ bits, and bit $x$ of that number is the value of channel $k$ on input number $x$; at the start it is bit $k$ of $x$. On the values $0$ and $1$ the minimum is the bitwise AND and the maximum is the bitwise OR, so a comparator replaces the numbers $a$ and $b$ on its channels by $a$ AND $b$ and $a$ OR $b$. The kernel runs the $45$ comparators on these $13$ numbers and checks that the results are nested: for channels $a\le b$, every bit set in the number on channel $a$ is also set in the number on channel $b$. So every $0$-$1$ input leaves the network sorted. The check is proved by \texttt{decide +kernel}, with no compiled code, and takes the kernel about $50$ milliseconds. Lemmas prove that the bitwise computation agrees with \texttt{Network.eval} at every bit position, that the starting numbers have the stated bits, and that every $0$-$1$ input vector is one of the $8{,}192$ bit patterns. \texttt{\#print axioms} gives \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound} for \texttt{S13\_le\_45} and \texttt{juille\_sorts}, and \texttt{propext} alone for \texttt{juille\_length}. The proof also passes a replay of its modules by Lean's kernel (\texttt{leanchecker}) and checks of an export of the three theorems with their dependencies by two independent implementations of the kernel, lean4lean and nanoda. Two altered networks show that the check can fail: replacing the last comparator $(6,5)$ by $(6,4)$, or the comparator $(12,10)$ of layer $4$ by $(11,10)$, makes the kernel reject it, and for these two networks a brute-force run over the $8{,}192$ inputs leaves $216$ and $255$ of them unsorted. \subsection{The bound \texorpdfstring{$P(2,13)\ge9$}{P(2,13) >= 9}}\label{ssec:p213lean} The supplement~\cite{SuppTwo} contains two Lean proofs of $P(2,13)\ge9$, one checked by the kernel and one that uses native code. They define runs, $W(x,y)$, top-two correctness and $P(2,n)$ as in Section~\ref{sec:defs}, for networks whose comparators may put the maximum on either channel; the run $(x,y)$ has the value $n+1$ on input $x$, $n$ on input $y$, and $z$ on each other input $z$. They also prove Lemma~\ref{lem:prune} for sorting networks as defined in Lean: for $x\ne y$, deleting the comparators of $W(x,y)$ from a sorting network $T$ on $n+2$ channels leaves a network that sorts with respect to a fixed order of its outputs, and untangling it~\cite[Exercise~5.3.4--16]{Knu98} gives a sorting network on $n$ channels with $|T|-|W(x,y)|$ comparators. With $S(11)\ge35$ (Section~\ref{ssec:harderlean}) they derive the theorem \texttt{Sortnet.S13\_ge\_44}, the bound that inequality~\eqref{eq:two} gives with $P(2,13)=9$ (Section~\ref{sec:intro}); Theorem~\ref{thm:main} improves it to $45$. The computation works with the compressed states of method~A (Section~\ref{ssec:tverify}). A state assigns to each pair of channels $(p,q)$, $p\ne q$, the largest number of comparators met so far by a run that has the largest value on $p$ and the second largest on $q$, or nothing if no run is there. A network with $p_2\le L$ is a sequence of comparators that leads from the start state (cost $0$ at every pair) to a state with a single entry, and that entry is at most $L$. We prove three facts about the step from a state $f$ to the state $f'$ after a comparator: \begin{itemize} \item The potential $\Theta(f)=\sum_pR\bigl(\sum_{q\ne p}2^{f(p,q)}\bigr)$, where $R(s)$ is the least power of two that is at least $s$ ($R(0)=0$) and absent entries contribute $0$, satisfies $\Theta(f')\ge\Theta(f)$. At a goal $\Theta\le2^L$, so a state with $\Theta>2^L$ cannot reach a goal. This is the Kraft prune of method~A. \item Relabeling the channels by a permutation maps reachable goals to reachable goals with the same number of comparators. \item The two orientations of a comparator give states that differ by the transposition of its channels, so comparators with $\mathrm{lo}<\mathrm{hi}$ suffice. \end{itemize} From these facts we prove in Lean: if a set $H$ of states contains no goal and, for every state in $H$ and every comparator with $\mathrm{lo}<\mathrm{hi}$, the next state is the same state, or has $\Theta>2^L$, or has a relabeling in $H$, then no state in $H$ reaches a goal. It remains to exhibit such a set $H$ for $N=13$ and $L=8$ that contains the start state, and to check the conditions; the formalization shows that a successful check implies $P(2,13)\ge9$. In the kernel-checked proof, an untrusted program produces a certificate: a list $H$ of $99{,}736$ states, the start state first, and for each state and each comparator with $\mathrm{lo}<\mathrm{hi}$ whose next state is neither unchanged nor pruned by the potential $\Theta$, a permutation of the channels and the index of the state of $H$ that the relabeled next state equals. Of the $99{,}736\cdot78=7{,}779{,}408$ next states, $275{,}115$ are unchanged, $6{,}396{,}523$ have $\Theta>2^8$ and $1{,}107{,}770$ are relabelings of states of $H$. A checking function written for Lean's kernel verifies, for each state of $H$ and each comparator, that the next state is unchanged, that a lower bound for its potential computed from the entries and row sums of the state exceeds $2^8$, or that the next state, relabeled by the given permutation, equals the listed state entry by entry. It also confirms that no state of $H$ is a goal. Lean's kernel evaluates the check itself (\texttt{decide +kernel}), in $1{,}102$ theorems of about $90$ states each, and every theorem of this formalization, \texttt{S13\_ge\_44} included, depends only on the standard axioms. \begin{sloppypar} The check rejects each of seven corrupted certificates or chunk claims that we tried, and the certificate files that it accepts (\texttt{data/keys.txt} followed by \texttt{data/c/*.txt} in name order) have the SHA-256 hash \certhash. \end{sloppypar} In the native proof, a search, whose code is not trusted, proposes a set $H$ of $138{,}537$ states, each relabeled by colour refinement with ties broken by channel index, and a checking function of about $50$ lines of Lean verifies the conditions. Lean evaluates this check and the native checker of Harder's certificate with \texttt{native\_decide} (Section~\ref{ssec:leandata}). The output of \texttt{\#print axioms Sortnet.S13\_ge\_44} is \begin{alltt}\small [propext, Classical.choice, Quot.sound, certOK_harder11._native.native_decide.ax_1_1, fullCheck_13_8._native.native_decide.ax_1_1] \end{alltt} The last two axioms, in the namespace \texttt{Sortnet}, state that the checks of Harder's certificate and of the states return \texttt{true}. As a test, the native check of the states reproduces $P(2,N)\ge\cl{\lg F(N)}$ for $3\le N\le12$, and explicit networks, checked by Lean's kernel without native code, give $P(2,N)\le\cl{\lg F(N)}$ for $3\le N\le13$ (theorem \texttt{p2\_values}). On $117{,}200$ random and exhaustively enumerated networks with $3\le N\le8$, the Lean definitions of $W(x,y)$, of top-two correctness and of the state step agree with the programs of method~A. \section{Consequences for larger networks}\label{sec:cons} We now combine Theorems~\ref{thm:main} and~\ref{thm:P}. \begin{proof}[Proof of Corollary~\ref{cor:table}] For $N\ge3$, $S(N)\ge S(N-1)+\cl{\lg N}$ by the one-value bound~\cite{VV72a} (Remark~\ref{rem:onevalue}), and $S(N)\ge S(N-2)+P(2,N)$ by Lemma~\ref{lem:prune}. Let \[ \Lambda(N)=\max\bigl(\Lambda(N-1)+\cl{\lg N},\ \Lambda(N-2)+\cl{\lg F(N)}\bigr),\qquad \Lambda(11)=35,\ \Lambda(12)=39, \] and let $\Lambda'$ satisfy the same recursion with $\Lambda'(12)=39$ and $\Lambda'(13)=45$. Since $S(12)=39$~\cite{Har22} and $S(13)=45$ (Theorem~\ref{thm:main}), Theorem~\ref{thm:P} and induction give $S(N)\ge\Lambda'(N)$ for $13\le N\le32$. Theorem~\ref{thm:main} enters only through the initial value $\Lambda'(13)=45$. Since $\Lambda(13)=44$, we have $\Lambda'(14)=\max(49,48)=49=\Lambda(14)+1$, and if $\Lambda'=\Lambda+1$ at $N-1$ and $N-2$, then also at $N$. Hence $\Lambda'(N)=\Lambda(N)+1$ for $13\le N\le32$. \end{proof} \begin{table}[ht] \centering\small \setlength{\tabcolsep}{4pt} \begin{tabular}{@{}l*{10}{r}@{}} \toprule $N$ & 13 & 14 & 15 & 16 & 17 & 18 & 19 & 20 & 21 & 22\\ $\Lambda(N)$ & 44 & 48 & 53 & 57 & 63 & 68 & 73 & 78 & 84 & 89\\ $\Lambda(N)+1$ & 45 & 49 & 54 & 58 & 64 & 69 & 74 & 79 & 85 & 90\\ \midrule $N$ & 23 & 24 & 25 & 26 & 27 & 28 & 29 & 30 & 31 & 32\\ $\Lambda(N)$ & 95 & 100 & 106 & 111 & 117 & 123 & 129 & 135 & 141 & 147\\ $\Lambda(N)+1$ & 96 & 101 & 107 & 112 & 118 & 124 & 130 & 136 & 142 & 148\\ \bottomrule \end{tabular} \caption{The values $\Lambda(N)$ and the lower bounds $S(N)\ge\Lambda(N)+1$ of Corollary~\ref{cor:table}.}\label{tab:chain} \end{table} Table~\ref{tab:chain} lists the bounds. Each step of the recursion takes the larger of the two bounds, so $\Lambda(N)+1$ is the strongest lower bound on $S(N)$ that the one-value bound and Lemma~\ref{lem:prune} give from $S(11)$, $S(12)$, $S(13)$ and Theorem~\ref{thm:P}. The values $\Lambda(N)$ are the lower bounds for $13\le N\le32$ in Dobbelaere's table~\cite{Dob}, consulted on 18 October 2026. Mericanii~\cite{Mer26} derives them from Lemma~\ref{lem:prune}, the one-value bound and Van Voorhis's inequality $P(2,N)\ge\cl{\lg F(N)}$, which Theorem~\ref{thm:P} proves for $N\le32$, and finds that each of them exceeds what the one-value bound alone gives. Corollary~\ref{cor:table} proves each of these twenty values and raises it by one. The corollary rests on Theorem~\ref{thm:P}, whose computations are archived in~\cite{SuppTwo}, and on Theorem~\ref{thm:main}, whose certificate and proofs are archived in~\cite{Supp} and~\cite{LeanKernel}. For $14\le N\le32$, the values of $P(2,N)$ that it uses rest on the searches of Section~\ref{sec:tsearch} and their checks, and Lean checks none of them; Section~\ref{ssec:p213lean} lists what the Lean proofs cover. \section*{Data and code availability} The certificate, the verifier with \texttt{lb2cr}, the two tables of exact values, the logs of the verification, the specification of the certificate format, the search program and the native Lean project with its data are archived on Zenodo as~\cite{Supp} (\href{https://doi.org/\suppdoi}{doi:\suppdoi}). \availabilitysentence\ The kernel-checked proof of the lower bound, with its data and the record of its build, and that of the upper bound are archived on Zenodo as~\cite{LeanKernel} (\href{https://doi.org/\kerneldoi}{doi:\kerneldoi}). The programs and logs of the computation of $P(2,N)$, the independent checks and the Lean proofs of $P(2,13)\ge9$ are archived on Zenodo as~\cite{SuppTwo} (\href{https://doi.org/\supptwodoi}{doi:\supptwodoi}); they are the contents of the repository~\cite{Repo} at commit \texttt{\repocommit}, whose README files number results, sections and tables as in the paper ``Sorting networks on 13 inputs need at least 44 comparators'' (\href{https://doi.org/10.5281/zenodo.23498528}{doi:10.5281/zenodo.23498528}), not as in the present paper. None of these archives contains Harder's file~\cite{Har19}. The build instructions of the native proof and of the proofs in~\cite{SuppTwo} fetch it and give its SHA-256 digest; the kernel-checked proof of the lower bound ships the data converted from it and records the digest of the file. This paper is \href{https://doi.org/\paperdoi}{doi:\paperdoi}. Our code is under the Apache License 2.0, and the text and the data under CC BY 4.0. \begin{thebibliography}{99} \bibitem{BN62} R.~C. Bose and R.~J. Nelson, \emph{A sorting problem}, J. ACM \textbf{9} (1962), no.~2, 282--296, \href{https://doi.org/10.1145/321119.321126}{doi:10.1145/321119.321126}. \bibitem{CCFS16} M.~Codish, L.~Cruz-Filipe, M.~Frank, and P.~Schneider-Kamp, \emph{Sorting nine inputs requires twenty-five comparisons}, J. Comput. System Sci. \textbf{82} (2016), no.~3, 551--563, \href{https://doi.org/10.1016/j.jcss.2015.11.014}{doi:10.1016/j.jcss.2015.11.014}. \bibitem{Dob} B.~Dobbelaere, \emph{Smallest and fastest sorting networks for a given number of inputs}, web page, \url{https://bertdobbelaere.github.io/sorting_networks.html}, consulted 2026-10-18 (history entry of 2025-04-21). \bibitem{FK73} R.~W. Floyd and D.~E. Knuth, \emph{The Bose--Nelson sorting problem}, A Survey of Combinatorial Theory (J.~N. Srivastava et al., eds.), North-Holland, Amsterdam, 1973, pp.~163--172, \href{https://doi.org/10.1016/B978-0-7204-2262-7.50020-X}{doi:10.1016/B978-0-7204-2262-7.50020-X}. \bibitem{Har19} J.~Harder, \emph{Certificate of the minimal size of 11-channel sorting networks}, Zenodo, 2019, dataset, \href{https://doi.org/10.5281/zenodo.4108365}{doi:10.5281/zenodo.4108365}. \bibitem{Har22} J.~Harder, \emph{An answer to the Bose--Nelson sorting problem for 11 and 12 channels}, arXiv:2012.04400v3 [cs.DS], 2022. \bibitem{HarRepo} J.~Harder, \emph{Lower size bounds for sorting networks}, source code, 2020, \url{https://github.com/jix/sortnetopt}, commit \texttt{0b5d09c}. The bound is defined as \texttt{lower\_size\_bound} in the file \texttt{checker/\allowbreak verified/\allowbreak Sorting\_Network\_Bound.thy}, and the correctness of the checking function is the lemma \texttt{check\_proof\_get\_bound\_spec} in \texttt{checker/\allowbreak verified/\allowbreak Checker.thy}. \bibitem{HH18} Q.~Huangfu and J.~A.~J. Hall, \emph{Parallelizing the dual revised simplex method}, Math. Program. Comput. \textbf{10} (2018), no.~1, 119--142, \href{https://doi.org/10.1007/s12532-017-0130-5}{doi:10.1007/s12532-017-0130-5}. \bibitem{Jui95} H.~Juill\'e, \emph{Evolution of non-deterministic incremental algorithms as a new approach for search in state spaces}, Proceedings of the Sixth International Conference on Genetic Algorithms (L.~J. Eshelman, ed.), Morgan Kaufmann, San Francisco, 1995, pp.~351--358. \bibitem{Knu98} D.~E. Knuth, \emph{The Art of Computer Programming, Vol.~3: Sorting and Searching}, 2nd ed., Addison-Wesley, Reading, MA, 1998. \bibitem{Lean4} L.~de Moura and S.~Ullrich, \emph{The Lean~4 theorem prover and programming language}, Automated Deduction -- CADE~28, Lecture Notes in Comput. Sci., vol.~12699, Springer, 2021, pp.~625--635, \href{https://doi.org/10.1007/978-3-030-79876-5_37}{doi:10.1007/978-3-030-79876-5\_37}. \bibitem{Mathlib} The mathlib Community, \emph{The Lean mathematical library}, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, pp.~367--381, \href{https://doi.org/10.1145/3372885.3373824}{doi:10.1145/3372885.3373824}. \bibitem{Mer26} Mericanii, \emph{Twenty tabulated lower bounds for sorting networks rest on an invalid proof: an audit of Van Voorhis (1972), and a partial repair}, draft, August 2026, \url{https://mericanii.com/work/s13/paper-correction.pdf}, consulted 2026-10-18. \bibitem{Repo} {\raggedright T.~S. Tomar, \emph{\reponame}, GitHub repository, \url{\repourl}, commit \texttt{\repocommit}.\par} \bibitem{Supp} T.~S. Tomar, \emph{Certificate and verifier for ``Sorting networks on 13 inputs need 45 comparators''}, Zenodo, 2026, \href{https://doi.org/\suppdoi}{doi:\suppdoi}. \bibitem{SuppTwo} T.~S. Tomar, \emph{Programs and logs for ``Sorting networks on 13 inputs need at least 44 comparators''}, Zenodo, 2026, \href{https://doi.org/\supptwodoi}{doi:\supptwodoi}. \bibitem{LeanKernel} T.~S. Tomar, \emph{A kernel-checked Lean proof that sorting networks on 13 inputs need 45 comparators}, Zenodo, 2026, \href{https://doi.org/\kerneldoi}{doi:\kerneldoi}. \bibitem{VV72a} D.~C. Van Voorhis, \emph{An improved lower bound for sorting networks}, IEEE Trans. Comput. \textbf{C-21} (1972), no.~6, 612--613, \href{https://doi.org/10.1109/TC.1972.5009021}{doi:10.1109/TC.1972.5009021}. \bibitem{VV72b} D.~C. Van Voorhis, \emph{Toward a lower bound for sorting networks}, Complexity of Computer Computations (R.~E. Miller and J.~W. Thatcher, eds.), Plenum Press, New York, 1972, pp.~119--129, \href{https://doi.org/10.1007/978-1-4684-2001-2_12}{doi:10.1007/978-1-4684-2001-2\_12}. \end{thebibliography} \end{document}