NimGame

Comment and keyword shading is a reading aid only. It is not a verification marker; the evidence is the build record on the Build page.

1import NimRollout23/- Phase 2, targets 1 and 2.  Written by Claude for the independent review4   (9 October 2026).  Lean 4.26.0, core/Std only.  Imports the unchanged5   NimCore.lean and NimRollout.lean.67   Target 1  Normal-play semantics of Nim, the classical characterisation8             (losing iff nim-sum zero), reconstruction of the nim-sum from the B9             structured rollout outcomes, a deterministic move selector driven by10             that reconstruction, and the adversarial guarantee: the selector wins11             from every nonzero position against every legal opponent.  Also the12             finite bound B*N*(2^B-1) on simulated rollout moves.13   Target 2  The parity reduction on boards (2, b_1, ..., b_m).1415   Nothing here formalises circuits, AC0, or probability. -/1617namespace NimAudit18namespace Game1920open Rollout2122/-! ## Target 1A: legal moves and normal-play semantics -/2324/-- An ordinary legal Nim move: exactly one heap strictly decreases. -/25def Move (p q : List Nat) : Prop :=26  ∃ pre x post y, p = pre ++ x :: post ∧ q = pre ++ y :: post ∧ y < x2728/-- Terminal board: every heap is empty. -/29def Terminal (p : List Nat) : Prop := ∀ x ∈ p, x = 03031/-- B-bit board: every heap is below 2^B. -/32def Width (B : Nat) (p : List Nat) : Prop := ∀ x ∈ p, x < 2 ^ B3334/- Normal play: `Win p` (an N-position) and `Lose p` (a P-position), for the35   player to move.  A player who cannot move loses. -/36mutual37inductive Win : List Nat → Prop38  | intro (p q : List Nat) : Move p q → Lose q → Win p39inductive Lose : List Nat → Prop40  | intro (p : List Nat) : (∀ q, Move p q → Win q) → Lose p41end4243theorem move_sum_lt {p q : List Nat} (hm : Move p q) : q.sum < p.sum := by44  obtain ⟨pre, x, post, y, rfl, rfl, hlt⟩ := hm45  simp only [List.sum_append_nat, List.sum_cons]46  omega4748theorem terminal_iff_no_move (p : List Nat) : Terminal p ↔ ∀ q, ¬ Move p q := by49  constructor50  · intro ht q ⟨pre, x, post, y, hp, _, hlt⟩51    have : x = 0 := ht x (by rw [hp]; simp)52    omega53  · intro hno x hx54    obtain ⟨pre, post, rfl⟩ := List.append_of_mem hx55    by_cases h0 : x = 056    · exact h057    · exact absurd ⟨pre, x, post, 0, rfl, rfl, by omega⟩ (hno (pre ++ 0 :: post))5859theorem terminal_lose {p : List Nat} (ht : Terminal p) : Lose p :=60  Lose.intro p (fun q hm => absurd hm ((terminal_iff_no_move p).1 ht q))6162theorem xor_eq_zero_imp {x y : Nat} (h : x ^^^ y = 0) : x = y := by63  have := xor_cancel_left x y64  rw [h, Nat.xor_zero] at this65  exact this6667theorem nimSum_move {pre post : List Nat} {x y : Nat} :68    nimSum (pre ++ y :: post) = nimSum (pre ++ x :: post) ^^^ (x ^^^ y) := by69  rw [one_heap_update pre post x y, Nat.xor_assoc]7071/-- Every legal move from a zero-nim-sum board reaches a nonzero nim-sum. -/72theorem move_from_zero {p q : List Nat} (hm : Move p q) (h0 : nimSum p = 0) :73    nimSum q ≠ 0 := by74  obtain ⟨pre, x, post, y, rfl, rfl, hlt⟩ := hm75  rw [nimSum_move, h0, Nat.zero_xor]76  intro h77  have := xor_eq_zero_imp h78  omega7980/-- From a nonzero nim-sum there is a legal move to nim-sum zero (from NimRollout). -/81theorem exists_move_to_zero {p : List Nat} (h : nimSum p ≠ 0) :82    ∃ q, Move p q ∧ nimSum q = 0 := by83  obtain ⟨pre, x, post, rfl, hlt, hz⟩ := exists_decreasing_heap p h84  exact ⟨_, ⟨pre, x, post, _, rfl, rfl, hlt⟩, hz⟩8586theorem lose_of_zero_win_of_ne (p : List Nat) :87    (nimSum p = 0 → Lose p) ∧ (nimSum p ≠ 0 → Win p) := by88  constructor89  · intro h90    exact Lose.intro p (fun q hm =>91      have := move_sum_lt hm92      (lose_of_zero_win_of_ne q).2 (move_from_zero hm h))93  · intro h94    obtain ⟨q, hm, hq⟩ := exists_move_to_zero h95    have := move_sum_lt hm96    exact Win.intro p q hm ((lose_of_zero_win_of_ne q).1 hq)97termination_by p.sum9899theorem not_win_and_lose (p : List Nat) (hw : Win p) (hl : Lose p) : False := by100  cases hw with101  | intro _ q hm hlq =>102    cases hl with103    | intro _ hall =>104      have := move_sum_lt hm105      exact not_win_and_lose q (hall q hm) hlq106termination_by p.sum107108/-- CLASSICAL CHARACTERISATION (paper Theorem nim-win). -/109theorem lose_iff (p : List Nat) : Lose p ↔ nimSum p = 0 := by110  constructor111  · intro hl112    by_cases h : nimSum p = 0113    · exact h114    · exact (not_win_and_lose p ((lose_of_zero_win_of_ne p).2 h) hl).elim115  · exact (lose_of_zero_win_of_ne p).1116117theorem win_iff (p : List Nat) : Win p ↔ nimSum p ≠ 0 := by118  constructor119  · intro hw h120    exact not_win_and_lose p hw ((lose_of_zero_win_of_ne p).1 h)121  · exact (lose_of_zero_win_of_ne p).2122123/-! ### The adversarial guarantee -/124125/-- `Wins sel p`: the player to move at `p`, always playing the successor chosen by126    `sel`, wins against EVERY legal opponent.  The selected move is legal, and after127    every legal opponent reply the player is again in a `Wins` position.  Because128    the predicate is inductive, every such play is finite and ends with the129    opponent facing a terminal board (normal play: the opponent loses). -/130inductive Wins (sel : List Nat → Option (List Nat)) : List Nat → Prop131  | intro (p q : List Nat) : sel p = some q → Move p q →132      (∀ r, Move q r → Wins sel r) → Wins sel p133134/-- `Wins` is sound for the game semantics. -/135theorem wins_sound {sel : List Nat → Option (List Nat)} {p : List Nat}136    (h : Wins sel p) : Win p := by137  induction h with138  | intro p q _ hm _ ih => exact Win.intro p q hm (Lose.intro q ih)139140/-! ## Target 1B: rollout measurements and reconstruction of the nim-sum -/141142/-- 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  omega153154theorem testBit0_succ (n : Nat) : (n + 1).testBit 0 = !(n.testBit 0) := by155  rw [lowBit_add]156  cases n.testBit 0 <;> rfl157158/-- The first player wins the rollout iff the number of rollout moves is odd. -/159theorem rolloutWinner_eq (j : Nat) (p : List Nat) :160    rolloutWinner j p = (rolloutMoves j p).testBit 0 := by161  induction p using rolloutWinner.induct j with162  | case1 p h =>163    rw [rolloutWinner, rolloutMoves, h]164    show false = (0 : Nat).testBit 0165    simp166  | case2 p q h ih =>167    rw [rolloutWinner, rolloutMoves, h]168    show (!rolloutWinner j q) = (rolloutMoves j q + 1).testBit 0169    rw [ih, testBit0_succ]170171/-- RO_{pi_0}(P) = sigma_0 and RO_{pi_j}(P) = sigma_j XOR sigma_0 (j ≥ 1), proved for172    the executed rollout. -/173theorem rolloutWinner_channel (j : Nat) (p : List Nat) :174    rolloutWinner j p = channel j (nimSum p) := by175  rw [rolloutWinner_eq]176  exact rolloutMoves_parity j p177178/-- The number with bits f 0, ..., f (B-1). -/179def ofBits : Nat → (Nat → Bool) → Nat180  | 0, _ => 0181  | B + 1, f => 2 ^ B * (if f B then 1 else 0) + ofBits B f182183theorem ofBits_lt (B : Nat) (f : Nat → Bool) : ofBits B f < 2 ^ B := by184  induction B with185  | zero => simp [ofBits]186  | succ B ih =>187    simp only [ofBits, Nat.pow_succ]188    split <;> omega189190theorem testBit_ofBits (B : Nat) (f : Nat → Bool) (i : Nat) :191    (ofBits B f).testBit i = (decide (i < B) && f i) := by192  induction B with193  | zero => simp [ofBits]194  | succ B ih =>195    simp only [ofBits]196    rw [Nat.testBit_two_pow_mul_add _ (ofBits_lt B f)]197    by_cases hi : i < B198    · simp [hi, ih, show i < B + 1 by omega]199    · by_cases hiB : i = B200      · subst hiB; cases f i <;> simp201      · have h1 : ¬ i < B + 1 := by omega202        have h2 : (1 : Nat).testBit (i - B) = false :=203          Nat.testBit_lt_two_pow (Nat.one_lt_two_pow (by omega))204        simp only [hi, if_false, h1, decide_false, Bool.false_and]205        cases hf : f B <;> simp [h2]206207/-- Bit recovery from the outcomes o j = RO_{pi_j}: sigma_0 = o 0, sigma_j = o j XOR o 0. -/208def recoverBit (o : Nat → Bool) (j : Nat) : Bool :=209  if j = 0 then o 0 else xor (o j) (o 0)210211/-- The nim-sum reconstructed from the B rollout outcomes o 0, ..., o (B-1). -/212def reconstruct (B : Nat) (o : Nat → Bool) : Nat := ofBits B (recoverBit o)213214/-- The B actual rollout measurements of board p. -/215def outcomes (p : List Nat) : Nat → Bool := fun j => rolloutWinner j p216217theorem nimSum_lt {B : Nat} {p : List Nat} (hw : Width B p) : nimSum p < 2 ^ B := by218  induction p with219  | nil => simp only [nimSum]; exact Nat.two_pow_pos B220  | cons x t ih =>221    exact Nat.xor_lt_two_pow (hw x (by simp))222      (ih (fun y hy => hw y (List.mem_cons_of_mem _ hy)))223224/-- 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))241242/-! ## Target 1C: the selected move and the winning strategy -/243244/-- Replace the first heap x with x ^^^ s < x by x ^^^ s. -/245def cancelFirst (s : Nat) : List Nat → Option (List Nat)246  | [] => none247  | x :: t => if x ^^^ s < x then some ((x ^^^ s) :: t) else (cancelFirst s t).map (x :: ·)248249/-- Move selector from a claimed nim-sum s: if s ≠ 0 cancel s at the first qualifying250    heap; otherwise (or if no heap qualifies) subtract 1 from the first nonzero heap;251    halt (`none`) only on a terminal board. -/252def selectMove (s : Nat) (p : List Nat) : Option (List Nat) :=253  match (if s = 0 then none else cancelFirst s p) with254  | some q => some q255  | none => subFirstPos p256257/-- The agent: reconstruct the nim-sum from the B root rollouts, then select. -/258def agent (B : Nat) (p : List Nat) : Option (List Nat) :=259  selectMove (reconstruct B (outcomes p)) p260261theorem cancelFirst_some {s : Nat} {p q : List Nat} (h : cancelFirst s p = some q) :262    ∃ pre x post, p = pre ++ x :: post ∧ x ^^^ s < x ∧ q = pre ++ (x ^^^ s) :: post := by263  induction p generalizing q with264  | nil => simp [cancelFirst] at h265  | cons x t ih =>266    by_cases hx : x ^^^ s < x267    · simp only [cancelFirst, hx, if_true, Option.some.injEq] at h268      exact ⟨[], x, t, rfl, hx, h.symm⟩269    · simp only [cancelFirst, hx, if_false] at h270      cases ht : cancelFirst s t with271      | none => simp [ht] at h272      | some a =>273        simp only [ht, Option.map_some, Option.some.injEq] at h274        obtain ⟨pre, y, post, h1, h2, h3⟩ := ih ht275        exact ⟨x :: pre, y, post, by simp [h1], h2, by rw [← h, h3]; rfl⟩276277theorem cancelFirst_none {s : Nat} {p : List Nat} (h : cancelFirst s p = none) :278    ∀ x ∈ p, ¬ x ^^^ s < x := by279  induction p with280  | nil => simp281  | cons x t ih =>282    by_cases hx : x ^^^ s < x283    · simp [cancelFirst, hx] at h284    · simp only [cancelFirst, hx, if_false] at h285      cases ht : cancelFirst s t with286      | some a => simp [ht] at h287      | none =>288        intro y hy289        rcases List.mem_cons.mp hy with rfl | hy290        · exact hx291        · exact ih ht y hy292293theorem cancelFirst_terminal {s : Nat} {p : List Nat} (ht : Terminal p) :294    cancelFirst s p = none := by295  induction p with296  | nil => rfl297  | cons x t ih =>298    have hx : x = 0 := ht x (by simp)299    subst hx300    simp [cancelFirst, ih (fun y hy => ht y (List.mem_cons_of_mem _ hy))]301302theorem subFirstPos_terminal {p : List Nat} (ht : Terminal p) : subFirstPos p = none := by303  induction p with304  | nil => rfl305  | cons x t ih =>306    have hx : x = 0 := ht x (by simp)307    subst hx308    simp [subFirstPos, ih (fun y hy => ht y (List.mem_cons_of_mem _ hy))]309310/-- Every selected move is a legal Nim move, whatever claimed nim-sum is used. -/311theorem selectMove_legal {s : Nat} {p q : List Nat} (h : selectMove s p = some q) :312    Move p q := by313  unfold selectMove at h314  split at h315  · next q' hq' =>316    cases h317    by_cases hs : s = 0318    · simp [hs] at hq'319    · simp only [hs, if_false] at hq'320      obtain ⟨pre, x, post, rfl, hlt, rfl⟩ := cancelFirst_some hq'321      exact ⟨pre, x, post, _, rfl, rfl, hlt⟩322  · obtain ⟨pre, x, post, rfl, hx, rfl⟩ := subFirstPos_some h323    exact ⟨pre, x, post, x - 1, rfl, rfl, by omega⟩324325/-- The selector halts exactly on terminal boards. -/326theorem selectMove_none_iff (s : Nat) (p : List Nat) :327    selectMove s p = none ↔ Terminal p := by328  constructor329  · intro h330    unfold selectMove at h331    split at h332    · cases h333    · exact subFirstPos_none h334  · intro ht335    unfold selectMove336    rw [cancelFirst_terminal ht, subFirstPos_terminal ht]337    split <;> simp_all338339/-- With the true nonzero nim-sum, the selected move is legal and reaches nim-sum zero. -/340theorem selectMove_zero {p : List Nat} (h : nimSum p ≠ 0) :341    ∃ q, selectMove (nimSum p) p = some q ∧ Move p q ∧ nimSum q = 0 := by342  cases hc : cancelFirst (nimSum p) p with343  | none =>344    obtain ⟨pre, x, post, hp, hlt, _⟩ := exists_decreasing_heap p h345    exact absurd hlt (cancelFirst_none hc x (by rw [hp]; simp))346  | some q =>347    refine ⟨q, ?_, ?_, ?_⟩348    · simp [selectMove, h, hc]349    · exact selectMove_legal (s := nimSum p) (by simp [selectMove, h, hc])350    · obtain ⟨pre, x, post, hp, _, rfl⟩ := cancelFirst_some hc351      rw [hp]352      exact move_to_zero_algebra pre post x353354theorem width_move {B : Nat} {p q : List Nat} (hw : Width B p) (hm : Move p q) :355    Width B q := by356  obtain ⟨pre, x, post, y, rfl, rfl, hlt⟩ := hm357  intro z hz358  simp only [List.mem_append, List.mem_cons] at hz359  rcases hz with hz | rfl | hz360  · exact hw z (by simp [hz])361  · exact Nat.lt_trans hlt (hw x (by simp))362  · exact hw z (by simp [hz])363364/-- The agent's move is the rollout-reconstructed selection; on B-bit boards it365    coincides with selection from the true nim-sum. -/366theorem agent_eq {B : Nat} {p : List Nat} (hw : Width B p) :367    agent B p = selectMove (nimSum p) p := by368  rw [agent, reconstruct_eq hw]369370theorem agent_legal {B : Nat} {p q : List Nat} (h : agent B p = some q) : Move p q :=371  selectMove_legal h372373theorem agent_none_iff (B : Nat) (p : List Nat) : agent B p = none ↔ Terminal p :=374  selectMove_none_iff _ p375376/-- 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.sum389390/-- Strong mastery on B-bit boards: from every N-position the agent wins. -/391theorem agent_wins_of_win {B : Nat} {p : List Nat} (hw : Width B p) (h : Win p) :392    Wins (agent B) p :=393  agent_wins p hw ((win_iff p).1 h)394395/-- At a P-position no winning move exists; the agent still plays a legal move,396    or halts exactly when the board is terminal. -/397theorem agent_at_zero {B : Nat} {p : List Nat} (h : nimSum p = 0) :398    Lose p ∧ (agent B p = none ↔ Terminal p) ∧ (∀ q, agent B p = some q → Move p q) :=399  ⟨(lose_iff p).2 h, agent_none_iff B p, fun _ hq => agent_legal hq⟩400401/-- Restoration / invariant maintenance: once the agent has reached a zero-nim-sum402    B-bit board, it wins after every legal opponent reply. -/403theorem agent_maintains {B : Nat} {q : List Nat} (hw : Width B q) (hq : nimSum q = 0) :404    ∀ r, Move q r → Wins (agent B) r :=405  fun r hr => agent_wins r (width_move hw hr) (move_from_zero hr hq)406407/-- Two-frame restoration selector (paper Prop. restore / Thm search-gap (iii)):408    from the predecessor Q and current board Q', cancel delta = nim(Q) XOR nim(Q'). -/409def restore (Q Q' : List Nat) : Option (List Nat) :=410  cancelFirst (nimSum Q ^^^ nimSum Q') Q'411412theorem restore_correct {Q Q' : List Nat} (h0 : nimSum Q = 0) (hm : Move Q Q') :413    ∃ R, restore Q Q' = some R ∧ Move Q' R ∧ nimSum R = 0 := by414  have hne := move_from_zero hm h0415  have hd : nimSum Q ^^^ nimSum Q' = nimSum Q' := by rw [h0, Nat.zero_xor]416  obtain ⟨R, hsel, hmR, hR⟩ := selectMove_zero hne417  refine ⟨R, ?_, hmR, hR⟩418  unfold restore419  rw [hd]420  simp only [selectMove, hne, if_false] at hsel421  split at hsel422  · next q' hq' => cases hsel; exact hq'423  · next _ hnone =>424    obtain ⟨pre, x, post, hp, hlt, _⟩ := exists_decreasing_heap Q' hne425    exact absurd hlt (cancelFirst_none hnone x (by rw [hp]; simp))426427/-! ## Target 1D: finite bound on simulated rollout moves -/428429theorem heapCount_le (j h : Nat) : heapCount j h ≤ h := by430  unfold heapCount431  have hd := Nat.div_add_mod h (2 ^ j)432  have hm : h / 2 ^ j ≤ 2 ^ j * (h / 2 ^ j) := Nat.le_mul_of_pos_left _ (Nat.two_pow_pos j)433  generalize 2 ^ j * (h / 2 ^ j) = t at hd hm434  omega435436theorem rolloutMoves_le {B j : Nat} {p : List Nat} (hw : Width B p) :437    rolloutMoves j p ≤ p.length * (2 ^ B - 1) := by438  rw [rolloutMoves_eq]439  induction p with440  | nil => simp [rolloutCount]441  | cons x t ih =>442    have hx : x < 2 ^ B := hw x (by simp)443    have ht := ih (fun y hy => hw y (List.mem_cons_of_mem _ hy))444    have hc := heapCount_le j x445    have e : rolloutCount j (x :: t) = heapCount j x + rolloutCount j t := by446      simp [rolloutCount]447    rw [e, List.length_cons, Nat.succ_mul]448    omega449450/-- Total simulated moves of the B root rollouts. -/451def totalRolloutMoves (B : Nat) (p : List Nat) : Nat :=452  ((List.range B).map (fun j => rolloutMoves j p)).sum453454theorem 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 B468469/-! ## Target 2: the parity reduction -/470471/-- XOR of a list of Booleans (false on the empty list). -/472def parity : List Bool → Bool473  | [] => false474  | b :: bs => xor b (parity bs)475476/-- The board (2, b_1, ..., b_m), Boolean heaps encoded as 0/1. -/477def encode (bs : List Bool) : List Nat := 2 :: bs.map Bool.toNat478479theorem nimSum_bits (bs : List Bool) :480    nimSum (bs.map Bool.toNat) = (parity bs).toNat := by481  induction bs with482  | nil => rfl483  | cons b bs ih =>484    simp only [List.map_cons, nimSum, ih, parity]485    cases b <;> cases parity bs <;> rfl486487theorem nimSum_encode (bs : List Bool) : nimSum (encode bs) = 2 ^^^ (parity bs).toNat := by488  simp [encode, nimSum, nimSum_bits]489490theorem nimSum_encode_ne (bs : List Bool) : nimSum (encode bs) ≠ 0 := by491  rw [nimSum_encode]492  cases parity bs <;> decide493494/-- The reduced board: leading heap replaced by the parity. -/495def reduced (bs : List Bool) : List Nat := (parity bs).toNat :: bs.map Bool.toNat496497theorem reduced_move (bs : List Bool) :498    Move (encode bs) (reduced bs) ∧ nimSum (reduced bs) = 0 := by499  refine ⟨⟨[], 2, bs.map Bool.toNat, (parity bs).toNat, rfl, rfl, ?_⟩, ?_⟩500  · cases parity bs <;> decide501  · simp only [reduced, nimSum, nimSum_bits]502    exact Nat.xor_self _503504/-- UNIQUENESS: the only legal move from (2, b_1, ..., b_m) to nim-sum zero sets the505    leading heap to b_1 XOR ... XOR b_m.  Holds for every m, including m = 0. -/506theorem unique_zero_move (bs : List Bool) (q : List Nat)507    (hm : Move (encode bs) q) (hq : nimSum q = 0) : q = reduced bs := by508  obtain ⟨pre, x, post, y, hp, rfl, hlt⟩ := hm509  cases pre with510  | nil =>511    simp only [encode, List.nil_append, List.cons.injEq] at hp512    obtain ⟨rfl, rfl⟩ := hp513    simp only [List.nil_append, nimSum, nimSum_bits] at hq514    have := xor_eq_zero_imp hq515    simp [reduced, this]516  | cons h pre' =>517    simp only [encode, List.cons_append, List.cons.injEq] at hp518    obtain ⟨rfl, hM⟩ := hp519    have hx1 : x ≤ 1 := by520      have hmem : x ∈ bs.map Bool.toNat := by rw [hM]; simp521      obtain ⟨b, _, rfl⟩ := List.mem_map.mp hmem522      exact Bool.toNat_le b523    have hx : x = 1 := by omega524    have hy : y = 0 := by omega525    subst hx; subst hy526    exfalso527    have e1 : nimSum (pre' ++ 0 :: post) = nimSum (pre' ++ 1 :: post) ^^^ (1 ^^^ 0) :=528      nimSum_move529    rw [← hM, nimSum_bits] at e1530    simp only [List.cons_append, nimSum, e1] at hq531    revert hq532    cases parity bs <;> decide533534/-- Every winning-move selector outputs the reduced board, hence the parity, on535    (2, b_1, ..., b_m).  The hypothesis uses the normal-play semantics. -/536theorem winning_selector_parity (sel : List Nat → Option (List Nat))537    (hsel : ∀ p, Win p → ∃ q, sel p = some q ∧ Move p q ∧ Lose q) (bs : List Bool) :538    sel (encode bs) = some (reduced bs) := by539  have hw : Win (encode bs) := (win_iff _).2 (nimSum_encode_ne bs)540  obtain ⟨q, hs, hm, hl⟩ := hsel _ hw541  rw [hs, unique_zero_move bs q hm ((lose_iff q).1 hl)]542543/-- The rollout agent (B = 2) computes the parity on these boards. -/544theorem agent_parity (bs : List Bool) : agent 2 (encode bs) = some (reduced bs) := by545  have hw : Width 2 (encode bs) := by546    intro x hx547    simp only [encode, List.mem_cons, List.mem_map] at hx548    rcases hx with rfl | ⟨b, _, rfl⟩549    · decide550    · have := Bool.toNat_le b; omega551  obtain ⟨q, hs, hm, hq⟩ := selectMove_zero (nimSum_encode_ne bs)552  rw [agent_eq hw, hs, unique_zero_move bs q hm hq]553554/-- Read the parity bit off a selector's output (the new leading heap). -/555def decodeHead : Option (List Nat) → Bool556  | some (x :: _) => x == 1557  | _ => false558559theorem decode_reduced (bs : List Bool) : decodeHead (some (reduced bs)) = parity bs := by560  simp only [decodeHead, reduced]561  cases parity bs <;> rfl562563/-- CONDITIONAL COMPLEXITY CONSEQUENCE (logic only).  For ANY predicate `C` on564    Boolean functions and ANY predicate `S` on selectors, assuming565      (closure)  S sel implies C (bs ↦ decodeHead (sel (encode bs))), and566      (hardness) ¬ C parity,567    no selector satisfying S is a winning-move selector.  Instantiating C as568    "computable by polynomial-size constant-depth circuits" requires the569    closure of that class under the encoding/decoding, and the parity lower570    bound; NEITHER is formalised here.  They are explicit hypotheses. -/571theorem no_winning_selector_of_hardness572    (C : (List Bool → Bool) → Prop) (S : (List Nat → Option (List Nat)) → Prop)573    (closure : ∀ sel, S sel → C (fun bs => decodeHead (sel (encode bs))))574    (hard : ¬ C parity) (sel : List Nat → Option (List Nat)) (hS : S sel) :575    ¬ (∀ p, Win p → ∃ q, sel p = some q ∧ Move p q ∧ Lose q) := by576  intro hsel577  apply hard578  have e : (fun bs => decodeHead (sel (encode bs))) = parity := by579    funext bs580    rw [winning_selector_parity sel hsel bs, decode_reduced]581  rw [← e]582  exact closure sel hS583584585#print axioms move_sum_lt586#print axioms terminal_iff_no_move587#print axioms terminal_lose588#print axioms xor_eq_zero_imp589#print axioms nimSum_move590#print axioms move_from_zero591#print axioms exists_move_to_zero592#print axioms lose_of_zero_win_of_ne593#print axioms not_win_and_lose594#print axioms lose_iff595#print axioms win_iff596#print axioms wins_sound597#print axioms testBit0_succ598#print axioms rolloutWinner_eq599#print axioms rolloutWinner_channel600#print axioms ofBits_lt601#print axioms testBit_ofBits602#print axioms nimSum_lt603#print axioms reconstruct_eq604#print axioms cancelFirst_some605#print axioms cancelFirst_none606#print axioms cancelFirst_terminal607#print axioms subFirstPos_terminal608#print axioms selectMove_legal609#print axioms selectMove_none_iff610#print axioms selectMove_zero611#print axioms width_move612#print axioms agent_eq613#print axioms agent_legal614#print axioms agent_none_iff615#print axioms agent_wins616#print axioms agent_wins_of_win617#print axioms agent_at_zero618#print axioms agent_maintains619#print axioms restore_correct620#print axioms heapCount_le621#print axioms rolloutMoves_le622#print axioms totalRolloutMoves_le623#print axioms nimSum_bits624#print axioms nimSum_encode625#print axioms nimSum_encode_ne626#print axioms reduced_move627#print axioms unique_zero_move628#print axioms winning_selector_parity629#print axioms agent_parity630#print axioms decode_reduced631#print axioms no_winning_selector_of_hardness632633end Game634end NimAudit