Section 7.3, paragraph 3 (arithmetic)For k=4, the r₀ classifier detects 8 of 15 nonzero nim-sums; balanced accuracy 23/30

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

1 Paper text

Single-head baseline. The single-head baseline achieves 0.768 overall accuracy and 0.536 N-position recall. These numbers have an exact theoretical explanation. With $k=4$ bits, an N-position has nim-sum $\sigma \in \{1,\dots,15\}$ . Of these 15 values, exactly 8 are odd ( $\sigma_0 = 1$ : the values $1,3,5,7,9,11,13,15$ ) and 7 are even ( $\sigma_0 = 0$ ). Head $\pi_0$ detects an N-position only when $\sigma_0 = 1$ , so the theoretical N-position recall is $8/15 \approx 0.533$ (observed: 0.536 on the finite test set). All P-positions are correctly classified (since $\sigma = 0$ implies $\sigma_0 = 0$ ), so on a balanced test set the overall accuracy is $\tfrac{1}{2}\cdot 1 + \tfrac{1}{2}\cdot\tfrac{8}{15} = \tfrac{23}{30} \approx 0.767$ (observed: 0.768). This calculation describes the particular classifier that declares an N-position exactly when $r_0=1$ . It is not the winning-move success bound of Theorem 5.12(i), and does not establish a limit on arbitrary classifiers or rollout policies.

Generated from paper_jmlr.tex, lines 1181–1187.

2 Explain this

The single-head baseline declares " $N$ -position" exactly when $r_0=\sigma_0=1$ . With 4 bits there are 15 nonzero nim-sums, of which 8 are odd: $1,3,5,\dots,15$ . So the classifier detects $8/15\approx0.533$ of $N$ -positions and never errs on $P$ -positions ( $\sigma=0$ has $\sigma_0=0$ ). On a balanced set its accuracy is $\tfrac12\cdot1+\tfrac12\cdot\tfrac8{15}=\tfrac{23}{30}\approx0.767$ .

Caveat: this describes that particular classifier. It is not the winning-move bound of Theorem 5.12 and not a limit on other classifiers.

3 How this is formalised

Misc.detected_count: among the $2^B-1$ nonzero $B$ -bit values exactly $2^{B-1}$ are odd.
Misc.baseline_numbers: for $B=4$ : $8$ odd values, $15$ nonzero values, and $\tfrac12\cdot1+\tfrac12\cdot\tfrac8{15}=\tfrac{23}{30}$ .
Misc.baseline_P: the classifier never errs on $P$ -positions.
Misc.board_recall: for uniformly random boards the detected fraction among nonzero nim-sums is $2^{B-1}/(2^B-1)$ , so the value-level ratio is also the board-level ratio.

Coverage record
Paper anchor	`par-results-p3` (website anchor; the manuscript has no label here)
Displayed as	Section 7.3, paragraph 3 (arithmetic)
Claim	For k=4, the r₀ classifier detects 8 of 15 nonzero nim-sums; balanced accuracy 23/30
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1181–1187; SHA-256 of the normalised block source `e23068ca456c51b6…`
Lean declarations	`NimAudit.Misc.detected_count` (Misc, lines 502–516, file `07766c03566d…`) `NimAudit.Misc.baseline_numbers` (Misc, lines 518–522, file `07766c03566d…`) `NimAudit.Misc.baseline_P` (Misc, lines 524–526, file `07766c03566d…`) `NimAudit.Misc.board_recall` (Misc, lines 757–767, file `07766c03566d…`)
Audited correspondence rows	`sec:supervised-restoration`, `sec:exp-fsm-shootout`
Explanations	`explain/c-baseline-arith`, `formal/c-baseline-arith`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `Misc.detected_count`

Module Misc (lean/phase6/Misc.lean, lines 502–516) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Among the 2^B − 1 nonzero nim-sums of B ≥ 1 bits, exactly 2^{B−1} have σ₀ = 1, i.e. are detected by the classifier "declare N iff r₀ = 1" (r₀ = σ₀).

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ},
  1 ≤ B →
    (List.filter (fun σ => σ % 2 == 1) (List.range (2 ^ B))).length = 2 ^ (B - 1) ∧
      (List.filter (fun σ => σ != 0) (List.range (2 ^ B))).length = 2 ^ B - 1

Exact source text, lines 502–516

502/-- Among the 2^B − 1 nonzero nim-sums of B ≥ 1 bits, exactly 2^{B−1} have σ₀ = 1, i.e.503    are detected by the classifier "declare N iff r₀ = 1" (r₀ = σ₀). -/504theorem detected_count {B : Nat} (hB : 1 ≤ B) :505    ((List.range (2 ^ B)).filter (fun σ => σ % 2 == 1)).length = 2 ^ (B - 1) ∧506    ((List.range (2 ^ B)).filter (fun σ => σ != 0)).length = 2 ^ B - 1 := by507  obtain ⟨k, rfl⟩ : ∃ k, B = k + 1 := ⟨B - 1, by omega⟩508  refine ⟨by rw [Nat.pow_succ, Nat.mul_comm, show k + 1 - 1 = k by omega]; exact odd_count _, ?_⟩509  have : ∀ n, ((List.range (n + 1)).filter (fun σ => σ != 0)).length = n := by510    intro n511    induction n with512    | zero => rfl513    | succ n ih => rw [List.range_succ, List.filter_append, List.length_append, ih]; simp514  have hp : 2 ^ (k + 1) = (2 ^ (k + 1) - 1) + 1 := by have := Nat.one_le_two_pow (n := k + 1); omega515  have h2 := this (2 ^ (k + 1) - 1)516  rw [← hp] at h2; exact h2

Project declarations in the statement: none

Project declarations used by the proof or definition body

Misc.odd_count

theorem `Misc.baseline_numbers`

Module Misc (lean/phase6/Misc.lean, lines 518–522) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Statement as elaborated and printed by Lean 4.26.0

(List.filter (fun σ => σ % 2 == 1) (List.range (2 ^ 4))).length = 8 ∧
  (List.filter (fun σ => σ != 0) (List.range (2 ^ 4))).length = 15 ∧
    1 / 2 * 1 + 1 / 2 * (8 / 15) = 23 / 30

Exact source text, lines 518–522

518theorem baseline_numbers :519    ((List.range (2 ^ 4)).filter (fun σ => σ % 2 == 1)).length = 8 ∧520    ((List.range (2 ^ 4)).filter (fun σ => σ != 0)).length = 15 ∧521    (1 / 2 : Rat) * 1 + 1 / 2 * (8 / 15) = 23 / 30 := by522  refine ⟨by decide, by decide, by grind⟩

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

theorem `Misc.baseline_P`

Module Misc (lean/phase6/Misc.lean, lines 524–526) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext, Quot.sound

The r₀ classifier never errs on P-positions: σ = 0 has σ₀ = 0.

Statement as elaborated and printed by Lean 4.26.0

∀ (P : List ℕ), NimAudit.nimSum P = 0 → NimAudit.Game.rolloutWinner 0 P = false

Exact source text, lines 524–526

524/-- The r₀ classifier never errs on P-positions: σ = 0 has σ₀ = 0. -/525theorem baseline_P (P : List Nat) (h : nimSum P = 0) : rolloutWinner 0 P = false := by526  rw [rolloutWinner_channel, h]; simp [channel]

Project declarations in the statement: Game.rolloutWinner, nimSum

Project declarations used by the proof or definition body

Game.rolloutWinner, Game.rolloutWinner_channel, channel, nimSum

theorem `Misc.board_recall`

Module Misc (lean/phase6/Misc.lean, lines 757–767) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

BOARD-LEVEL RECALL OF THE r₀ CLASSIFIER: among uniform boards with nonzero nim-sum the detected fraction is 2^{B−1}/(2^B − 1); for B = 4 it is 8/15.

Statement as elaborated and printed by Lean 4.26.0

∀ {B : ℕ},
  1 ≤ B →
    ∀ (N : ℕ),
      (NimAudit.Prob.rsum (NimAudit.Prob.boards (2 ^ B) (N + 1)) fun P =>
            if (NimAudit.nimSum P % 2 == 1) = true then 1 else 0) =
          ↑(2 ^ (B - 1)) * ↑(2 ^ B) ^ N ∧
        (NimAudit.Prob.rsum (NimAudit.Prob.boards (2 ^ B) (N + 1)) fun P =>
            if (NimAudit.nimSum P != 0) = true then 1 else 0) =
          ↑(2 ^ B - 1) * ↑(2 ^ B) ^ N

Exact source text, lines 757–767

757/-- BOARD-LEVEL RECALL OF THE r₀ CLASSIFIER: among uniform boards with nonzero nim-sum the758    detected fraction is 2^{B−1}/(2^B − 1); for B = 4 it is 8/15. -/759theorem board_recall {B : Nat} (hB : 1 ≤ B) (N : Nat) :760    rsum (boards (2 ^ B) (N + 1)) (fun P => if (nimSum P % 2 == 1) then 1 else 0) =761      ((2 ^ (B - 1) : Nat) : Rat) * ((2 ^ B : Nat) : Rat) ^ N ∧762    rsum (boards (2 ^ B) (N + 1)) (fun P => if (nimSum P != 0) then 1 else 0) =763      ((2 ^ B - 1 : Nat) : Rat) * ((2 ^ B : Nat) : Rat) ^ N := by764  obtain ⟨h1, h2⟩ := detected_count hB765  refine ⟨?_, ?_⟩766  · rw [boards_count B N (fun σ => σ % 2 == 1), h1]767  · rw [boards_count B N (fun σ => σ != 0), h2]

Project declarations in the statement: Prob.boards, Prob.rsum, nimSum

Project declarations used by the proof or definition body

Misc.boards_count, Misc.detected_count, Prob.boards, Prob.rsum, nimSum

Definitions these statements use

def `Game.rolloutWinner`

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

Rollout outcome RO_{pi_j}(P) as a game: both players follow pi_j; the result is `true` iff the player to move at P (the first player) wins under normal play. At a terminal start it is `false`.

Statement as elaborated and printed by Lean 4.26.0

ℕ → List ℕ → Bool

Exact source text, lines 142–152

142/-- Rollout outcome RO_{pi_j}(P) as a game: both players follow pi_j; the result is143    `true` iff the player to move at P (the first player) wins under normal play.144    At a terminal start it is `false`. -/145def rolloutWinner (j : Nat) (p : List Nat) : Bool :=146  match h : policyStep j p with147  | none => false148  | some q => !rolloutWinner j q149termination_by rolloutCount j p150decreasing_by151  have := policyMove_count (policyStep_some h)152  omega

Project declarations in the statement: none

Project declarations used by the proof or definition body

Rollout.policyMove_count, Rollout.policyStep, Rollout.policyStep_some, rolloutCount

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

Module NimProbability (lean/phase2/NimProbability.lean, lines 194–197) · file SHA-256 1d5d7977a43e854d…

All boards of N heaps with values below q (each exactly once).

Statement as elaborated and printed by Lean 4.26.0

ℕ → ℕ → List (List ℕ)

Exact source text, lines 194–197

194/-- All boards of N heaps with values below q (each exactly once). -/195def boards (q : Nat) : Nat → List (List Nat)196  | 0 => [[]]197  | N + 1 => (List.range q).flatMap (fun h => (boards q N).map (h :: ·))

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Prob.rsum`

Module NimProbability (lean/phase2/NimProbability.lean, lines 33–33) · file SHA-256 1d5d7977a43e854d…

Statement as elaborated and printed by Lean 4.26.0

{α : Type} → List α → (α → ℚ) → ℚ

Exact source text, lines 33–33

33def rsum {α : Type} (l : List α) (f : α → Rat) : Rat := (l.map f).sum

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

Full modules

Module	File	Lines	Imports
Misc	`lean/phase6/Misc.lean`	912	Bypass
NimCore	`lean/NimCore.lean`	139	`Std`
NimGame	`lean/phase2/NimGame.lean`	634	NimRollout
NimProbability	`lean/phase2/NimProbability.lean`	1074	NimGame

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 7.3, paragraph 3 (arithmetic)For k=4, the r₀ classifier detects 8 of 15 nonzero nim-sums; balanced accuracy 23/30

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem Misc.detected_count

theorem Misc.baseline_numbers

theorem Misc.baseline_P

theorem Misc.board_recall

Definitions these statements use

def Game.rolloutWinner

def nimSum

def Prob.boards

def Prob.rsum

Full modules

theorem `Misc.detected_count`

theorem `Misc.baseline_numbers`

theorem `Misc.baseline_P`

theorem `Misc.board_recall`

def `Game.rolloutWinner`

def `nimSum`

def `Prob.boards`

def `Prob.rsum`