Section 5.4, paragraph 3With arbitrary start positions, one rollout of π₀ on the boards of k-th bits returns σ_k(P)

If the planner could start rollouts anywhere, the restriction would be meaningless. Example: build the board whose heaps are the $k$-th bits of the heaps of $P$ (each heap becomes $0$ or $1$). A rollout of $\pi_0$ on it removes one stone per move, so the outcome is the parity of the number of ones, which is bit $k$ of the nim-sum of $P$. Doing this for each $k$ recovers the whole nim-sum with one policy. So the lower bound must restrict queries.

Misc.bitBoard_query: one rollout of $\pi_0$ on the board of $k$-th bits of $P$ returns $\sigma_k(P)$; Misc.nimSum_bitBoard is the underlying identity (the low bit of that board's nim-sum is bit $k$ of $\operatorname{nim}(P)$).

Principal declarations

∀ (k : ℕ) (P : List ℕ),
  NimAudit.Game.rolloutWinner 0 (List.map (fun h => if h.testBit k = true then 1 else 0) P) =
    (NimAudit.nimSum P).testBit k

843/-- WHY ARBITRARY START POSITIONS ARE EXCLUDED (Definition def:agent-types): a single844    rollout of π₀ on the board whose heaps are the k-th bits of P returns σ_k(P). -/845theorem bitBoard_query (k : Nat) (P : List Nat) :846    rolloutWinner 0 (P.map (fun h => if h.testBit k then 1 else 0)) = (nimSum P).testBit k := by847  rw [rolloutWinner_channel]; simp only [channel, if_true]; exact nimSum_bitBoard k P

∀ (k : ℕ) (P : List ℕ),
  (NimAudit.nimSum (List.map (fun h => if h.testBit k = true then 1 else 0) P)).testBit 0 =
    (NimAudit.nimSum P).testBit k

834theorem nimSum_bitBoard (k : Nat) : ∀ P : List Nat,835    (nimSum (P.map (fun h => if h.testBit k then 1 else 0))).testBit 0 = (nimSum P).testBit k836  | [] => by simp [nimSum]837  | h :: P => by838    have ih := nimSum_bitBoard k P839    simp only [List.map_cons, nimSum] at ih ⊢840    rw [Nat.testBit_xor, Nat.testBit_xor, ih]841    by_cases hb : h.testBit k <;> simp [hb]

Definitions these statements use

ℕ → List ℕ → Bool

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

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