Theorem 5.2 (reduction)Strong mastery on the boards (2,b₁,…,b_m) forces the winning move to reveal the parity of b

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

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 winning move therefore removes two tokens for even parity and one token for odd parity from the first heap. The concise proof in the paper uses this observation; the encoding and extraction below explain why it gives a circuit reduction.

The reduction. Look at boards $(2,b_1,\dots,b_m)$ where each $b_i$ is $0$ or $1$ . The nim-sum is $2\oplus(b_1\oplus\cdots\oplus b_m)$ , which is $2$ or $3$ , so every such board is winning. Only the first heap has the $2$ s bit, so a winning move must change the first heap, and the only value that makes the nim-sum zero is $b_1\oplus\cdots\oplus b_m$ .

Example. $(2,1,0,1)$ : parity $0$ , so the winning move is $2\to0$ . $(2,1,1,1)$ : parity $1$ , so it is $2\to1$ .

Consequence. Any agent that always finds the winning move on these boards computes the parity of $b$ : read off the new value of the first heap. With two bits per heap, encoding and decoding are mere wiring, so they keep size and depth unchanged.

3 How this is formalised

Game.unique_zero_move: the only legal move from Game.encode $b$ to nim-sum zero produces Game.reduced $b$ , the board with first heap $b_1\oplus\cdots\oplus b_m$ (for every $m$ , including $m=0$ ).
Game.winning_selector_parity: any selector that plays a winning move at every winning position outputs the reduced board on these inputs.
ParityCircuit.extraction: circuit form. If a binary move selector (a formula family producing a valid bit, index bits and two value bits) of depth $d$ and size $s$ strongly masters 2-bit boards with $m+1$ heaps, then a formula of the same depth and size, reading only the $m$ parity inputs, computes parity. The encoding is a leaf substitution, so no resources are added.

Coverage record
Paper anchor	`thm:singleframe-impossible` (manuscript label)
Displayed as	Theorem 5.2 (reduction)
Claim	Strong mastery on the boards (2,b₁,…,b_m) forces the winning move to reveal the parity of b
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 469–474; SHA-256 of the normalised block source `a21606992573ea17…`
Lean declarations	`NimAudit.Game.unique_zero_move` (NimGame, lines 504–532, file `23df6bb87ecf…`) `NimAudit.Game.winning_selector_parity` (NimGame, lines 534–541, file `23df6bb87ecf…`) `NimAudit.ParityCircuit.extraction` (ParityCircuit, lines 127–167, file `03525bcfcb9f…`)
Assumptions and domain	Boards $(2,b_1,\dots,b_m)$ with $b_i\in\{0,1\}$ , two bits per heap; all such boards are winning.
Audited correspondence rows	`thm:singleframe-impossible`
Explanations	`explain/thm:singleframe-impossible.a`, `formal/thm:singleframe-impossible.a`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Game.unique_zero_move`

Module NimGame (lean/phase2/NimGame.lean, lines 504–532) · file SHA-256 23df6bb87ecfd344… Axioms reported by the fresh build: propext, Quot.sound

UNIQUENESS: the only legal move from (2, b_1, ..., b_m) to nim-sum zero sets the leading heap to b_1 XOR ... XOR b_m. Holds for every m, including m = 0.

Statement as elaborated and printed by Lean 4.26.0

∀ (bs : List Bool) (q : List ℕ),
  NimAudit.Game.Move (NimAudit.Game.encode bs) q →
    NimAudit.nimSum q = 0 → q = NimAudit.Game.reduced bs

Exact source text, lines 504–532

504/-- UNIQUENESS: the only legal move from (2, b_1, ..., b_m) to nim-sum zero sets the505    leading heap to b_1 XOR ... XOR b_m.  Holds for every m, including m = 0. -/506theorem unique_zero_move (bs : List Bool) (q : List Nat)507    (hm : Move (encode bs) q) (hq : nimSum q = 0) : q = reduced bs := by508  obtain ⟨pre, x, post, y, hp, rfl, hlt⟩ := hm509  cases pre with510  | nil =>511    simp only [encode, List.nil_append, List.cons.injEq] at hp512    obtain ⟨rfl, rfl⟩ := hp513    simp only [List.nil_append, nimSum, nimSum_bits] at hq514    have := xor_eq_zero_imp hq515    simp [reduced, this]516  | cons h pre' =>517    simp only [encode, List.cons_append, List.cons.injEq] at hp518    obtain ⟨rfl, hM⟩ := hp519    have hx1 : x ≤ 1 := by520      have hmem : x ∈ bs.map Bool.toNat := by rw [hM]; simp521      obtain ⟨b, _, rfl⟩ := List.mem_map.mp hmem522      exact Bool.toNat_le b523    have hx : x = 1 := by omega524    have hy : y = 0 := by omega525    subst hx; subst hy526    exfalso527    have e1 : nimSum (pre' ++ 0 :: post) = nimSum (pre' ++ 1 :: post) ^^^ (1 ^^^ 0) :=528      nimSum_move529    rw [← hM, nimSum_bits] at e1530    simp only [List.cons_append, nimSum, e1] at hq531    revert hq532    cases parity bs <;> decide

Project declarations in the statement: Game.Move, Game.encode, Game.reduced, nimSum

Project declarations used by the proof or definition body

Game.Move, Game.encode, Game.nimSum_bits, Game.nimSum_move, Game.parity, Game.reduced, Game.xor_eq_zero_imp, nimSum

theorem `Game.winning_selector_parity`

Module NimGame (lean/phase2/NimGame.lean, lines 534–541) · file SHA-256 23df6bb87ecfd344… Axioms reported by the fresh build: propext, Quot.sound

Every winning-move selector outputs the reduced board, hence the parity, on (2, b_1, ..., b_m). The hypothesis uses the normal-play semantics.

Statement as elaborated and printed by Lean 4.26.0

∀ (sel : List ℕ → Option (List ℕ)),
  (∀ (p : List ℕ),
      NimAudit.Game.Win p → ∃ q, sel p = some q ∧ NimAudit.Game.Move p q ∧ NimAudit.Game.Lose q) →
    ∀ (bs : List Bool), sel (NimAudit.Game.encode bs) = some (NimAudit.Game.reduced bs)

Exact source text, lines 534–541

534/-- Every winning-move selector outputs the reduced board, hence the parity, on535    (2, b_1, ..., b_m).  The hypothesis uses the normal-play semantics. -/536theorem winning_selector_parity (sel : List Nat → Option (List Nat))537    (hsel : ∀ p, Win p → ∃ q, sel p = some q ∧ Move p q ∧ Lose q) (bs : List Bool) :538    sel (encode bs) = some (reduced bs) := by539  have hw : Win (encode bs) := (win_iff _).2 (nimSum_encode_ne bs)540  obtain ⟨q, hs, hm, hl⟩ := hsel _ hw541  rw [hs, unique_zero_move bs q hm ((lose_iff q).1 hl)]

Project declarations in the statement: Game.Lose, Game.Move, Game.Win, Game.encode, Game.reduced

Project declarations used by the proof or definition body

Game.Lose, Game.Move, Game.Win, Game.encode, Game.lose_iff, Game.nimSum_encode_ne, Game.reduced, Game.unique_zero_move, Game.win_iff, nimSum

theorem `ParityCircuit.extraction`

Module ParityCircuit (lean/phase4/ParityCircuit.lean, lines 127–167) · file SHA-256 03525bcfcb9f3acd… Axioms reported by the fresh build: propext, Quot.sound

EXTRACTION THEOREM. If a binary selector with BBound (depth ≤ d, size ≤ s, 2 value bits) has strong mastery on 2-bit boards with m+1 heaps, then parityFormula S m computes parity of every y ∈ {0,1}^m, has depth ≤ d and size ≤ s, and reads only the m parity inputs.

Statement as elaborated and printed by Lean 4.26.0

∀ {S : NimAudit.BinReadout.BCirc} {m r d s : ℕ},
  NimAudit.BinReadout.BBound S (m + 1) 2 r d s →
    NimAudit.ParityCircuit.StrongMastery S (m + 1) →
      (∀ (y : List Bool),
          y.length = m →
            NimAudit.AC0.Circ.eval (NimAudit.Bridge.vfun y)
                (NimAudit.ParityCircuit.parityFormula S m) =
              NimAudit.Bridge.par y) ∧
        (NimAudit.ParityCircuit.parityFormula S m).depth ≤ d ∧
          (NimAudit.ParityCircuit.parityFormula S m).size ≤ s ∧
            (NimAudit.ParityCircuit.parityFormula S m).maxInput ≤ m

Exact source text, lines 127–167

127/-- EXTRACTION THEOREM.  If a binary selector with BBound (depth ≤ d, size ≤ s,128    2 value bits) has strong mastery on 2-bit boards with m+1 heaps, then129    parityFormula S m computes parity of every y ∈ {0,1}^m, has depth ≤ d and size130    ≤ s, and reads only the m parity inputs. -/131theorem extraction {S : BCirc} {m r d s : Nat} (hb : BBound S (m + 1) 2 r d s)132    (hS : StrongMastery S (m + 1)) :133    (∀ y : List Bool, y.length = m → eval (vfun y) (parityFormula S m) = par y) ∧134    depth (parityFormula S m) ≤ d ∧ size (parityFormula S m) ≤ s ∧135    maxInput (parityFormula S m) ≤ m := by136  have hval1 : getC S.val 1 ∈ S.val := getC_mem (by rw [hb.val_len]; decide)137  refine ⟨?_, ?_, ?_, ?_⟩138  · intro y hy139    unfold parityFormula140    rw [eval_subst]141    have hz : (fun j => eval (vfun y) (parSubst m j)) = boardBits 2 (encode y) := by142      funext j; exact parSubst_eval hy j143    rw [hz]144    have hW : Win (encode y) := (win_iff _).2 (nimSum_encode_ne y)145    obtain ⟨i, v, x, hmove, hx, hlt, hlose⟩ :=146      hS (encode y) (by rw [length_encode, hy]) (encode_width y) hW147    have hz0 := (lose_iff _).1 hlose148    obtain ⟨_, hvp⟩ := winning_move_on_encode y hx hlt hz0149    -- read the value bits off the selector's output150    unfold binMove binReadoutOf at hmove151    split at hmove152    · split at hmove153      · simp only [Option.some.injEq, Prod.mk.injEq] at hmove154        obtain ⟨_, hvdef⟩ := hmove155        rw [hvp] at hvdef156        have hl : (S.val.map (eval (boardBits 2 (encode y)))).length = 2 := by simp [hb.val_len]157        have := low_bit_of_two hl hvdef158        rw [eval_getC, this, par_eq_parity]159      · cases hmove160    · cases hmove161  · unfold parityFormula162    rw [depth_subst_leaf _ (parSubst_leaf m)]163    exact hb.depth_val _ hval1164  · unfold parityFormula165    rw [size_subst_leaf _ (parSubst_leaf m)]166    exact hb.size_val _ hval1167  · exact maxInput_subst_le _ m (parSubst_max m) _

Project declarations in the statement: AC0.Circ.depth, AC0.Circ.eval, AC0.Circ.maxInput, AC0.Circ.size, BinReadout.BBound, BinReadout.BCirc, Bridge.par, Bridge.vfun, ParityCircuit.StrongMastery, ParityCircuit.parityFormula

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.depth_subst_leaf, AC0.Circ.eval, AC0.Circ.eval_subst, AC0.Circ.maxInput, AC0.Circ.maxInput_subst_le, AC0.Circ.size, AC0.Circ.size_subst_leaf, AC0.Circ.subst, BinReadout.BBound, BinReadout.BBound.depth_val, BinReadout.BBound.size_val, BinReadout.BBound.val_len, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid, BinReadout.getC_mem, Bridge.par, Bridge.toNatBE, Bridge.vfun, CorrBridge.boardBits, CorrBridge.eval_getC, CorrBridge.getC, Game.Lose, Game.Win, Game.encode, Game.lose_iff, Game.nimSum_encode_ne, Game.parity, Game.win_iff, ParityCircuit.StrongMastery, ParityCircuit.binMove, ParityCircuit.encode_width, ParityCircuit.length_encode, ParityCircuit.low_bit_of_two, ParityCircuit.parSubst, ParityCircuit.parSubst_eval, ParityCircuit.parSubst_leaf, ParityCircuit.parSubst_max, ParityCircuit.par_eq_parity, ParityCircuit.parityFormula, ParityCircuit.winning_move_on_encode, nimSum

Definitions these statements use

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

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

The reduced board: leading heap replaced by the parity.

Statement as elaborated and printed by Lean 4.26.0

List Bool → List ℕ

Exact source text, lines 494–495

494/-- The reduced board: leading heap replaced by the parity. -/495def reduced (bs : List Bool) : List Nat := (parity bs).toNat :: bs.map Bool.toNat

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.parity

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

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

Statement as elaborated and printed by Lean 4.26.0

List ℕ → ℕ

Exact source text, lines 7–9

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

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

inductive `Game.Lose`

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

Statement as elaborated and printed by Lean 4.26.0

List ℕ → Prop

Exact source text, lines 39–40

39inductive Lose : List Nat → Prop40  | intro (p : List Nat) : (∀ q, Move p q → Win q) → Lose p

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.Move, Game.Win

inductive `Game.Win`

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

Statement as elaborated and printed by Lean 4.26.0

List ℕ → Prop

Exact source text, lines 37–38

37inductive Win : List Nat → Prop38  | intro (p q : List Nat) : Move p q → Lose q → Win p

Project declarations in the statement: none

Project declarations used by the proof or definition body

Game.Lose, Game.Move

def `AC0.Circ.depth`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 61–66

61def depth : Circ → Nat62  | input _ => 063  | const _ => 064  | not c => depth c + 165  | and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 166  | or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => depth c)) + 1

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.listMax, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

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

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

One more than the largest input index used (0 if none).

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 68–74

68/-- One more than the largest input index used (0 if none). -/69def maxInput : Circ → Nat70  | input i => i + 171  | const _ => 072  | not c => maxInput c73  | and cs => listMax (cs.attach.map (fun ⟨c, _⟩ => maxInput c))74  | or cs => listMax (cs.attach.map (fun ⟨c, _⟩ => maxInput 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.listMax, AC0.Circ.not, AC0.Circ.or, AC0.Circ.rec, AC0.Circ.rec_1

def `AC0.Circ.size`

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

Statement as elaborated and printed by Lean 4.26.0

NimAudit.AC0.Circ → ℕ

Exact source text, lines 51–56

51def size : Circ → Nat52  | input _ => 153  | const _ => 154  | not c => size c + 155  | and cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 156  | or cs => (cs.attach.map (fun ⟨c, _⟩ => size c)).sum + 1

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

inductive `BinReadout.BBound`

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

Resource bounds for binary readout formulas.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → ℕ → ℕ → ℕ → ℕ → ℕ → Prop

Exact source text, lines 131–144

131/-- Resource bounds for binary readout formulas. -/132structure BBound (R : BCirc) (N B r d s : Nat) : Prop where133  idx_len : R.idx.length = r134  val_len : R.val.length = B135  width : N ≤ 2 ^ r136  depth_valid : depth R.valid ≤ d137  depth_idx : ∀ c ∈ R.idx, depth c ≤ d138  depth_val : ∀ c ∈ R.val, depth c ≤ d139  size_valid : size R.valid ≤ s140  size_idx : ∀ c ∈ R.idx, size c ≤ s141  size_val : ∀ c ∈ R.val, size c ≤ s142  max_valid : maxInput R.valid ≤ B * N143  max_idx : ∀ c ∈ R.idx, maxInput c ≤ B * N144  max_val : ∀ c ∈ R.val, maxInput c ≤ B * N

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

AC0.Circ, AC0.Circ.depth, AC0.Circ.maxInput, AC0.Circ.size, BinReadout.BCirc, BinReadout.BCirc.idx, BinReadout.BCirc.val, BinReadout.BCirc.valid

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

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

Parity of all bits.

Statement as elaborated and printed by Lean 4.26.0

List Bool → Bool

Exact source text, lines 348–351

348/-- Parity of all bits. -/349def par : List Bool → Bool350  | [] => false351  | b :: bs => xor b (par bs)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

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

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

Strong mastery on 2-bit boards with N heaps: from every winning position the selector outputs a legal move to a losing position.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → ℕ → Prop

Exact source text, lines 27–31

27/-- Strong mastery on 2-bit boards with N heaps: from every winning position the28    selector outputs a legal move to a losing position. -/29def StrongMastery (S : BCirc) (N : Nat) : Prop :=30  ∀ P : List Nat, P.length = N → Width 2 P → Win P →31    ∃ i v x, binMove S N P = some (i, v) ∧ P[i]? = some x ∧ v < x ∧ Lose (P.set i v)

Project declarations in the statement: BinReadout.BCirc

Project declarations used by the proof or definition body

BinReadout.BCirc, Game.Lose, Game.Width, Game.Win, ParityCircuit.binMove

def `ParityCircuit.parityFormula`

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

The parity formula extracted from a selector: the low value bit, restricted to the encoded boards.

Statement as elaborated and printed by Lean 4.26.0

NimAudit.BinReadout.BCirc → ℕ → NimAudit.AC0.Circ

Exact source text, lines 123–125

123/-- The parity formula extracted from a selector: the low value bit, restricted to124    the encoded boards. -/125def parityFormula (S : BCirc) (m : Nat) : Circ := subst (parSubst m) (getC S.val 1)

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

Project declarations used by the proof or definition body

AC0.Circ.subst, BinReadout.BCirc, BinReadout.BCirc.val, CorrBridge.getC, ParityCircuit.parSubst

Full modules

Module	File	Lines	Imports
BinaryReadout	`lean/phase4/BinaryReadout.lean`	333	FiniteNet, NimCorrBridge
BitBridge	`lean/phase3/BitBridge.lean`	560	Circuit
Circuit	`lean/phase3/Circuit.lean`	1151	NimProbability
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
ParityCircuit	`lean/phase4/ParityCircuit.lean`	259	BinaryReadout

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 (reduction)Strong mastery on the boards (2,b₁,…,b_m) forces the winning move to reveal the parity of b

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Game.unique_zero_move

theorem Game.winning_selector_parity

theorem ParityCircuit.extraction

Definitions these statements use

def Game.encode

def Game.reduced

def Game.Move

def nimSum

inductive Game.Lose

inductive Game.Win

def AC0.Circ.depth

def AC0.Circ.eval

def AC0.Circ.maxInput

def AC0.Circ.size

inductive BinReadout.BBound

inductive BinReadout.BCirc

def Bridge.par

def Bridge.vfun

def ParityCircuit.StrongMastery

def ParityCircuit.parityFormula

Full modules

theorem `Game.unique_zero_move`

theorem `Game.winning_selector_parity`

theorem `ParityCircuit.extraction`

def `Game.encode`

def `Game.reduced`

def `Game.Move`

def `nimSum`

inductive `Game.Lose`

inductive `Game.Win`

def `AC0.Circ.depth`

def `AC0.Circ.eval`

def `AC0.Circ.maxInput`

def `AC0.Circ.size`

inductive `BinReadout.BBound`

inductive `BinReadout.BCirc`

def `Bridge.par`

def `Bridge.vfun`

def `ParityCircuit.StrongMastery`

def `ParityCircuit.parityFormula`