NimCore

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 Std23/- Elementary algebra for the revised Nim paper. Authored locally by Codex.4   This file does not formalise AC0, the correlation theorem, or neural training. -/5namespace NimAudit67def nimSum : List Nat → Nat8  | [] => 09  | h :: t => h ^^^ nimSum t1011def scan (initial : Nat) (rows : List Nat) : Nat :=12  rows.foldl (fun acc row => acc ^^^ row) initial1314theorem xor_left_comm (a b c : Nat) : a ^^^ (b ^^^ c) = b ^^^ (a ^^^ c) := by15  ac_rfl1617@[simp] theorem xor_cancel_left (a b : Nat) : a ^^^ (a ^^^ b) = b := by18  rw [← Nat.xor_assoc, Nat.xor_self, Nat.zero_xor]1920theorem nimSum_append (xs ys : List Nat) :21    nimSum (xs ++ ys) = nimSum xs ^^^ nimSum ys := by22  induction xs with23  | nil => simp [nimSum]24  | cons h t ih => simp [nimSum, ih, Nat.xor_assoc]2526theorem scan_invariant (rows : List Nat) (initial : Nat) :27    scan initial rows = initial ^^^ nimSum rows := by28  induction rows generalizing initial with29  | nil => simp [scan, nimSum]30  | cons h t ih =>31    change scan (initial ^^^ h) t = initial ^^^ (h ^^^ nimSum t)32    rw [ih, Nat.xor_assoc]3334theorem scan_from_zero (rows : List Nat) : scan 0 rows = nimSum rows := by35  simp [scan_invariant]3637theorem one_heap_difference (pre post : List Nat) (a b : Nat) :38    nimSum (pre ++ a :: post) ^^^ nimSum (pre ++ b :: post) = a ^^^ b := by39  simp [nimSum_append, nimSum, Nat.xor_comm, xor_left_comm]4041theorem one_heap_update (pre post : List Nat) (a b : Nat) :42    nimSum (pre ++ b :: post) = nimSum (pre ++ a :: post) ^^^ a ^^^ b := by43  simp [nimSum_append, nimSum, Nat.xor_comm, xor_left_comm]4445theorem matching_deltas_restore_original (q q' r : Nat)46    (matched : q ^^^ q' = q' ^^^ r) : r = q := by47  have eq := congrArg (fun z => q' ^^^ z) matched48  simpa [Nat.xor_assoc, Nat.xor_comm, xor_left_comm] using eq.symm4950theorem conditional_restoration (q q' r : Nat)51    (zero : q = 0) (matched : q ^^^ q' = q' ^^^ r) : r = 0 := by52  exact (matching_deltas_restore_original q q' r matched).trans zero5354theorem move_to_zero_algebra (pre post : List Nat) (heap : Nat) :55    nimSum (pre ++ (heap ^^^ nimSum (pre ++ heap :: post)) :: post) = 0 := by56  rw [one_heap_update pre post heap]57  simp [Nat.xor_comm]5859theorem summary_comparison (pre post : List Nat) (a b : Nat) :60    scan 0 (pre ++ a :: post) ^^^ scan 0 (pre ++ b :: post) = a ^^^ b := by61  simpa [scan_from_zero] using one_heap_difference pre post a b6263/- A finite fibre check, not a theorem about the limiting distribution of all boards. -/64def guessFromLowBit (sigma : Nat) : Nat := if sigma % 2 = 1 then 1 else 26566theorem two_of_three_fibre_values :67    ([1, 2, 3].filter (fun sigma => guessFromLowBit sigma == sigma)).length = 2 := by68  decide6970theorem failure_on_third_value : guessFromLowBit 3 ≠ 3 := by decide7172theorem no_zero_without_zero_promise :73    (1 ^^^ 3 = 3 ^^^ 1) ∧ (1 : Nat) ≠ 0 := by decide747576/- Algebraic move-count model. Actual execution of the policy is outside this file. -/77def channel (j sigma : Nat) : Bool :=78  if j = 0 then sigma.testBit 0 else xor (sigma.testBit j) (sigma.testBit 0)7980def heapCount (j h : Nat) : Nat := h / 2^j + h % 2^j8182def rolloutCount (j : Nat) (rows : List Nat) : Nat := (rows.map (heapCount j)).sum8384theorem lowBit_add (a b : Nat) :85    (a+b).testBit 0 = xor (a.testBit 0) (b.testBit 0) := by86  rcases Nat.mod_two_eq_zero_or_one a with ha | ha <;>87    rcases Nat.mod_two_eq_zero_or_one b with hb | hb <;>88    simp [Nat.testBit_zero, Nat.add_mod, ha, hb]8990theorem channel_xor (j a b : Nat) :91    channel j (a ^^^ b) = xor (channel j a) (channel j b) := by92  by_cases hj : j = 093  · subst j94    simp only [channel]95    exact Nat.testBit_xor a b 096  · simp only [channel, hj, if_false, Nat.testBit_xor]97    cases a.testBit j <;> cases a.testBit 0 <;>98      cases b.testBit j <;> cases b.testBit 0 <;> rfl99100theorem heap_count_channel (j h : Nat) :101    (heapCount j h).testBit 0 = channel j h := by102  by_cases hj : j = 0103  · subst j104    simp only [heapCount, Nat.pow_zero, Nat.div_one, Nat.mod_one, Nat.add_zero,105      channel]106    rfl107  · have hpos : 0 < j := Nat.pos_of_ne_zero hj108    unfold heapCount109    rw [lowBit_add]110    simp only [Nat.testBit_div_two_pow, Nat.zero_add, Nat.testBit_mod_two_pow]111    simp [channel, hj, hpos]112113theorem rollout_count_channel (j : Nat) (rows : List Nat) :114    (rolloutCount j rows).testBit 0 = channel j (nimSum rows) := by115  induction rows with116  | nil => simp [rolloutCount, nimSum, channel]117  | cons h t ih =>118    change (heapCount j h + rolloutCount j t).testBit 0 = channel j (h ^^^ nimSum t)119    rw [lowBit_add, heap_count_channel, ih, channel_xor]120121#print axioms xor_left_comm122#print axioms xor_cancel_left123#print axioms nimSum_append124#print axioms scan_invariant125#print axioms scan_from_zero126#print axioms one_heap_difference127#print axioms one_heap_update128#print axioms matching_deltas_restore_original129#print axioms conditional_restoration130#print axioms move_to_zero_algebra131#print axioms summary_comparison132#print axioms two_of_three_fibre_values133#print axioms failure_on_third_value134#print axioms no_zero_without_zero_promise135#print axioms lowBit_add136#print axioms channel_xor137#print axioms heap_count_channel138#print axioms rollout_count_channel139end NimAudit