\section*{Acknowledgements}
The paper builds on Claude Shannon's coding theorem, David Huffman's algorithm, the inequalities of Leon Kraft and Brockway McMillan, Alfr\'ed R\'enyi's entropies and L.~L. Campbell's coding theorem for them, the branching processes of Watson, Galton, Otter, Kesten and Stigum, and the Borel--Cantelli lemmas. The recent analyses of verifiers by Jia, Rakhlin and Xie, by Rohatgi and coauthors and by Balcan and coauthors, and Toby Ord's study of the dynamics of intelligence explosions, fixed the questions it answers. We thank the developers of Lean and Mathlib.

\section*{Data and code availability}
Everything the paper uses is in the repository \href{https://github.com/creelie/eBLLM}{\nolinkurl{github.com/creelie/eBLLM}}, the package of the engine Anaxia (command \texttt{anaxia}), released as version~\anaxiaVersion{} and archived at Zenodo under \anaxiaDOIlink{} \cite{Bha26c}. The folder \texttt{paper/bllm} holds the \LaTeX{} source, the figure programs with their data, the Lean~4 development of Appendix~\ref{app:checks}, and the Python, C, C\texttt{++} and shell programs of the numerical checks; the compiled paper is the file \texttt{preprintBLLM/BLLM.pdf} of the repository. The package contains the crossing network and its controls, the benchmark of Section~\ref{sec:benchmark} with its trees and the logs of every run, construction mode with the Steinberg gadgets of Section~\ref{ssec:steinberg}, the layer towers and the bench of Section~\ref{ssec:towerbench}, the per-round records of the Hodge round of Section~\ref{sec:hodgeround}, the exact and weighted-poset searches for Erd\H{o}s problem 1183 and the colourings of Theorem~\ref{thm:fvalues}, and the registry of Appendix~\ref{app:sources}. A container image of the engine is published as \texttt{ghcr.io/creelie/bllm-engine}; it contains no model weights. Earlier versions of the paper are in the folder \texttt{BLLM} of \href{https://github.com/creelie/D7}{\nolinkurl{github.com/creelie/D7}}. Deep Bhattacharjee carried out the computations and the Lean, C, C\texttt{++}, Python and shell verifications with the help of AI assistance (Claude, Anthropic). Both authors approved the final version.

\section*{Ethical declarations}
Funding: none. Competing interests: none.