NimRollout

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 NimCore23/- Extension to NimCore.lean, written for the independent Claude review (9 October 2026).4   Lean 4.26.0, core/Std only.  NimCore.lean is imported unchanged.56   Part A.  Actual execution of the structured rollout policy pi_j.7     A legal policy move from board p (a list of heap sizes) to board q is:8       * subtract 2^j from some heap of size >= 2^j, or9       * if every heap is < 2^j, subtract 1 from some nonzero heap.10     The tie-breaking rule (which eligible heap is used) is left arbitrary in11     `PolicyMove`/`Run`, so the count theorem covers every tie-breaking rule.12     `rolloutMoves` is a concrete deterministic simulator that uses the first13     eligible heap, exactly as `rollout` in checks/check_revision.py.14     Main results: every complete run has length rolloutCount j p15     (= sum of h / 2^j + h % 2^j), and its parity is channel j (nimSum p).1617   Part B.  If the nim-sum is nonzero, some heap x satisfies x ^^^ nimSum p < x,18     so the replacement in `move_to_zero_algebra` is a legal (strictly19     decreasing) Nim move to a zero-nim-sum position.2021   Nothing here concerns circuit complexity, probability or learning. -/2223namespace NimAudit24namespace Rollout2526/-! ## Part A: rollout execution -/2728/-- 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)3334/-- `Run j p n`: following `pi_j` from board `p` reaches the all-zero board after35    exactly `n` policy moves. -/36inductive Run (j : Nat) : List Nat → Nat → Prop37  | done (p : List Nat) : (∀ x ∈ p, x = 0) → Run j p 038  | step (p q : List Nat) (n : Nat) : PolicyMove j p q → Run j q n → Run j p (n + 1)3940/-- Every policy move is a legal Nim move: one heap decreases by a positive41    amount `d ≤ x`, with `d = 2^j` or `d = 1`; all other heaps are unchanged. -/42theorem policyMove_legal {j : Nat} {p q : List Nat} (hm : PolicyMove j p q) :43    ∃ pre x post d, p = pre ++ x :: post ∧ q = pre ++ (x - d) :: post ∧44      0 < d ∧ d ≤ x ∧ (d = 2 ^ j ∨ d = 1) := by45  rcases hm with ⟨pre, x, post, hp, hx, hq⟩ | ⟨_, pre, x, post, hp, hx, hq⟩46  · exact ⟨pre, x, post, 2 ^ j, hp, hq, Nat.two_pow_pos j, hx, Or.inl rfl⟩47  · exact ⟨pre, x, post, 1, hp, hq, Nat.one_pos, hx, Or.inr rfl⟩4849theorem rolloutCount_split (j : Nat) (pre post : List Nat) (x : Nat) :50    rolloutCount j (pre ++ x :: post) =51      rolloutCount j pre + heapCount j x + rolloutCount j post := by52  simp [rolloutCount, List.sum_append_nat, Nat.add_assoc]5354theorem heapCount_sub_pow {j x : Nat} (hx : 2 ^ j ≤ x) :55    heapCount j (x - 2 ^ j) + 1 = heapCount j x := by56  obtain ⟨y, rfl⟩ : ∃ y, x = y + 2 ^ j := ⟨x - 2 ^ j, (Nat.sub_add_cancel hx).symm⟩57  simp only [heapCount, Nat.add_sub_cancel, Nat.add_div_right _ (Nat.two_pow_pos j),58    Nat.add_mod_right]59  omega6061theorem heapCount_sub_one {j x : Nat} (hpos : 0 < x) (hlt : x < 2 ^ j) :62    heapCount j (x - 1) + 1 = heapCount j x := by63  have h1 : x - 1 < 2 ^ j := by omega64  simp only [heapCount, Nat.div_eq_of_lt hlt, Nat.mod_eq_of_lt hlt,65    Nat.div_eq_of_lt h1, Nat.mod_eq_of_lt h1]66  omega6768theorem rolloutCount_zero {j : Nat} {p : List Nat} (hz : ∀ x ∈ p, x = 0) :69    rolloutCount j p = 0 := by70  induction p with71  | nil => rfl72  | cons h t ih =>73    have hh : h = 0 := hz h (List.mem_cons_self ..)74    have ht : ∀ x ∈ t, x = 0 := fun x hx => hz x (List.mem_cons_of_mem _ hx)75    simp [rolloutCount, heapCount, hh] at ih ⊢76    exact ih ht7778/-- Each policy move lowers the algebraic count by exactly one. -/79theorem policyMove_count {j : Nat} {p q : List Nat} (hm : PolicyMove j p q) :80    rolloutCount j q + 1 = rolloutCount j p := by81  rcases hm with ⟨pre, x, post, rfl, hx, rfl⟩ | ⟨hall, pre, x, post, rfl, hx, rfl⟩82  · rw [rolloutCount_split, rolloutCount_split, ← heapCount_sub_pow hx]83    omega84  · have hlt : x < 2 ^ j := hall x (by simp)85    rw [rolloutCount_split, rolloutCount_split, ← heapCount_sub_one hx hlt]86    omega8788/-- 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]9596/-- 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 p103104/-! ### A concrete deterministic simulator (first eligible heap), and its correctness -/105106/-- Subtract `u` from the first heap of size ≥ `u`. -/107def subFirstGe (u : Nat) : List Nat → Option (List Nat)108  | [] => none109  | h :: t => if u ≤ h then some ((h - u) :: t) else (subFirstGe u t).map (h :: ·)110111/-- Subtract 1 from the first nonzero heap. -/112def subFirstPos : List Nat → Option (List Nat)113  | [] => none114  | h :: t => if 0 < h then some ((h - 1) :: t) else (subFirstPos t).map (h :: ·)115116/-- 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 p121122theorem subFirstGe_some {u : Nat} {p q : List Nat} (h : subFirstGe u p = some q) :123    ∃ pre x post, p = pre ++ x :: post ∧ u ≤ x ∧ q = pre ++ (x - u) :: post := by124  induction p generalizing q with125  | nil => simp [subFirstGe] at h126  | cons x t ih =>127    by_cases hx : u ≤ x128    · simp only [subFirstGe, hx, if_true, Option.some.injEq] at h129      exact ⟨[], x, t, rfl, hx, h.symm⟩130    · simp only [subFirstGe, hx, if_false] at h131      cases ht : subFirstGe u t with132      | none => simp [ht] at h133      | some a =>134        simp only [ht, Option.map_some, Option.some.injEq] at h135        obtain ⟨pre, y, post, h1, h2, h3⟩ := ih ht136        exact ⟨x :: pre, y, post, by simp [h1], h2, by rw [← h, h3]; rfl⟩137138theorem subFirstGe_none {u : Nat} {p : List Nat} (h : subFirstGe u p = none) :139    ∀ x ∈ p, x < u := by140  induction p with141  | nil => simp142  | cons x t ih =>143    by_cases hx : u ≤ x144    · simp [subFirstGe, hx] at h145    · simp only [subFirstGe, hx, if_false] at h146      cases ht : subFirstGe u t with147      | some a => simp [ht] at h148      | none =>149        intro y hy150        rcases List.mem_cons.mp hy with rfl | hy151        · omega152        · exact ih ht y hy153154theorem subFirstPos_some {p q : List Nat} (h : subFirstPos p = some q) :155    ∃ pre x post, p = pre ++ x :: post ∧ 0 < x ∧ q = pre ++ (x - 1) :: post := by156  induction p generalizing q with157  | nil => simp [subFirstPos] at h158  | cons x t ih =>159    by_cases hx : 0 < x160    · simp only [subFirstPos, hx, if_true, Option.some.injEq] at h161      exact ⟨[], x, t, rfl, hx, h.symm⟩162    · simp only [subFirstPos, hx, if_false] at h163      cases ht : subFirstPos t with164      | none => simp [ht] at h165      | some a =>166        simp only [ht, Option.map_some, Option.some.injEq] at h167        obtain ⟨pre, y, post, h1, h2, h3⟩ := ih ht168        exact ⟨x :: pre, y, post, by simp [h1], h2, by rw [← h, h3]; rfl⟩169170theorem subFirstPos_none {p : List Nat} (h : subFirstPos p = none) :171    ∀ x ∈ p, x = 0 := by172  induction p with173  | nil => simp174  | cons x t ih =>175    by_cases hx : 0 < x176    · simp [subFirstPos, hx] at h177    · simp only [subFirstPos, hx, if_false] at h178      cases ht : subFirstPos t with179      | some a => simp [ht] at h180      | none =>181        intro y hy182        rcases List.mem_cons.mp hy with rfl | hy183        · omega184        · exact ih ht y hy185186theorem policyStep_some {j : Nat} {p q : List Nat} (h : policyStep j p = some q) :187    PolicyMove j p q := by188  unfold policyStep at h189  cases hg : subFirstGe (2 ^ j) p with190  | some a =>191    rw [hg] at h192    cases h193    exact Or.inl (subFirstGe_some hg)194  | none =>195    rw [hg] at h196    exact Or.inr ⟨subFirstGe_none hg, subFirstPos_some h⟩197198theorem policyStep_none {j : Nat} {p : List Nat} (h : policyStep j p = none) :199    ∀ x ∈ p, x = 0 := by200  unfold policyStep at h201  cases hg : subFirstGe (2 ^ j) p with202  | some a => rw [hg] at h; cases h203  | none => rw [hg] at h; exact subFirstPos_none h204205/-- The simulator: apply `policyStep` until no move is available, counting moves.206    Termination is justified by `policyMove_count`. -/207def rolloutMoves (j : Nat) (p : List Nat) : Nat :=208  match h : policyStep j p with209  | none => 0210  | some q => rolloutMoves j q + 1211termination_by rolloutCount j p212decreasing_by213  have := policyMove_count (policyStep_some h)214  omega215216/-- The simulator's trace is a complete run of `pi_j`. -/217theorem rolloutMoves_run (j : Nat) (p : List Nat) : Run j p (rolloutMoves j p) := by218  induction p using rolloutMoves.induct j with219  | case1 p h =>220    rw [rolloutMoves, h]221    exact Run.done p (policyStep_none h)222  | case2 p q h ih =>223    rw [rolloutMoves, h]224    exact Run.step p q _ (policyStep_some h) ih225226/-- The simulated rollout length equals the algebraic count. -/227theorem rolloutMoves_eq (j : Nat) (p : List Nat) :228    rolloutMoves j p = rolloutCount j p :=229  run_length (rolloutMoves_run j p)230231/-- Per-heap execution count (single-heap board). -/232theorem rolloutMoves_single (j h : Nat) :233    rolloutMoves j [h] = h / 2 ^ j + h % 2 ^ j := by234  rw [rolloutMoves_eq]235  simp [rolloutCount, heapCount]236237/-- Parity of the simulated rollout length equals the channel of the nim-sum. -/238theorem rolloutMoves_parity (j : Nat) (p : List Nat) :239    (rolloutMoves j p).testBit 0 = channel j (nimSum p) :=240  run_parity (rolloutMoves_run j p)241242/-! ## Part B: a decreasing heap exists when the nim-sum is nonzero -/243244/-- Two numbers agreeing above bit `k`, with bit `k` 0 in `a` and 1 in `b`, satisfy `a < b`. -/245theorem lt_of_top_testBit {a b k : Nat}246    (hk : a.testBit k = false) (hb : b.testBit k = true)247    (hi : ∀ i, k < i → a.testBit i = b.testBit i) : a < b := by248  have hq : a / 2 ^ (k + 1) = b / 2 ^ (k + 1) := by249    apply Nat.eq_of_testBit_eq250    intro i251    rw [Nat.testBit_div_two_pow, Nat.testBit_div_two_pow]252    exact hi _ (by omega)253  have hra : a % 2 ^ (k + 1) < 2 ^ k := by254    apply Nat.lt_pow_two_of_testBit255    intro i hi'256    rw [Nat.testBit_mod_two_pow]257    by_cases hik : i = k258    · subst hik; simp [hk]259    · have : ¬ i < k + 1 := by omega260      simp [this]261  have hrb : 2 ^ k ≤ b % 2 ^ (k + 1) := by262    apply Nat.ge_two_pow_of_testBit263    rw [Nat.testBit_mod_two_pow]264    simp [hb]265  rw [← Nat.div_add_mod a (2 ^ (k + 1)), ← Nat.div_add_mod b (2 ^ (k + 1)), hq]266  exact Nat.add_lt_add_left (Nat.lt_of_lt_of_le hra hrb) _267268theorem exists_heap_testBit {p : List Nat} {k : Nat}269    (h : (nimSum p).testBit k = true) : ∃ x ∈ p, x.testBit k = true := by270  induction p with271  | nil => simp [nimSum] at h272  | cons x t ih =>273    simp only [nimSum, Nat.testBit_xor] at h274    cases hx : x.testBit k with275    | true => exact ⟨x, List.mem_cons_self .., hx⟩276    | false =>277      rw [hx, Bool.false_xor] at h278      obtain ⟨y, hy, hyk⟩ := ih h279      exact ⟨y, List.mem_cons_of_mem _ hy, hyk⟩280281/-- 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⟩315316/-! ## A sharper form of the zero-predecessor caveat -/317318/-- Matching deltas alone never force a zero result: the universal statement is false. -/319theorem matching_deltas_do_not_force_zero :320    ¬ ∀ q q' r : Nat, q ^^^ q' = q' ^^^ r → r = 0 := by321  intro h322  have := h 1 3 1 (by decide)323  exact absurd this (by decide)324325#print axioms policyMove_legal326#print axioms rolloutCount_split327#print axioms heapCount_sub_pow328#print axioms heapCount_sub_one329#print axioms rolloutCount_zero330#print axioms policyMove_count331#print axioms run_length332#print axioms run_parity333#print axioms subFirstGe_some334#print axioms subFirstGe_none335#print axioms subFirstPos_some336#print axioms subFirstPos_none337#print axioms policyStep_some338#print axioms policyStep_none339#print axioms rolloutMoves_run340#print axioms rolloutMoves_eq341#print axioms rolloutMoves_single342#print axioms rolloutMoves_parity343#print axioms lt_of_top_testBit344#print axioms exists_heap_testBit345#print axioms exists_decreasing_heap346#print axioms matching_deltas_do_not_force_zero347348end Rollout349end NimAudit