Section 5.6, paragraph 1The complete multi-head and recurrent board-to-move maps are not AC⁰ families

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

1 Paper text

These are three ways around the same restricted inference problem, not three shallow algorithms for unrestricted parity. The two-frame construction changes the input and imposes a promise. The other constructions allow processing time to grow. Their complete board-to-winning-move maps cannot themselves form an $\AC^0$ family: otherwise applying either to $(2,b_1,\ldots,b_m)$ would contradict Theorem 5.2. Parallel output heads alone do not supply the rollout computation, and separators alone do not supply a recurrent scan. Appendix C illustrates the explicit network constructions and explains their conservative depth and layer bounds.

Generated from paper_jmlr.tex, lines 894–894.

2 Explain this

The three bypasses are not three shallow algorithms for parity. They are three ways around the same restricted inference problem:

the two-frame construction changes the input and adds a promise;
the rollout and recurrent constructions let the processing time grow.

The complete board-to-move maps of the last two cannot be AC⁰ families: otherwise, applied to the boards $(2,b_1,\dots,b_m)$ , they would compute parity, contradicting Theorem 5.2. Parallel output heads alone do not supply the rollout computation, and separators alone do not supply a recurrent scan.

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.bypass_barriers: under Barrier.ParityNotAC0, (a) neither the complete finite-register multi-head map nor the complete recurrent map is computed by any AC⁰ formula family on the encoding family; (b) nor by any fixed-scale network family; (c) the promised two-frame map does compute parity on promised pairs, but no AC⁰ family produces the promised predecessor from a single frame (Barrier.no_ac0_predecessor). The individual barriers are Barrier.no_ac0_mh and Barrier.no_ac0_rec. ParityNotAC0 comes from the named input HastadNegl.

Coverage record
Paper anchor	`sec:bypass-scope-p1` (website anchor; the manuscript has no label here)
Displayed as	Section 5.6, paragraph 1
Claim	The complete multi-head and recurrent board-to-move maps are not AC⁰ families
Coverage category	Checked conditional theorem using named classical input
Statement source	paper_jmlr.tex lines 894–894; SHA-256 of the normalised block source `d43e7103cb5d3591…`
Lean declarations	`NimAudit.Bypass.bypass_barriers` (Bypass, lines 143–172, file `d2e3ef2e7122…`) `NimAudit.Barrier.no_ac0_mh` (Barrier, lines 247–254, file `474ac44cf86d…`) `NimAudit.Barrier.no_ac0_rec` (Barrier, lines 256–262, file `474ac44cf86d…`) `NimAudit.Barrier.no_ac0_predecessor` (Barrier, lines 361–441, file `474ac44cf86d…`)
Named classical inputs	`HastadNegl`
Depends on	Theorem 5.2 (barrier), Proposition 5.14
Audited correspondence rows	`prop:bypass-interfaces`
Explanations	`explain/c-bypass-not-ac0`, `formal/c-bypass-not-ac0`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

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

theorem `Barrier.no_ac0_mh`

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

MULTI-HEAD BARRIER: under ParityNotAC0 the complete multi-head decision map is not computed by any single-frame AC0 formula family, even on the two-bit encoding family.

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.mhMove 2 (NimAudit.Game.encode y)) →
          False

Exact source text, lines 247–254

247/-- MULTI-HEAD BARRIER: under ParityNotAC0 the complete multi-head decision map is not248    computed by any single-frame AC0 formula family, even on the two-bit encoding family. -/249theorem no_ac0_mh (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)250    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)251    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)252    (hcomp : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → binMove (S m) (m + 1) (Game.encode y) = mhMove 2 (Game.encode y)) :253    False :=254  barrier_map hard _ mhMove_winsOnEnc S r d hfam hidx hcomp

Project declarations in the statement: AC0.Circ, Barrier.ParityNotAC0, Barrier.encAdm, Barrier.encLen, Barrier.mhMove, 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.mhMove, Barrier.mhMove_winsOnEnc, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, Family.AC0Fam, Game.encode, ParityCircuit.binMove, ThresholdInst.bForms

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 `Barrier.no_ac0_predecessor`

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

NO AC0 FAMILY PRODUCES PROMISED PREDECESSORS: under ParityNotAC0 there is no AC0 family G m (input: the m bits y; outputs: the 2(m+1) bits of a board Q) such that, for every y, Q is a predecessor of Game.encode y with nim(Q) = 0 reached by a legal move. The two-frame selector is AC0 only because this promised frame is SUPPLIED.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Barrier.ParityNotAC0 →
  ∀ (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) →
        False

Exact source text, lines 361–441

361/-- NO AC0 FAMILY PRODUCES PROMISED PREDECESSORS: under ParityNotAC0 there is no AC0362    family G m (input: the m bits y; outputs: the 2(m+1) bits of a board Q) such that, for363    every y, Q is a predecessor of Game.encode y with nim(Q) = 0 reached by a legal move.  The364    two-frame selector is AC0 only because this promised frame is SUPPLIED. -/365theorem no_ac0_predecessor (hard : ParityNotAC0) (G : Nat → List Circ) (d : Nat)366    (hfam : AC0Fam encAdm (fun m => m) G d)367    (hpred : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → ∃ Q : List Nat, Q.length = m + 1 ∧368      nimSum Q = 0 ∧ Move Q (Game.encode y) ∧ ∀ w, w < 2 * (m + 1) → eval (vfun y) (getC (G m) w) = boardBits 2 Q w) :369    False := by370  have hp : ∀ m, encAdm m → 1 ≤ m := fun m hm => hm371  have hT : PolyIn encAdm (fun m => m) (fun m => tsize (G m)) := hfam.size_poly372  have hP : PolyIn encAdm (fun m => m) (fun m => (m + 1) * (2 * (tsize (G m) + 1) + 7) + 1) :=373    polyIn_add hp (polyIn_mul (polyIn_add hp (polyIn_leaf (fun _ _ => Nat.le_refl _)) (polyIn_const _ _ 1))374      (polyIn_add hp (polyIn_mul (polyIn_const _ _ 2) (polyIn_add hp hT (polyIn_const _ _ 1))) (polyIn_const _ _ 7)))375      (polyIn_const _ _ 1)376  obtain ⟨c, k, hsz⟩ := hP377  obtain ⟨m0, hm0⟩ := hard (d + 4) c k378  have hm : 1 ≤ m0 + 1 := by omega379  -- the parity formula computes parity on every y of length m0 + 1380  have heval : ∀ y : List Bool, y.length = m0 + 1 → eval (vfun y) (predParity (G (m0 + 1)) (m0 + 1)) = par y := by381    intro y hy382    obtain ⟨Q, hQl, h0, hmv, hbits⟩ := hpred (m0 + 1) hm y hy383    rw [par_eq_parity, ← promised_pred_parity y h0 hmv]384    unfold predParity lowXorOr385    simp only [eval_or, List.any_map, length_encode, hy]386    apply any_congr_mem387    intro i hi388    have hi' := List.mem_range.mp hi389    simp only [Function.comp_apply, eval_xor2]390    have hw := hbits (2 * i + 1) (by omega)391    rw [hw, lowEnc_eval (by omega)]392    unfold boardBits393    rw [hQl, if_pos (by omega)]394    have e1 : (2 * i + 1) / 2 = i := by omega395    have e2 : 2 - 1 - (2 * i + 1) % 2 = 0 := by omega396    rw [e1, e2, Nat.testBit_xor]397  -- resources of the parity formula398  have hget : ∀ w, depth (getC (G (m0 + 1)) w) ≤ d ∧ maxInput (getC (G (m0 + 1)) w) ≤ m0 + 1 ∧399      size (getC (G (m0 + 1)) w) ≤ tsize (G (m0 + 1)) + 1 := by400    intro w; unfold getC; rw [List.getD_eq_getElem?_getD]401    cases h : (G (m0 + 1))[w]? with402    | none => simp403    | some c' =>404      have hmem := List.mem_of_getElem? h405      exact ⟨hfam.depth_le _ hm c' hmem, hfam.reads _ hm c' hmem, Nat.le_succ_of_le (size_le_tsize hmem)⟩406  have hlow : ∀ i, i ≤ m0 + 1 → depth (lowEnc i) = 0 ∧ size (lowEnc i) = 1 ∧ maxInput (lowEnc i) ≤ m0 + 1 := by407    intro i hi; unfold lowEnc; split <;> simp <;> omega408  have hx : ∀ i, i ≤ m0 + 1 → depth (xor2 (getC (G (m0 + 1)) (2 * i + 1)) (lowEnc i)) ≤ d + 3 ∧409      size (xor2 (getC (G (m0 + 1)) (2 * i + 1)) (lowEnc i)) ≤ 2 * (tsize (G (m0 + 1)) + 1) + 7 ∧410      maxInput (xor2 (getC (G (m0 + 1)) (2 * i + 1)) (lowEnc i)) ≤ m0 + 1 := by411    intro i hi412    obtain ⟨a1, a2, a3⟩ := hget (2 * i + 1)413    obtain ⟨b1, b2, b3⟩ := hlow i hi414    simp only [xor2, depth_or, depth_and, depth_not, size_or, size_and, size_not, maxInput_or, maxInput_and,415      maxInput_not, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, b1, b2]416    simp only [listMax, List.foldr]417    refine ⟨by omega, by omega, by omega⟩418  have hd : depth (predParity (G (m0 + 1)) (m0 + 1)) ≤ d + 4 := by419    unfold predParity420    apply depth_or_le; intro c' hc'421    obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc'422    exact (hx i (by have := List.mem_range.mp hi; omega)).1423  have hmx : maxInput (predParity (G (m0 + 1)) (m0 + 1)) ≤ m0 + 1 := by424    unfold predParity425    apply ControllerBits.maxInput_or_le; intro c' hc'426    obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc'427    exact (hx i (by have := List.mem_range.mp hi; omega)).2.2428  have hs : size (predParity (G (m0 + 1)) (m0 + 1)) ≤ c * (m0 + 1) ^ k := by429    unfold predParity430    rw [size_or]431    have h1 := sum_le_len_mul (cs := (List.range (m0 + 1 + 1)).map432      (fun i => xor2 (getC (G (m0 + 1)) (2 * i + 1)) (lowEnc i))) (S := 2 * (tsize (G (m0 + 1)) + 1) + 7)433      (fun c' hc' => by434        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc'435        exact (hx i (by have := List.mem_range.mp hi; omega)).2.1)436    rw [List.length_map, List.length_range] at h1437    have h2 := hsz (m0 + 1) hm438    dsimp only at h2439    omega440  obtain ⟨y, hy, hne⟩ := hm0 (m0 + 1) (by omega) _ hd hs hmx441  exact hne (heval y (mem_bitvecs_length hy))

Project declarations in the statement: AC0.Circ, AC0.Circ.eval, Barrier.ParityNotAC0, Barrier.encAdm, Bridge.vfun, CorrBridge.boardBits, CorrBridge.getC, Family.AC0Fam, Game.Move, Game.encode, nimSum

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.and, AC0.Circ.any_congr_mem, AC0.Circ.const, AC0.Circ.depth, AC0.Circ.depth_and, AC0.Circ.depth_const, AC0.Circ.depth_input, AC0.Circ.depth_not, AC0.Circ.depth_or, AC0.Circ.eval, AC0.Circ.eval_or, AC0.Circ.input, AC0.Circ.listMax, AC0.Circ.maxInput, AC0.Circ.maxInput_and, AC0.Circ.maxInput_const, AC0.Circ.maxInput_input, AC0.Circ.maxInput_not, AC0.Circ.maxInput_or, AC0.Circ.not, AC0.Circ.or, AC0.Circ.size, AC0.Circ.size_and, AC0.Circ.size_const, AC0.Circ.size_input, AC0.Circ.size_not, AC0.Circ.size_or, Barrier.ParityNotAC0, Barrier.encAdm, Barrier.lowEnc, Barrier.lowEnc_eval, Barrier.lowXorOr, Barrier.predParity, Barrier.promised_pred_parity, Barrier.size_le_tsize, Bridge.bitvecs, Bridge.mem_bitvecs_length, Bridge.par, Bridge.vfun, ControllerBits.maxInput_or_le, CorrBridge.boardBits, CorrBridge.depth_or_le, CorrBridge.eval_xor2, CorrBridge.getC, CorrBridge.sum_le_len_mul, CorrBridge.xor2, Family.AC0Fam, Family.AC0Fam.depth_le, Family.AC0Fam.reads, Family.AC0Fam.size_poly, Family.PolyIn, Family.polyIn_add, Family.polyIn_const, Family.polyIn_leaf, Family.polyIn_mul, Family.tsize, Game.Move, Game.encode, Game.parity, ParityCircuit.ParityHard, ParityCircuit.length_encode, ParityCircuit.par_eq_parity, nimSum

Definitions these statements use

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 `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 `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

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

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

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

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

def `Barrier.mhMove`

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

The COMPLETE multi-head decision map: B rollouts executed by the compiled policy networks (sequential), their outcome parities, then the compiled readout network.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Option (ℕ × ℕ)

Exact source text, lines 216–220

216/-- The COMPLETE multi-head decision map: B rollouts executed by the compiled policy217    networks (sequential), their outcome parities, then the compiled readout network. -/218def mhMove (B : Nat) (P : List Nat) : Option (Nat × Nat) :=219  netBinSem (mhNet B P.length (rIdx P.length)) P.length (rIdx P.length) B220    (obsIn B P.length P (fun j => rollOut B j P))

Project declarations in the statement: none

Project declarations used by the proof or definition body

SelectCircuit.obsIn, ThresholdInst.mhNet, ThresholdInst.netBinSem, WholeGame.rIdx, WholeGame.rollOut

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.6, paragraph 1The complete multi-head and recurrent board-to-move maps are not AC0 families

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

theorem Barrier.no_ac0_mh

theorem Barrier.no_ac0_rec

theorem Barrier.no_ac0_predecessor

Definitions these statements use

def Barrier.ParityNotAC0

inductive AC0.Circ

def AC0.Circ.eval

def AC0.Layer

def Barrier.encAdm

def Barrier.encLen

def Barrier.recMove

inductive BinReadout.BCirc

def BinReadout.BCirc.idx

def BinReadout.BCirc.val

def Bridge.vfun

def CorrBridge.boardBits

def CorrBridge.getC

inductive Family.AC0Fam

inductive Family.NetFam

def Game.Move

def Game.encode

def ParityCircuit.binMove

def RolloutExec.mhExec

def ThresholdInst.bForms

def ThresholdInst.netBinSem

def nimSum

def Barrier.mhMove

Full modules

Section 5.6, paragraph 1The complete multi-head and recurrent board-to-move maps are not AC⁰ families

theorem `Bypass.bypass_barriers`

theorem `Barrier.no_ac0_mh`

theorem `Barrier.no_ac0_rec`

theorem `Barrier.no_ac0_predecessor`

def `Barrier.ParityNotAC0`

inductive `AC0.Circ`

def `AC0.Circ.eval`

def `AC0.Layer`

def `Barrier.encAdm`

def `Barrier.encLen`

def `Barrier.recMove`

inductive `BinReadout.BCirc`

def `BinReadout.BCirc.idx`

def `BinReadout.BCirc.val`

def `Bridge.vfun`

def `CorrBridge.boardBits`

def `CorrBridge.getC`

inductive `Family.AC0Fam`

inductive `Family.NetFam`

def `Game.Move`

def `Game.encode`

def `ParityCircuit.binMove`

def `RolloutExec.mhExec`

def `ThresholdInst.bForms`

def `ThresholdInst.netBinSem`

def `nimSum`

def `Barrier.mhMove`