Lean sources
All 38 project-local modules, exactly as audited (each file’s SHA-256 is checked against the audit’s declaration index when the site is built). Raw files, with their phase directories, build scripts and pinned Lake metadata, are in lean/. See Build for the reproducible build.
Phase 1 (lean/)
| Module | Lines | Theorems | Summary (from the file header) |
|---|
| NimCore | 139 | 18 | Elementary algebra for the revised Nim paper. Authored locally by Codex. This file does not formalise AC0, the correlation theorem, or neural training. |
| NimRollout | 349 | 22 | Extension to NimCore.lean, written for the independent Claude review (9 October 2026). Lean 4.26.0, core/Std only. NimCore.lean is imported unchanged. Part A. Actual execution of the structured rollout policy pi_j. A legal policy move from … |
Phase 2 (lean/phase2/)
| Module | Lines | Theorems | Summary (from the file header) |
|---|
| NimGame | 634 | 47 | Phase 2, targets 1 and 2. Written by Claude for the independent review (9 October 2026). Lean 4.26.0, core/Std only. Imports the unchanged NimCore.lean and NimRollout.lean. Target 1 Normal-play semantics of Nim, the classical characterisati… |
| NimProbability | 1074 | 73 | Phase 2, target 3. Written by Claude for the independent review (9 October 2026). Lean 4.26.0, core/Std only (core `Rat`). Paper Appendix G(i) as a finite rational-probability theorem. Model: q = 2^B, N independent uniform B-bit heaps. The … |
Phase 3 (lean/phase3/)
| Module | Lines | Theorems | Summary (from the file header) |
|---|
| NimAttain | 673 | 34 | Phase 3, target A: attainability. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Imports the unchanged phase 1-2 files. For B ≥ 2 and any nonzero B-bit functional ell(sigma) = <w, sigma>, an explicit readout (cancel a gues… |
| Circuit | 1151 | 86 | Phase 3, target C: network-to-AC0 simulation. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Circuit model. `Circ` is a Boolean FORMULA (tree, no sharing) over input variables indexed by Nat, with constants, NOT, and unbou… |
| NimRecurrent | 555 | 38 | Phase 3, target B: the complete recurrent separator/state protocol. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Stream: each position P is serialised as its rows (one token per heap, in order, empty heaps included) foll… |
| BitBridge | 560 | 36 | Phase 3, target D (generic part). Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. * Bit vectors, big-endian heap encoding, and transfer of uniform sums from boards (N heaps < 2^B) to bit vectors of length B·N (heap-major). … |
| NimCorrBridge | 922 | 36 | Phase 3, target D (paper-specific part). Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Readouts given by circuits. For each observed bit b the readout is a family of formulas on the N·B input bits (heap-major, big-endian)… |
| AttainCircuit | 935 | 28 | Phase 3, targets A + D: an explicit circuit realisation of the attainability readout, and the resulting CONDITIONAL sharpness. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. For a nonzero guess t < 2^B with top bit k = log… |
Phase 4 (lean/phase4/)
| Module | Lines | Theorems | Summary (from the file header) |
|---|
| FiniteNet | 220 | 14 | Phase 4, Priority 1: finite-input network simulation. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Repair of the phase-3 specification gap found by the audit: `network_ac0` bounded the inputs of a clipped formula, while … |
| BinaryReadout | 333 | 14 | Phase 4, Priority 2a: binary-index readouts. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. The paper's readout outputs a move as (valid bit, binary heap index, binary new value). `BCirc` packages formulas for these bits; … |
| ParityCircuit | 259 | 13 | Phase 4, Priority 2c: the concrete parity reduction. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Replaces the phase-2 generic closure/hardness packaging by an explicit circuit composition. A binary move selector (BCirc,… |
| Controller | 401 | 17 | Phase 4, Priority 3: one explicit two-pass recurrent controller. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Tokens: row x | sep | reset. Modes: scan / replay. Registers: acc, prev, valid (summary part, as in phase 3), … |
| ControllerBits | 1148 | 81 | Phase 4, Priority 3 (bit level): per-update circuits for the two-pass controller and their refinement. Written by Claude (10 October 2026). Lean 4.26.0, core/Std. State layout (B value bits, r counter bits; little-endian bit k at offset + k… |
| SharedCircuit | 510 | 30 | Phase 4, Priority 2b: formula versus shared-circuit (DAG) conventions. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. All earlier circuit statements use FORMULAS (`AC0.Circ`, trees without sharing). The classical parity th… |
| SelectCircuit | 1064 | 53 | Phase 4, Priority 4: constructive selection circuits. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. * A GENERIC first-index move selector `genSel` (primary test with its new value, fallback "subtract 1 from the first nonz… |
| LocalRestore | 587 | 34 | Phase 4, Priority 4: LOCAL two-frame delta and restoration circuits, and the bounded-change difference lemma. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Input: two frames Q (wires below B·N) and Q' (wires B·N … 2B·N − … |
| Foundation | 450 | 24 | Phase 4, CLASSICAL FOUNDATION (separate, quantitative track). Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Target. `Bridge.ParityCorrPremise d s m ε` (every depth-d, size-s formula on m inputs has correlation at most ε w… |
| Coverage | 77 | 5 | Phase 4: composition of the phase-4 interfaces (coverage glue). Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. The negative (single-frame) results now accept the classical input in any of three forms, each PROVED here to i… |
Phase 5 (lean/phase5/)
| Module | Lines | Theorems | Summary (from the file header) |
|---|
| PriorityEncoder | 430 | 29 | Phase 5, task 1: an explicit, resource-bounded priority encoder from selection readouts (RCirc: valid flag, N candidate flags, B value bits) to the paper's binary move format (BCirc: valid flag, r big-endian index bits, B big-endian value b… |
| ThresholdNet | 780 | 54 | Phase 5, task 2: compiling bounded-depth Boolean formulas into the paper's fixed-scale literal-threshold networks (the existing AC0.Gate / Layer / evalNet model), in the direction opposite to Circuit.compileNet. Written by Claude (10 Octobe… |
| ThresholdInst | 475 | 33 | Phase 5, task 2 (instances): the threshold-network compiler applied to the recurrent controller's per-update circuits and to the binary selectors. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. * THRESHOLD UPDATE. One fixe… |
| WholeGame | 347 | 23 | Phase 5, task 3: whole-game strategies driven by the actual implementations. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. A. TWO-FRAME RESTORATION. The player stores its last established zero-nim-sum board Q. After any l… |
Phase 6 (lean/phase6/)
| Module | Lines | Theorems | Summary (from the file header) |
|---|
| Family | 574 | 54 | Phase 6, Priority 1a: family-level resource certificates. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. CONVENTIONS (stated once, used throughout phase 6). * A FAMILY is indexed by a type ι with an admissibility predicate… |
| Barrier | 496 | 30 | Phase 6, Priority 1b: the barrier side of the three bypasses. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. EXTERNAL INPUT. `ParityNotAC0` is the classical worst-case statement (Furst–Saxe– Sipser, Ajtai, Håstad): for eac… |
| RolloutExec | 896 | 50 | Phase 6, Priority 2: a finite-register rollout executor. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. The phase-5 loop `WholeGame.rollMoves` is an exact semantic specification, but it uses Nat fuel P.sum + 1 and reads th… |
| Bypass | 275 | 18 | Phase 6, Priority 1c: the paper's Proposition prop:bypass-interfaces, the barrier side, and the recurrent-history caveat. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Each bypass is stated as: (a) family certificates for… |
| Classical | 587 | 44 | Phase 6, Priority 3a: the classical external boundary and its paper-specific consequences. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. EXTERNAL INPUT (a theorem PARAMETER, never an axiom), as authorised by Søren Riis: H… |
| BoardStore | 824 | 44 | Phase 6, Priority 3b: the board-storage (one-pass) alternative of Section sec:recurrent-bypass, at bit level. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. REGISTERS (finite, B·N + B + r bits): the stored board (N heaps ×… |
| Windows | 261 | 16 | Phase 6, Priority 3c: the remaining parts of Theorem thm:sim-ac0 and two small local claims. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. * FIXED MULTI-STATE RECURRENCE WINDOWS (Definition def:RNN-formal): an update may … |
| Misc | 912 | 60 | Phase 6, Priority 3d: remaining paper-specific mathematical statements. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. A. Appendix app:weak (pairing strategy) and Definition def:mastery (weak mastery): on paired boards the… |
Phase 7 (lean/phase7/)
| Module | Lines | Theorems | Summary (from the file header) |
|---|
| NoiseModel | 1008 | 69 | Phase 7, Part B: the independent outcome-flip model of Remark rem:noisy-rollout-decay as a genuine finite probability law, and the two-sided order-a^{-2} repetition bound. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. PAR… |
| Shootout | 1491 | 100 | Phase 7, Part A: the outer shootout controller in bounded binary registers, composed with the actual rollout executor. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. ONE MACHINE, TWO SCHEDULES. The register vector holds * … |
Phase 8 (lean/phase8/)
| Module | Lines | Theorems | Summary (from the file header) |
|---|
| WeakMastery | 959 | 69 | Phase 8, part C: general weak mastery for Nim, its game semantics, and the checked instances. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Paper target: Definition def:mastery (weak mastery relative to an initial positio… |
| Fourier | 1379 | 117 | Phase 8, part B: Fourier analysis on the Boolean cube, tails, the parity spectrum, and the unknown-index delta. Written by Claude (10 October 2026). Lean 4.26.0, core/Std only. Paper target: Section sec:spectral-view (Walsh–Hadamard charact… |
| RealNoise | 483 | 46 | Phase 8, part A: the noise model at Mathlib's real numbers, an explicit integer sample count, the minimum sample count and its two-sided a^{-2} bounds, and the flip model. Written by Claude (10 October 2026). Lean 4.26.0 with Mathlib v4.26.… |
| RealFourier | 275 | 29 | Phase 8, part B at ℝ: the Fourier results of Fourier.lean instantiated at Mathlib's real numbers, with an explicit equivalence between the list cube `bitvecs n` and Mathlib's finite type Fin n → Bool (cube points and character indices), and… |