\documentclass[11pt]{amsart} \pdfsuppressptexinfo=-1 \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage[margin=1.1in]{geometry} \usepackage{amssymb,mathtools} \usepackage{booktabs} \usepackage{placeins} \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{\oM}{o_{M}} \newcommand{\om}{o_{m}} \hypersetup{pdftitle={Sorting networks on 13 inputs need at least 44 comparators}, pdfauthor={Tejasvi Singh Tomar}} \title{Sorting networks on 13 inputs need at least 44 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, 68V20} \keywords{Sorting networks, Bose--Nelson problem, comparator networks, lower bounds, computer-assisted proof, formal verification, Lean theorem prover} \begin{document} \begin{abstract} Let $S(N)$ be the least number of comparators in a sorting network on $N$ inputs. We prove $S(13)\ge44$, one more than the previously best proved lower bound. We also prove $P(2,N)=\cl{\lg F(N)}$ for $3\le N\le32$, where $P(2,N)$ is the least worst-case number of comparators met by the two largest inputs in a network that delivers them to fixed outputs and $F$ is an explicit function of Van Voorhis; the lower bound comes from a finite search based on the structure of the paths of these two values. Starting from Harder's $S(11)=35$ and $S(12)=39$, these values of $P(2,N)$, the two-value bound $S(N)\ge S(N-2)+P(2,N)$ and the one-value bound $S(N)\ge S(N-1)+\cl{\lg N}$ give the twenty lower bounds on $S(N)$ for $13\le N\le32$ in Dobbelaere's table; these bounds rested on Van Voorhis's inequality $P(2,N)\ge\cl{\lg F(N)}$, whose published proof is invalid. The bound $S(13)\ge44$ is also proved in Lean~4, with every step checked by Lean's kernel. \end{abstract} \maketitle \vspace*{-3pt} \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\le 8$~\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)\ge 35$ 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. Van Voorhis's one-value bound $S(N)\ge S(N-1)+\cl{\lg N}$~\cite{VV72a} gives $S(13)\ge 43$, and this has been the best proved lower bound. In a chapter published the same year~\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, together with lower bounds for $14\le N\le 32$, crediting them to a suggestion of Jelmer Firet and to principles in Van Voorhis's chapter. Mericanii~\cite{Mer26}, however, showed that the chapter's 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; we call such a comparator a \emph{pass-through}. Pass-throughs occur already in a size-optimal network on $3$ inputs (see the example after Lemma~\ref{lem:antichain}). 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\le 32$ 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 use neither Van Voorhis's inequality $P(2,N)\ge\cl{\lg F(N)}$ nor its proof in~\cite{VV72b}; instead we compute $P(2,N)$ for $3\le N\le32$. \begin{theorem}\label{thm:main} $S(13)\ge 44$. \end{theorem} \begin{theorem}\label{thm:P} $P(2,N)=\cl{\lg F(N)}$ for $3\le N\le 32$. \end{theorem} \begin{corollary}\label{cor:table} For $13\le N\le 32$, $S(N)$ is at least the value $\Lambda(N)$ listed in Section~\ref{sec:cons}. \end{corollary} The proofs of these three results include computations. The sequel~\cite{S45} proves $S(13)=45$, and so raises each bound of Corollary~\ref{cor:table} by one; it extends the structure theory of Section~\ref{sec:structure} to a weighted form of~\eqref{eq:two}, which it applies to suffixes of a network. The upper bound in Theorem~\ref{thm:P} comes from an explicit network for each $N$ (Proposition~\ref{prop:upper}). The lower bound rests on a computation, and two observations keep it 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. 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}). Then the numbers of comparators met by the two values, for all $N(N-1)$ choices of $x\ne y$, are determined by a small amount of data (Theorem~\ref{thm:config}): the tree, the number of pass-throughs on each of its edges, and, for each place where the second maximum leaves the tree, the pass-through at which it re-enters the tree, or its output if it never does, with the number of comparators it meets on the way. For the places that share a re-entry point, and for those that reach the output, Kraft's equality describes which combinations of these numbers of comparators are possible. Second, the paths of the maximum are short in any network in which the two values meet few comparators (Lemma~\ref{lem:fixedx}), which bounds the height of the tree. By Lemma~\ref{lem:mono} and Table~\ref{tab:F}, searches for $3\le N\le13$ and $N=17$, $21$ and $28$ suffice for the lower bound (Theorem~\ref{thm:search}); those for $N\le21$ are small. The search for $N=28$ is far larger, and for some of its slowest tree shapes we also use the symmetries of the tree and its pass-throughs, so that only some of the equivalent choices of re-entry points and numbers of comparators are searched, but at least one from each class is searched (Lemma~\ref{lem:sym}). Section~\ref{sec:defs} defines $P(2,N)$ and proves~\eqref{eq:two}, the monotonicity of $P(2,N)$ in $N$ and the upper bound. Section~\ref{sec:structure} describes networks that deliver the two largest values to fixed outputs, and Section~\ref{sec:search} gives the search and the validity of each pruning rule. Section~\ref{sec:results} reports the searches and proves Theorem~\ref{thm:P}, Section~\ref{sec:verify} and Appendix~\ref{app:checks} describe the checks, Section~\ref{sec:lean} gives two formal proofs of Theorem~\ref{thm:main} in Lean~4, and Section~\ref{sec:cons} proves Theorem~\ref{thm:main} and Corollary~\ref{cor:table}. \section{Networks, two-value pruning and an upper bound}\label{sec:defs} \subsection{Comparator networks} A \emph{comparator network} $T$ on $N$ inputs is a finite acyclic circuit made of $N$ input leads 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 $N$ of them. Given distinct real 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. $T$ is a \emph{sorting network} if its outputs can be listed as $o_1,\dots,o_N$ so that $o_i$ carries the $i$-th smallest input value for all inputs. Drawing $T$ on $N$ channels along a topological order of its comparators gives a network in the usual sense in which a comparator may send its maximum to either of its two channels, followed by a permutation of the channels. Renaming the channels removes the permutation, and a sorting network of this kind can be untangled into a standard one with the same number of comparators~\cite[Exercise~5.3.4--16]{Knu98}. Thus $S(N)$ is the same in both models. \subsection{Runs and the quantity \texorpdfstring{$P(2,N)$}{P(2,N)}} Let $N\ge2$. For distinct inputs $x$ and $y$, the \emph{run} $(x,y)$ puts the largest value $M$ on $x$, the second largest value $m$ on $y$, and smaller 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. Consequently, the leads that carry $M$ and $m$ depend only on $(x,y)$. We write $P_x$ for the set of leads that carry $M$, which depends only on $x$, and $W(x,y)$ for the set of comparators with $M$ or $m$ on an input lead. \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$ and $\om=o_{N-1}$. The next lemma establishes inequality~\eqref{eq:two}, which is equation~(2) of~\cite{VV72b} (see~\cite[Section~2]{Mer26}). 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$ and $o_{N-1}$, and $o_1,\dots,o_{N-2}$ 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 an internal vertex $c$ let $\mathrm{dep}(c)$ be its depth, the root having depth $0$, and 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)=\mathrm{dep}(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\\ $\beta(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\\ $\beta(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 $\beta(N)=\cl{\lg N}+\cl{\lg(N-1)}$ of Corollary~\ref{cor:beta}.}\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 $\mathrm{dep}(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} \subsection{The tree of maximum paths} A lead is \emph{red} if it lies in $P_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:red} 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 $P_x$. The maximum leaves each comparator on $\hi$, so no $\lo$ output is red. If an input lead of $g$ lies in $P_x$, the maximum enters $g$ on it and leaves on $\hi(g)$, so $\hi(g)\in P_x$. Conversely, if $\hi(g)\in P_x$, the maximum entered $g$ on an input lead, which lies in $P_x$. (b) Let $\ell\in P_x$. If $\ell$ enters a comparator $g$, then $\hi(g)$ is the next lead of $P_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 $T$ is a top-two correct network on $N\ge3$ inputs and $B$ is its tree. For a vertex $v$ of $B$ (an input or a branch node), $\seg(v)$ denotes the edge from $v$ to its parent, or from $v$ to $\oM$ if $v$ is the root, and $k(v)$ denotes the number of pass-throughs on $\seg(v)$. For a pass-through $q$ let $u(q)$ be the vertex with $q$ on $\seg(u(q))$. We call the branch nodes and the pass-throughs the \emph{red comparators}. For a red comparator $v$, let $A(v)$ be the set of comparators on the path from $v$ to $\oM$, $v$ included, and let $\bar v=v$ if $v$ is a branch node and $\bar v=u(v)$ if $v$ is a pass-through. For an input $x$ let $\delta(x)$ be the number of comparators on the path from $x$ to $\oM$, which are the comparators that $M$ passes when it starts on $x$. For a branch node $c$ and an input $y$ below $c$, let $\pre(y,c)$ be the number of comparators on the path from $y$ up to $c$, with $c$ excluded, so that $\delta(x)=|A(c)|+\pre(x,c)$ for each branch node $c$ above $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}. \end{remark} \subsection{The runs} \begin{lemma}[the second maximum before the meeting]\label{lem:run} 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 $P_x$. When $m$ enters a comparator $g$, the lead that carries $m$ is not in $P_x$, so $m$ leaves on $\lo(g)$ exactly when the other input lead of $g$ lies in $P_x$, that is, when $g$ is on the path from $x$ to $\oM$. (a) In the tree of Lemma~\ref{lem:red}(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)\setminus\{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 $\bar v$ are incomparable in $B$, let $w(q,v)=\lca_B(u(q),\bar v)$, and let $\kappa(q,v)$ be the number of comparators from $q$ up to $w(q,v)$, with $w(q,v)$ excluded: \[ \kappa(q,v)=1+\#\{\text{pass-throughs above $q$ on }\seg(u(q))\}+\sum_{w'}\bigl(1+k(w')\bigr), \] where $w'$ runs over the branch nodes strictly between $u(q)$ and $w(q,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 $\bar v$ are incomparable in $B$, the vertex $w=w(q,v)$ lies in $A(v)$, the value $m$ passes $\kappa(q,v)$ comparators outside $A(v)$ from $q$ up to $w$, meets $M$ at $w$ and leaves on $\lo(w)$, and $\tau(v)=d(v)+\kappa(q,v)+\tau(w)$. \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:red}(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 $\bar v$, or equal to $\bar v$ with $q$ above $v$, then $q$ would lie in $A(v)$. If $u(q)$ were a proper descendant of $\bar v$, or equal to $\bar v$ with $q$ below $v$, then $q$ would come before $v$ in the circuit. Hence $u(q)$ and $\bar v$ are incomparable, and $w$ is a proper ancestor of $\bar v$, hence $w\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 $w'$ strictly between $u(q)$ and $w$ is not an ancestor of $\bar v$, so $w'\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(w')$, whose pass-throughs are not in $A(v)$ either. At $w$ the value $M$ arrives on the input lead on the side of $\bar v$ and $m$ on the other one, so $m$ leaves on $\lo(w)$. The comparators passed from $q$ up to $w$, with $w$ excluded, are $\kappa(q,v)$ in number and none 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)$ strictly above $v$, so it ends, in case~(i). \subsection{Reduced networks and the forest of the second maximum} 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=(N\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~(N1). 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~(N1) or~(N2) 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~(N1) 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~(N2). 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~(N2) an irrelevant one enters no blue comparator, and by~(N1) 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:config} \begin{definition}\label{def:config} 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(v)\ge0$ of pass-throughs on each edge $\seg(v)$, placed in order along the edge; \item for each \emph{source}, that is, each internal vertex $c$ of $B$ and each pass-through $q$, either the mark \emph{dead}, allowed for pass-throughs only, or a \emph{root} $\rho\in\{\om\}\cup\{\text{pass-throughs}\}$ and a \emph{depth} $d\ge0$; \end{enumerate} subject to two conditions: \begin{enumerate}[label=(\Alph*)] \item[(K)] for each $\rho\in\{\om\}\cup\{\text{pass-throughs}\}$, the sources assigned to $\rho$ form a nonempty set whose depths satisfy $\sum2^{-d}=1$; \item[(A)] the directed graph $G(\Gamma)$ on the red comparators, with an arc from each red comparator to the next comparator above it and an arc from each source $v$ to its root $q$ whenever $q$ is a pass-through, is acyclic. \end{enumerate} We call the pair $(B,k)$ of (i) and (ii) the \emph{skeleton} of $\Gamma$. The quantities $\delta$, $\pre$, $A(\cdot)$, $\kappa$ and $w$ are defined from the skeleton as above. For each source $v$ that is not dead, 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)+\kappa(q,v)+\tau_\Gamma(w(q,v)) & \text{if }\rho(v)=q\notin A(v), \end{cases} \] and put $\tau_\Gamma(v)=\infty$ if the recursion reaches a dead source. 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$. \end{definition} In the third case of the recursion, $u(q)$ and $\bar v$ are incomparable by~(A). Otherwise $q$ would lie 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 $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:red} and~\ref{lem:forest} is feasible at level $L$ and gives each source that is not dead 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:red} gives $B$ and the numbers $k(v)$. By Lemma~\ref{lem:forest}, give each branch node $c$, and each pass-through $q$ for which $\lo(q)$ is relevant, 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). An arc of $G(\Gamma)$ is a directed path in the circuit: from a red comparator up to the next one, or from a source $v$ through $\lo(v)$ and the blue comparators of its tree into the pass-through $q$. Consequently, a cycle in $G(\Gamma)$ would give a cycle in the circuit, and~(A) holds. By Lemmas~\ref{lem:run}, \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 source, because the sources it reaches carry $m$ in the run. Hence $\Gamma$ is feasible at level $L$. A source $v$ that is not dead carries $m$ 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(v)$ comparators on each edge $\seg(v)$, 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 $\rho$, take a binary tree of blue comparators whose leaves are the $\lo$ outputs of the sources assigned to $\rho$, 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 $\rho$, or the output $\om$ if $\rho=\om$. The $\lo$ outputs of dead sources 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~(A) 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:run} and~\ref{lem:after} use top-two correctness only to identify the output in case~(i), and here each walk from a source ends at its root by construction. Since $\Gamma$ is feasible, the recursion from each $\lo(c)$ avoids dead sources 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 at the $i$-th place on $\seg(h(v))$, counted from below, is the image of the one at the $i$-th place on $\seg(v)$, and of the assignment that gives the source $h(v)$ the root $h(\rho(v))$ and the depth $d(v)$ if $v$ is not dead, 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$ (the last is defined in Lemma~\ref{lem:budget}) 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)$, $\kappa$ and $w$ 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 $w(h(q),h(v))=h(w(q,v))$. The sources assigned to $h(\rho)$ in $h\Gamma$ are the images of those assigned to $\rho$ 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~(A) holds. Induction along the recursion of Definition~\ref{def:config} gives $\tau_{h\Gamma}(h(v))=\tau_\Gamma(v)$ for every source $v$ that is not dead, 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} \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 a comparator network on the $N-1$ inputs other than $x$. In the run $(x,y)$ of $T$, the value $m$ is never on a lead of $P_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:red}(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$ meets 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:beta} $P(2,N)\ge\beta(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:beta} 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)+\pi(c)\ \le\ \tau_\Gamma(c)\ \le\ \sigma(c,x):=L-\delta(x)-\max_{y\text{ below }c_2}\pre(y,c), \] where $\pi(c)=\kappa(\rho(c),c)$ if $\rho(c)$ is a pass-through outside $A(c)$, and $\pi(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{The search}\label{sec:search} Fix $N\ge3$ and $L$, and put $H=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$, 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 $t$ lexicographically. \item For each $B$, enumerate the numbers $k(v)\in\{0,\dots,H\}$ with $\delta(x)\le H$ 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 sources: 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 $v\to q$ to a pass-through $q$ is added only if the graph of the arcs present so far has no path from $q$ to $v$; \item each internal vertex $c$ satisfies $d(c)+\pi(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 source 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$ and that $\delta(x)\le H$ for each $x$. 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=\phi h_0$ for some automorphism $\phi$ of $B'$. By the same lemma, $h\Gamma$ is feasible at level $L$, has depths at most $L$ and satisfies $\delta(x)\le H$. 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, (A) 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 source $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 $v\to q$. \subsection{Three further tests}\label{ssec:extra} We add 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 $\rho$ that $c$ may join under~(b), let $\mu(c,\rho)$ be $\min_x\sigma(c,x)$ minus the value that $\pi(c)$ would take if $\rho(c)=\rho$, 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,\rho)<0$ for each open root $\rho$, or if \[ \sum_{c\in U}2^{-\max_\rho\mu(c,\rho)}\ >\ \sum_{\rho\text{ open}}\Bigl(1-\sum_{v\text{ assigned to }\rho} 2^{-d(v)}\Bigr). \] \item \emph{Partial costs.} During (S4), define $\tau^-(v)$ by the recursion of Definition~\ref{def:config} with $\tau^-(v)=0$ for sources 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:red}(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 $w(q,v)$, where $v$ is the comparator of the previous meeting. Here $w(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 $(0,1),(0,2),(1,2)$ on $3$ inputs, written as usual on channels, with $(i,j)$ sending the maximum to channel $j$~\cite[Proposition~3]{Mer26}. Its branch nodes are $c_1=(0,1)$ and $c_2=(1,2)$, and $(0,2)$ is a pass-through on the edge of input~$2$. For $x=0$ the value $m$ leaves $c_1$, enters $(0,2)$ 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:capacity} 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,\rho)$. It therefore adds at least $2^{-\max_\rho\mu(c,\rho)}$ 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 sources do not change, and the other terms are nonnegative or infinite. Induction along the recursion gives $\tau^-(v)\le \tau_\Gamma(v)$ for every source $v$. \end{proof} \subsection{A symmetry reduction}\label{ssec:sym} 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 sources are visited in a fixed order $s_1,\dots,s_n$. We order the possible values of a source 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 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_44 : \(\forall\) net : Network 13, net.Sorts \(\to\) 44 \(\le\) net.length theorem main_theorem : (\(\forall\) net : Network 11, net.Sorts \(\to\) 35 \(\le\) net.length) \(\to\) \(\forall\) net : Network 13, net.Sorts \(\to\) 44 \(\le\) net.length \end{alltt} The theorem \texttt{S13\_ge\_44} is in the namespace \texttt{Sortnet}. Both formalizations derive it from the proposition shown as \texttt{main\_theorem} and from the bound $S(11)\ge35$ for these networks. The formalizations also prove the 0-1 principle, so the theorems hold equally with sorting defined on inputs in $\{0,1\}$. \subsection{What is proved} The formalizations 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$. The proof combines three results. \begin{enumerate}[label=(\roman*)] \item Lemma~\ref{lem:prune} for sorting networks in the form above: 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. \item A Boolean computation that implies $P(2,13)\ge9$. \item A Boolean computation that implies $S(11)\ge35$. \end{enumerate} By (i) and (ii), $S(11)\ge35$ implies $S(13)\ge44$, which is \texttt{main\_theorem}; with (iii) this gives \texttt{S13\_ge\_44}. The two formalizations share the definitions, the proof of (i), and the reductions of (ii) and (iii) to conditions on states and on the steps of a certificate. They differ in the checking functions that verify these conditions and in how the checks are evaluated. For (ii), the computation works with the states of method~A, which compress the runs. 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 \emph{goal}, a state with a single entry that 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 $\Phi(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 $\Phi(f')\ge\Phi(f)$. At a goal $\Phi\le2^L$, so a state with $\Phi>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 $\Phi>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; each formalization shows that a successful check implies $P(2,13)\ge9$. For (iii), the formalizations follow the proof system of Harder's certificates~\cite{Har22}. A network \emph{works} on a set $V$ of vectors in $\{0,1\}^n$ if outputs of equal weight are equal; a sorting network works on every set, and its comparators may here be any pairs of channels. Each step of a certificate claims that every network that works on its set has at least a given number of comparators. In each formalization the rules that the steps use, those of Harder's proof system, are proved in Lean, 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~\cite{Har19}, with $12{,}659{,}079$ 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. \subsection{The two formalizations}\label{ssec:kernel} In the first formalization, the data for (ii) are a list $H$ of states, the start state first, with a permutation of the channels and the index of a state of $H$ for each state and each comparator with $\mathrm{lo}<\mathrm{hi}$ whose next state is neither unchanged nor pruned by the potential $\Phi$, so that the indexed state equals the relabeled next state; for (iii) they are Harder's file, converted into data that Lean modules read. Checking functions written for Lean's kernel verify these conditions and that no state of $H$ is a goal; sets of vectors are stored as numbers read as bitmaps, with operations proved correct in Lean, and the kernel evaluates the checks itself. In the second, an untrusted search proposes for (ii) a set $H$ of states, each relabeled by colour refinement, and Harder's certificate is re-encoded as text that Lean reads at build time; Lean compiles the two checks, runs them, and records each outcome as an axiom. Besides the standard axioms, \texttt{\#print axioms Sortnet.S13\_ge\_44} lists exactly these two. The theorem \texttt{p2\_values} of the second formalization states $P(2,N)=\cl{\lg F(N)}$ for $3\le N\le13$. Its upper bounds come from explicit networks checked by Lean's kernel, and its lower bounds from native checks of the kind in (ii), one for each $N$. %% LEAN-SECTION-END \section{Consequences for sorting networks}\label{sec:cons} \begin{proof}[Proof of Theorem~\ref{thm:main}] By Lemma~\ref{lem:prune}, $S(13)\ge S(11)+P(2,13)$. Harder proved $S(11)=35$~\cite{Har22}, and Theorem~\ref{thm:P} gives $P(2,13)=9$. Therefore $S(13)\ge44$. \end{proof} \begin{proof}[Proof of Corollary~\ref{cor:table}] For $N\ge3$ we have $S(N)\ge S(N-1)+\cl{\lg N}$~\cite{VV72a} (see Remark~\ref{rem:onevalue}) and $S(N)\ge S(N-2)+P(2,N)$ by Lemma~\ref{lem:prune}. Starting from $S(11)=35$ and $S(12)=39$~\cite{Har22}, put \[ \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. \] By Theorem~\ref{thm:P} and induction, $S(N)\ge\Lambda(N)$ for $13\le N\le32$. The values are \begin{center} \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\\ \midrule $N$ & 23 & 24 & 25 & 26 & 27 & 28 & 29 & 30 & 31 & 32\\ $\Lambda(N)$ & 95 & 100 & 106 & 111 & 117 & 123 & 129 & 135 & 141 & 147\\ \bottomrule \end{tabular} \end{center} These are the lower bounds in Dobbelaere's table~\cite{Dob}. \end{proof} The method of this paper cannot decide between $44$ and the $45$ comparators of Juill\'e's network~\cite{Jui95}, because $P(2,13)=9$ is exact: the two-value bound with $S(11)=35$ gives no more than $44$. \appendix \section{The checks of the computation}\label{app:checks} In the first group of Table~\ref{tab:verify}, method~A searches comparator networks directly, with exact compression of states, rejection of isomorphic states and a pruning rule based on a Kraft inequality over the runs, and methods~B and~C search a relaxed tree model, with and without a height bound. Notes in the supplement~\cite{Supp} prove the Kraft inequality and the structure theorem of the relaxed model. The search over standard networks in the third group prunes with two lower bounds of Huffman type and a reduction by symmetry. \begin{table}[!htbp] \centering\footnotesize \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.5\textwidth}>{\raggedright\arraybackslash}p{0.42\textwidth}@{}} \toprule check & outcome\\ \midrule \multicolumn{2}{@{}l}{\emph{1. Programs that use neither the search nor its model}}\\ method A (networks, 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 (relaxed tree model), $3\le N\le13$ & $P(2,N)$ as in Theorem~\ref{thm:P}\\ tests of the pruning rules of method A on all $15{,}113{,}524$ states reachable with costs at most $L$, for $N=8$ and $L=6,7,8$ & no state from which a goal is reachable is pruned\\ tests of the relaxed tree model on $3{,}420$ random top-two correct networks with $3\le N\le8$ & no failure\\ \midrule \multicolumn{2}{@{}l}{\emph{2. Tests of the basic search and its model}}\\ an integer program (HiGHS~\cite{HH18}) for each skeleton, $15$ pairs $(N,L)$ with $N\le13$ & the same skeletons feasible as in the basic search; at $(13,8)$ none of $508$ skeletons on ordered trees\\ $4{,}464{,}896$ top-two correct networks with $4\le N\le11$, mapped into the model & costs equal to simulation, each accepted at its own $p_2$\\ simulation of the feasible configurations at $L=\cl{\lg F(N)}$: the basic search for $N\le8$ and $N=11$, the refined search also for $N=9,10$ & $1{,}258$ and $118{,}825$ configurations, no mismatch\\ \midrule \multicolumn{2}{@{}l}{\emph{3. A search over standard networks, without the model}}\\ $(N,L)=(12,8),(13,8),(12,9),(13,9)$ & infeasible, infeasible, feasible, feasible\\ tests of its two lower bounds and its symmetry reduction on \lemmaprefixes\ prefixes of \lemmanets\ networks, $4\le N\le13$ & no violation\\ \midrule \multicolumn{2}{@{}l}{\emph{4. Consistency of the searches with (P1)--(P3)}}\\ the refined search against the basic search: 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 numbers of feasible configurations\\ the extended search against the refined search, on the refined search's $22$ runs (Table~\ref{tab:runs} for $N\le21$, and $L=\cl{\lg F(N)}$ for $N\le11$) & same numbers of skeletons and of feasible configurations for each shape\\ the extended search with the symmetry test against the extended search, on the same runs & feasible configurations in the same shapes; with the test switched off the same output, with it the same classes of feasible assignments\\ split runs against unsplit runs: the extended search with and without the symmetry test, $7$ pairs $(N,L)$, every kind of split used at $N=28$, alone and nested (with the symmetry test, up to seven nested splits) & skeletons, feasible configurations and complete assignments add up\\ a separate run at $N=28$ by the basic search, the refined search and two variants of the refined search, which differ only in how (S2) keeps one skeleton from each class, on all shapes except the $119$ slowest ($62{,}522$ shapes) & no feasible configuration; for each shape not run by the basic search, the same number of skeletons as the extended search\\ \midrule \multicolumn{2}{@{}l}{\emph{The upper bound}}\\ the networks of Proposition~\ref{prop:upper}, $2\le N\le32$ & $p_2=\cl{\lg F(N)}$\\ \bottomrule \end{tabular} \caption{The checks of the computation, in four groups, and a check of the upper bound. The supplement lists the programs and logs for each row, and every split of the run at $N=28$.}\label{tab:verify} \end{table} \FloatBarrier \section*{Data and code availability} The programs, the logs of every computation in this paper, and the independent checks are archived on Zenodo as~\cite{Supp} (\href{https://doi.org/\suppdoi}{doi:\suppdoi}). They are the contents of the repository~\cite{Repo} at commit \texttt{\repocommit}, where the four programs of Section~\ref{ssec:programs} are \texttt{abs5} (basic), \texttt{abs9} (refined), \texttt{abs9f} (extended) and \texttt{abs9g} (extended, with the symmetry test). The Lean proofs of Section~\ref{sec:lean} read Harder's certificate~\cite{Har19}, which the supplement does not contain; their build instructions download the file and check its SHA-256 hash. Part of the logs of the shapes searched with the symmetry test were written by four earlier revisions of \texttt{abs9g}; they give the same output as the released program on $53$ small runs, and on $42$ shares at $N=28$ the released program reproduces the results in the logs. This paper is \href{https://doi.org/\paperdoi}{doi:\paperdoi}. The code is under the Apache License 2.0, and the text 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, ed.), 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{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{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{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{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}. \bibitem{S45} T.~S. Tomar, \emph{Sorting networks on 13 inputs need 45 comparators}, Zenodo, 2026, \href{https://doi.org/10.5281/zenodo.23504358}{doi:10.5281/zenodo.23504358}. \bibitem{Repo} T.~S. Tomar, \emph{\reponame}, GitHub repository, \url{\repourl}, commit \texttt{\repocommit}. \bibitem{LeanRepo} T.~S. Tomar, \emph{Lean formalization of $S(13)\ge44$}, part of the supplement~\cite{Supp}. \bibitem{LeanKernelRepo} T.~S. Tomar, \emph{Kernel-checked Lean formalization of $S(13)\ge44$}, part of the supplement~\cite{Supp}. \bibitem{Supp} T.~S. Tomar, \emph{Programs and logs for ``Sorting networks on 13 inputs need at least 44 comparators''}, Zenodo, 2026, \href{https://doi.org/\suppdoi}{doi:\suppdoi}. \end{thebibliography} \end{document}