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 AC⁰

Checked conditional theorem using named classical input Lean checks the implication from a named, unproved classical hypothesis.

1 Paper text

Why the lower bound is respected. Unrolling $N$ constant-depth updates gives a computation of depth $O(N)$ , so Proposition 5.13 lies outside the fixed- $T$ premise of Theorem 2.4. A one-step recurrent dependency can nevertheless carry information accumulated over the whole stream. Merely appending positions and separators to a fixed-depth input does not supply this growing computation horizon. The bypass comes from sequential computation with retained state, not from the delimiter itself. For growing heap bit-width, the accumulator also needs $O(B)$ bits; a fixed-width hidden state is not claimed to store arbitrary-size invariants or histories. The construction establishes representational sufficiency for NIM, but does not establish that training a recurrent network will discover the update or preserve it reliably over long games. We do not report recurrent training experiments here.

Generated from paper_jmlr.tex, lines 872–874.

2 Explain this

No contradiction with the lower bound. $N$ shallow updates in sequence form a computation of depth about $N$ , which is outside the fixed- $T$ premise of Theorem 2.4. A one-step dependency can still carry information accumulated over the whole stream.

Separators are not the bypass. Merely writing positions and separators into the input of a fixed-depth network adds nothing. The bypass is the sequential computation with retained state.

Scope. For larger heaps the accumulator needs $B$ bits; a fixed-width state is not claimed to store arbitrary invariants. And the construction says nothing about whether training discovers the update; no recurrent training experiments are reported.

Row-wise recurrence: registers, separators and replay

Exact construction trace Every value is computed from the construction’s definitions for the example shown.

The board arrives as a stream of rows, one heap per token, with separators (SEP) between positions and a reset at the start of a game. Step through the replay controller: in scan mode it XORs each row into the accumulator; the first separator outputs the summary, stores it and switches to replay mode; during replay the same rows arrive again and each is tested against the stored summary, keeping the first cancelling candidate and a fallback; the second separator outputs the move. The board-storage variant instead writes the rows into memory and chooses the move at its single separator. In the replay controller a separator clears the accumulator and keeps the summary of the position just completed, with its validity bit; an extra separator is read as an empty position, whose summary is 0. Only a reset returns every register, validity included, to its initial value. The board-storage separator clears its accumulator and pointer and keeps the stored board. The third protocol shows the summary mechanism of Proposition 5.13 alone: it reports summaries and differences but chooses no move.

The current NIM board already determines optimal play. The memory shown here makes that answer computationally accessible by retaining partial results across rows; an earlier game position is needed only for the optional comparison of consecutive positions.

RESETreset
row 3scan
row 4scan
row 6scan
SEPsummary
row 3replay
row 4replay
row 6replay
SEPmove

9 / 9 SEP: separator after replay: output the move, return to scan mode

Registers after this update

mode: scan
accumulator: 0 000
previous summary: 1 001
stored summary used in replay: 1
heap counter: 0
first candidate: no move
first fallback: no move

Outputs so far

after token 5: summary σ = 1 (no previous summary)
after token 9: move heap 0 → 2

Counting the work

One decision on 3 heaps takes 2N + 2 = 8 updates: N scan rows, a separator, the same N rows again, a separator (plus one reset at the start of a game). The board is supplied twice; the controller does not store it.
Memory: accumulator, previous summary, stored summary, counter, candidate and fallback registers: 4 + 5B + 3r bits with N < 2^r; here B = 3, r = 2, so 25 bits.
Each single update is a shallow circuit (replay controller: Boolean depth ≤ 8, ≤ 18 threshold layers). The number of sequential updates grows with N. That no shallow family computes the complete board-to-move map is a separate statement, conditional on the named classical input that parity is not in AC⁰.

All 9 updates as a table

#	Token	Registers after	Output
1	RESET	scan, acc 0, prev 0*, idx 0, cand no move, fb no move
2	row 3	scan, acc 3, prev 0*, idx 0, cand no move, fb no move
3	row 4	scan, acc 7, prev 0*, idx 0, cand no move, fb no move
4	row 6	scan, acc 1, prev 0*, idx 0, cand no move, fb no move
5	SEP	replay, acc 0, prev 1, idx 0, cand no move, fb no move	σ = 1
6	row 3	replay, acc 0, prev 1, idx 1, cand heap 0 → 2, fb heap 0 → 2
7	row 4	replay, acc 0, prev 1, idx 2, cand heap 0 → 2, fb heap 0 → 2
8	row 6	replay, acc 0, prev 1, idx 3, cand heap 0 → 2, fb heap 0 → 2
9	SEP	scan, acc 0, prev 1, idx 0, cand no move, fb no move	move heap 0 → 2

* no previous summary yet (validity bit 0).

Game: (3, 4, 6) —your move (δ = 1)→ (2, 4, 6) —opponent (δ = 7)→ (2, 4, 1)

Only the boards at your decision times

Position fed	summary σ	difference
(3, 4, 6)	1	—
(2, 4, 1)	7	6

The difference 6 = 1 ⊕ 7 spans two moves: yours and the opponent’s.

Including your own post-move board

Position fed	summary σ	difference
(3, 4, 6)	1	—
(2, 4, 6)	0	1
(2, 4, 1)	7	7

Now the last difference is 7, the opponent’s move alone, because your post-move board (2, 4, 6) is the preceding frame.

Computed with the replay controller; feeding your post-move board costs another 2N + 2 updates, and the move it then outputs is discarded.

How this relates to the Lean proof. Each update is one step of Controller.cstep (replay) or BoardStore.bsStep (board storage) on the token streams Controller.dtoks and BoardStore.btoks. The whole-game theorems WholeGame.replay_wins and BoardStore.bits_store_wins prove that, from every board with nonzero nim-sum, iterating these updates wins against every legal opponent. The summary mechanism is Recurrent.step. The comparison of decision-time boards with the post-move board is Bypass.diff_with_postMove and Bypass.diff_decision_only.

What this does not show. Each single update is shallow; the number of updates per decision ( $2N+2$ , or $N+1$ with board storage) grows with the board. That no shallow family computes the complete board-to-move map is a separate statement, conditional on the named classical input that parity is not in $\mathrm{AC}^0$ . The edge cases (an extra separator, a reset) lie outside the protocol streams that the theorems quantify over; the update rule is simply applied. The recurrent strategies are proved in their own stateful game semantics; connecting them to the later history model of weak mastery is a separate adapter that has not been built (coverage record). No recurrent network was trained.

Depicted in Lean: Controller.cstep, Controller.dtoks, Recurrent.replayStep, Recurrent.step, Recurrent.sep_resets, ControllerBits.bstep_reset, BoardStore.bsStep, BoardStore.btoks, Controller.crun_decision, Controller.stream_fits, WholeGame.replay_wins, BoardStore.bits_store_wins, Bypass.diff_with_postMove, Bypass.diff_decision_only, Recurrent.circuit_resources, BoardStore.bsForms_res, BoardStore.bsOuts_res, BoardStore.bs_net.

Computed in your browser by a short re-implementation of the definitions above (tools/visuals/nimvis-core.js). It is not itself checked by Lean. At build time it agreed with Lean's own evaluation of those definitions on all 566 reference cases. The comparison compares every register and output after every token.

3 How this is formalised

Barrier.no_ac0_rec: under Barrier.ParityNotAC0, the complete recurrent decision map Barrier.recMove ( $2N+2$ threshold-controller updates from the initial state) is not computed by any single-frame AC⁰ formula family, even on the encoded boards. Bypass.bypass_barriers collects this together with the network form and the multi-head case. ParityNotAC0 is derived from the named input HastadNegl. The remarks about fixed-width states and training are informal.

Coverage record
Paper anchor	`par-why-the-lower-bound-is-respected-p1` (website anchor; the manuscript has no label here)
Displayed as	Section 5.5, “Why the lower bound is respected”
Claim	N sequential updates have depth O(N): outside Theorem 2.4; the complete recurrent map is not AC⁰
Coverage category	Checked conditional theorem using named classical input
Statement source	paper_jmlr.tex lines 872–874; SHA-256 of the normalised block source `f609eee9d30337f1…`
Lean declarations	`NimAudit.Barrier.no_ac0_rec` (Barrier, lines 256–262, file `474ac44cf86d…`) `NimAudit.Bypass.bypass_barriers` (Bypass, lines 143–172, file `d2e3ef2e7122…`)
Named classical inputs	`HastadNegl`
Prose-to-formal notes	Lean proves that, under `ParityNotAC0` (derived from `HastadNegl`), no AC⁰ formula family or fixed-scale network family computes the complete recurrent board-to-move map, even on the encoding family. The sentences about training and fixed-width state are informal scope statements.
Depends on	Proposition 5.13, Theorem 2.4, Remark 2.3 (global parity)
Explanations	`explain/c-lower-bound-respected`, `formal/c-lower-bound-respected`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Barrier.no_ac0_rec`

Module Barrier (lean/phase6/Barrier.lean, lines 256–262) · file SHA-256 474ac44cf86dd7e7… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

RECURRENT BARRIER (formula families).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Barrier.ParityNotAC0 →
  ∀ (S : ℕ → NimAudit.BinReadout.BCirc) (r : ℕ → ℕ) (d : ℕ),
    NimAudit.Family.AC0Fam NimAudit.Barrier.encAdm NimAudit.Barrier.encLen
        (fun m => NimAudit.ThresholdInst.bForms (S m)) d →
      (∀ (m : ℕ), 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m) →
        (∀ (m : ℕ),
            1 ≤ m →
              ∀ (y : List Bool),
                y.length = m →
                  NimAudit.ParityCircuit.binMove (S m) (m + 1) (NimAudit.Game.encode y) =
                    NimAudit.Barrier.recMove 2 (NimAudit.Game.encode y)) →
          False

Exact source text, lines 256–262

256/-- RECURRENT BARRIER (formula families). -/257theorem no_ac0_rec (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)258    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)259    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)260    (hcomp : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → binMove (S m) (m + 1) (Game.encode y) = recMove 2 (Game.encode y)) :261    False :=262  barrier_map hard _ recMove_winsOnEnc S r d hfam hidx hcomp

Project declarations in the statement: AC0.Circ, Barrier.ParityNotAC0, Barrier.encAdm, Barrier.encLen, Barrier.recMove, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, Family.AC0Fam, Game.encode, ParityCircuit.binMove, ThresholdInst.bForms

Project declarations used by the proof or definition body

AC0.Circ, Barrier.ParityNotAC0, Barrier.barrier_map, Barrier.encAdm, Barrier.encLen, Barrier.recMove, Barrier.recMove_winsOnEnc, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, Family.AC0Fam, Game.encode, ParityCircuit.binMove, ThresholdInst.bForms

theorem `Bypass.bypass_barriers`

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

BYPASS BARRIERS. Under ParityNotAC0: (a) the complete finite-register multi-head map mhExec and the complete recurrent map recMove are not computed by any AC0 formula family on the encoding family; (b) nor by any fixed-scale network family (fixed W, constant layers, polynomial size); (c) the promised two-frame map does compute parity on promised pairs, but no AC0 family produces the promised predecessor from the single frame.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Barrier.ParityNotAC0 →
  (∀ (S : ℕ → NimAudit.BinReadout.BCirc) (r : ℕ → ℕ) (d : ℕ),
      NimAudit.Family.AC0Fam NimAudit.Barrier.encAdm NimAudit.Barrier.encLen
          (fun m => NimAudit.ThresholdInst.bForms (S m)) d →
        (∀ (m : ℕ), 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m) →
          ¬∀ (m : ℕ),
              1 ≤ m →
                ∀ (y : List Bool),
                  y.length = m →
                    NimAudit.ParityCircuit.binMove (S m) (m + 1) (NimAudit.Game.encode y) =
                      NimAudit.RolloutExec.mhExec 2 (NimAudit.Game.encode y)) ∧
    (∀ (S : ℕ → NimAudit.BinReadout.BCirc) (r : ℕ → ℕ) (d : ℕ),
        NimAudit.Family.AC0Fam NimAudit.Barrier.encAdm NimAudit.Barrier.encLen
            (fun m => NimAudit.ThresholdInst.bForms (S m)) d →
          (∀ (m : ℕ), 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m) →
            ¬∀ (m : ℕ),
                1 ≤ m →
                  ∀ (y : List Bool),
                    y.length = m →
                      NimAudit.ParityCircuit.binMove (S m) (m + 1) (NimAudit.Game.encode y) =
                        NimAudit.Barrier.recMove 2 (NimAudit.Game.encode y)) ∧
      (∀ (net : ℕ → List NimAudit.AC0.Layer) (r : ℕ → ℕ) (W L : ℕ),
          NimAudit.Family.NetFam NimAudit.Barrier.encAdm NimAudit.Barrier.encLen net W L →
            (∀ (m : ℕ), 1 ≤ m → m + 1 ≤ 2 ^ r m) →
              ¬∀ (m : ℕ),
                  1 ≤ m →
                    ∀ (y : List Bool),
                      y.length = m →
                        NimAudit.ThresholdInst.netBinSem (net m) (m + 1) (r m) 2
                            (NimAudit.CorrBridge.boardBits 2 (NimAudit.Game.encode y)) =
                          NimAudit.RolloutExec.mhExec 2 (NimAudit.Game.encode y)) ∧
        (∀ (net : ℕ → List NimAudit.AC0.Layer) (r : ℕ → ℕ) (W L : ℕ),
            NimAudit.Family.NetFam NimAudit.Barrier.encAdm NimAudit.Barrier.encLen net W L →
              (∀ (m : ℕ), 1 ≤ m → m + 1 ≤ 2 ^ r m) →
                ¬∀ (m : ℕ),
                    1 ≤ m →
                      ∀ (y : List Bool),
                        y.length = m →
                          NimAudit.ThresholdInst.netBinSem (net m) (m + 1) (r m) 2
                              (NimAudit.CorrBridge.boardBits 2 (NimAudit.Game.encode y)) =
                            NimAudit.Barrier.recMove 2 (NimAudit.Game.encode y)) ∧
          ∀ (G : ℕ → List NimAudit.AC0.Circ) (d : ℕ),
            NimAudit.Family.AC0Fam NimAudit.Barrier.encAdm (fun m => m) G d →
              ¬∀ (m : ℕ),
                  1 ≤ m →
                    ∀ (y : List Bool),
                      y.length = m →
                        ∃ Q,
                          Q.length = m + 1 ∧
                            NimAudit.nimSum Q = 0 ∧
                              NimAudit.Game.Move Q (NimAudit.Game.encode y) ∧
                                ∀ w < 2 * (m + 1),
                                  NimAudit.AC0.Circ.eval (NimAudit.Bridge.vfun y)
                                      (NimAudit.CorrBridge.getC (G m) w) =
                                    NimAudit.CorrBridge.boardBits 2 Q w

Exact source text, lines 143–172

143/-- BYPASS BARRIERS.  Under ParityNotAC0:144    (a) the complete finite-register multi-head map mhExec and the complete recurrent map145        recMove are not computed by any AC0 formula family on the encoding family;146    (b) nor by any fixed-scale network family (fixed W, constant layers, polynomial size);147    (c) the promised two-frame map does compute parity on promised pairs, but no AC0148        family produces the promised predecessor from the single frame. -/149theorem bypass_barriers (hard : ParityNotAC0) :150    (∀ (S : Nat → BCirc) (r : Nat → Nat) (d : Nat), AC0Fam encAdm encLen (fun m => bForms (S m)) d →151      (∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m) →152      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → ParityCircuit.binMove (S m) (m + 1) (Game.encode y) = mhExec 2 (Game.encode y))) ∧153    (∀ (S : Nat → BCirc) (r : Nat → Nat) (d : Nat), AC0Fam encAdm encLen (fun m => bForms (S m)) d →154      (∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m) →155      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → ParityCircuit.binMove (S m) (m + 1) (Game.encode y) = recMove 2 (Game.encode y))) ∧156    (∀ (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat), NetFam encAdm encLen net W L →157      (∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m) →158      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m →159        netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 (Game.encode y)) = mhExec 2 (Game.encode y))) ∧160    (∀ (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat), NetFam encAdm encLen net W L →161      (∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m) →162      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m →163        netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 (Game.encode y)) = recMove 2 (Game.encode y))) ∧164    (∀ (G : Nat → List Circ) (d : Nat), AC0Fam encAdm (fun m => m) G d →165      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → ∃ Q : List Nat, Q.length = m + 1 ∧166        nimSum Q = 0 ∧ Move Q (Game.encode y) ∧167        ∀ w, w < 2 * (m + 1) → eval (vfun y) (getC (G m) w) = boardBits 2 Q w)) := by168  refine ⟨fun S r d hf hi hc => barrier_map hard _ mhExec_winsOnEnc S r d hf hi hc,169    fun S r d hf hi hc => no_ac0_rec hard S r d hf hi hc,170    fun net r W L hn hr hc => barrier_net hard _ mhExec_winsOnEnc net r W L hn hr hc,171    fun net r W L hn hr hc => no_net_rec hard net r W L hn hr hc,172    fun G d hf hp => no_ac0_predecessor hard G d hf hp⟩

Project declarations in the statement: AC0.Circ, AC0.Circ.eval, AC0.Layer, Barrier.ParityNotAC0, Barrier.encAdm, Barrier.encLen, Barrier.recMove, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, Bridge.vfun, CorrBridge.boardBits, CorrBridge.getC, Family.AC0Fam, Family.NetFam, Game.Move, Game.encode, ParityCircuit.binMove, RolloutExec.mhExec, ThresholdInst.bForms, ThresholdInst.netBinSem, nimSum

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.eval, AC0.Layer, Barrier.ParityNotAC0, Barrier.barrier_map, Barrier.barrier_net, Barrier.encAdm, Barrier.encLen, Barrier.no_ac0_predecessor, Barrier.no_ac0_rec, Barrier.no_net_rec, Barrier.recMove, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, Bridge.vfun, Bypass.mhExec_winsOnEnc, CorrBridge.boardBits, CorrBridge.getC, Family.AC0Fam, Family.NetFam, Game.Move, Game.encode, ParityCircuit.binMove, RolloutExec.mhExec, ThresholdInst.bForms, ThresholdInst.netBinSem, nimSum

Definitions these statements use

def `Barrier.recMove`

Module Barrier (lean/phase6/Barrier.lean, lines 227–230) · file SHA-256 474ac44cf86dd7e7…

The COMPLETE recurrent decision map: 2N + 2 threshold-controller updates from the initial state on rows, SEP, rows, SEP.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Option (ℕ × ℕ)

Exact source text, lines 227–230

227/-- The COMPLETE recurrent decision map: 2N + 2 threshold-controller updates from the228    initial state on rows, SEP, rows, SEP. -/229def recMove (B : Nat) (P : List Nat) : Option (Nat × Nat) :=230  (WholeGame.decide B (rIdx P.length) (sbits B (rIdx P.length) cinit) P).2

Project declarations in the statement: none

Project declarations used by the proof or definition body

Controller.cinit, ControllerBits.sbits, WholeGame.decide, WholeGame.rIdx

def `Barrier.ParityNotAC0`

Module Barrier (lean/phase6/Barrier.lean, lines 36–37) · file SHA-256 474ac44cf86dd7e7…

CLASSICAL WORST-CASE PARITY HARDNESS, family form (EXTERNAL HYPOTHESIS).

Statement as elaborated and printed by Lean 4.26.0

Prop

Exact source text, lines 36–37

36/-- CLASSICAL WORST-CASE PARITY HARDNESS, family form (EXTERNAL HYPOTHESIS). -/37def ParityNotAC0 : Prop := ∀ d c k : Nat, ∃ m0 : Nat, ∀ m, m0 ≤ m → ParityHard d (c * m ^ k) m

Project declarations in the statement: none

Project declarations used by the proof or definition body

ParityCircuit.ParityHard

inductive `AC0.Circ`

Module Circuit (lean/phase3/Circuit.lean, lines 35–40) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 35–40

35inductive Circ where36  | input (i : Nat)37  | const (b : Bool)38  | not (c : Circ)39  | and (cs : List Circ)40  | or (cs : List Circ)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Barrier.encAdm`

Module Barrier (lean/phase6/Barrier.lean, lines 123–124) · file SHA-256 474ac44cf86dd7e7…

The encoding family: m parity bits, m + 1 heaps of 2 bits, input length 2(m+1).

Statement as elaborated and printed by Lean 4.26.0

ℕ → Prop

Exact source text, lines 123–124

123/-- The encoding family: m parity bits, m + 1 heaps of 2 bits, input length 2(m+1). -/124def encAdm : Nat → Prop := fun m => 1 ≤ m

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Barrier.encLen`

Module Barrier (lean/phase6/Barrier.lean, lines 125–125) · file SHA-256 474ac44cf86dd7e7…

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ

Exact source text, lines 125–125

125def encLen : Nat → Nat := fun m => 2 * (m + 1)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `BinReadout.BCirc`

Module BinaryReadout (lean/phase4/BinaryReadout.lean, lines 24–28) · file SHA-256 17ef1a62ba9edafb…

Binary readout formulas for one observed bit.

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 24–28

24/-- Binary readout formulas for one observed bit. -/25structure BCirc where26  valid : Circ27  idx : List Circ28  val : List Circ

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Circ

def `BinReadout.BCirc.idx`

Module BinaryReadout (lean/phase4/BinaryReadout.lean, lines 27–27) · file SHA-256 17ef1a62ba9edafb…

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 27–27

27  idx : List Circ

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

Project declarations used by the proof or definition body

BinReadout.BCirc

def `BinReadout.BCirc.val`

Module BinaryReadout (lean/phase4/BinaryReadout.lean, lines 28–28) · file SHA-256 17ef1a62ba9edafb…

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 28–28

28  val : List Circ

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

Project declarations used by the proof or definition body

BinReadout.BCirc

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

def `Game.encode`

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

The board (2, b_1, ..., b_m), Boolean heaps encoded as 0/1.

Statement as elaborated and printed by Lean 4.26.0

List Bool → List ℕ

Exact source text, lines 476–477

476/-- The board (2, b_1, ..., b_m), Boolean heaps encoded as 0/1. -/477def encode (bs : List Bool) : List Nat := 2 :: bs.map Bool.toNat

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `ParityCircuit.binMove`

Module ParityCircuit (lean/phase4/ParityCircuit.lean, lines 23–25) · file SHA-256 03525bcfcb9f3acd…

The move of a binary selector (no observed bit).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → ℕ → List ℕ → Option (ℕ × ℕ)

Exact source text, lines 23–25

23/-- The move of a binary selector (no observed bit). -/24def binMove (S : BCirc) (N : Nat) (P : List Nat) : Option (Nat × Nat) :=25  binReadoutOf 2 N (fun _ => S) P false

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

BinReadout.BCirc, BinReadout.binReadoutOf

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 `AC0.Circ.eval`

Module Circuit (lean/phase3/Circuit.lean, lines 44–49) · file SHA-256 af97cc0eec7d8464…

Statement as elaborated and printed by Lean 4.26.0

(ℕ → Bool) → NimAudit.AC0.Circ → Bool

Exact source text, lines 44–49

44def eval (x : Nat → Bool) : Circ → Bool45  | input i => x i46  | const b => b47  | not c => !(eval x c)48  | and cs => cs.attach.all (fun ⟨c, _⟩ => eval x c)49  | or cs => cs.attach.any (fun ⟨c, _⟩ => eval x c)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.casesOn, AC0.Circ.const, AC0.Circ.input, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `AC0.Layer`

Module Circuit (lean/phase3/Circuit.lean, lines 743–744) · file SHA-256 af97cc0eec7d8464…

A layer: a list of gates reading the previous layer's outputs (indexed by Nat).

Statement as elaborated and printed by Lean 4.26.0

Type

Exact source text, lines 743–744

743/-- A layer: a list of gates reading the previous layer's outputs (indexed by Nat). -/744abbrev Layer := List Gate

Project declarations in the statement: none

Project declarations used by the proof or definition body

AC0.Gate

def `Bridge.vfun`

Module BitBridge (lean/phase3/BitBridge.lean, lines 407–408) · file SHA-256 000644dc271d27f9…

Bit vector as an input assignment.

Statement as elaborated and printed by Lean 4.26.0

List Bool → ℕ → Bool

Exact source text, lines 407–408

407/-- Bit vector as an input assignment. -/408def vfun (x : List Bool) : Nat → Bool := fun j => x.getD j false

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `CorrBridge.boardBits`

Module NimCorrBridge (lean/phase3/NimCorrBridge.lean, lines 39–41) · file SHA-256 d3fb2e4a64db3e92…

Input bits of a board: heap i, big-endian position p (bit B-1-p) at index B·i + p.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → ℕ → Bool

Exact source text, lines 39–41

39/-- Input bits of a board: heap i, big-endian position p (bit B-1-p) at index B·i + p. -/40def boardBits (B : Nat) (P : List Nat) : Nat → Bool := fun j =>41  if j < B * P.length then (P.getD (j / B) 0).testBit (B - 1 - j % B) else false

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `CorrBridge.getC`

Module NimCorrBridge (lean/phase3/NimCorrBridge.lean, lines 87–87) · file SHA-256 d3fb2e4a64db3e92…

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 87–87

87def getC (cs : List Circ) (i : Nat) : Circ := cs.getD i (const false)

Project declarations in the statement: AC0.Circ

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.const

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

def `Game.Move`

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

An ordinary legal Nim move: exactly one heap strictly decreases.

Statement as elaborated and printed by Lean 4.26.0

List ℕ → List ℕ → Prop

Exact source text, lines 24–26

24/-- An ordinary legal Nim move: exactly one heap strictly decreases. -/25def Move (p q : List Nat) : Prop :=26  ∃ pre x post y, p = pre ++ x :: post ∧ q = pre ++ y :: post ∧ y < x

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `RolloutExec.mhExec`

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

THE FULLY EXECUTED MULTI-HEAD DECISION: finite-register rollouts, then the readout network on the board and the B executed outcome bits.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Option (ℕ × ℕ)

Exact source text, lines 495–499

495/-- THE FULLY EXECUTED MULTI-HEAD DECISION: finite-register rollouts, then the readout496    network on the board and the B executed outcome bits. -/497def mhExec (B : Nat) (P : List Nat) : Option (Nat × Nat) :=498  netBinSem (mhNet B P.length (rIdx P.length)) P.length (rIdx P.length) B499    (obsIn B P.length P (fun j => outBit B j P))

Project declarations in the statement: none

Project declarations used by the proof or definition body

RolloutExec.outBit, SelectCircuit.obsIn, ThresholdInst.mhNet, ThresholdInst.netBinSem, WholeGame.rIdx

def `ThresholdInst.netBinSem`

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

Decoding the output wires of a binary-selector network (bit reading only).

Statement as elaborated and printed by Lean 4.26.0

List NimAudit.AC0.Layer → ℕ → ℕ → ℕ → (ℕ → Bool) → Option (ℕ × ℕ)

Exact source text, lines 322–329

322/-- Decoding the output wires of a binary-selector network (bit reading only). -/323def netBinSem (net : List Layer) (N r B : Nat) (x : Nat → Bool) : Option (Nat × Nat) :=324  if evalNet net x 0 then325    if toNatBE ((List.range r).map (fun q => evalNet net x (1 + q))) < N then326      some (toNatBE ((List.range r).map (fun q => evalNet net x (1 + q))),327        toNatBE ((List.range B).map (fun k => evalNet net x (1 + r + k))))328    else none329  else none

Project declarations in the statement: AC0.Layer

Project declarations used by the proof or definition body

AC0.Layer, AC0.evalNet, Bridge.toNatBE

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

Full modules

Module	File	Lines	Imports
Barrier	`lean/phase6/Barrier.lean`	496	Family, ParityCircuit
BinaryReadout	`lean/phase4/BinaryReadout.lean`	333	FiniteNet, NimCorrBridge
BitBridge	`lean/phase3/BitBridge.lean`	560	Circuit
Bypass	`lean/phase6/Bypass.lean`	275	RolloutExec
Circuit	`lean/phase3/Circuit.lean`	1151	NimProbability
Family	`lean/phase6/Family.lean`	574	WholeGame
NimCore	`lean/NimCore.lean`	139	`Std`
NimCorrBridge	`lean/phase3/NimCorrBridge.lean`	922	BitBridge
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
ParityCircuit	`lean/phase4/ParityCircuit.lean`	259	BinaryReadout
RolloutExec	`lean/phase6/RolloutExec.lean`	896	Barrier
ThresholdInst	`lean/phase5/ThresholdInst.lean`	475	ThresholdNet, PriorityEncoder

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

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

1 Paper text

2 Explain this

Row-wise recurrence: registers, separators and replay

Registers after this update

Outputs so far

Counting the work

Only the boards at your decision times

Including your own post-move board

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Barrier.no_ac0_rec

theorem Bypass.bypass_barriers

Definitions these statements use

def Barrier.recMove

def Barrier.ParityNotAC0

inductive AC0.Circ

def Barrier.encAdm

def Barrier.encLen

inductive BinReadout.BCirc

def BinReadout.BCirc.idx

def BinReadout.BCirc.val

inductive Family.AC0Fam

def Game.encode

def ParityCircuit.binMove

def ThresholdInst.bForms

def AC0.Circ.eval

def AC0.Layer

def Bridge.vfun

def CorrBridge.boardBits

def CorrBridge.getC

inductive Family.NetFam

def Game.Move

def RolloutExec.mhExec

def ThresholdInst.netBinSem

def nimSum

Full modules

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 AC⁰

theorem `Barrier.no_ac0_rec`

theorem `Bypass.bypass_barriers`

def `Barrier.recMove`

def `Barrier.ParityNotAC0`

inductive `AC0.Circ`

def `Barrier.encAdm`

def `Barrier.encLen`

inductive `BinReadout.BCirc`

def `BinReadout.BCirc.idx`

def `BinReadout.BCirc.val`

inductive `Family.AC0Fam`

def `Game.encode`

def `ParityCircuit.binMove`

def `ThresholdInst.bForms`

def `AC0.Circ.eval`

def `AC0.Layer`

def `Bridge.vfun`

def `CorrBridge.boardBits`

def `CorrBridge.getC`

inductive `Family.NetFam`

def `Game.Move`

def `RolloutExec.mhExec`

def `ThresholdInst.netBinSem`

def `nimSum`