Proposition 5.14Each bypass: shallow {0,1}-weight components and a complete strategy winning against every legal opponent

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

Proposition 5.14 (Shallow components and complete strategies) For $N\ge1$ heaps of $B\ge1$ bits, the following constructions use polynomial-size, constant-depth Boolean components, realisable by literal-threshold networks with weights and thresholds in $\{0,1\}$ .

(i) The two-frame selector maps a legal transition $Q\to Q'$ from $\operatorname{nim}(Q)=0$ to a legal binary-encoded response restoring zero. Retaining the response board as the next predecessor gives a winning strategy from this established invariant, with the opponent to move.
(ii) Each structured rollout policy and the readout from the board and its $B$ outcome bits are shallow. Executing the rollouts and then the readout gives a winning strategy from any nonzero nim-sum board, using at most $BN(2^B-1)$ simulated game moves per decision.
(iii) The recurrent state update is shallow. Iterating it over the replay protocol gives a winning strategy from any nonzero nim-sum board, with $O(B+\log N)$ memory and $2N+2$ updates per decision.

Here “winning strategy” quantifies over every legal opponent response. Polynomial size and constant depth refer to the indicated component, with depth independent of $N$ and $B$ ; they do not bound the number of sequential component evaluations.

Generated from paper_jmlr.tex, lines 879–888.

2 Explain this

What it says. For each bypass, the shallow pieces are genuinely shallow (polynomial size, constant depth, realisable with weights and thresholds in $\{0,1\}$ ), and running them as prescribed gives a strategy that wins against every legal opponent:

Two frames: the selector maps a legal transition from a zero-nim-sum board to a restoring reply; keeping the reply as the next predecessor wins from the established invariant.
Rollouts: each policy step and the final readout are shallow; executing the rollouts, then the readout, wins from any nonzero board with at most $BN(2^B-1)$ simulated moves per decision.
Recurrence: the state update is shallow; iterating it over the replay protocol wins from any nonzero board with $O(B+\log N)$ memory and $2N+2$ updates per decision.

The fine print. "Polynomial size and constant depth" refer to one component evaluation, with depth independent of $N$ and $B$ . They do not bound how many evaluations happen in sequence.

The three bypasses side by side

Schematic Boxes summarise resources or group operations; they are not gates, layers or measurements.

In the restricted model, no family of polynomial-size, fixed-depth networks that reads only the current board strongly masters NIM (Theorem 5.2, which uses the named classical input on parity). Each bypass adds a different resource: an extra frame and a promise, executed rollouts, or a growing number of recurrent updates. This schematic summarises Figure 4 and Proposition 5.14; each bypass column links to a worked, exact construction.

One frame, one evaluation
Input
the current board
Kept state
none
Sequential time per decision
1 evaluation
In the restricted model no such network family strongly masters NIM: it would give a shallow circuit for parity (using the named classical input on parity).
Theorem on single-frame inference
Two-frame restoration
Input
previous zero-nim-sum board and current board
Kept state
the restored board, kept as the next previous frame
Sequential time per decision
1 evaluation per decision
Shallow selector (Boolean depth ≤ 20). Maintains a winning position once established; does not find the first winning move.
worked restoration
Multi-head rollouts
Input
the current board (read-only); the controller runs the B rollouts itself
Kept state
working board, head index, outcome bits
Sequential time per decision
M + 2B + 2 evaluations, M ≤ BN(2^B − 1)
Each policy step, tick and the readout is shallow; the rollouts supply the nim-sum bits.
worked rollouts
Row-wise recurrence
Input
the board as a stream of rows, supplied twice (board storage: once)
Kept state
O(B + log N) bits: summary, counter, candidate (board storage: NB + B + r bits)
Sequential time per decision
2N + 2 updates (board storage: N + 1)
Each update is shallow (Boolean depth ≤ 8); the number of updates grows with N.
worked recurrence

All three routes use shallow (AC⁰) components. The complete rollout and recurrent board-to-move computations are not AC⁰ families, given the named classical input that parity is not in AC⁰: otherwise they would give shallow parity circuits. Their sequential time grows with the board; that growing computation is the resource the single-frame model lacks. The two-frame route instead changes the input and relies on a promise.

How this relates to the Lean proof. Bypass.prop_bypass_interfaces packages the three constructions with their shallow components and complete winning strategies; Bypass.bypass_barriers records why the complete rollout and recurrent maps cannot themselves be $\mathrm{AC}^0$ families, assuming the named classical input that parity is not in $\mathrm{AC}^0$ (Barrier.ParityNotAC0).

What this does not show. Nothing here claims that self-play training discovers these constructions, and the restricted model is not a model of every neural network.

Depicted in Lean: Bypass.prop_bypass_interfaces, Bypass.bypass_barriers. Explains the paper’s Figure 4.

Schematic: nothing on this panel is computed; the numbers are the bounds stated in the paper.

3 How this is formalised

Bypass.prop_bypass_interfaces states all three parts at once. For each bypass it gives an AC⁰ family certificate (Family.AC0Fam) and a $\{0,1\}$ -weight network family certificate (Family.NetFam) for the shallow components, with explicit depth and layer bounds, together with the complete strategy:

(i) two frames: formulas of depth at most 20, networks of at most 42 layers, and WholeGame.twoFrame_wins in the stateful predicate WholeGame.TwoFrameWins;
(ii) rollouts: policy step depth at most 17 (36 layers), register step depth at most 28 (58 layers), readout depth at most 19 (40 layers), and RolloutExec.mhExec_wins with the move bound;
(iii) recurrence: the controller update and the replay strategy, WholeGame.replay_wins; the board-storage variant is BoardStore.bits_store_wins.

Semantics used. The winning guarantees for (i) and (iii) are proved in their own stateful game predicates (TwoFrameWins, WholeGame.ReplayWins, BitStoreWins). The two-frame strategy is also connected to the general weak-mastery history model; the recurrent strategies are not (see the open item below).

Coverage record
Paper anchor	`prop:bypass-interfaces` (manuscript label)
Displayed as	Proposition 5.14
Claim	Each bypass: shallow {0,1}-weight components and a complete strategy winning against every legal opponent
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 879–888; SHA-256 of the normalised block source `42524208a19b28cf…`
Lean declarations	`NimAudit.Bypass.prop_bypass_interfaces` (Bypass, lines 88–111, file `d2e3ef2e7122…`) `NimAudit.WholeGame.twoFrame_wins` (WholeGame, lines 75–96, file `809a74ad589d…`) `NimAudit.RolloutExec.mhExec_wins` (RolloutExec, lines 517–520, file `c7b63a6e02d1…`) `NimAudit.WholeGame.replay_wins` (WholeGame, lines 282–302, file `809a74ad589d…`) `NimAudit.BoardStore.bits_store_wins` (BoardStore, lines 527–546, file `c35ac76d5db6…`)
Assumptions and domain	$N\ge1$ , $B\ge1$ ; for (i) the established zero-nim-sum invariant with the opponent to move; for (iii) the replay protocol supplied by the environment, with $N<2^r$ .
Prose-to-formal notes	Polynomial size and constant depth are certified for one evaluation of each component; they do not bound the number of sequential evaluations. The recurrent winning guarantees (part iii) are proved in their own stateful game semantics (`ReplayWins`, `BitStoreWins`), not in the general history model of Definition 5.1; see the open item on that bridge.
Depends on	Section 5.3.1, paragraph 2, Proposition 5.9, Section 5.5, “From a summary to a move”, Section 5.5, “From a summary to a move”, Appendix C, table
Audited correspondence rows	`prop:bypass-interfaces`
Explanations	`explain/prop:bypass-interfaces`, `formal/prop:bypass-interfaces`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Bypass.prop_bypass_interfaces`

Module Bypass (lean/phase6/Bypass.lean, lines 88–111) · file SHA-256 d2e3ef2e71220448… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

PROPOSITION prop:bypass-interfaces (all three parts): for each bypass the formula family AND the {0,1}-weight threshold-network family (W = 1) of its shallow components, and the complete strategy with its protocol and count bounds.

Statement as elaborated and printed by Lean 4.26.0

(NimAudit.Family.AC0Fam NimAudit.Family.restAdm NimAudit.Family.restLen
      (fun i => NimAudit.ThresholdInst.bForms (NimAudit.Family.restS i)) 20 ∧
    NimAudit.Family.NetFam NimAudit.Family.restAdm NimAudit.Family.restLen NimAudit.Family.restN 1
        42 ∧
      ∀ (B : ℕ) (Q : List ℕ),
        NimAudit.Game.Width B Q →
          NimAudit.nimSum Q = 0 →
            NimAudit.WholeGame.TwoFrameWins (NimAudit.WholeGame.restReply B) Q) ∧
  (NimAudit.Family.AC0Fam NimAudit.Family.polAdm NimAudit.Family.polLen
        (fun i => NimAudit.ThresholdInst.bForms (NimAudit.Family.polS i)) 17 ∧
      NimAudit.Family.NetFam NimAudit.Family.polAdm NimAudit.Family.polLen NimAudit.Family.polN 1
          36 ∧
        NimAudit.Family.AC0Fam NimAudit.Family.polAdm NimAudit.RolloutExec.stepLen
            NimAudit.RolloutExec.stepF 28 ∧
          NimAudit.Family.NetFam NimAudit.Family.polAdm NimAudit.RolloutExec.stepLen
              NimAudit.RolloutExec.stepN 1 58 ∧
            NimAudit.Family.AC0Fam NimAudit.Family.mhAdm NimAudit.Family.mhLen
                (fun i => NimAudit.ThresholdInst.bForms (NimAudit.Family.mhS i)) 19 ∧
              NimAudit.Family.NetFam NimAudit.Family.mhAdm NimAudit.Family.mhLen NimAudit.Family.mhN
                  1 40 ∧
                ∀ (B : ℕ) (P : List ℕ),
                  NimAudit.Game.Width B P →
                    NimAudit.nimSum P ≠ 0 →
                      NimAudit.Game.Wins (NimAudit.RolloutExec.mhExecSel B) P ∧
                        NimAudit.Game.totalRolloutMoves B P ≤ B * (P.length * (2 ^ B - 1)) ∧
                          (List.map (fun j => NimAudit.RolloutExec.polEvals B j P)
                                (List.range B)).sum =
                            NimAudit.Game.totalRolloutMoves B P + B) ∧
    NimAudit.Family.AC0Fam NimAudit.Family.ctrlAdm NimAudit.Family.ctrlLen NimAudit.Family.ctrlF 8 ∧
      NimAudit.Family.NetFam NimAudit.Family.ctrlAdm NimAudit.Family.ctrlLen NimAudit.Family.ctrlN 1
          18 ∧
        ∀ (B N : ℕ) (v : ℕ → Bool) (P : List ℕ),
          P.length = N →
            NimAudit.Game.Width B P →
              NimAudit.nimSum P ≠ 0 →
                (NimAudit.ThresholdInst.tstep B (NimAudit.WholeGame.rIdx N) v
                        NimAudit.Controller.Tok.reset).1 =
                    NimAudit.ControllerBits.sbits B (NimAudit.WholeGame.rIdx N)
                      NimAudit.Controller.cinit ∧
                  NimAudit.WholeGame.ReplayWins B (NimAudit.WholeGame.rIdx N)
                      NimAudit.Controller.cinit P ∧
                    (NimAudit.Controller.dtoks P).length = 2 * N + 2 ∧
                      NimAudit.ControllerBits.stateWidth B (NimAudit.WholeGame.rIdx N) =
                        7 + 5 * B + 3 * N.log2

Exact source text, lines 88–111

88/-- PROPOSITION prop:bypass-interfaces (all three parts): for each bypass the formula89    family AND the {0,1}-weight threshold-network family (W = 1) of its shallow components,90    and the complete strategy with its protocol and count bounds. -/91theorem prop_bypass_interfaces :92    (AC0Fam restAdm restLen (fun i => bForms (restS i)) 20 ∧ NetFam restAdm restLen restN 1 42 ∧93      ∀ (B : Nat) (Q : List Nat), Width B Q → nimSum Q = 0 → TwoFrameWins (restReply B) Q) ∧94    (AC0Fam polAdm polLen (fun i => bForms (polS i)) 17 ∧ NetFam polAdm polLen polN 1 36 ∧95      AC0Fam polAdm stepLen stepF 28 ∧ NetFam polAdm stepLen stepN 1 58 ∧96      AC0Fam mhAdm mhLen (fun i => bForms (mhS i)) 19 ∧ NetFam mhAdm mhLen mhN 1 40 ∧97      ∀ (B : Nat) (P : List Nat), Width B P → nimSum P ≠ 0 →98        Wins (mhExecSel B) P ∧ totalRolloutMoves B P ≤ B * (P.length * (2 ^ B - 1)) ∧99        ((List.range B).map (fun j => polEvals B j P)).sum = totalRolloutMoves B P + B) ∧100    (AC0Fam ctrlAdm ctrlLen ctrlF 8 ∧ NetFam ctrlAdm ctrlLen ctrlN 1 18 ∧101      ∀ (B N : Nat) (v : Nat → Bool) (P : List Nat), P.length = N → Width B P → nimSum P ≠ 0 →102        (tstep B (rIdx N) v Tok.reset).1 = sbits B (rIdx N) cinit ∧ ReplayWins B (rIdx N) cinit P ∧103        (dtoks P).length = 2 * N + 2 ∧ stateWidth B (rIdx N) = 7 + 5 * B + 3 * N.log2) := by104  obtain ⟨t1, t2, _, t4⟩ := bypass_twoFrame105  obtain ⟨m1, m2, m3, m4, m5, m6, m7⟩ := bypass_multiHead106  obtain ⟨r1, r2, _, r4, r5⟩ := bypass_recurrent107  refine ⟨⟨t1, t2, fun B Q hw h0 => (t4 B Q hw h0).1⟩, ⟨m1, m2, m3, m4, m5, m6, fun B P hw h0 => ?_⟩,108    ⟨r1, r2, fun B N v P hP hw h0 => ⟨(r4 B N v P hP hw h0).1, (r4 B N v P hP hw h0).2, (r5 B N P hP).1,109      (r5 B N P hP).2.2.1⟩⟩⟩110  obtain ⟨_, hwin, _, h4, h5, h6, _⟩ := m7 B P hw111  exact ⟨hwin h0, Nat.le_trans h5 h6, h4⟩

Project declarations in the statement: Controller.COut, Controller.Tok, Controller.Tok.reset, Controller.cinit, Controller.dtoks, ControllerBits.sbits, ControllerBits.stateWidth, Family.AC0Fam, Family.NetFam, Family.ctrlAdm, Family.ctrlF, Family.ctrlLen, Family.ctrlN, Family.mhAdm, Family.mhLen, Family.mhN, Family.mhS, Family.polAdm, Family.polLen, Family.polN, Family.polS, Family.restAdm, Family.restLen, Family.restN, Family.restS, Game.Width, Game.Wins, Game.totalRolloutMoves, RolloutExec.mhExecSel, RolloutExec.polEvals, RolloutExec.stepF, RolloutExec.stepLen, RolloutExec.stepN, ThresholdInst.bForms, ThresholdInst.tstep, WholeGame.ReplayWins, WholeGame.TwoFrameWins, WholeGame.rIdx, WholeGame.restReply, nimSum

Project declarations used by the proof or definition body

Bypass.bypass_multiHead, Bypass.bypass_recurrent, Bypass.bypass_twoFrame, Controller.COut, Controller.Tok, Controller.Tok.reset, Controller.cinit, Controller.decisionMove, Controller.dtoks, ControllerBits.bstep, ControllerBits.sbits, ControllerBits.stateWidth, Family.AC0Fam, Family.NetFam, Family.ctrlAdm, Family.ctrlF, Family.ctrlLen, Family.ctrlN, Family.mhAdm, Family.mhLen, Family.mhN, Family.mhS, Family.polAdm, Family.polLen, Family.polN, Family.polS, Family.restAdm, Family.restLen, Family.restN, Family.restS, Game.Lose, Game.Move, Game.Width, Game.Wins, Game.restore, Game.rolloutWinner, Game.totalRolloutMoves, LocalRestore.tf, Rollout.rolloutMoves, RolloutExec.clockBound, RolloutExec.mhExec, RolloutExec.mhExecSel, RolloutExec.outBit, RolloutExec.polEvals, RolloutExec.stepF, RolloutExec.stepLen, RolloutExec.stepN, ThresholdInst.bForms, ThresholdInst.inWidth, ThresholdInst.netBinSem, ThresholdInst.tstep, WholeGame.ReplayWins, WholeGame.TwoFrameWins, WholeGame.rIdx, WholeGame.restReply, nimSum

theorem `WholeGame.twoFrame_wins`

Module WholeGame (lean/phase5/WholeGame.lean, lines 75–96) · file SHA-256 809a74ad589db609… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

TWO-FRAME WHOLE-GAME THEOREM: from an established zero-nim-sum stored board (opponent to move), the network-driven two-frame player answers every legal opponent move legally, keeps the zero invariant, the board length and the bit width, and every play terminates with the player making the last move. Includes terminal and empty boards (no opponent move exists).

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ} (Q : List ℕ),
  NimAudit.Game.Width B Q →
    NimAudit.nimSum Q = 0 → NimAudit.WholeGame.TwoFrameWins (NimAudit.WholeGame.restReply B) Q

Exact source text, lines 75–96

75/-- TWO-FRAME WHOLE-GAME THEOREM: from an established zero-nim-sum stored board (opponent76    to move), the network-driven two-frame player answers every legal opponent move77    legally, keeps the zero invariant, the board length and the bit width, and every play78    terminates with the player making the last move.  Includes terminal and empty79    boards (no opponent move exists). -/80theorem twoFrame_wins {B : Nat} : ∀ (Q : List Nat), Width B Q → nimSum Q = 0 →81    TwoFrameWins (restReply B) Q := by82  intro Q83  induction Q using (measure List.sum).wf.induction with84  | h Q ih =>85    intro hw h086    refine TwoFrameWins.intro Q (fun Q' hm => ?_) (fun Q' R hm hR => ?_) (fun Q' R hm hR => ?_)87    · obtain ⟨R, h1, _⟩ := restReply_step hw h0 hm88      rw [h1]; rfl89    · obtain ⟨R', h1, _, h3, _⟩ := restReply_step hw h0 hm90      rw [h1] at hR; cases hR; exact h391    · obtain ⟨R', h1, _, h3, h4, _, h6⟩ := restReply_step hw h0 hm92      have hRR : R' = R := by rw [h1] at hR; exact Option.some.inj hR93      subst hRR94      refine ih R' ?_ h6 h495      have := move_sum_lt hm; have := move_sum_lt h396      show R'.sum < Q.sum; omega

Project declarations in the statement: Game.Width, WholeGame.TwoFrameWins, WholeGame.restReply, nimSum

Project declarations used by the proof or definition body

Game.Move, Game.Width, Game.move_sum_lt, Game.restore, WholeGame.TwoFrameWins, WholeGame.TwoFrameWins.intro, WholeGame.restReply, WholeGame.restReply_step, nimSum

theorem `RolloutExec.mhExec_wins`

Module RolloutExec (lean/phase6/RolloutExec.lean, lines 517–520) · file SHA-256 c7b63a6e02d1d425… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

WHOLE-GAME THEOREM FOR THE FULLY EXECUTED MULTI-HEAD PLAYER: from every nonzero board of width B it wins against every legal opponent; no outcome bit is supplied for free.

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ} {P : List ℕ},
  NimAudit.Game.Width B P →
    NimAudit.nimSum P ≠ 0 → NimAudit.Game.Wins (NimAudit.RolloutExec.mhExecSel B) P

Exact source text, lines 517–520

517/-- WHOLE-GAME THEOREM FOR THE FULLY EXECUTED MULTI-HEAD PLAYER: from every nonzero board518    of width B it wins against every legal opponent; no outcome bit is supplied for free. -/519theorem mhExec_wins {B : Nat} {P : List Nat} (hw : Width B P) (h : nimSum P ≠ 0) : Wins (mhExecSel B) P :=520  wins_congr (fun Q hQ => mhExecSel_eq hQ) hw (ctrl_wins P h)

Project declarations in the statement: Game.Width, Game.Wins, RolloutExec.mhExecSel, nimSum

Project declarations used by the proof or definition body

Controller.ctrlSel, Controller.ctrl_wins, Game.Width, RolloutExec.mhExecSel, RolloutExec.mhExecSel_eq, WholeGame.wins_congr, nimSum

theorem `WholeGame.replay_wins`

Module WholeGame (lean/phase5/WholeGame.lean, lines 282–302) · file SHA-256 809a74ad589db609… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

RECURRENT WHOLE-GAME THEOREM: with N < 2^r heaps of width B, from any idle controller state whose registers fit (the initial state, and every state reached after earlier decisions), the threshold controller driven by the replay protocol wins from every nonzero position against every legal opponent; the move applied is exactly the emitted one; all controller states over the whole interaction fit the registers.

Statement as elaborated and printed by Lean 4.26.0

∀ {B r N : ℕ},
  N < 2 ^ r →
    ∀ (P : List ℕ),
      P.length = N →
        NimAudit.Game.Width B P →
          NimAudit.nimSum P ≠ 0 →
            ∀ (s : NimAudit.Controller.CState),
              NimAudit.Controller.Idle s →
                NimAudit.Controller.Fits B N s → NimAudit.WholeGame.ReplayWins B r s P

Exact source text, lines 282–302

282/-- RECURRENT WHOLE-GAME THEOREM: with N < 2^r heaps of width B, from any idle controller283    state whose registers fit (the initial state, and every state reached after earlier284    decisions), the threshold controller driven by the replay protocol wins from every285    nonzero position against every legal opponent; the move applied is exactly the286    emitted one; all controller states over the whole interaction fit the registers. -/287theorem replay_wins {B r N : Nat} (hN : N < 2 ^ r) : ∀ (P : List Nat), P.length = N → Width B P →288    nimSum P ≠ 0 → ∀ s, Idle s → Fits B N s → ReplayWins B r s P := by289  intro P290  induction P using (measure List.sum).wf.induction with291  | h P ih =>292    intro hP hw h0 s hs hf293    obtain ⟨hdec, hfit⟩ := decide_spec hN hs hf hP hw294    obtain ⟨i, v, hd, hz⟩ := (decision_correct P).2.2 h0295    obtain ⟨x, _, _, hmv⟩ := (decision_correct P).2.1 i v hd296    refine ReplayWins.intro s P (P.set i v) hfit (by rw [hdec, hd]; rfl) hmv (by rw [hdec]) ?_297    intro P' hm'298    have hlt1 := move_sum_lt hmv299    have hlt2 := move_sum_lt hm'300    obtain ⟨hidle, hfit'⟩ := afterState_ok (N := N) hw301    exact ih P' (by show P'.sum < P.sum; omega) (by rw [move_length hm', move_length hmv, hP])302      (width_move (width_move hw hmv) hm') (move_from_zero hm' hz) _ hidle hfit'

Project declarations in the statement: Controller.CState, Controller.Fits, Controller.Idle, Game.Width, WholeGame.ReplayWins, nimSum

Project declarations used by the proof or definition body

Controller.CState, Controller.Fits, Controller.Idle, Controller.crunStates, Controller.decisionMove, Controller.decision_correct, Controller.dtoks, ControllerBits.FitsR, ControllerBits.sbits, Game.Move, Game.Terminal, Game.Width, Game.move_from_zero, Game.move_sum_lt, Game.width_move, SelectCircuit.applyM, WholeGame.ReplayWins, WholeGame.ReplayWins.intro, WholeGame.afterState, WholeGame.afterState_ok, WholeGame.decide, WholeGame.decide_spec, WholeGame.move_length, nimSum

theorem `BoardStore.bits_store_wins`

Module BoardStore (lean/phase6/BoardStore.lean, lines 527–546) · file SHA-256 c35ac76d5db6e833… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

BIT-LEVEL WHOLE-GAME THEOREM: with N < 2^r and N ≤ 2^r', from the encoding of any idle state storing a width-B board of N slots, the one-pass bit-level machine wins from every nonzero board of width B against every legal opponent.

Statement as elaborated and printed by Lean 4.26.0

∀ {B N r r' : ℕ},
  N < 2 ^ r →
    N ≤ 2 ^ r' →
      ∀ (P : List ℕ),
        P.length = N →
          NimAudit.Game.Width B P →
            NimAudit.nimSum P ≠ 0 →
              ∀ (b : List ℕ),
                b.length = N →
                  NimAudit.Game.Width B b →
                    NimAudit.BoardStore.BitStoreWins B N r r'
                      (NimAudit.BoardStore.bsBits B N r { board := b, acc := 0, idx := 0 }) P

Exact source text, lines 527–546

527/-- BIT-LEVEL WHOLE-GAME THEOREM: with N < 2^r and N ≤ 2^r', from the encoding of any idle528    state storing a width-B board of N slots, the one-pass bit-level machine wins from every529    nonzero board of width B against every legal opponent. -/530theorem bits_store_wins {B N r r' : Nat} (hN : N < 2 ^ r) (hr' : N ≤ 2 ^ r') :531    ∀ (P : List Nat), P.length = N → Width B P → nimSum P ≠ 0 →532    ∀ b, b.length = N → Width B b → BitStoreWins B N r r' (bsBits B N r ⟨b, 0, 0⟩) P := by533  intro P534  induction P using (measure List.sum).wf.induction with535  | h P ih =>536    intro hP hw h0 b hb hwb537    obtain ⟨h1, h2⟩ := bits_decision (r' := r') hN hr' b hb hwb P hP hw538    obtain ⟨i, v, hd, hz⟩ := (decision_correct P).2.2 h0539    obtain ⟨x, _, _, hmv⟩ := (decision_correct P).2.1 i v hd540    refine BitStoreWins.intro _ P (P.set i v) ?_ hmv h1 ?_541    · unfold bitMove; rw [h2]; simp [hd, applyM]542    · intro P' hm'543      have hlt1 := move_sum_lt hmv544      have hlt2 := move_sum_lt hm'545      exact ih P' (by show P'.sum < P.sum; omega) (by rw [move_length hm', move_length hmv, hP])546        (width_move (width_move hw hmv) hm') (move_from_zero hm' hz) P hP hw

Project declarations in the statement: BoardStore.BS.mk, BoardStore.BitStoreWins, BoardStore.bsBits, Game.Width, nimSum

Project declarations used by the proof or definition body

BoardStore.BOut, BoardStore.BOut.mk, BoardStore.BOut.move, BoardStore.BS.mk, BoardStore.BitStoreWins, BoardStore.BitStoreWins.intro, BoardStore.bitMove, BoardStore.bits_decision, BoardStore.bsBitRun, BoardStore.bsBits, BoardStore.bsDecode, BoardStore.btoks, BoardStore.inB, Controller.Tok, Controller.Tok.row, Controller.Tok.sep, Controller.decisionMove, Controller.decision_correct, Game.Move, Game.Terminal, Game.Width, Game.move_from_zero, Game.move_sum_lt, Game.width_move, SelectCircuit.applyM, WholeGame.move_length, nimSum

Definitions these statements use

inductive `Family.AC0Fam`

Module Family (lean/phase6/Family.lean, lines 126–134) · file SHA-256 7a647f0a667d5ede…

AC0 FAMILY CERTIFICATE (nonuniform, multi-output). For every admissible member: the input length is positive, every output formula has depth ≤ d and reads only the first len inputs, and the total size of the outputs is ≤ c·len^k with c, k independent of the member.

Statement as elaborated and printed by Lean 4.26.0

{ι : Type} → (ι → Prop) → (ι → ℕ) → (ι → List NimAudit.AC0.Circ) → ℕ → Prop

Exact source text, lines 126–134

126/-- AC0 FAMILY CERTIFICATE (nonuniform, multi-output).  For every admissible member:127    the input length is positive, every output formula has depth ≤ d and reads only128    the first len inputs, and the total size of the outputs is ≤ c·len^k with c, k129    independent of the member. -/130structure AC0Fam {ι : Type} (adm : ι → Prop) (len : ι → Nat) (outs : ι → List Circ) (d : Nat) : Prop where131  pos : ∀ i, adm i → 1 ≤ len i132  depth_le : ∀ i, adm i → ∀ c ∈ outs i, depth c ≤ d133  reads : ∀ i, adm i → ∀ c ∈ outs i, maxInput c ≤ len i134  size_poly : PolyIn adm len (fun i => tsize (outs i))

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, Family.PolyIn, Family.tsize

inductive `Family.NetFam`

Module Family (lean/phase6/Family.lean, lines 141–149) · file SHA-256 7a647f0a667d5ede…

NETWORK FAMILY CERTIFICATE: fixed grid W, at most L layers, valid gates, first layer reading only the len inputs, polynomial widths/fan-ins and polynomial gate count.

Statement as elaborated and printed by Lean 4.26.0

{ι : Type} → (ι → Prop) → (ι → ℕ) → (ι → List NimAudit.AC0.Layer) → ℕ → ℕ → Prop

Exact source text, lines 141–149

141/-- NETWORK FAMILY CERTIFICATE: fixed grid W, at most L layers, valid gates, first layer142    reading only the len inputs, polynomial widths/fan-ins and polynomial gate count. -/143structure NetFam {ι : Type} (adm : ι → Prop) (len : ι → Nat) (net : ι → List Layer) (W L : Nat) : Prop where144  pos : ∀ i, adm i → 1 ≤ len i145  valid : ∀ i, adm i → NetValid W (net i)146  wired : ∀ i, adm i → Wired (len i) (net i)147  layers : ∀ i, adm i → (net i).length ≤ L148  bounded : ∃ c k, ∀ i, adm i → NetBounded (c * len i ^ k) (net i)149  gates : PolyIn adm len (fun i => gateCount (net i))

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Layer, AC0.NetBounded, AC0.NetValid, Family.PolyIn, FiniteNet.Wired, ThresholdNet.gateCount

inductive `WholeGame.TwoFrameWins`

Module WholeGame (lean/phase5/WholeGame.lean, lines 41–50) · file SHA-256 809a74ad589db609…

Stateful two-frame game predicate (opponent to move at the stored board Q): every legal opponent move is answered by a legal reply, the reply's board becomes the new stored board, and play continues. Being inductive, every such play is finite; at a terminal stored board the opponent cannot move and loses.

Statement as elaborated and printed by Lean 4.26.0

(List ℕ → List ℕ → Option (List ℕ)) → List ℕ → Prop

Exact source text, lines 41–50

41/-- Stateful two-frame game predicate (opponent to move at the stored board Q): every42    legal opponent move is answered by a legal reply, the reply's board becomes the new43    stored board, and play continues.  Being inductive, every such play is finite; at a44    terminal stored board the opponent cannot move and loses. -/45inductive TwoFrameWins (reply : List Nat → List Nat → Option (List Nat)) : List Nat → Prop46  | intro (Q : List Nat) :47      (∀ Q', Move Q Q' → (reply Q Q').isSome = true) →48      (∀ Q' R, Move Q Q' → reply Q Q' = some R → Move Q' R) →49      (∀ Q' R, Move Q Q' → reply Q Q' = some R → TwoFrameWins reply R) →50      TwoFrameWins reply Q

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.Move

inductive `WholeGame.ReplayWins`

Module WholeGame (lean/phase5/WholeGame.lean, lines 266–276) · file SHA-256 809a74ad589db609…

Stateful interaction predicate (player to move at P; the controller holds the canonical encoding of the semantic state s). At each decision: every intermediate controller state fits the registers, the emitted move is applied to the board and is legal, the controller's new vector encodes `afterState P` (the stored summary feeds the next decision), and after every legal opponent reply the interaction continues.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Controller.CState → List ℕ → Prop

Exact source text, lines 266–276

266/-- Stateful interaction predicate (player to move at P; the controller holds the267    canonical encoding of the semantic state s).  At each decision: every intermediate268    controller state fits the registers, the emitted move is applied to the board and is269    legal, the controller's new vector encodes `afterState P` (the stored summary feeds270    the next decision), and after every legal opponent reply the interaction continues. -/271inductive ReplayWins (B r : Nat) : CState → List Nat → Prop272  | intro (s : CState) (P R : List Nat) :273      (∀ st ∈ crunStates s (dtoks P), FitsR B r st) →274      applyM P (decide B r (sbits B r s) P).2 = some R → Move P R →275      (decide B r (sbits B r s) P).1 = sbits B r (afterState P) →276      (∀ P', Move R P' → ReplayWins B r (afterState P) P') → ReplayWins B r s P

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState, Controller.crunStates, Controller.dtoks, ControllerBits.FitsR, ControllerBits.sbits, Game.Move, SelectCircuit.applyM, WholeGame.afterState, WholeGame.decide

inductive `Controller.COut`

Module Controller (lean/phase4/Controller.lean, lines 44–46) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 44–46

44inductive COut where45  | summary (s : Nat) (diff : Option Nat)46  | move (m : Option (Nat × Nat))

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `Controller.Tok`

Module Controller (lean/phase4/Controller.lean, lines 29–32) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 29–32

29inductive Tok where30  | row (x : Nat)31  | sep32  | reset

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Controller.cinit`

Module Controller (lean/phase4/Controller.lean, lines 48–48) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Controller.CState

Exact source text, lines 48–48

48def cinit : CState := ⟨false, 0, 0, false, 0, 0, none, none⟩

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState.mk

def `Controller.dtoks`

Module Controller (lean/phase4/Controller.lean, lines 75–76) · file SHA-256 63d0e09c002db91e…

The tokens of one decision: scan, separator, replay, separator.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → List NimAudit.Controller.Tok

Exact source text, lines 75–76

75/-- The tokens of one decision: scan, separator, replay, separator. -/76def dtoks (P : List Nat) : List Tok := P.map Tok.row ++ [Tok.sep] ++ P.map Tok.row ++ [Tok.sep]

Project declarations in the statement: Controller.Tok

Project declarations used by the proof or definition body

Controller.Tok, Controller.Tok.row, Controller.Tok.sep

def `ControllerBits.sbits`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 104–108) · file SHA-256 4e23680da471fd69…

The canonical state vector (4 + 5B + 3r bits; false beyond).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Controller.CState → ℕ → Bool

Exact source text, lines 104–108

104/-- The canonical state vector (4 + 5B + 3r bits; false beyond). -/105def sbits (B r : Nat) (s : CState) : Nat → Bool :=106  layout B r false s.replayMode s.acc.testBit s.prev.testBit s.valid s.sig.testBit s.idx.testBit107    s.sel.isSome (optI s.sel).testBit (optV s.sel).testBit s.fnz.isSome (optI s.fnz).testBit108    (optV s.fnz).testBit

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState, Controller.CState.acc, Controller.CState.fnz, Controller.CState.idx, Controller.CState.prev, Controller.CState.replayMode, Controller.CState.sel, Controller.CState.sig, Controller.CState.valid, ControllerBits.layout, ControllerBits.optI, ControllerBits.optV

def `ControllerBits.stateWidth`

Module ControllerBits (lean/phase4/ControllerBits.lean, lines 788–789) · file SHA-256 4e23680da471fd69…

Number of state wires.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ

Exact source text, lines 788–789

788/-- Number of state wires. -/789def stateWidth (B r : Nat) : Nat := 4 + 5 * B + 3 * r

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.ctrlAdm`

Module Family (lean/phase6/Family.lean, lines 445–445) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → Prop

Exact source text, lines 445–445

445def ctrlAdm : Nat × Nat → Prop := restAdm

Project declarations in the statement: none

Project declarations used by the proof or definition body

Family.restAdm

def `Family.ctrlF`

Module Family (lean/phase6/Family.lean, lines 448–448) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Circ

Exact source text, lines 448–448

448def ctrlF (i : Nat × Nat) : List Circ := ctrlForms i.1 (rIdx i.2)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

ThresholdInst.ctrlForms, WholeGame.rIdx

def `Family.ctrlLen`

Module Family (lean/phase6/Family.lean, lines 446–447) · file SHA-256 7a647f0a667d5ede…

Per-update input: state (4 + 5B + 3r bits) plus one token (2 + B bits), r = log₂N + 1.

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ

Exact source text, lines 446–447

446/-- Per-update input: state (4 + 5B + 3r bits) plus one token (2 + B bits), r = log₂N + 1. -/447def ctrlLen : Nat × Nat → Nat := fun i => inWidth i.1 (rIdx i.2)

Project declarations in the statement: none

Project declarations used by the proof or definition body

ThresholdInst.inWidth, WholeGame.rIdx

def `Family.ctrlN`

Module Family (lean/phase6/Family.lean, lines 481–481) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 481–481

481def ctrlN (i : Nat × Nat) : List Layer := ctrlNet i.1 (rIdx i.2)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

ThresholdInst.ctrlNet, WholeGame.rIdx

def `Family.mhAdm`

Module Family (lean/phase6/Family.lean, lines 390–391) · file SHA-256 7a647f0a667d5ede…

Readout members (board plus B outcome wires).

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → Prop

Exact source text, lines 390–391

390/-- Readout members (board plus B outcome wires). -/391def mhAdm : Nat × Nat → Prop := restAdm

Project declarations in the statement: none

Project declarations used by the proof or definition body

Family.restAdm

def `Family.mhLen`

Module Family (lean/phase6/Family.lean, lines 392–392) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ

Exact source text, lines 392–392

392def mhLen : Nat × Nat → Nat := fun i => i.1 * i.2 + i.1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.mhN`

Module Family (lean/phase6/Family.lean, lines 422–422) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 422–422

422def mhN (i : Nat × Nat) : List Layer := mhNet i.1 i.2 (rIdx i.2)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

ThresholdInst.mhNet, WholeGame.rIdx

def `Family.mhS`

Module Family (lean/phase6/Family.lean, lines 393–393) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → NimAudit.BinReadout.BCirc

Exact source text, lines 393–393

393def mhS (i : Nat × Nat) : BCirc := mhBin i.1 i.2 (rIdx i.2)

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

PriorityEncoder.mhBin, WholeGame.rIdx

def `Family.polAdm`

Module Family (lean/phase6/Family.lean, lines 344–345) · file SHA-256 7a647f0a667d5ede…

Policy members are indexed by (B, (N, j)).

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → Prop

Exact source text, lines 344–345

344/-- Policy members are indexed by (B, (N, j)). -/345def polAdm : Nat × (Nat × Nat) → Prop := fun i => 1 ≤ i.1 ∧ 1 ≤ i.2.1 ∧ i.2.2 < i.1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.polLen`

Module Family (lean/phase6/Family.lean, lines 346–346) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → ℕ

Exact source text, lines 346–346

346def polLen : Nat × (Nat × Nat) → Nat := fun i => i.1 * i.2.1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.polN`

Module Family (lean/phase6/Family.lean, lines 376–376) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 376–376

376def polN (i : Nat × (Nat × Nat)) : List Layer := polNet i.1 i.2.1 i.2.2 (rIdx i.2.1)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

ThresholdInst.polNet, WholeGame.rIdx

def `Family.polS`

Module Family (lean/phase6/Family.lean, lines 347–347) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → NimAudit.BinReadout.BCirc

Exact source text, lines 347–347

347def polS (i : Nat × (Nat × Nat)) : BCirc := polBin i.1 i.2.1 i.2.2 (rIdx i.2.1)

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

PriorityEncoder.polBin, WholeGame.rIdx

def `Family.restAdm`

Module Family (lean/phase6/Family.lean, lines 282–282) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → Prop

Exact source text, lines 282–282

282def restAdm : Nat × Nat → Prop := fun i => 1 ≤ i.1 ∧ 1 ≤ i.2

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.restLen`

Module Family (lean/phase6/Family.lean, lines 283–284) · file SHA-256 7a647f0a667d5ede…

Supplied input: the two frames, 2·B·N bits.

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → ℕ

Exact source text, lines 283–284

283/-- Supplied input: the two frames, 2·B·N bits. -/284def restLen : Nat × Nat → Nat := fun i => 2 * (i.1 * i.2)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Family.restN`

Module Family (lean/phase6/Family.lean, lines 318–318) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 318–318

318def restN (i : Nat × Nat) : List Layer := restNet i.1 i.2 (rIdx i.2)

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

ThresholdInst.restNet, WholeGame.rIdx

def `Family.restS`

Module Family (lean/phase6/Family.lean, lines 285–285) · file SHA-256 7a647f0a667d5ede…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ → NimAudit.BinReadout.BCirc

Exact source text, lines 285–285

285def restS (i : Nat × Nat) : BCirc := restBin i.1 i.2 (rIdx i.2)

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

PriorityEncoder.restBin, WholeGame.rIdx

def `Game.Width`

Module NimGame (lean/phase2/NimGame.lean, lines 31–32) · file SHA-256 23df6bb87ecfd344…

B-bit board: every heap is below 2^B.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Prop

Exact source text, lines 31–32

31/-- B-bit board: every heap is below 2^B. -/32def Width (B : Nat) (p : List Nat) : Prop := ∀ x ∈ p, x < 2 ^ B

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `Game.Wins`

Module NimGame (lean/phase2/NimGame.lean, lines 125–132) · file SHA-256 23df6bb87ecfd344…

`Wins sel p`: the player to move at `p`, always playing the successor chosen by `sel`, wins against EVERY legal opponent. The selected move is legal, and after every legal opponent reply the player is again in a `Wins` position. Because the predicate is inductive, every such play is finite and ends with the opponent facing a terminal board (normal play: the opponent loses).

Statement as elaborated and printed by Lean 4.26.0

(List ℕ → Option (List ℕ)) → List ℕ → Prop

Exact source text, lines 125–132

125/-- `Wins sel p`: the player to move at `p`, always playing the successor chosen by126    `sel`, wins against EVERY legal opponent.  The selected move is legal, and after127    every legal opponent reply the player is again in a `Wins` position.  Because128    the predicate is inductive, every such play is finite and ends with the129    opponent facing a terminal board (normal play: the opponent loses). -/130inductive Wins (sel : List Nat → Option (List Nat)) : List Nat → Prop131  | intro (p q : List Nat) : sel p = some q → Move p q →132      (∀ r, Move q r → Wins sel r) → Wins sel p

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.Move

def `Game.totalRolloutMoves`

Module NimGame (lean/phase2/NimGame.lean, lines 450–452) · file SHA-256 23df6bb87ecfd344…

Total simulated moves of the B root rollouts.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → ℕ

Exact source text, lines 450–452

450/-- Total simulated moves of the B root rollouts. -/451def totalRolloutMoves (B : Nat) (p : List Nat) : Nat :=452  ((List.range B).map (fun j => rolloutMoves j p)).sum

Project declarations in the statement: none

Project declarations used by the proof or definition body

Rollout.rolloutMoves

def `RolloutExec.mhExecSel`

Module RolloutExec (lean/phase6/RolloutExec.lean, lines 501–501) · file SHA-256 c7b63a6e02d1d425…

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Option (List ℕ)

Exact source text, lines 501–501

501def mhExecSel (B : Nat) (P : List Nat) : Option (List Nat) := applyM P (mhExec B P)

Project declarations in the statement: none

Project declarations used by the proof or definition body

RolloutExec.mhExec, SelectCircuit.applyM

def `RolloutExec.polEvals`

Module RolloutExec (lean/phase6/RolloutExec.lean, lines 492–493) · file SHA-256 c7b63a6e02d1d425…

Policy-network evaluations used by rollout j (clocked steps of the executor).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → List ℕ → ℕ

Exact source text, lines 492–493

492/-- Policy-network evaluations used by rollout j (clocked steps of the executor). -/493def polEvals (B j : Nat) (P : List Nat) : Nat := (execRollN B j (fun _ => false) P).2

Project declarations in the statement: none

Project declarations used by the proof or definition body

RolloutExec.execRollN

def `RolloutExec.stepF`

Module RolloutExec (lean/phase6/RolloutExec.lean, lines 700–700) · file SHA-256 c7b63a6e02d1d425…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → List NimAudit.AC0.Circ

Exact source text, lines 700–700

700def stepF (i : Nat × (Nat × Nat)) : List Circ := stepForms i.1 i.2.1 (polS i)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

Family.polS, RolloutExec.stepForms

def `RolloutExec.stepLen`

Module RolloutExec (lean/phase6/RolloutExec.lean, lines 698–699) · file SHA-256 c7b63a6e02d1d425…

Step-circuit members: index (B, (N, j)), input = registers + reset + external board.

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → ℕ

Exact source text, lines 698–699

698/-- Step-circuit members: index (B, (N, j)), input = registers + reset + external board. -/699def stepLen : Nat × (Nat × Nat) → Nat := fun i => 2 * (i.1 * i.2.1) + 3

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `RolloutExec.stepN`

Module RolloutExec (lean/phase6/RolloutExec.lean, lines 724–724) · file SHA-256 c7b63a6e02d1d425…

Statement as elaborated and printed by Lean 4.26.0

ℕ × ℕ × ℕ → List NimAudit.AC0.Layer

Exact source text, lines 724–724

724def stepN (i : Nat × (Nat × Nat)) : List Layer := stepNet i.1 i.2.1 i.2.2

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

RolloutExec.stepNet

def `ThresholdInst.bForms`

Module ThresholdInst (lean/phase5/ThresholdInst.lean, lines 317–318) · file SHA-256 c8c66599c8e24804…

Output order: wire 0 valid, wires 1..r index bits, wires r+1..r+B value bits.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → List NimAudit.AC0.Circ

Exact source text, lines 317–318

317/-- Output order: wire 0 valid, wires 1..r index bits, wires r+1..r+B value bits. -/318def bForms (S : BCirc) : List Circ := S.valid :: (S.idx ++ S.val)

Project declarations in the statement: AC0.Circ, BinReadout.BCirc

Project declarations used by the proof or definition body

AC0.Circ, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid

def `ThresholdInst.tstep`

Module ThresholdInst (lean/phase5/ThresholdInst.lean, lines 128–131) · file SHA-256 c8c66599c8e24804…

One update of the threshold-network controller.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → (ℕ → Bool) → NimAudit.Controller.Tok → (ℕ → Bool) × Option NimAudit.Controller.COut

Exact source text, lines 128–131

128/-- One update of the threshold-network controller. -/129def tstep (B r : Nat) (v : Nat → Bool) (t : Tok) : (Nat → Bool) × Option COut :=130  ((fun j => if j < stateWidth B r then evalNet (ctrlNet B r) (inp B r v t) j else false),131   outDecode B r (fun k => evalNet (ctrlNet B r) (inp B r v t) (stateWidth B r + k)))

Project declarations in the statement: Controller.COut, Controller.Tok

Project declarations used by the proof or definition body

AC0.evalNet, Controller.COut, Controller.Tok, ControllerBits.inp, ControllerBits.stateWidth, ThresholdInst.ctrlNet, ThresholdInst.outDecode

def `WholeGame.rIdx`

Module WholeGame (lean/phase5/WholeGame.lean, lines 108–109) · file SHA-256 809a74ad589db609…

Index width used for N heaps.

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ

Exact source text, lines 108–109

108/-- Index width used for N heaps. -/109def rIdx (N : Nat) : Nat := N.log2 + 1

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `WholeGame.restReply`

Module WholeGame (lean/phase5/WholeGame.lean, lines 35–39) · file SHA-256 809a74ad589db609…

The player's reply: evaluate the compiled restoration network on (Q, Q'), decode its output wires and apply the decoded move to Q'. Index width r = log₂N + 1.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → List ℕ → Option (List ℕ)

Exact source text, lines 35–39

35/-- The player's reply: evaluate the compiled restoration network on (Q, Q'), decode its36    output wires and apply the decoded move to Q'.  Index width r = log₂N + 1. -/37def restReply (B : Nat) (Q Q' : List Nat) : Option (List Nat) :=38  applyM Q' (netBinSem (restNet B Q'.length (Q'.length.log2 + 1)) Q'.length (Q'.length.log2 + 1) B39    (LocalRestore.tf B Q'.length Q Q'))

Project declarations in the statement: none

Project declarations used by the proof or definition body

LocalRestore.tf, SelectCircuit.applyM, ThresholdInst.netBinSem, ThresholdInst.restNet

def `nimSum`

Module NimCore (lean/NimCore.lean, lines 7–9) · file SHA-256 b07db6c505210d5a…

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ

Exact source text, lines 7–9

7def nimSum : List Nat → Nat8  | [] => 09  | h :: t => h ^^^ nimSum t

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `Controller.CState`

Module Controller (lean/phase4/Controller.lean, lines 34–42) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 34–42

34structure CState where35  replayMode : Bool36  acc : Nat37  prev : Nat38  valid : Bool39  sig : Nat40  idx : Nat41  sel : Option (Nat × Nat)42  fnz : Option (Nat × Nat)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Controller.Fits`

Module Controller (lean/phase4/Controller.lean, lines 237–241) · file SHA-256 63d0e09c002db91e…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → NimAudit.Controller.CState → Prop

Exact source text, lines 237–241

237/-- Register bounds for N heaps of B bits and an r-bit counter (N < 2^r). -/238def Fits (B N : Nat) (s : CState) : Prop :=239  s.acc < 2 ^ B ∧ s.prev < 2 ^ B ∧ s.sig < 2 ^ B ∧ s.idx ≤ N ∧240  (∀ i v, s.sel = some (i, v) → i < N ∧ v < 2 ^ B) ∧241  (∀ i v, s.fnz = some (i, v) → i < N ∧ v < 2 ^ B)

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState, Controller.CState.acc, Controller.CState.fnz, Controller.CState.idx, Controller.CState.prev, Controller.CState.sel, Controller.CState.sig

def `Controller.Idle`

Module Controller (lean/phase4/Controller.lean, lines 83–84) · file SHA-256 63d0e09c002db91e…

Idle: scan mode with empty accumulator and cleared replay registers.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Controller.CState → Prop

Exact source text, lines 83–84

83/-- Idle: scan mode with empty accumulator and cleared replay registers. -/84def Idle (s : CState) : Prop := s.replayMode = false ∧ s.acc = 0 ∧ s.idx = 0 ∧ s.sel = none ∧ s.fnz = none

Project declarations in the statement: Controller.CState

Project declarations used by the proof or definition body

Controller.CState, Controller.CState.acc, Controller.CState.fnz, Controller.CState.idx, Controller.CState.replayMode, Controller.CState.sel

inductive `BoardStore.BitStoreWins`

Module BoardStore (lean/phase6/BoardStore.lean, lines 515–520) · file SHA-256 c35ac76d5db6e833…

Stateful interaction driven by the BIT-LEVEL machine (register vector v).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → ℕ → (ℕ → Bool) → List ℕ → Prop

Exact source text, lines 515–520

515/-- Stateful interaction driven by the BIT-LEVEL machine (register vector v). -/516inductive BitStoreWins (B N r r' : Nat) : (Nat → Bool) → List Nat → Prop517  | intro (v : Nat → Bool) (P R : List Nat) :518      applyM P (bitMove B N r r' v P) = some R → Move P R →519      bsBitRun B N r v (btoks P) = bsBits B N r ⟨P, 0, 0⟩ →520      (∀ P', Move R P' → BitStoreWins B N r r' (bsBits B N r ⟨P, 0, 0⟩) P') → BitStoreWins B N r r' v P

Project declarations in the statement: none

Project declarations used by the proof or definition body

BoardStore.BS.mk, BoardStore.bitMove, BoardStore.bsBitRun, BoardStore.bsBits, BoardStore.btoks, Game.Move, SelectCircuit.applyM

def `BoardStore.bsBits`

Module BoardStore (lean/phase6/BoardStore.lean, lines 154–157) · file SHA-256 c35ac76d5db6e833…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → ℕ → NimAudit.BoardStore.BS → ℕ → Bool

Exact source text, lines 154–157

154def bsBits (B N r : Nat) (s : BS) : Nat → Bool := fun w =>155  if w < B * N then boardBits B s.board w156  else if w < B * N + B then s.acc.testBit (w - B * N)157  else if w < sw B N r then s.idx.testBit (w - (B * N + B)) else false

Project declarations in the statement: BoardStore.BS

Project declarations used by the proof or definition body

BoardStore.BS, BoardStore.BS.acc, BoardStore.BS.board, BoardStore.BS.idx, BoardStore.sw, CorrBridge.boardBits

Full modules

Module	File	Lines	Imports
BoardStore	`lean/phase6/BoardStore.lean`	824	Bypass
Bypass	`lean/phase6/Bypass.lean`	275	RolloutExec
Controller	`lean/phase4/Controller.lean`	401	NimRecurrent, AttainCircuit
ControllerBits	`lean/phase4/ControllerBits.lean`	1148	Controller, NimCorrBridge
Family	`lean/phase6/Family.lean`	574	WholeGame
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
RolloutExec	`lean/phase6/RolloutExec.lean`	896	Barrier
ThresholdInst	`lean/phase5/ThresholdInst.lean`	475	ThresholdNet, PriorityEncoder
WholeGame	`lean/phase5/WholeGame.lean`	347	ThresholdInst

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).

Proposition 5.14Each bypass: shallow {0,1}-weight components and a complete strategy winning against every legal opponent

1 Paper text

2 Explain this

The three bypasses side by side

One frame, one evaluation

Two-frame restoration

Multi-head rollouts

Row-wise recurrence

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Bypass.prop_bypass_interfaces

theorem WholeGame.twoFrame_wins

theorem RolloutExec.mhExec_wins

theorem WholeGame.replay_wins

theorem BoardStore.bits_store_wins

Definitions these statements use

inductive Family.AC0Fam

inductive Family.NetFam

inductive WholeGame.TwoFrameWins

inductive WholeGame.ReplayWins

inductive Controller.COut

inductive Controller.Tok

def Controller.cinit

def Controller.dtoks

def ControllerBits.sbits

def ControllerBits.stateWidth

def Family.ctrlAdm

def Family.ctrlF

def Family.ctrlLen

def Family.ctrlN

def Family.mhAdm

def Family.mhLen

def Family.mhN

def Family.mhS

def Family.polAdm

def Family.polLen

def Family.polN

def Family.polS

def Family.restAdm

def Family.restLen

def Family.restN

def Family.restS

def Game.Width

inductive Game.Wins

def Game.totalRolloutMoves

def RolloutExec.mhExecSel

def RolloutExec.polEvals

def RolloutExec.stepF

def RolloutExec.stepLen

def RolloutExec.stepN

def ThresholdInst.bForms

def ThresholdInst.tstep

def WholeGame.rIdx

def WholeGame.restReply

def nimSum

inductive Controller.CState

def Controller.Fits

def Controller.Idle

inductive BoardStore.BitStoreWins

def BoardStore.bsBits

Full modules

theorem `Bypass.prop_bypass_interfaces`

theorem `WholeGame.twoFrame_wins`

theorem `RolloutExec.mhExec_wins`

theorem `WholeGame.replay_wins`

theorem `BoardStore.bits_store_wins`

inductive `Family.AC0Fam`

inductive `Family.NetFam`

inductive `WholeGame.TwoFrameWins`

inductive `WholeGame.ReplayWins`

inductive `Controller.COut`

inductive `Controller.Tok`

def `Controller.cinit`

def `Controller.dtoks`

def `ControllerBits.sbits`

def `ControllerBits.stateWidth`

def `Family.ctrlAdm`

def `Family.ctrlF`

def `Family.ctrlLen`

def `Family.ctrlN`

def `Family.mhAdm`

def `Family.mhLen`

def `Family.mhN`

def `Family.mhS`

def `Family.polAdm`

def `Family.polLen`

def `Family.polN`

def `Family.polS`

def `Family.restAdm`

def `Family.restLen`

def `Family.restN`

def `Family.restS`

def `Game.Width`

inductive `Game.Wins`

def `Game.totalRolloutMoves`

def `RolloutExec.mhExecSel`

def `RolloutExec.polEvals`

def `RolloutExec.stepF`

def `RolloutExec.stepLen`

def `RolloutExec.stepN`

def `ThresholdInst.bForms`

def `ThresholdInst.tstep`

def `WholeGame.rIdx`

def `WholeGame.restReply`

def `nimSum`

inductive `Controller.CState`

def `Controller.Fits`

def `Controller.Idle`

inductive `BoardStore.BitStoreWins`

def `BoardStore.bsBits`