\section{What is proved and what is open}\label{sec:status}

\subsection{Proved}

Inside the model of Section~\ref{sec:model}, the paper determines the least cost of soundness. For finitely many candidates and exponential checks it is the entropy law, exact up to an additive term that is sharp (Theorem~\ref{thm:A}) and exact without remainder when the soundness is the reciprocal of an integer and the budget a power of it, where the optimal schedule is a Huffman code (Theorem~\ref{thm:C}). For checks of polynomial order the least cost is given in closed form by a R\'enyi entropy (Theorem~\ref{thm:D}), and for every cost function an infinite sequence of candidates admits a sound schedule of finite cost exactly when one series built from the concave conjugate of the cost converges (Theorem~\ref{thm:dual}). The same price, rescaled by the error rate of the generator, governs chains of improvements (Theorem~\ref{thm:B}), and checking only the outcome of a chain of $n$ steps is exponentially more expensive than checking every step (Theorem~\ref{thm:gating}). An infinite chain reaches a singularity soundly exactly when the costs of its checks have finite entropy in addition to a finite sum, which fails for a nonempty range of cost laws (Theorem~\ref{thm:E}, Corollary~\ref{cor:gap}); a branching takeoff with a fixed false acceptance rate keeps infinitely many errors on survival, and a sound one needs a number of runs that grows linearly with the generation (Theorem~\ref{thm:F}). In the Osgood model of growth every singular takeoff can be made sound with exponential checks, at a price of order $1/(\alpha-1)^{2}$ near the critical exponent, while polynomial checks move the threshold of a sound takeoff from $\alpha=1$ to $\alpha=1+s$ (Proposition~\ref{prop:osgood}).

None of this needs foresight or a single agent. A rule that sees only the past costs is sound for every future and pays over the offline optimum an excess of order $\frac{A}{L}\log\log\frac{A}{a_{1}}$, which no online rule avoids (Theorem~\ref{thm:G}), so sound singularities are reached online whenever they are reached at all (Corollary~\ref{cor:onlinesing}). Splitting the work among subagents is free when the budget is split in proportion to cost, and costs exactly a Kullback--Leibler divergence otherwise (Theorem~\ref{thm:H}); cheap checks before one exact check reduce the cost of the exact check to the correct candidates, up to a logarithmic premium (Theorem~\ref{thm:cascade}). Depth has a price of the same kind: $n$ verified layers that share one budget cost at least $n\log(n/\theta)$ nats of soundness, each added layer at least $\log((n+1)/\theta)$ more, and past a finite depth every tower costs more than any fixed amount (Theorem~\ref{thm:tower}).

Outside the model, two results come from the experiments. Theorem~\ref{thm:onethird} proves a lattice mass gap $m\ge-\log(3\beta_{W})$ for four-dimensional $\mathrm{SU}(2)$ on $\beta_{W}<\frac13$ by a gauge fixing with one fixed link per plaquette, and Proposition~\ref{prop:forestceiling} shows that no forest gauge fixing goes further; the theorem is proved here and has not been refereed. Lemma~\ref{lem:levelposet} reduces monochromatic sublattices of a level colouring to weighted posets, and with it Theorem~\ref{thm:fvalues} determines $f(n)$ for $n\le20$.

The measurements of Section~\ref{sec:experiments} are these: typing the constructions is what lets the network reach a step that random pairing does not; Hebbian boosters do not improve on the unboosted network; memory halves the checks needed to reach the plateau and does not raise it; agents reach the plateau sooner and no further; and no transfer of a pattern in the matrix of Section~\ref{ssec:matrix} closes a blocking step. Construction mode rebuilds from the rules of Steinberg's problem the two gadgets of the counterexample of \cite{CHK17} and the counterexample itself, where random combination of library pieces finds nothing, and finds nothing on Erd\H{o}s's question for cycles of length $4$ to $6$ (Section~\ref{ssec:steinberg}). On three targets at equal budgets of exact checks, depth paid once: a second layer whose curriculum turns an easier gadget into a lemma reaches a gadget that the builder alone does not, a third layer adds nothing, and sharing one library and one set of weights shortens the step after the lemma (Section~\ref{ssec:towerbench}). Pointed at the Hodge conjecture alone, the network leaves the gap of every target point where it was after twelve rounds, including a burst that multiplied the cost of a round; counting excludes two of the configurations on $E_{0}^{6}$ left open in \cite{BB26c} and reduces two others to explicit Massey products (Section~\ref{sec:hodgeround}).

The finite inequalities behind these statements are proved in Lean~4 (Appendix~\ref{app:checks}). The probabilistic limit theorems, Wald's identity, the Kesten--Stigum theorem, L\'evy's conditional Borel--Cantelli lemma and the extinction theorem of Galton--Watson processes, are classical and are proved or cited in Appendix~\ref{app:derivations}; the asymptotics of $\zeta$ near $1$ are proved in the text.

\subsection{Open}

Five questions are left open, and each is a precise mathematical question.

\emph{Adaptive protocols.} Remark~\ref{rem:adaptive} shows that a protocol which looks at the outcomes of the checks can avoid the entropy term by halting at the first rejection, at the price of losing the correct work after it. Let a protocol be \emph{conservative} if, in every world, it keeps every correct candidate with probability one. Is the least worst-case expected cost of a conservative $\theta$-sound protocol equal to $\Vs(\theta)$ up to an additive $O(A)$? An adaptive protocol may let the number of runs of later checks depend on the results of earlier ones; since a correct candidate never fails, a conservative protocol learns nothing from the runs of a candidate that passes, and the question is whether the information it gains from rejections can be converted into a saving that is not $O(A)$.

\emph{Two-sided checks.} For checks that make errors on both sides Proposition~\ref{prop:twosided} gives the entropy law with the rate $D=\mathrm{KL}(\mathrm{Ber}(\frac12)\,\|\,\mathrm{Ber}(q))$ in the upper bound and $\log(1/q)$ in the lower bound. The exact rate of a sequential test with two error probabilities is Wald's \cite{Wal45}, and the question is whether the optimal schedule for many two-sided checks attains the entropy law with the Chernoff rate of the pair of hypotheses, in both directions.

\emph{Correlated runs.} The model assumes that the runs of a check are independent. A real verifier, a learned reward model or a test suite run on the same machine, has correlated errors, and repeated runs of a deterministic check gain nothing. The entropy law holds for every family of checks whose false acceptance probability after $r$ runs is at most $\eps^{r}$, whatever the mechanism; the open question is which checks used in practice have this property, with which $\eps$, and what replaces the law for those that do not.

\emph{Monochromatic sublattices.} Is $f(n)=O(n)$? For every $n\le20$ some level colouring is optimal (Theorem~\ref{thm:fvalues}); if level colourings are optimal for every $n$, Lemma~\ref{lem:levelposet} reduces the question to words in two letters.

\emph{The online constant.} The upper and lower bounds of Theorem~\ref{thm:G} differ by a factor of four in the term $\frac{A_{N}}{L}\log\log\frac{A_{N}}{a_{1}}$. The exact constant is the least $\kappa$ such that a $\theta$-sound online rule has excess $(\kappa+o(1))\frac{A_{N}}{L}\log\log\frac{A_{N}}{a_{1}}$ on every sequence; the bounds give $\frac12\le\kappa\le2$.

\subsection{What is not claimed}

The paper does not claim that any existing system is sound or that an intelligence explosion will or will not occur. It does not claim progress on the five problems of Section~\ref{sec:benchmark} beyond the two results above: no pass line is crossed, the Yang--Mills step lies below the crossover where the open problem begins, and the values of $f(n)$ do not decide whether $f(n)=O(n)$. The Steinberg gadgets are a rediscovery of a published construction, and the exclusions on $E_{0}^{6}$ leave (F2) and (F3$'$) open. Passing all five lines is a definition we use to score a proposer, not a property any system has shown. The theorems are statements about a model with independent runs, perfect completeness and schedules fixed in advance, and their value for a real system depends on how well it satisfies them. What is claimed is that inside the model the cost of soundness is computable, that it is an entropy, and that it divides the singular processes into those that can be made sound and those that cannot; and that on five open problems a typed crossing network with memory reaches what its libraries can reach at half the cost, and stops where the libraries stop, while construction mode writes down objects that no combination of the library reaches and has so far written down only known ones.