%
%
\newcommand{\kerneldoi}{10.5281/zenodo.23603571}
\newcommand{\leannativea}{1{,}724}
\newcommand{\leanrootchunks}{1{,}499}
\newcommand{\leanroots}{280{,}617}
\newcommand{\leanderived}{3{,}344{,}121}
\newcommand{\leanbfs}{36}
\newcommand{\leankl}{161}
\newcommand{\leanhint}{24}
\newcommand{\leanclaims}{12{,}315{,}738}
\newcommand{\leanstream}{1{,}011{,}669{,}465}
\newcommand{\leanjobs}{9{,}559}
\newcommand{\leandiff}{1{,}585{,}789}
\newcommand{\leandiffdistinct}{1{,}359{,}753}
\newcommand{\leandifffeas}{84{,}128}
\newcommand{\leanneg}{33}
\newcommand{\hardersteps}{12{,}659{,}079}
\newcommand{\pubdate}{25 October 2026}
\newcommand{\paperdoi}{10.5281/zenodo.23620051}
\newcommand{\suppdoi}{10.5281/zenodo.23504361}
\newcommand{\childrecs}{41{,}142{,}659}
\newcommand{\nineexact}{3{,}624{,}738}
\newcommand{\sevenexact}{4{,}028{,}993}
\newcommand{\claimsKT}{11{,}708{,}977}
\newcommand{\claimsKL}{12{,}381{,}230}
\newcommand{\tagsE}{148{,}319{,}131}
\newcommand{\tagsB}{78{,}082{,}756}
\newcommand{\tagsEbyB}{56{,}549{,}674}
\newcommand{\tagsEbyOracle}{91{,}769{,}457}
\newcommand{\insttt}{32{,}176{,}451}
\newcommand{\insteleven}{12{,}381{,}230}
\newcommand{\nineinst}{43{,}451{,}218}
\newcommand{\maxbudget}{41}
\newcommand{\maxbudgett}{41}
\newcommand{\maxbudgete}{28}
\newcommand{\maxbudgetn}{25}
\newcommand{\crossninecalls}{7{,}249{,}476}
\newcommand{\exsevensample}{20{,}145}
\newcommand{\bfanswers}{28{,}877}
\newcommand{\ninelines}{6{,}936{,}167}
\newcommand{\bfinst}{7{,}340}
\newcommand{\computeparagraph}{All servers had $384$ hardware threads unless stated otherwise. Layers $1$ to $12$ took under $9$ minutes on one server. Layers $13$ to $25$ took $10$ hours and $50$ minutes of wall-clock time on $35$ to $55$ servers, with two more that ran only backup processes. The processing times that the coordinator recorded for the layers add up to about $190$ server-hours. The exact values took under an hour of one server for the sets on $7$ channels and about $110$ server-hours for the sets on $9$ channels. The verification of the released files took \verifytime\ on a server with $192$ threads.}
\newcommand{\verifytime}{20 minutes}
\newcommand{\availabilitysentence}{Harder's repository~\cite{HarRepo} carries no licence, so the supplement~\cite{Supp} contains our changes to his program as a patch against commit \texttt{0b5d09c}, and its build instructions fetch his code.}
\newcommand{\ninecores}{15{,}430{,}581}
\newcommand{\crossninerow}{never infeasible}
\newcommand{\nineoverlap}{9{,}481}
\newcommand{\nineoverlapdiff}{9{,}348}
\newcommand{\ninerecovered}{3{,}294}
\newcommand{\juilleinst}{528}
\newcommand{\juilleorders}{3}
\newcommand{\mutations}{20}
\newcommand{\budgetcheck}{Since Proposition~\ref{prop:checker} covers budgets up to $56$, every instance passed to \texttt{lb2cr} must have budgets between $0$ and $56$. The verifier records the largest budget of each kind of instance.}
\newcommand{\invocation}{No option switches off any of these checks. Since the check of alive children requires the merged set of every layer, the job files of the released run list all of these sets, and the supplement~\cite{Supp} records the invocations of both programs.}
\newcommand{\crosscheckninesentence}{For each core with an exact value $e$, the verifier also passes the two instances on $9$ channels with budget $e$ to \texttt{lb2cr}, with the exact values on $7$ channels as weights, and requires that neither is infeasible. An infeasible answer would show that \texttt{lb2cr} or Harder's program is wrong.}
\newcommand{\supptwodoi}{10.5281/zenodo.23498529}
\newcommand{\reponame}{sortnet13-two-value-v5}
\newcommand{\repourl}{https://github.com/tejasvi/sortnet13-two-value-v5}
\newcommand{\repocommit}{be14346d67fd89b14f7e036ea03eae8d561b81ef}
\newcommand{\lemmaprefixes}{$351{,}541$}
\newcommand{\lemmanets}{$20{,}369$}
\newcommand{\cfgsXXVIII}{$262{,}417{,}641{,}559$}
\newcommand{\nodesXXVIII}{$30{,}972{,}138{,}194{,}473$}
\newcommand{\leavesXXVIII}{$12{,}416{,}681{,}168{,}846$}
\newcommand{\splitcheckscope}{\texttt{abs9f} and \texttt{abs9g}, $7$ pairs $(N,L)$, all kinds of split, nested up to five deep}
\newcommand{\certhash}{\texttt{092f8a343d02be3e1980cfc2da78343d}\allowbreak\texttt{a9d907ba1f55ef076437060bde8fd403}}
\newcommand{\hardersha}{\texttt{95da7e06ebef17bf76a50ae0e9d19d56}\allowbreak\texttt{cf87e0ec9e61b941528dc2cf05521fef}}
\newcommand{\hardershaU}{\texttt{7fe9f5cd694714bf83da0bcab162a290}\allowbreak\texttt{eb076ad4257265507a74cea8fab85b7e}}