Section 10, paragraph 2What the Lean development covers, and its size (1,588 theorem and lemma declarations, 38 files)
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
The accompanying Lean development (Riis, 2026b) connects the mathematical results to explicit Boolean circuits, fixed-scale networks and complete game strategies. It checks the parity reduction, the finite probability bound and its attainability, move selection with binary outputs, the rollout executors and both shootout schedules, and the recurrent protocols with replay or board storage. The general weak-mastery definition, Fourier expansion and the real-parameter noise calculation are also formalised. An independent rebuild checks 1,588 theorem and lemma declarations across 38 local Lean files, comprising 24,493 source lines; these counts include auxiliary results and exclude Lean and Mathlib themselves.
Generated from paper_jmlr.tex, lines 1289–1289.
2 Explain this
This paragraph describes the Lean development: it connects the mathematics to explicit circuits, fixed-scale networks and complete game strategies, and checks the parity reduction, the probability bound and its attainability, binary move selection, rollout executors and both shootout schedules, and the recurrent protocols. The size figures (1,588 theorem and lemma declarations, 38 files, 24,493 source lines) include auxiliary lemmas and exclude Lean and Mathlib.
Caveat: these are counts of formal declarations, not of independent paper results.
3 How this is formalised
A description, not a formal claim. Its figures agree with the independent audit (38 modules; 1,588 theorem and lemma declarations; 24,493 source lines) and with the fresh rebuild for this edition, which produced exactly one axiom report for each of the 1,588 indexed theorems. See the coverage page and the build page.
| Paper anchor | sec:development-p2 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 10, paragraph 2 |
| Claim | What the Lean development covers, and its size (1,588 theorem and lemma declarations, 38 files) |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1289–1289; SHA-256 of the normalised block source 6c61a275b1dc1c78… |
| Explanations | explain/c-verification-extent, formal/c-verification-extent |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).