Definition 5.6Deterministic rollout policies and the rollout outcome bit

A rollout policy is a deterministic rule that, given a board, names one legal move. A rollout lets both players follow that same rule from a start position until the board is empty; the only thing reported back is one bit: did the first player win (make the last move)?

Example: the policy $\pi_0$ "subtract 1 from the leftmost nonzero heap" played from $(2,1)$ goes $(2,1)\to(1,1)\to(0,1)\to(0,0)$: three moves, so the first player wins and the outcome bit is $1$.

Why only one bit: this isolates how much information repeated simulation can expose, without letting the interface pass whole trajectories or move counts to the planner.

Lean formalises the structured policies $\pi_j$ that the results use. A legal $\pi_j$ step (Rollout.PolicyMove) subtracts $2^j$ from some heap of size at least $2^j$, or, when every heap is below $2^j$, subtracts $1$ from some nonzero heap; the tie-breaking rule is left arbitrary. Rollout.policyStep is the concrete first-eligible-heap version, and Game.rolloutWinner executes the rollout and returns whether the first player made the last move. Prob.rollout_outcome_linear proves that this executed outcome equals the linear functional $\langle w_j,\sigma(P)\rangle$ of the nim-sum.

The general notion of an arbitrary AC⁰-bounded rollout policy is not a separate Lean object; no result depends on it.

Principal declarations

ℕ → 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 ℕ → Option (List ℕ)

116/-- One step of `pi_j` with first-eligible tie-breaking; `none` means no move. -/117def policyStep (j : Nat) (p : List Nat) : Option (List Nat) :=118  match subFirstGe (2 ^ j) p with119  | some q => some q120  | none => subFirstPos p

ℕ → 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)

∀ {B j : ℕ},
  j < B →
    ∀ (P : List ℕ),
      NimAudit.Game.rolloutWinner j P =
        NimAudit.Prob.dotB B (NimAudit.Prob.headVec j) (NimAudit.nimSum P)

920/-- RO_{pi_j}(P), the executed rollout outcome, is the linear functional <w_j, sigma(P)>. -/921theorem rollout_outcome_linear {B j : Nat} (hj : j < B) (P : List Nat) :922    rolloutWinner j P = dotB B (headVec j) (nimSum P) := by923  rw [rolloutWinner_channel, head_linear hj]

Definitions these statements use

ℕ → ℕ → ℕ → Bool

259/-- The F_2 inner product of the first B bits of u and v. -/260def dotB : Nat → Nat → Nat → Bool261  | 0, _, _ => false262  | B + 1, u, v => xor (dotB B u v) (u.testBit B && v.testBit B)

ℕ → ℕ

875/-- The vector w_j with RO_{pi_j}(P) = <w_j, sigma(P)>: w_0 = 1, w_j = 2^j XOR 1. -/876def headVec (j : Nat) : Nat := if j = 0 then 1 else 2 ^ j ^^^ 1

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