Theorem 5.2 (barrier)No polynomial-size, constant-depth fixed-scale network family strongly masters NIM

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

1 Paper text

Theorem 5.2 (Single-frame parity barrier) Consider the restricted family of NIM positions $P(\mathbf{b})=(2,b_1,\dots,b_m)$ where $b_i\in\{0,1\}$ . Any single-frame agent that achieves strong mastery must compute the parity $b_1\oplus\cdots\oplus b_m$ . Since $\mathrm{PARITY}\notin \AC^0$ , no polynomial-size, constant-depth fixed-scale quantised network can strongly master NIM.

Generated from paper_jmlr.tex, lines 469–474.

2 Explain this

The barrier. Put the reduction together with the simulation theorem: a polynomial-size, constant-depth fixed-scale network that strongly masters NIM would give AC⁰ circuits computing parity of $m$ bits for every $m$ . Parity is not in AC⁰, so no such network family exists.

Why it matters. This is the obstruction behind the whole paper: a single board, processed by a shallow fixed-scale network in one pass, does not give access to the global invariant.

Caveats. It is a worst-case statement within the restricted model (some boards defeat the network, and the encoded family is enough). It does not say that every learned network fails on typical positions, and it says nothing about networks outside the model.

3 How this is formalised

Named classical input. Barrier.ParityNotAC0 is the classical worst-case statement in family form; it is a theorem parameter, never an axiom. ClassicalBoundary.parityNotAC0_of_hastad derives it from ClassicalBoundary.HastadNegl, the negligible-correlation form of Håstad (2014).

Checked barrier.

Barrier.barrier_fam: under ParityNotAC0, no AC⁰ formula family of binary selectors plays a winning move on every encoded board.
Barrier.barrier_net: the same for fixed-scale network families (fixed $W$ , at most $L$ layers, polynomial widths and fan-ins) whose output wires are decoded as a binary move. The proof compiles the networks to formulas (Theorem 2.4) and applies the extraction.

Relationship to the paper. The paper says "must compute the parity"; Lean proves the extraction exactly. The paper says "no network can strongly master NIM"; Lean proves that no family wins on every board of the encoded subfamily, which is stronger. Parity hardness itself is the external input.

Coverage record
Paper anchor	`thm:singleframe-impossible` (manuscript label)
Displayed as	Theorem 5.2 (barrier)
Claim	No polynomial-size, constant-depth fixed-scale network family strongly masters NIM
Coverage category	Checked conditional theorem using named classical input
Statement source	paper_jmlr.tex lines 469–474; SHA-256 of the normalised block source `a21606992573ea17…`
Lean declarations	`NimAudit.Barrier.barrier_net` (Barrier, lines 183–212, file `474ac44cf86d…`) `NimAudit.Barrier.barrier_fam` (Barrier, lines 134–143, file `474ac44cf86d…`) `NimAudit.ClassicalBoundary.parityNotAC0_of_hastad` (Classical, lines 333–350, file `ee9d365e1611…`)
Named classical inputs	`HastadNegl`
Assumptions and domain	Fixed grid $W$ , a fixed number of layers, polynomial widths and fan-ins; the network's output is decoded as a binary move (valid bit, index bits, value bits).
Prose-to-formal notes	Lean proves: if `ParityNotAC0` holds, no such network family plays a winning move on every encoded board; and `HastadNegl` implies `ParityNotAC0`. Parity hardness itself is the external classical input.
Depends on	Theorem 5.2 (reduction), Theorem 2.4, Remark 2.3 (global parity)
Audited correspondence rows	`thm:singleframe-impossible`
Explanations	`explain/thm:singleframe-impossible.b`, `formal/thm:singleframe-impossible.b`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Barrier.barrier_net`

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

BARRIER FOR FIXED-SCALE NETWORK FAMILIES: under ParityNotAC0 no family of W-valid networks with at most L layers (W, L fixed) and polynomial widths/fan-ins, decoded as (valid, r index bits, 2 value bits), computes on all encoded boards a map that wins there. (The network-to-AC0 compilation is applied to the same networks.)

Statement as elaborated and printed by Lean 4.26.0

NimAudit.Barrier.ParityNotAC0 →
  ∀ (F : List ℕ → Option (ℕ × ℕ)),
    NimAudit.Barrier.WinsOnEnc F →
      ∀ (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)) =
                        F (NimAudit.Game.encode y)) →
              False

Exact source text, lines 183–212

183/-- BARRIER FOR FIXED-SCALE NETWORK FAMILIES: under ParityNotAC0 no family of W-valid184    networks with at most L layers (W, L fixed) and polynomial widths/fan-ins, decoded as185    (valid, r index bits, 2 value bits), computes on all encoded boards a map that wins186    there.  (The network-to-AC0 compilation is applied to the same networks.) -/187theorem barrier_net (hard : ParityNotAC0) (F : List Nat → Option (Nat × Nat)) (hF : WinsOnEnc F)188    (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat)189    (hnet : NetFam encAdm encLen net W L) (hr : ∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m)190    (hcomp : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m →191      netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 (Game.encode y)) = F (Game.encode y)) : False := by192  obtain ⟨c, k, hbd⟩ := hnet.bounded193  let s : Nat → Nat := fun m => 2 * ((2 * W + 3) ^ L * (c * encLen m ^ k + 1) ^ (W * L))194  have hpoly : PolyIn encAdm (fun m => m) s :=195    polyE (fun m hm => hm) (fun _ m => m) (fun _ _ _ => Nat.le_refl _)196      (2 * (PE.c (2 * W + 3) ^ L * (PE.c c * (2 * (vB + 1)) ^ k + 1) ^ (W * L))) s (fun _ => rfl)197  obtain ⟨c', k', hs⟩ := hpoly198  apply barrier_core hard (fun m => netBCirc W 2 (m + 1) (r m) (net m)) r s (3 * L) c' k' _ hs199  · intro m hm y hy200    obtain ⟨i, v, x, h1, h2⟩ := hF y201    refine ⟨i, v, x, ?_, h2⟩202    rw [binMove_netBCirc (net m) (hnet.valid m hm) (by rw [length_encode, hy]), hcomp m hm y hy, h1]203  · intro m hm204    have hb := netBCirc_BBound (B := 2) (N := m + 1) (r := r m) (net m) (hnet.valid m hm) (hbd m hm) (hr m hm)205    have hl := hnet.layers m hm206    refine bbound_mono hb (Nat.mul_le_mul_left 3 hl) ?_207    have e1 : (2 * W + 3) ^ (net m).length ≤ (2 * W + 3) ^ L := Nat.pow_le_pow_right (by omega) hl208    have e2 : (c * encLen m ^ k + 1) ^ (W * (net m).length) ≤ (c * encLen m ^ k + 1) ^ (W * L) :=209      Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left W hl)210    have := Nat.mul_le_mul e1 e2211    show 2 * ((2 * W + 3) ^ (net m).length * (c * encLen m ^ k + 1) ^ (W * (net m).length)) ≤ s m212    simp only [s]; omega

Project declarations in the statement: AC0.Layer, Barrier.ParityNotAC0, Barrier.WinsOnEnc, Barrier.encAdm, Barrier.encLen, CorrBridge.boardBits, Family.NetFam, Game.encode, ThresholdInst.netBinSem

Project declarations used by the proof or definition body

AC0.Layer, AC0.NetBounded, Barrier.ParityNotAC0, Barrier.WinsOnEnc, Barrier.barrier_core, Barrier.bbound_mono, Barrier.binMove_netBCirc, Barrier.encAdm, Barrier.encLen, BinReadout.BBound, BinReadout.netBCirc, BinReadout.netBCirc_BBound, CorrBridge.boardBits, Family.NetFam, Family.NetFam.bounded, Family.NetFam.layers, Family.NetFam.valid, Family.PE, Family.PE.c, Family.PolyIn, Family.instAddPE, Family.instMulPE, Family.instOfNatPE, Family.instPowPENat, Family.polyE, Family.vB, Game.encode, ParityCircuit.binMove, ParityCircuit.length_encode, ThresholdInst.netBinSem, nimSum

theorem `Barrier.barrier_fam`

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

BARRIER FOR AC0 FORMULA FAMILIES on the 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 → NimAudit.Barrier.EncWin (S m) m) → False

Exact source text, lines 134–143

134/-- BARRIER FOR AC0 FORMULA FAMILIES on the encoding family. -/135theorem barrier_fam (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)136    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)137    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)138    (hwin : ∀ m, 1 ≤ m → EncWin (S m) m) : False := by139  obtain ⟨c, k, hsz⟩ := hfam.size_poly140  apply barrier_core hard S r (fun m => c * encLen m ^ k) d (c * 4 ^ k) k _ (fun m hm => enc_poly hm) hwin141  intro m hm142  exact bbound_of_forms (hidx m hm).1 (hidx m hm).2.1 (hidx m hm).2.2 (hfam.depth_le m hm)143    (fun c' hc => hfam.reads m hm c' hc) (hsz m hm)

Project declarations in the statement: AC0.Circ, Barrier.EncWin, Barrier.ParityNotAC0, Barrier.encAdm, Barrier.encLen, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, Family.AC0Fam, ThresholdInst.bForms

Project declarations used by the proof or definition body

AC0.Circ, Barrier.EncWin, Barrier.ParityNotAC0, Barrier.barrier_core, Barrier.bbound_of_forms, Barrier.encAdm, Barrier.encLen, Barrier.enc_poly, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, Family.AC0Fam, Family.AC0Fam.depth_le, Family.AC0Fam.reads, Family.AC0Fam.size_poly, Family.PolyIn, Family.tsize, ThresholdInst.bForms

theorem `ClassicalBoundary.parityNotAC0_of_hastad`

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

WORST-CASE HARDNESS FROM THE EXTERNAL INPUT: HastadNegl ⇒ ParityNotAC0.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.ClassicalBoundary.HastadNegl → NimAudit.Barrier.ParityNotAC0

Exact source text, lines 333–350

333/-- WORST-CASE HARDNESS FROM THE EXTERNAL INPUT: HastadNegl ⇒ ParityNotAC0. -/334theorem parityNotAC0_of_hastad (hH : HastadNegl) : ParityNotAC0 := by335  intro d c k336  obtain ⟨δ, ⟨hnn, hneg⟩, hcorr⟩ := hH d c k337  obtain ⟨n0, hn0⟩ := hneg 1338  refine ⟨max n0 1, fun m hm => hard_of_premise (ε := 1 / 4) (by omega) (by grind)339    (premise_mono (premise_of_classical (by omega) (hcorr m (by omega))) ?_)⟩340  have h1 := hn0 m (by omega)341  have hm1 : (1 : Rat) ≤ (m : Rat) := by exact_mod_cast (show 1 ≤ m by omega)342  have hpos := hnn m343  simp only [Rat.pow_one] at h1344  -- δ m · (m + 1) ≤ 1 with m ≥ 1 gives δ m ≤ 1/2 < 1345  have : δ m ≤ 1 / 2 := by346    have h2 : δ m * 2 ≤ δ m * ((m : Rat) + 1) := Rat.mul_le_mul_of_nonneg_left (by grind) hpos347    grind348  have h3 := div_le_div_of_le (show (0 : Rat) < 2 by decide) this349  have e : (1 / 2 : Rat) / 2 = 1 / 4 := by grind350  rw [e] at h3; exact h3

Project declarations in the statement: Barrier.ParityNotAC0, ClassicalBoundary.HastadNegl

Project declarations used by the proof or definition body

ClassicalBoundary.ClassicalCorr, ClassicalBoundary.HastadNegl, ClassicalBoundary.Negligible, ClassicalBoundary.premise_mono, ClassicalBoundary.premise_of_classical, ParityCircuit.ParityHard, ParityCircuit.hard_of_premise, Prob.div_le_div_of_le

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

def `ClassicalBoundary.HastadNegl`

Module Classical (lean/phase6/Classical.lean, lines 282–286) · file SHA-256 ee9d365e1611d40c…

THE EXTERNAL CLASSICAL THEOREM (Håstad 2014, Cor. 3.2, negligible family form), a hypothesis: for every depth d and polynomial gate bound c·m^k there is a negligible δ with ClassicalCorr d (c·m^k) m (δ m) for all m ≥ 1.

Statement as elaborated and printed by Lean 4.26.0

Prop

Exact source text, lines 282–286

282/-- THE EXTERNAL CLASSICAL THEOREM (Håstad 2014, Cor. 3.2, negligible family form), a283    hypothesis: for every depth d and polynomial gate bound c·m^k there is a negligible δ284    with ClassicalCorr d (c·m^k) m (δ m) for all m ≥ 1. -/285def HastadNegl : Prop :=286  ∀ d c k : Nat, ∃ δ : Nat → Rat, Negligible δ ∧ ∀ m, 1 ≤ m → ClassicalCorr d (c * m ^ k) m (δ m)

Project declarations in the statement: none

Project declarations used by the proof or definition body

ClassicalBoundary.ClassicalCorr, ClassicalBoundary.Negligible

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

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

A move map plays a zero-restoring legal move on every encoded board.

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 147–150

147/-- A move map plays a zero-restoring legal move on every encoded board. -/148def WinsOnEnc (F : List Nat → Option (Nat × Nat)) : Prop :=149  ∀ y : List Bool, ∃ i v x, F (Game.encode y) = some (i, v) ∧ (Game.encode y)[i]? = some x ∧ v < x ∧150    nimSum ((Game.encode y).set i v) = 0

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.encode, nimSum

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

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

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

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

The selector plays a zero-restoring legal move on every encoded board with m bits.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → ℕ → Prop

Exact source text, lines 41–44

41/-- The selector plays a zero-restoring legal move on every encoded board with m bits. -/42def EncWin (S : BCirc) (m : Nat) : Prop :=43  ∀ y : List Bool, y.length = m → ∃ i v x, binMove S (m + 1) (Game.encode y) = some (i, v) ∧44    (Game.encode y)[i]? = some x ∧ v < x ∧ nimSum ((Game.encode y).set i v) = 0

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

BinReadout.BCirc, Game.encode, ParityCircuit.binMove, nimSum

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

Full modules

Module	File	Lines	Imports
Barrier	`lean/phase6/Barrier.lean`	496	Family, ParityCircuit
BinaryReadout	`lean/phase4/BinaryReadout.lean`	333	FiniteNet, NimCorrBridge
Circuit	`lean/phase3/Circuit.lean`	1151	NimProbability
Classical	`lean/phase6/Classical.lean`	587	Bypass
Family	`lean/phase6/Family.lean`	574	WholeGame
NimCorrBridge	`lean/phase3/NimCorrBridge.lean`	922	BitBridge
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
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).

Theorem 5.2 (barrier)No polynomial-size, constant-depth fixed-scale network family strongly masters NIM

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Barrier.barrier_net

theorem Barrier.barrier_fam

theorem ClassicalBoundary.parityNotAC0_of_hastad

Definitions these statements use

def Barrier.ParityNotAC0

def ClassicalBoundary.HastadNegl

def AC0.Layer

def Barrier.WinsOnEnc

def Barrier.encAdm

def Barrier.encLen

def CorrBridge.boardBits

inductive Family.NetFam

def Game.encode

def ThresholdInst.netBinSem

inductive AC0.Circ

def Barrier.EncWin

inductive BinReadout.BCirc

def BinReadout.BCirc.idx

def BinReadout.BCirc.val

inductive Family.AC0Fam

def ThresholdInst.bForms

Full modules

theorem `Barrier.barrier_net`

theorem `Barrier.barrier_fam`

theorem `ClassicalBoundary.parityNotAC0_of_hastad`

def `Barrier.ParityNotAC0`

def `ClassicalBoundary.HastadNegl`

def `AC0.Layer`

def `Barrier.WinsOnEnc`

def `Barrier.encAdm`

def `Barrier.encLen`

def `CorrBridge.boardBits`

inductive `Family.NetFam`

def `Game.encode`

def `ThresholdInst.netBinSem`

inductive `AC0.Circ`

def `Barrier.EncWin`

inductive `BinReadout.BCirc`

def `BinReadout.BCirc.idx`

def `BinReadout.BCirc.val`

inductive `Family.AC0Fam`

def `ThresholdInst.bForms`