Proposition 5.10One fixed structured head reveals only known affine functions of one linear functional of σ(P)

With a single fixed head, every allowed query returns the same unknown bit up to a known correction. At the root, the outcome is $\ell_j(\sigma)$. If one heap changes from $h$ to $h'$ (for example when evaluating a candidate move), the nim-sum changes by $h\oplus h'$, and by linearity the outcome becomes $\ell_j(\sigma)\oplus\ell_j(h\oplus h')$, where the correction is computable from the known heap values.

So one channel yields one unknown bit of the $B$-bit invariant, however often it is queried in this way.

Caveat: this concerns one member of the structured family, not arbitrary rollout policies.

• Prob.rollout_outcome_linear: the executed outcome of $\pi_j$ equals $\langle w_j,\sigma(P)\rangle$.
• Prob.single_policy_affine: if $P'$ differs from $P$ in one heap $h\to h'$, then $\mathrm{RO}_{\pi_j}(P') = \mathrm{RO}_{\pi_j}(P)\oplus\langle w_j, h\oplus h'\rangle$.
• Misc.single_policy_correction: the same with the channel function.

Principal declarations

∀ {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]

∀ {B j : ℕ},
  j < B →
    ∀ (pre post : List ℕ) (h h' : ℕ),
      NimAudit.Game.rolloutWinner j (pre ++ h' :: post) =
        (NimAudit.Game.rolloutWinner j (pre ++ h :: post) ^^
          NimAudit.Prob.dotB B (NimAudit.Prob.headVec j) (h ^^^ h'))

925/-- SINGLE-POLICY INFORMATION BOUND (paper Prop. single-policy-bound): if P' differs926    from P in one heap h -> h', then RO_{pi_j}(P') = RO_{pi_j}(P) XOR <w_j, h XOR h'>,927    a correction bit computable from the known heap values. -/928theorem single_policy_affine {B j : Nat} (hj : j < B) (pre post : List Nat) (h h' : Nat) :929    rolloutWinner j (pre ++ h' :: post) =930      xor (rolloutWinner j (pre ++ h :: post)) (dotB B (headVec j) (h ^^^ h')) := by931  rw [rollout_outcome_linear hj, rollout_outcome_linear hj, nimSum_move, dotB_xor_right]

∀ (j : ℕ) (pre post : List ℕ) (h h' : ℕ),
  NimAudit.Game.rolloutWinner j (pre ++ h' :: post) =
    (NimAudit.Game.rolloutWinner j (pre ++ h :: post) ^^ NimAudit.channel j (h ^^^ h'))

718theorem single_policy_correction (j : Nat) (pre post : List Nat) (h h' : Nat) :719    rolloutWinner j (pre ++ h' :: post) = xor (rolloutWinner j (pre ++ h :: post)) (channel j (h ^^^ h')) := by720  rw [rolloutWinner_channel, rolloutWinner_channel, one_heap_update pre post h h', Nat.xor_assoc, channel_xor]

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

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

ℕ → ℕ → Bool

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

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