Section 7.3, “Training the rollout heads”Every tie-breaking rule gives the same rollout length, hence the same outcome bit

When several heaps qualify for the same move of $\pi_j$ (for example several heaps of size at least $2^j$), the choice does not matter for the outcome: every complete rollout has the same number of moves, $\sum_i\lfloor h_i/2^j\rfloor+\sum_i(h_i\bmod2^j)$, whichever eligible heap is used each time. So the training labels can spread probability evenly over all equivalent actions without changing the channel bit.

Rollout.run_length: every complete run of $\pi_j$ (Rollout.Run, built from Rollout.PolicyMove steps with arbitrary tie-breaking) has exactly that length. Rollout.run_parity: its parity is the channel bit of the nim-sum.

Principal declarations

∀ {j : ℕ} {p : List ℕ} {n : ℕ}, NimAudit.Rollout.Run j p n → n = NimAudit.rolloutCount j p

88/-- EXECUTION COUNT: every complete run of `pi_j`, under any tie-breaking rule,89    has exactly `sum_h (h / 2^j + h % 2^j)` moves. -/90theorem run_length {j : Nat} {p : List Nat} {n : Nat} (hr : Run j p n) :91    n = rolloutCount j p := by92  induction hr with93  | done p hz => exact (rolloutCount_zero hz).symm94  | step p q n hm _ ih => rw [ih, policyMove_count hm]

∀ {j : ℕ} {p : List ℕ} {n : ℕ},
  NimAudit.Rollout.Run j p n → n.testBit 0 = NimAudit.channel j (NimAudit.nimSum p)

96/-- PARITY OF EXECUTION: the number of moves of any complete run of `pi_j` has97    low bit equal to the channel value of the nim-sum98    (bit 0 for j = 0; bit j XOR bit 0 for j ≥ 1). -/99theorem run_parity {j : Nat} {p : List Nat} {n : Nat} (hr : Run j p n) :100    n.testBit 0 = channel j (nimSum p) := by101  rw [run_length hr]102  exact rollout_count_channel j p

Definitions these statements use

ℕ → List ℕ → ℕ → Prop

34/-- `Run j p n`: following `pi_j` from board `p` reaches the all-zero board after35    exactly `n` policy moves. -/36inductive Run (j : Nat) : List Nat → Nat → Prop37  | done (p : List Nat) : (∀ x ∈ p, x = 0) → Run j p 038  | step (p q : List Nat) (n : Nat) : PolicyMove j p q → Run j q n → Run j p (n + 1)

ℕ → List ℕ → List ℕ → Prop

28/-- One legal move of the structured policy `pi_j` (tie-breaking unspecified). -/29def PolicyMove (j : Nat) (p q : List Nat) : Prop :=30  (∃ pre x post, p = pre ++ x :: post ∧ 2 ^ j ≤ x ∧ q = pre ++ (x - 2 ^ j) :: post) ∨31  ((∀ x ∈ p, x < 2 ^ j) ∧32    ∃ pre x post, p = pre ++ x :: post ∧ 0 < x ∧ q = pre ++ (x - 1) :: post)

ℕ → List ℕ → ℕ

82def rolloutCount (j : Nat) (rows : List Nat) : Nat := (rows.map (heapCount j)).sum

ℕ → ℕ → Bool

77def channel (j sigma : Nat) : Bool :=78  if j = 0 then sigma.testBit 0 else xor (sigma.testBit j) (sigma.testBit 0)

List ℕ → ℕ

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

Full modules

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