Proof coverage
Scope: what is and is not covered
This page records, claim by claim, how the paper's statements are supported. It is a map of evidence, not a certificate for the paper as a whole.
- What Lean checks. The Lean development states formal versions of the paper's definitions, theorems and constructions, and the Lean kernel checks every proof. A successful build establishes the formal statement. Whether that statement says the same thing as an English sentence is a separate question; each claim record answers it in plain language under How this is formalised and names any gap.
- Named classical inputs. The classical circuit lower bounds are not proved here. Håstad's negligible
parity-correlation theorem enters as an explicit hypothesis,
HastadNegl, of the theorems that need it; the worst-case statementParityNotAC0is derived from it. Results that use it are marked checked conditional theorem using named classical input. The Linial–Mansour–Nisan and Tal spectral bounds are cited only: the Fourier-tail hypothesisTailPremiseis used in a checked implication, but it has not been connected to a precise published statement with reconciled conventions. - What the counts mean. The counts further down include helper lemmas, adapters and auxiliary definitions; they measure the size of the development, not the number of results in the paper.
- What is not certified. Training runs, learning curves, checkpoint diagnostics and the cause of the plateau near 0.54 are empirical. They rest on saved run records and are marked empirical result. The experiments do not show that AlphaZero-style self-play discovers any of the constructions. Background literature and interpretive remarks are marked external cited result or informal interpretation.
- Bridges that are absent. The recurrent replay and board-storage strategies are proved to win in their own
stateful game semantics. A bridge from that semantics to the newer general history model of weak mastery
(
Mastery.Hist) has not been built; the audit lists it as optional. Until it exists, those guarantees hold in the controller's own semantics only. The website reports this rather than hiding it. - The full sequential bypasses are not AC0. Each bypass keeps individual updates shallow while adding
information or processing time. The complete multi-head and recurrent board-to-move maps are proved not to be
AC0 families (conditional on
ParityNotAC0); nothing here says that full parity computation is in AC0.
Coverage categories
Every mathematical, empirical or interpretive claim inventoried in the paper has one record and exactly one category. Statements that mix kinds are split into parts. Counts are of claim records, not of Lean declarations.
| Category | Meaning | Claims |
|---|---|---|
| Checked theorem | Lean checks a formal statement corresponding to this claim. | 53 |
| Checked definition or construction | Lean contains the definition or construction, with checked properties. | 19 |
| Checked conditional theorem using named classical input | Lean checks the implication from a named, unproved classical hypothesis. | 6 |
| External cited result | A published result used as background or input; not proved in Lean here. | 12 |
| Empirical result | Supported by saved experimental runs, not by a proof. | 20 |
| Informal interpretation | Motivation, interpretation or scope; not a formal claim. | 51 |
| Open or deferred item | Explicitly left open, deferred or not yet connected. | 4 |
| All claim records | 165 | |
78 records cite at least one Lean declaration; together they cite 215 distinct declarations as principal statements.
Lean's axiom basis
Every theorem in the development was checked by the Lean kernel in the fresh rebuild, and the build printed the
axioms each theorem depends on. Only Lean's three standard axioms occur (propositional extensionality, the axiom
of choice and quotient soundness). No sorry, custom axiom or unchecked code was found by the audit.
These axioms are the ordinary foundation of Lean and Mathlib; they are different from the named mathematical
hypotheses described above, which appear as explicit premises of the conditional theorems.
| Axioms used | Theorems |
|---|---|
| propext, Quot.sound | 765 |
| propext, Classical.choice, Quot.sound | 629 |
| propext | 149 |
| none | 45 |
Extent of the Lean development
Scope first: the counts below measure the whole local development, including helper lemmas, adapters and auxiliary definitions. They do not mean 1,588 independent paper results, and they exclude Lean, Std, Mathlib, logs and audit copies.
| Local Lean modules | 38 |
|---|---|
| Theorem and lemma declarations (audit count, helper lemmas included) | 1,588 |
| Definition declarations (audit count) | 632 |
| Source lines / nonblank lines | 24,493 / 21,813 |
Code lines (comments, strings and #print axioms removed) | 17,689 |
| Toolchain | Lean 4.26.0; Mathlib v4.26.0
(2df2f0150c275ad53cb3c90f7c98ec15a56a1a67), used only by RealNoise and RealFourier |
The site's own declaration export lists 1661 theorem constants: the 1,588 written theorem and lemma declarations plus 73 proof fields that Lean generates for structures with propositional fields. The audit convention counts only the written declarations.
All claim records
| Where | Claim | Category | Record |
|---|---|---|---|
| Abstract | |||
| Abstract | Summary of the results; each is stated and qualified in the body of the paper | Informal interpretation | record |
| Section 1 | |||
| Section 1, paragraph 2 | NIM rules, impartiality and why NIM is central | Informal interpretation | record |
| Section 1, paragraph 4 | Earlier experiments (Zhou and Riis) found AlphaZero-style learning deteriorating on larger NIM boards | External cited result | record |
| Section 1, paragraph 5 | AC0 circuits cannot compute global parity; the connection is made for an explicitly restricted model | External cited result | record |
| Section 1, paragraph 6 | AC0 representability is necessary within the restricted model, not sufficient for training and not universal | Informal interpretation | record |
| Section 1, paragraph 7 | History supplies computational context without changing optimal play | Informal interpretation | record |
| Section 1, paragraph 8 | Shallow components versus the complete sequential computation in the three bypasses | Informal interpretation | record |
| Figure 1 | Schematic of the barrier and the three bypasses | Informal interpretation | record |
| Section 1.1 | |||
| Section 1.1, list | List of contributions; each item points to a precise statement | Informal interpretation | record |
| Section 1.2 | |||
| Section 1.2, list | Scope: worst-case representational statements under explicit constraints, not training results | Informal interpretation | record |
| Section 2.1 | |||
| Section 2.1, paragraph 4 | The fixed grid Q_{W,D}; rewriting a negative term as a literal raises the threshold | Checked definition or construction | record · 3 Lean declarations |
| Definition 2.1 | Fixed-scale quantised NN, RNN and LTST models: constant depth, polynomial size, fixed grid, bounded unrolling | Checked definition or construction | record · 3 Lean declarations |
| Section 2.1, paragraph 6 | A one-step recurrence h_{r+1}=h_r⊕x_r accumulates parity over an arbitrarily long stream | Checked theorem | record · 2 Lean declarations |
| Section 2.1, “Why fixed-scale quantisation suggests an AC0 abstraction” | Fixed scale gives a witness of at most W literals, hence a constant-width DNF for each unit | Checked theorem | record · 2 Lean declarations |
| Section 2.1, paragraph 2 | The abstraction excludes scale-adaptive regimes, which move towards TC0 | Informal interpretation | record |
| Remark 2.2 (model scope) | The model has bounded thresholds; a fan-in-dependent threshold such as majority lies outside it | Checked definition or construction | record · 1 Lean declaration |
| Remark 2.2 (TC0) | Scale-adaptive threshold circuits (TC0) can represent parity-like computations | External cited result | record |
| Remark 2.3 (local XOR) | XOR of a constant number of bits or B-bit blocks is computable in AC0 | Checked theorem | record · 2 Lean declarations |
| Remark 2.3 (global parity) | Global parity of n = NB bits is not in AC0 | Checked conditional theorem using named classical input | record · 1 Lean declaration |
| Section 2.1, table | What the model captures and does not capture about deployed inference | Informal interpretation | record |
| Section 2.1, “Circuit complexity primer” | Circuit-complexity background: PARITY ∉ AC0, TC0 computes parity, fixed scale collapses to AC0 | External cited result | record |
| Section 2.2 | |||
| Theorem 2.4 | Fixed-depth, fixed-grid literal-threshold networks (and bounded-unrolling extensions) are simulated by AC0 circuit families | Checked theorem | record · 5 Lean declarations |
| Section 3 | |||
| Section 3, “Circuit complexity and neural networks” | Related results on parity, threshold circuits and attention models | External cited result | record |
| Section 3, “Quantised inference and deployment constraints” | The proof needs nonnegative literal weights, bounded thresholds and Boolean states, not just a quantisation format | Informal interpretation | record |
| Section 3, “Reinforcement learning in combinatorial games” | Prior work on RL difficulties in impartial games; the lower bound is about a restricted model | External cited result | record |
| Section 3, “History and memory in RL” | History can reduce computational complexity even in fully observable games, given the zero-nim-sum promise | Informal interpretation | record |
| Section 4.1 | |||
| Definition 4.1 | Finite terminating impartial games under normal play | External cited result | record |
| Section 4.1, paragraph 1 | A position with no legal moves is terminal | Checked definition or construction | record · 1 Lean declaration |
| Section 4.1, paragraph 2 | Encoding decisive endings using terminal positions and a forced last move | Informal interpretation | record |
| Section 4.2 | |||
| Definition 4.2 | NIM positions and legal moves | Checked definition or construction | record · 2 Lean declarations |
| Section 4.3 | |||
| Section 4.3, paragraph 1 | Sprague–Grundy theorem; for NIM the Grundy value is the XOR of the heaps | External cited result | record |
| Definition 4.3 | The nim-sum is the bitwise XOR of the heap sizes | Checked definition or construction | record · 2 Lean declarations |
| Theorem 4.4 | A NIM position is losing iff its nim-sum is zero; from a nonzero nim-sum there is a move to zero | Checked theorem | record · 4 Lean declarations |
| Section 4.3, “Why NIM is a useful barrier example” | NIM isolates the XOR aggregation obstruction; extensions to other games need explicit reductions | Informal interpretation | record |
| Section 5.1 | |||
| Definition 5.1 | Strong, weak and restoration mastery | Checked definition or construction | record · 6 Lean declarations |
| Section 5.1, paragraph 2 | Weak mastery = moving to a P-position at every decision history consistent with the agent's own play | Checked theorem | record · 3 Lean declarations |
| Section 5.2 | |||
| Theorem 5.2 (reduction) | Strong mastery on the boards (2,b₁,…,b_m) forces the winning move to reveal the parity of b | Checked theorem | record · 3 Lean declarations |
| Theorem 5.2 (barrier) | No polynomial-size, constant-depth fixed-scale network family strongly masters NIM | Checked conditional theorem using named classical input | record · 3 Lean declarations |
| Section 5.3 | |||
| Definition 5.3 | The nimber difference Δ(P,P') = nim(P) ⊕ nim(P') | Checked definition or construction | record · 1 Lean declaration |
| Section 5.3, paragraph 2 | If one heap changes from x_i to x_i', then Δ = x_i ⊕ x_i' | Checked theorem | record · 2 Lean declarations |
| Lemma 5.4 | With at most t changed heaps (t fixed), Δ is computed by polynomial-size constant-depth circuits | Checked theorem | record · 3 Lean declarations |
| Section 5.3, paragraph 3 | Explicit layer bounds, depth versus size, and remaining learning difficulties | Informal interpretation | record |
| Section 5.3.1 | |||
| Proposition 5.5 | Matching the opponent's nimber difference restores nim-sum zero | Checked theorem | record · 2 Lean declarations |
| Section 5.3.1, paragraph 2 | A restoration move can be selected from (Q,Q') by a constant-depth circuit | Checked theorem | record · 4 Lean declarations |
| Figure 2 | Worked example: (3,5,6) → (3,4,6) → (2,4,6) | Checked theorem | record · 1 Lean declaration |
| Section 5.3.1, paragraph 2 | Testing whether a candidate move realises δ is a local check on the heap being changed | Checked theorem | record · 2 Lean declarations |
| Section 5.3.1, paragraph 3 | The significance of two frames for learning is representational | Informal interpretation | record |
| Section 5.3.2 | |||
| Section 5.3.2, list | The two-frame components: encoding, changed-heap detection, Δ, and a move selector for a target δ | Checked definition or construction | record · 4 Lean declarations |
| Section 5.4 | |||
| Section 5.4, paragraph 1 | Restatement of the single-frame barrier as the motivation for rollouts | Informal interpretation | record |
| Definition 5.6 | Deterministic rollout policies and the rollout outcome bit | Checked definition or construction | record · 4 Lean declarations |
| Definition 5.7 | The restricted measurement interface: root and one-heap queries to one fixed structured head, bounded readout | Checked definition or construction | record · 4 Lean declarations |
| Section 5.4, paragraph 3 | With arbitrary start positions, one rollout of π₀ on the boards of k-th bits returns σ_k(P) | Checked theorem | record · 2 Lean declarations |
| Remark 5.8 | Each rollout follows one policy and yields one bit; different heads give independent linear functionals | Checked theorem | record · 3 Lean declarations |
| Section 5.4, “Finite-state shootout controller (FSM over policy heads)” | Early stopping after a nonzero outcome leaves the decision (the OR of all channel bits) unchanged | Checked theorem | record · 3 Lean declarations |
| Section 5.4, paragraph 2 | A finite-state shootout controller: states, head selection, transitions, halting states | Checked definition or construction | record · 3 Lean declarations |
| Section 5.4, paragraph 3 | The controller organises which head is queried and when to stop; it adds no per-step power | Informal interpretation | record |
| Section 5.4, paragraph 4 | The implemented outer controller: early-exit classifier and all-head schedule for move selection | Checked theorem | record · 6 Lean declarations |
| Figure 3 | The depicted controller decides whether σ(P) ≠ 0 using at most B queries | Checked theorem | record · 2 Lean declarations |
| Section 5.4, paragraph 5 | Channels versus protocol: heads supply measurement channels, the FSM sequential control | Informal interpretation | record |
| Section 5.4, “Depth amplification” | Iterating an AC0 policy for L game steps gives a depth-Θ(L) computation | Informal interpretation | record |
| Proposition 5.9 | B structured rollout heads recover all nim-sum bits; an AC0 readout then plays a winning move | Checked theorem | record · 7 Lean declarations |
| Proposition 5.10 | One fixed structured head reveals only known affine functions of one linear functional of σ(P) | Checked theorem | record · 3 Lean declarations |
| Remark 5.11 | Independent outcome flips: agreement (1+(1−2ε)^L)/2 and Θ(a⁻²) repetitions with fresh randomness | Checked theorem | record · 9 Lean declarations |
| Section 5.4, “The initialisation boundary for restoration” | Matching deltas preserves nim(Q); a completed matching-delta policy loses from the winning position (2) | Checked theorem | record · 3 Lean declarations |
| Figure 4 | Resource table for the three bypasses | Informal interpretation | record |
| Theorem 5.12 (i) | One structured head plus an AC0 readout wins with probability at most 2/(2^B−1)+negl(N) | Checked conditional theorem using named classical input | record · 5 Lean declarations |
| Theorem 5.12 (ii) | B structured heads and an AC0 readout select an optimal move with O(BN2^B) rollout steps | Checked theorem | record · 3 Lean declarations |
| Theorem 5.12 (iii) | From a known zero-nim-sum predecessor a two-frame AC0 selector restores zero and maintains it | Checked theorem | record · 3 Lean declarations |
| Section 5.5 | |||
| Section 5.5, “Serialising positions and retaining state” | Serialisation: rows of each position, a separator, aligned indices; the separator resets only the accumulator | Checked definition or construction | record · 4 Lean declarations |
| Proposition 5.13 | A constant-depth recurrent update computes the nim-sum after N row updates and reports consecutive differences | Checked theorem | record · 6 Lean declarations |
| Section 5.5, “From a summary to a move” | Replay protocol rows,SEP,rows,SEP: 2N+2 updates, 4+5B+3r state bits, a legal winning move | Checked theorem | record · 8 Lean declarations |
| Section 5.5, “From a summary to a move” | Board-storage variant: NB+B+r state bits, N+1 updates per decision, plus a reset | Checked theorem | record · 6 Lean declarations |
| Section 5.5, “Connecting recurrence to the history bypass” | Retained summaries give Δ of consecutive supplied boards; with decision-time boards only it spans two moves | Checked theorem | record · 4 Lean declarations |
| Section 5.5, “Why the lower bound is respected” | N sequential updates have depth O(N): outside Theorem 2.4; the complete recurrent map is not AC0 | Checked conditional theorem using named classical input | record · 2 Lean declarations |
| Section 5.6 | |||
| Proposition 5.14 | Each bypass: shallow {0,1}-weight components and a complete strategy winning against every legal opponent | Checked theorem | record · 5 Lean declarations |
| Proposition 5.14 (open item) | Bridge from the recurrent strategies' game semantics to the general weak-mastery history model | Open or deferred item | record |
| Section 5.6, paragraph 1 | The complete multi-head and recurrent board-to-move maps are not AC0 families | Checked conditional theorem using named classical input | record · 4 Lean declarations |
| Section 6.1 | |||
| Section 6.1, list | Practical takeaways: single-frame brittleness, three bypasses, optimisation still hard | Informal interpretation | record |
| Section 6.2 | |||
| Section 6.2, paragraph 1 | A noisy teacher plays optimally with probability 1−ε and otherwise uniformly at random | Informal interpretation | record |
| Section 6.3 | |||
| Section 6.3, paragraph 1 | Scale-adaptive threshold models (TC0) can represent parity | External cited result | record |
| Section 6.3, paragraph 2 | In the restricted regime gates collapse to AC0; AC0 approximates counting but has tiny parity correlation | External cited result | record |
| Section 6.4 | |||
| Section 6.4, paragraph 1 | Walsh–Hadamard characters are orthonormal; every f equals its Fourier expansion | Checked theorem | record · 5 Lean declarations |
| Definition 6.1 | The degree->k Fourier tail and (k,ε)-spectral band-limitation | Checked definition or construction | record · 3 Lean declarations |
| Equation (6.1) | Parity is a single character; a (k,ε)-band-limited f has squared correlation ≤ ε with χ_S for |S|>k | Checked theorem | record · 3 Lean declarations |
| Section 6.4, “AC0 has little high-frequency mass” | Linial–Mansour–Nisan and Tal: AC0 functions have little Fourier mass above low degree | External cited result | record |
| Section 6.4, “Local vs. global parity in NIM” | A nim-sum bit is a degree-N character; for a known changed heap a delta bit is a two-coordinate character | Checked theorem | record · 4 Lean declarations |
| Equation (6.2) | The total OR-of-XORs extension equals Δ's bit on single-change pairs; not a character for N≥2; degree two for N=1 | Checked theorem | record · 7 Lean declarations |
| Section 6.4, “Connection to optimisation (informal)” | Spectral bias suggests an analogy for parity learning; a hypothesis requiring separate measurements | Informal interpretation | record |
| Section 6.5 | |||
| Section 6.5, paragraph 1 | Global invariant hard from one frame; transition quantity local from two frames | Informal interpretation | record |
| Section 7 | |||
| Section 7, paragraph 1 | The experiments do not show that an AlphaZero-style learner discovers the bypasses by self-play | Informal interpretation | record |
| Section 7.1.1 | |||
| Section 7.1.1, paragraph 1 | Experimental state and action representation (binary heaps, set-heap actions, unmasked restoration argmax) | Empirical result | record |
| Section 7.1.2 | |||
| Table 1 | The policy-only MLP used in the experiments | Empirical result | record |
| Section 7.1.3 | |||
| Section 7.1.3, paragraph 1 | Soft-target cross-entropy to the uniform distribution over optimal restoration moves | Empirical result | record |
| Section 7.1.4 | |||
| Section 7.1.4, paragraph 1 | Evaluation by functional correctness on nonzero nim-sum positions and P/N classification | Empirical result | record |
| Section 7.2 | |||
| Section 7.2, paragraph 1 | After any move from a zero-nim-sum position, every optimal reply restores nim-sum zero | Checked theorem | record · 3 Lean declarations |
| Section 7.2.2 | |||
| Section 7.2.2, paragraph 1 | Teacher–random–teacher dataset of 10⁶ examples with soft optimal-move labels | Empirical result | record |
| Section 7.2.3 | |||
| Section 7.2.3, paragraph 1 | Training protocol and the ten saved checkpoints | Empirical result | record |
| Section 7.2.4 | |||
| Section 7.2.4, “Restoration accuracy (validation/test)” | Restoration accuracy: unmasked argmax in the optimal support; batch-mean convention | Empirical result | record |
| Section 7.2.5 | |||
| Section 7.2.5, “One-frame does not learn restoration; two-frame eventually does” | 1F stays near 0.075–0.081; 2F rises to 0.99998 test accuracy by epoch 178 (one saved run) | Empirical result | record |
| Figure 5 | Saved validation curve: 1F low; 2F plateau near 0.54, then near-perfect | Empirical result | record |
| Figure 6 | Saved test accuracy at the ten checkpoints | Empirical result | record |
| Section 7.2.5, “Learning in stages: the plateau and subsequent improvement” | The plateau and rise suggest a temporary learning bottleneck; its cause is not established | Empirical result | record |
| Section 7.2.5, paragraph 2 | Checkpoint diagnostic: almost all remaining errors differ from the required change only in the lowest bit | Empirical result | record |
| Section 7.2.5, paragraph 3 | Staged acquisition at the output level; no internal mechanism and no 8/15 explanation are established | Informal interpretation | record |
| Section 7.2.5, “Scope and provenance of the reported result” | Scope and provenance: one configuration, seed 0, run 20260214_120801_cd18fc9f | Empirical result | record |
| Section 7.3 | |||
| Section 7.3, “Setup” | FSM experiment setup: N=20, k=4, balanced test set of 2000 positions | Empirical result | record |
| Section 7.3, “Training the rollout heads” | Every tie-breaking rule gives the same rollout length, hence the same outcome bit | Checked theorem | record · 2 Lean declarations |
| Section 7.3, paragraph 2 | Imitation training of the four heads (seed 7, 12 epochs, 2×10⁵ examples) | Empirical result | record |
| Section 7.3, paragraph 2 | Per-head accuracy compares channel bits with the exact teacher; the FSM uses the OR of queried outcomes | Empirical result | record |
| Section 7.3, paragraph 2 | Multi-head FSM classifies all 2,000 test positions correctly, with imperfect per-head channel accuracy | Empirical result | record |
| Section 7.3, paragraph 3 (arithmetic) | For k=4, the r₀ classifier detects 8 of 15 nonzero nim-sums; balanced accuracy 23/30 | Checked theorem | record · 4 Lean declarations |
| Section 7.3, paragraph 3 (observed) | Observed single-head accuracy 0.768 and recall 0.536 on the finite test set | Empirical result | record |
| Section 7.3, paragraph 4 | Recall 8/15 and restoration accuracy measure different things | Informal interpretation | record |
| Section 7.3, paragraph 5 | Average 2.87 shootouts because positions with σ₀=1 stop at head 0; scope of the result | Empirical result | record |
| Table 2 | Saved FSM shootout results for model and teacher heads | Empirical result | record |
| Section 7.3, “Reproducibility status” | No public reproducibility package yet; a versioned package and repeated evaluation are future work | Open or deferred item | record |
| Section 8 | |||
| Section 8, paragraph 1 | The three bypasses supply different resources for a global invariant | Informal interpretation | record |
| Section 8.1 | |||
| Section 8.1, paragraph 1 | The experiments' networks differ from the theorem's gates; finite results do not settle asymptotic ones | Informal interpretation | record |
| Section 8.2 | |||
| Section 8.2, paragraph 1 | Local restrictions in Condorcet-domain search: a motivating analogy, not a reduction | Informal interpretation | record |
| Section 8.3 | |||
| Section 8.3, paragraph 1 | Some impartial games (Geography) have PSPACE-complete winner problems | External cited result | record |
| Section 8.3, paragraph 2 | NIM is a diagnostic starting point for harder self-play benchmarks | Informal interpretation | record |
| Section 8.3, list | Sprouts, Chomp and Grundy's game offer distinct proposed self-play challenges | Informal interpretation | record |
| Section 8.3, paragraph 3 | Evaluate unseen sizes and positions with explicit computation budgets and solver baselines | Informal interpretation | record |
| Section 8.4 | |||
| Section 8.4, paragraph 1 | Theorem 5.12(i) bounds one restricted interface, not general single-policy search | Informal interpretation | record |
| Section 8.5 | |||
| Section 8.5, paragraph 1 | Representability removes one obstacle; it does not determine whether training finds the computation | Informal interpretation | record |
| Section 8.5, paragraph 2 | Empirical evidence of a remaining learning bottleneck alongside the representational theorem | Informal interpretation | record |
| Section 8.5, paragraph 3 | Whether AlphaZero-style self-play discovers the constructions is open | Open or deferred item | record |
| Section 8.6 | |||
| Section 8.6, list | Broader implications for learning theory, architecture and practice | Informal interpretation | record |
| Section 9 | |||
| Section 9, paragraph 1 | Conclusion: AC0 simulation and the single-frame barrier, restated | Informal interpretation | record |
| Section 9, paragraph 2 | Conclusion: what the three constructions supply | Informal interpretation | record |
| Section 9, paragraph 3 | Conclusion: what the saved experiments do and do not show | Informal interpretation | record |
| Section 10 | |||
| Section 10, paragraph 1 | AI-assisted development and sole author responsibility | Informal interpretation | record |
| Section 10, paragraph 2 | What the Lean development covers, and its size (1,588 theorem and lemma declarations, 38 files) | Informal interpretation | record |
| Section 10, paragraph 3 | The verification boundary: external classical inputs, conditional results, empirical runs | Informal interpretation | record |
| Section 10, paragraph 3 (open item) | The Fourier-tail premise is not connected to a precise LMN/Tal statement with reconciled conventions | Open or deferred item | record |
| Section 10, paragraph 4 | Author review of the paper–Lean correspondence is distinct from manual inspection of every proof | Informal interpretation | record |
| Section 10, paragraph 6 | Neither the verification nor the experiments show that gradient descent or self-play discovers the constructions | Informal interpretation | record |
| Section A.1 | |||
| Section A.1 | Representable parameters: a fixed finite grid independent of n; negations allowed on wires | Checked definition or construction | record · 2 Lean declarations |
| Section A.2 | |||
| Definition A.1 | Literal-threshold network: layers of gates with grid weights, grid thresholds and negation bits | Checked definition or construction | record · 6 Lean declarations |
| Section A.3 | |||
| Definition A.2 | Bounded-unrolling recurrence: at most T updates in total from an input-independent initial state | Checked definition or construction | record · 3 Lean declarations |
| Section A.4 | |||
| Definition A.3 | Gate-realised attention-style model: every operation implemented in the permitted gates | Checked definition or construction | record · 1 Lean declaration |
| Remark A.4 | Theorem 2.4 applies because L, T, W, D are constants and parameters come from a finite grid | Informal interpretation | record |
| Section B.1 | |||
| Lemma B.1 | One fixed-scale threshold gate is a depth-2 DNF of size O(m^W) | Checked theorem | record · 3 Lean declarations |
| Remark B.2 | Negated inputs replace z_j by ¬z_j in each conjunction; the lemma still applies | Checked theorem | record · 2 Lean declarations |
| Section B.2 | |||
| Lemma B.3 | A layer of polynomially many fixed-scale units is simulated with constant depth and polynomial size | Checked theorem | record · 3 Lean declarations |
| Appendix C | |||
| Appendix C | Shared shallow operations: candidate tests, binary index, recurrent update, threshold realisation | Checked theorem | record · 4 Lean declarations |
| Section C, “From a game rule to a network” | Worked two-frame construction: explicit weights and operations, not a trained network | Informal interpretation | record |
| Figure 7 | Schematic restoration pipeline on (3,5,6) to (3,4,6) | Informal interpretation | record |
| Appendix C, “Local differences and candidate moves” | Delta bits by OR under the single-change promise; the shallow test y_i < x_i; the subtract-one fallback | Checked theorem | record · 5 Lean declarations |
| Appendix C, “A binary index is part of the circuit” | The priority encoder produces the binary index of the first candidate, for every flag pattern | Checked theorem | record · 6 Lean declarations |
| Appendix C, “The recurrent update” | Scan and replay updates are shallow; bit-level refinement and register bounds hold on well-formed streams | Checked theorem | record · 5 Lean declarations |
| Appendix C, “Realisation with fixed-scale threshold gates” | Compiler from formulas to {0,1}-weight threshold networks: ≤2d+2 layers, ≤(2d+1)S+K gates, widths ≤ S+n | Checked theorem | record · 3 Lean declarations |
| Figure 8 | Schematic Boolean-to-threshold compiler with fixed weights and thresholds | Informal interpretation | record |
| Appendix C, table | Certified depth and layer bounds for one evaluation of each component | Checked theorem | record · 10 Lean declarations |
| Section C, “Where the layer counts come from” | Origin and limitations of the 20-to-42 layer bound | Informal interpretation | record |
| Section C, “Outer-controller storage and time” | Shootout controller: NB+4+r+B state bits plus the read-only original board | Checked theorem | record · 4 Lean declarations |
| Appendix C, paragraph 2 | All-head schedule: M+2B+2 component evaluations, with M ≤ BN(2^B−1) | Checked theorem | record · 3 Lean declarations |
| Appendix D | |||
| Example 1 | Pairing strategy: a constant-depth mirror selector wins as second player on paired boards | Checked theorem | record · 5 Lean declarations |
| Appendix D, paragraph 1 | From (3), taking all stones weakly masters the position but is not strong mastery | Checked theorem | record · 3 Lean declarations |
| Appendix F | |||
| Appendix F, paragraph 1 | Symmetric channel with agreement (1+a)/2; m*(a) is the least sample count with both errors ≤ 1/4 | Checked definition or construction | record · 5 Lean declarations |
| Proposition F.1 | 3/(32a²) ≤ m*(a) ≤ ⌈4/a²⌉ ≤ 17/(4a²); majority with ties declared 0 attains the middle bound | Checked theorem | record · 5 Lean declarations |
| Appendix F, paragraph 2 | The flip model gives a=(1−2ε)^L; small bias eventually; ε=0 or L=0 exact; a=0 hopeless; reuse gives nothing | Checked theorem | record · 7 Lean declarations |
| Appendix G | |||
| Appendix G | Full proof of Proposition 5.9: rollout counts, outcome identities, selector, winning, step bound | Checked theorem | record · 6 Lean declarations |
| Appendix H | |||
| Appendix H | Full proof of Theorem 5.12: uniform σ, character expansion, finite bound, Håstad input, attainability | Checked conditional theorem using named classical input | record · 5 Lean declarations |
| Equation (H.1) | Under the stated correlation premise η_N: success ≤ 2/(q−1) + (q−1)η_N | Checked theorem | record · 1 Lean declaration |