Appendix GFull proof of Proposition 5.9: rollout counts, outcome identities, selector, winning, step bound

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]

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

224/-- RECONSTRUCTION: on a B-bit board (any N, including the empty and terminal225    boards), the B rollout outcomes determine the full nim-sum. -/226theorem reconstruct_eq {B : Nat} {p : List Nat} (hw : Width B p) :227    reconstruct B (outcomes p) = nimSum p := by228  apply Nat.eq_of_testBit_eq229  intro i230  rw [reconstruct, testBit_ofBits]231  by_cases hi : i < B232  · simp only [hi, decide_true, Bool.true_and, recoverBit, outcomes, rolloutWinner_channel]233    by_cases h0 : i = 0234    · subst h0; simp [channel]235    · simp only [h0, if_false, channel, if_true]236      cases (nimSum p).testBit i <;> cases (nimSum p).testBit 0 <;> rfl237  · simp only [hi, decide_false, Bool.false_and]238    symm239    apply Nat.testBit_lt_two_pow240    exact Nat.lt_of_lt_of_le (nimSum_lt hw) (Nat.pow_le_pow_right (by decide) (by omega))

281/-- LEGAL MOVE TO ZERO: if the nim-sum `s` is nonzero, some heap `x` has282    `x ^^^ s < x`; replacing it by `x ^^^ s` is a legal Nim move and, by283    `move_to_zero_algebra`, yields nim-sum zero. -/284theorem exists_decreasing_heap (p : List Nat) (hs : nimSum p ≠ 0) :285    ∃ pre x post, p = pre ++ x :: post ∧ x ^^^ nimSum p < x ∧286      nimSum (pre ++ (x ^^^ nimSum p) :: post) = 0 := by287  let s := nimSum p288  let k := s.log2289  have htop : s.testBit k = true := by290    cases hb : s.testBit k with291    | true => rfl292    | false =>293      exfalso294      have hlt : s < 2 ^ k := by295        apply Nat.lt_pow_two_of_testBit296        intro i hi297        by_cases hik : i = k298        · subst hik; exact hb299        · apply Nat.testBit_lt_two_pow300          exact Nat.lt_of_lt_of_le Nat.lt_log2_self (Nat.pow_le_pow_right (by decide) (by omega))301      exact absurd (Nat.log2_self_le hs) (Nat.not_le.mpr hlt)302  have habove : ∀ i, k < i → s.testBit i = false := by303    intro i hi304    apply Nat.testBit_lt_two_pow305    exact Nat.lt_of_lt_of_le Nat.lt_log2_self (Nat.pow_le_pow_right (by decide) (by omega))306  obtain ⟨x, hxmem, hxk⟩ := exists_heap_testBit htop307  have hlt : x ^^^ s < x := by308    apply lt_of_top_testBit (k := k)309    · rw [Nat.testBit_xor, hxk, htop]; rfl310    · exact hxk311    · intro i hi312      rw [Nat.testBit_xor, habove i hi, Bool.xor_false]313  obtain ⟨pre, post, rfl⟩ := List.append_of_mem hxmem314  exact ⟨pre, x, post, rfl, hlt, move_to_zero_algebra pre post x⟩

376/-- END-TO-END STRATEGY GUARANTEE (Target 1C): on B-bit boards, the agent that377    queries the B structured rollouts, reconstructs the nim-sum and plays the378    selected move wins from every nonzero-nim-sum position against every legal379    opponent. -/380theorem agent_wins {B : Nat} (p : List Nat) (hw : Width B p) (h : nimSum p ≠ 0) :381    Wins (agent B) p := by382  obtain ⟨q, hsel, hm, hq⟩ := selectMove_zero h383  refine Wins.intro p q (by rw [agent_eq hw]; exact hsel) hm ?_384  intro r hr385  have h1 := move_sum_lt hm386  have h2 := move_sum_lt hr387  exact agent_wins r (width_move (width_move hw hm) hr) (move_from_zero hr hq)388termination_by p.sum

454theorem totalRolloutMoves_le {B : Nat} {p : List Nat} (hw : Width B p) :455    totalRolloutMoves B p ≤ B * (p.length * (2 ^ B - 1)) := by456  unfold totalRolloutMoves457  have key : ∀ k, ((List.range k).map (fun j => rolloutMoves j p)).sum ≤458      k * (p.length * (2 ^ B - 1)) := by459    intro k460    induction k with461    | zero => simp462    | succ k ih =>463      rw [List.range_succ, List.map_append, List.sum_append_nat, Nat.succ_mul]464      simp only [List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, Nat.add_zero]465      have := rolloutMoves_le (j := k) hw466      omega467  exact key B