Misc

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 Bypass23/- Phase 6, Priority 3d: remaining paper-specific mathematical statements.  Written by4   Claude (10 October 2026).  Lean 4.26.0, core/Std only.56   A. Appendix app:weak (pairing strategy) and Definition def:mastery (weak mastery):7      on paired boards the second player answers every legal move by copying it on the8      partner heap; the reply is computed by a binary selector built from LOCAL two-heap9      comparisons (no nim-sum); it wins against every opponent (SecondWins, hence Lose10      for the player to move, hence nim-sum 0).11   B. The finite-state shootout controller (Figure fig:fsm-shootout-controller): generic12      finite-state controllers over rollout heads; the depicted controller outputs the OR13      of the queried channel bits, which for the exact structured heads is (nim(P) ≠ 0),14      using 1 + (index of the first 1) ≤ B queries.15   C. The single-head baseline numbers: among nonzero nim-sums of B bits exactly 2^{B−1}16      are detected by the r₀ classifier; for B = 4 this is 8 of 15 and the balanced17      accuracy is 23/30; with uniform boards the board-level recall is the same ratio.18   D. Remark rem:noisy-rollout-decay: for independent Bernoulli(ε) flips E₁..E_L,19      Pr[Y ⊕ E₁ ⊕ … ⊕ E_L = Y] = (1 + (1 − 2ε)^L)/2 (exact finite probability model); for20      ε = 1/100, L = 50 the value lies in [0.682, 0.6822].  (No claim is made about21      erroneous game moves or learned heads.)22   E. Section sec:spectral-view: characters are orthonormal on {0,1}^n (char_orth), i.e.23      the Fourier coefficient of PARITY_S at T is 1 if T = S and 0 otherwise; nim-sum bit j24      is the parity of a mask with exactly N ones (a degree-N character); a single-heap25      change makes each delta bit a two-coordinate character.  (No Fourier-tail theorem26      for AC0 is stated: Linial–Mansour–Nisan stays external and unused.)27   F. The initialisation boundary (Section sec:search-gap): the completed matching-delta28      policy plays (2) → (1) → (0) and loses from the winning position (2).29   G. Proposition prop:single-policy-bound: a one-heap modification shifts the channel30      bit by the known correction ℓ_j(h ⊕ h'). -/3132namespace NimAudit33namespace Misc3435attribute [local simp] Rat.add_zero Rat.zero_add Rat.mul_one Rat.one_mul Rat.mul_zero Rat.zero_mul3637open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit38  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet ThresholdInst FiniteNet WholeGame39  Family4041/-! ## A. Pairing strategy and weak mastery -/4243/-- Partner of heap k in the pairs (0,1), (2,3), … -/44def partner (k : Nat) : Nat := if k % 2 = 0 then k + 1 else k - 14546theorem partner_partner (k : Nat) : partner (partner k) = k := by unfold partner; split <;> split <;> omega47theorem partner_ne (k : Nat) : partner k ≠ k := by unfold partner; split <;> omega48theorem partner_lt {k N : Nat} (hk : k < N) (hN : N % 2 = 0) : partner k < N := by unfold partner; split <;> omega4950/-- Paired boards (a, a, b, b, …). -/51def Paired (P : List Nat) : Prop := P.length % 2 = 0 ∧ ∀ k, k < P.length → P.getD k 0 = P.getD (partner k) 05253/-- Second-player guarantee for a reply rule: every legal opponent move is answered54    legally and the guarantee persists (weak mastery for the second-player role). -/55inductive SecondWins (sel : List Nat → Option (List Nat)) : List Nat → Prop56  | intro (P : List Nat) :57      (∀ Q, Move P Q → (sel Q).isSome = true) →58      (∀ Q R, Move P Q → sel Q = some R → Move Q R) →59      (∀ Q R, Move P Q → sel Q = some R → SecondWins sel R) → SecondWins sel P6061theorem secondWins_sound {sel : List Nat → Option (List Nat)} {P : List Nat} (h : SecondWins sel P) : Lose P := by62  induction h with63  | intro P hsome hmove _ ih =>64    refine Lose.intro P (fun Q hm => ?_)65    cases hr : sel Q with66    | none => have := hsome Q hm; rw [hr] at this; cases this67    | some R => exact Win.intro Q R (hmove Q R hm hr) (ih Q R hm hr)6869theorem getD_set_ne' (P : List Nat) {i k : Nat} (v : Nat) (h : k ≠ i) : (P.set i v).getD k 0 = P.getD k 0 := by70  simp [List.getD_eq_getElem?_getD, List.getElem?_set, Ne.symm h]7172theorem getD_set_eq' (P : List Nat) {i : Nat} (v : Nat) (h : i < P.length) : (P.set i v).getD i 0 = v := by73  simp [List.getD_eq_getElem?_getD, h]7475/-- After one legal move from a paired board, exactly one heap is larger than its partner:76    the partner j of the changed heap i; the mirror reply sets heap j to the new value. -/77theorem paired_move {P Q : List Nat} (hp : Paired P) (hm : Move P Q) :78    ∃ i y, i < P.length ∧ Q = P.set i y ∧ y < P.getD i 0 ∧ Q.length = P.length ∧79      (∀ k, k < Q.length → (Q.getD (partner k) 0 < Q.getD k 0 ↔ k = partner i)) ∧80      Paired (Q.set (partner i) y) ∧ Move Q (Q.set (partner i) y) := by81  obtain ⟨pre, x, post, y, hP, hQ, hlt⟩ := hm82  let i := pre.length83  have hi : i < P.length := by rw [hP]; simp [i]84  have hPi : P.getD i 0 = x := by rw [hP]; simp [i]85  have hQset : Q = P.set i y := by rw [hQ, hP]; simp [i]86  have hQl : Q.length = P.length := by rw [hQset]; simp87  have hNe := hp.188  have hj : partner i < P.length := partner_lt hi hNe89  have hQi : Q.getD i 0 = y := by rw [hQset]; exact getD_set_eq' P y hi90  have hQj : Q.getD (partner i) 0 = x := by91    rw [hQset, getD_set_ne' P y (partner_ne i), ← hp.2 i hi, hPi]92  refine ⟨i, y, hi, hQset, by rw [hPi]; exact hlt, hQl, fun k hk => ?_, ⟨?_, fun k hk => ?_⟩, ?_⟩93  · constructor94    · intro h95      by_cases hki : k = i96      · subst hki; rw [hQi, hQj] at h; omega97      · by_cases hkj : k = partner i98        · exact hkj99        · exfalso100          have hpk : partner k ≠ i := fun e => hkj (by rw [← e, partner_partner])101          rw [hQset, getD_set_ne' P y hpk, getD_set_ne' P y hki, ← hp.2 k (by omega)] at h102          omega103    · intro h; subst h; rw [partner_partner, hQi, hQj]; exact hlt104  · simp [hQl, hNe]105  · simp only [List.length_set] at hk106    by_cases hk1 : k = partner i107    · subst hk1; rw [partner_partner, getD_set_eq' Q y (by omega), getD_set_ne' Q y (Ne.symm (partner_ne i)), hQi]108    · by_cases hk2 : k = i109      · subst hk2; rw [getD_set_ne' Q y (Ne.symm (partner_ne _)), hQi, getD_set_eq' Q y (by omega)]110      · have hpk : partner k ≠ partner i := fun e => hk2 (by rw [← partner_partner k, e, partner_partner])111        have hpk2 : partner k ≠ i := fun e => hk1 (by rw [← e, partner_partner])112        rw [getD_set_ne' Q y hk1, getD_set_ne' Q y hpk, hQset, getD_set_ne' P y hk2, getD_set_ne' P y hpk2]113        exact hp.2 k (by omega)114  · apply set_move (x := x)115    · rw [List.getElem?_eq_getElem (by omega)]116      have := hQj; rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (by omega)] at this117      simpa using this118    · exact hlt119120/-! ### The local mirror circuit -/121122/-- Comparison formulas: heap partner(k) < heap k (both big-endian B-bit blocks). -/123def cmpR (B k : Nat) : RCirc := ⟨const true, [], (List.range B).map (fun p => heapC B (partner k) p)⟩124def flagC (B k : Nat) : Circ := ltC (cmpR B k) B k125126/-- The mirror selector: flag k = (partner k < k); the value is the flagged heap's partner. -/127def pairR (B N : Nat) : RCirc :=128  ⟨or ((List.range N).map (flagC B)), (List.range N).map (flagC B),129   (List.range B).map (fun p => or ((List.range N).map (fun k => and [flagC B k, heapC B (partner k) p])))⟩130131/-- The binary mirror selector and the reply rule it defines. -/132def pairBin (B N r : Nat) : BCirc := encode (pairR B N) N r133def pairSel (B : Nat) (Q : List Nat) : Option (List Nat) :=134  applyM Q (binSem (pairBin B Q.length (rIdx Q.length)) Q.length (boardBits B Q))135136theorem toNatBE_heap {B N : Nat} {Q : List Nat} (hQ : Q.length = N) (hw : Width B Q) {k : Nat} (hk : k < N) :137    toNatBE ((List.range B).map (fun p => boardBits B Q (B * k + p))) = Q.getD k 0 := by138  have hlt : Q.getD k 0 < 2 ^ B := by139    apply hw; rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (by omega)]; simp140  rw [toNatBE_eq_iff _ (by simpa using hlt)]141  intro q hq142  simp only [List.length_map, List.length_range] at hq ⊢143  rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range hq]144  simp only [Option.map_some, Option.getD_some]145  exact boardBits_heap hQ hk hq146147theorem flagC_eval {B N : Nat} {Q : List Nat} (hQ : Q.length = N) (hw : Width B Q) (hN : N % 2 = 0)148    {k : Nat} (hk : k < N) : eval (boardBits B Q) (flagC B k) = decide (Q.getD (partner k) 0 < Q.getD k 0) := by149  unfold flagC150  rw [ltC_eval hQ hw (by simp [cmpR]) hk]151  congr 2152  simp only [cmpR, List.map_map, Function.comp_def, heapC, eval_input]153  exact toNatBE_heap hQ hw (partner_lt hk hN)154155/-- MIRROR CIRCUIT CORRECTNESS: after a legal move from a paired board, the selector156    outputs (partner of the changed heap, new value). -/157theorem pairR_correct {B : Nat} {P Q : List Nat} (hp : Paired P) (hw : Width B P) (hm : Move P Q) :158    ∃ i y, Q = P.set i y ∧ selReadout (pairR B Q.length) (boardBits B Q) = some (partner i, y) ∧159      Paired (Q.set (partner i) y) ∧ Move Q (Q.set (partner i) y) := by160  obtain ⟨i, y, hi, hQ, hy, hQl, hflag, hpair, hmv⟩ := paired_move hp hm161  refine ⟨i, y, hQ, ?_, hpair, hmv⟩162  have hN : Q.length % 2 = 0 := by rw [hQl]; exact hp.1163  have hwQ : Width B Q := width_move hw (by164    obtain ⟨pre, x, post, z, h1, h2, h3⟩ := hm; exact ⟨pre, x, post, z, h1, h2, h3⟩)165  have hj : partner i < Q.length := by rw [hQl]; exact partner_lt hi hp.1166  have hfl : ∀ k, k < Q.length → eval (boardBits B Q) (flagC B k) = decide (k = partner i) := by167    intro k hk; rw [flagC_eval rfl hwQ hN hk]; exact decide_eq_decide.mpr (hflag k hk)168  unfold selReadout pairR169  simp only170  have hvalid : eval (boardBits B Q) (or ((List.range Q.length).map (flagC B))) = true := by171    rw [eval_or, List.any_eq_true]172    exact ⟨flagC B (partner i), List.mem_map.mpr ⟨_, List.mem_range.mpr hj, rfl⟩, by rw [hfl _ hj]; simp⟩173  rw [if_pos hvalid]174  have hft : firstTrue (((List.range Q.length).map (flagC B)).map (eval (boardBits B Q))) = some (partner i) := by175    rw [firstTrue_some_iff]176    simp only [List.map_map, List.length_map, List.length_range]177    refine ⟨hj, ?_, fun i' hi' => ?_⟩178    · rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range hj]179      simp [hfl _ hj]180    · rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range (by omega)]181      simp [hfl _ (by omega : i' < Q.length)]; omega182  rw [hft]183  simp only [Option.some.injEq, Prod.mk.injEq, true_and]184  -- the value bits are the bits of heap i (the flagged heap's partner)185  have hval : ((List.range B).map (fun p => or ((List.range Q.length).map186      (fun k => and [flagC B k, heapC B (partner k) p])))).map (eval (boardBits B Q)) =187      (List.range B).map (fun p => boardBits B Q (B * i + p)) := by188    simp only [List.map_map]189    apply List.map_congr_left190    intro p hp191    simp only [Function.comp_apply, eval_or, List.any_map]192    apply Bool.eq_iff_iff.mpr193    rw [List.any_eq_true]194    constructor195    · rintro ⟨k, hk, he⟩196      have hk' := List.mem_range.mp hk197      simp only [Function.comp_apply, eval_and, List.all_cons, List.all_nil, Bool.and_true, Bool.and_eq_true,198        hfl k hk', decide_eq_true_eq, heapC, eval_input] at he199      obtain ⟨rfl, h2⟩ := he200      rw [partner_partner] at h2; exact h2201    · intro h202      refine ⟨partner i, List.mem_range.mpr hj, ?_⟩203      simp only [Function.comp_apply, eval_and, List.all_cons, List.all_nil, Bool.and_true, hfl _ hj, decide_true,204        Bool.true_and, heapC, eval_input, partner_partner]205      exact h206  rw [hval, toNatBE_heap rfl hwQ (by omega)]207  rw [hQ, getD_set_eq' P y hi]208209/-- PAIRING STRATEGY (weak mastery for the second player): from every paired board of210    width B, the reply rule computed by the local binary mirror circuit wins against every211    legal opponent. -/212theorem pairing_wins {B : Nat} : ∀ P : List Nat, Paired P → Width B P → SecondWins (pairSel B) P := by213  intro P214  induction P using (measure List.sum).wf.induction with215  | h P ih =>216    intro hp hw217    have key : ∀ Q, Move P Q → ∃ i y, pairSel B Q = some (Q.set (partner i) y) ∧218        Paired (Q.set (partner i) y) ∧ Move Q (Q.set (partner i) y) := by219      intro Q hm220      obtain ⟨i, y, _, hsel, hpair, hmv⟩ := pairR_correct hp hw hm221      refine ⟨i, y, ?_, hpair, hmv⟩222      unfold pairSel223      rw [pairBin, encode_correct _ Q.length _ (by simp [pairR]) (rIdx_width _), hsel]; rfl224    refine SecondWins.intro P (fun Q hm => ?_) (fun Q R hm hR => ?_) (fun Q R hm hR => ?_)225    · obtain ⟨i, y, h1, _⟩ := key Q hm; rw [h1]; rfl226    · obtain ⟨i, y, h1, _, h3⟩ := key Q hm; rw [h1] at hR; cases hR; exact h3227    · obtain ⟨i, y, h1, h2, h3⟩ := key Q hm228      rw [h1] at hR; cases hR229      have e1 := move_sum_lt hm; have e2 := move_sum_lt h3230      exact ih _ (by show (Q.set (partner i) y).sum < P.sum; omega) h2 (width_move (width_move hw hm) h3)231232theorem paired_lose {B : Nat} {P : List Nat} (hp : Paired P) (hw : Width B P) : Lose P ∧ nimSum P = 0 :=233  ⟨secondWins_sound (pairing_wins (B := B) P hp hw), (lose_iff P).1 (secondWins_sound (pairing_wins (B := B) P hp hw))⟩234235/-- The mirror circuit uses no nim-sum: every formula reads only board bits. -/236theorem pairR_reads (B N : Nat) (hN : N % 2 = 0) : ∀ c ∈ (pairR B N).valid :: ((pairR B N).sel ++ (pairR B N).val),237    maxInput c ≤ B * N := by238  have hflag : ∀ k, k < N → maxInput (flagC B k) ≤ B * N := by239    intro k hk240    unfold flagC ltC241    apply maxInput_or_le; intro c hc242    obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hc243    have hp' := List.mem_range.mp hp244    have hpk := partner_lt hk hN245    have hv : ∀ q, q < B → maxInput (valC (cmpR B k) q) ≤ B * N := by246      intro q hq247      simp only [valC, cmpR, getC, List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range hq,248        Option.map_some, Option.getD_some, heapC, maxInput_input]249      have := Nat.mul_le_mul_left B (show partner k + 1 ≤ N by omega); rw [Nat.mul_add, Nat.mul_one] at this; omega250    have hh : ∀ q, q < B → maxInput (heapC B k q) ≤ B * N := by251      intro q hq; simp only [heapC, maxInput_input]252      have := Nat.mul_le_mul_left B (show k + 1 ≤ N by omega); rw [Nat.mul_add, Nat.mul_one] at this; omega253    apply maxInput_and_le; intro c hc254    simp only [List.mem_append, List.mem_cons, List.mem_nil_iff, or_false, List.mem_map, List.mem_range] at hc255    rcases hc with (rfl | rfl) | ⟨q, hq, rfl⟩256    · simpa using hv p hp'257    · exact hh p hp'258    · simp only [eqC, maxInput_or, maxInput_and, maxInput_not, List.map_cons, List.map_nil, listMax, List.foldr]259      have := hv q (by omega); have := hh q (by omega); omega260  intro c hc261  simp only [pairR, List.mem_cons, List.mem_append, List.mem_map, List.mem_range] at hc262  rcases hc with rfl | ⟨k, hk, rfl⟩ | ⟨p, hp, rfl⟩263  · apply maxInput_or_le; intro c hc; obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hc; exact hflag k (List.mem_range.mp hk)264  · exact hflag k hk265  · apply maxInput_or_le; intro c hc266    obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hc267    have hk' := List.mem_range.mp hk268    apply maxInput_and_le; intro c hc269    simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc270    rcases hc with rfl | rfl271    · exact hflag k hk'272    · simp only [heapC, maxInput_input]273      have := Nat.mul_le_mul_left B (show partner k + 1 ≤ N by have := partner_lt hk' hN; omega)274      rw [Nat.mul_add, Nat.mul_one] at this; omega275276/-- Size bound for one mirror flag (a B-bit comparison of a heap with its partner). -/277def pairF (B : Nat) : Nat := B * ((2 + B) * 9 + 1) + 1278279theorem valC_cmpR_res (B k q : Nat) : depth (valC (cmpR B k) q) = 0 ∧ size (valC (cmpR B k) q) = 1 := by280  by_cases hq : q < B281  · simp only [valC, cmpR, getC, List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range hq,282      Option.map_some, Option.getD_some, heapC, depth_input, size_input]283    exact ⟨trivial, trivial⟩284  · have : ((List.range B).map (fun p => heapC B (partner k) p))[q]? = none := by285      rw [List.getElem?_eq_none]; simp; omega286    simp only [valC, cmpR, getC, List.getD_eq_getElem?_getD, this, Option.getD_none, depth_const, size_const]287    exact ⟨trivial, trivial⟩288289theorem flagC_res (B k : Nat) : depth (flagC B k) ≤ 5 ∧ size (flagC B k) ≤ pairF B := by290  have hv := valC_cmpR_res B k291  have hin : ∀ p, p < B → ∀ c ∈ [not (valC (cmpR B k) p), heapC B k p] ++292      (List.range p).map (fun p' => eqC (valC (cmpR B k) p') (heapC B k p')), depth c ≤ 3 ∧ size c ≤ 9 := by293    intro p hp c hc294    simp only [List.mem_append, List.mem_cons, List.mem_nil_iff, or_false, List.mem_map, List.mem_range] at hc295    rcases hc with (rfl | rfl) | ⟨q, hq, rfl⟩296    · simp only [depth_not, size_not]; have := hv p; omega297    · simp [heapC]298    · have := hv q299      simp only [eqC, heapC, depth_or, depth_and, depth_not, depth_input, size_or, size_and, size_not,300        size_input, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, listMax, List.foldr]301      omega302  constructor303  · unfold flagC ltC304    apply depth_or_le (D := 4); intro c hc305    obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hc306    apply depth_and_le (D := 3); intro c hc; exact (hin p (List.mem_range.mp hp) c hc).1307  · unfold flagC ltC pairF308    have h1 := ControllerBits.size_or_le' (S := (2 + B) * 9 + 1)309      (cs := (List.range B).map (fun p => and ([not (valC (cmpR B k) p), heapC B k p] ++310        (List.range p).map (fun p' => eqC (valC (cmpR B k) p') (heapC B k p'))))) (by311        intro c hc312        obtain ⟨p, hp, rfl⟩ := List.mem_map.mp hc313        have hp' := List.mem_range.mp hp314        have h2 := ControllerBits.size_and_le' (S := 9) (fun c hc => (hin p hp' c hc).2)315        simp only [List.length_append, List.length_cons, List.length_nil, List.length_map,316          List.length_range] at h2317        omega)318    rw [List.length_map, List.length_range] at h1; exact h1319320/-- RESOURCES of the mirror selector: every formula has depth ≤ 7 and size ≤ N(2F+1)+1321    with F = pairF B = O(B²). -/322theorem pairR_res (B N : Nat) : ∀ c ∈ (pairR B N).valid :: ((pairR B N).sel ++ (pairR B N).val),323    depth c ≤ 7 ∧ size c ≤ N * (2 * pairF B + 1) + 1 := by324  intro c hc325  simp only [pairR, List.mem_cons, List.mem_append, List.mem_map, List.mem_range] at hc326  rcases hc with rfl | ⟨k, hk, rfl⟩ | ⟨p, hp, rfl⟩327  · constructor328    · apply depth_or_le (D := 6); intro c hc329      obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc; have := (flagC_res B k).1; omega330    · have h1 := ControllerBits.size_or_le' (cs := (List.range N).map (flagC B)) (S := pairF B)331        (fun c hc => by obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc; exact (flagC_res B k).2)332      rw [List.length_map, List.length_range] at h1333      have := Nat.mul_le_mul_left N (show pairF B ≤ 2 * pairF B + 1 by omega); omega334  · refine ⟨by have := (flagC_res B k).1; omega, ?_⟩335    have h2 := (flagC_res B k).2336    have : 2 * pairF B + 1 ≤ N * (2 * pairF B + 1) := Nat.le_mul_of_pos_left _ (by omega)337    omega338  · constructor339    · apply depth_or_le (D := 6); intro c hc; obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc340      apply depth_and_le (D := 5); intro c hc341      simp only [List.mem_cons, List.mem_nil_iff, or_false] at hc342      rcases hc with rfl | rfl343      · exact (flagC_res B k).1344      · simp [heapC]345    · have h1 := ControllerBits.size_or_le'346        (cs := (List.range N).map (fun k => and [flagC B k, heapC B (partner k) p])) (S := 2 * pairF B + 1) (by347          intro c hc; obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc348          simp only [size_and, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, heapC, size_input]349          have := (flagC_res B k).2; have : 1 ≤ pairF B := by unfold pairF; omega350          omega)351      rw [List.length_map, List.length_range] at h1; exact h1352353/-- The binary mirror selector is a constant-depth (≤ 10), polynomial-size formula family354    reading only the B·N board bits. -/355theorem pairBin_bound (B N r : Nat) (hr : N ≤ 2 ^ r) (hN : N % 2 = 0) :356    BinBound (pairBin B N r) N B r 10 (4 * ((N + 2) * (N * (2 * pairF B + 1) + 1 + 2)) ^ 3) (B * N) :=357  encode_bound (pairR B N) (by simp [pairR]) (by simp [pairR]) hr358    (fun c hc => ⟨(pairR_res B N c hc).1, (pairR_res B N c hc).2, pairR_reads B N hN c hc⟩)359360/-! ## B. Finite-state shootout controllers -/361362/-- A finite-state controller over rollout heads: states are numbers; `head s` is the head363    queried in state s; `next s b` is the successor after outcome b; `out s` is the364    decision of a halting state. -/365structure FSM where366  init : Nat367  head : Nat → Nat368  next : Nat → Bool → Nat369  out : Nat → Option Bool370371/-- Run with fuel against outcome oracle o: decision and number of queries. -/372def FSM.run (C : FSM) (o : Nat → Bool) : Nat → Nat → Option Bool × Nat373  | 0, _ => (none, 0)374  | f + 1, s => match C.out s with375    | some d => (some d, 0)376    | none => ((C.run o f (C.next s (o (C.head s)))).1, (C.run o f (C.next s (o (C.head s)))).2 + 1)377378/-- The controller of the figure: states 0..B−1 query heads 0..B−1 in turn; state B379    declares σ ≠ 0 (N-position), state B+1 declares σ = 0 (P-position). -/380def shootout (B : Nat) : FSM :=381  ⟨0, id, fun s b => if b then B else if s + 1 < B then s + 1 else B + 1,382   fun s => if s = B then some true else if s = B + 1 then some false else none⟩383384/-- Index of the first true outcome among heads j..B−1 (B if none). -/385def firstHit (o : Nat → Bool) (B : Nat) : Nat → Nat386  | j => if h : j < B then (if o j then j else firstHit o B (j + 1)) else B387termination_by j => B - j388389theorem firstHit_ge (o : Nat → Bool) (B : Nat) : ∀ j, j ≤ B → j ≤ firstHit o B j := by390  intro j391  induction j using (measure (fun j => B - j)).wf.induction with392  | h j ih =>393    intro hj394    rw [firstHit]395    by_cases h : j < B396    · simp only [h, dif_pos]397      split398      · omega399      · have := ih (j + 1) (by show B - (j + 1) < B - j; omega) (by omega); omega400    · simp only [h, dif_neg, not_false_eq_true]; omega401402theorem run_query {B j : Nat} (o : Nat → Bool) (hj : j < B) (f : Nat) :403    (shootout B).run o (f + 1) j =404      (((shootout B).run o f (if o j then B else if j + 1 < B then j + 1 else B + 1)).1,405       ((shootout B).run o f (if o j then B else if j + 1 < B then j + 1 else B + 1)).2 + 1) := by406  have hout : (shootout B).out j = none := by407    simp only [shootout]; rw [if_neg (by omega), if_neg (by omega)]408  simp only [FSM.run, hout]; rfl409410theorem run_yes (B : Nat) (o : Nat → Bool) (f : Nat) : (shootout B).run o (f + 1) B = (some true, 0) := by411  simp [FSM.run, shootout]412413theorem run_no (B : Nat) (o : Nat → Bool) (f : Nat) : (shootout B).run o (f + 1) (B + 1) = (some false, 0) := by414  simp [FSM.run, shootout]415416theorem firstHit_hit {o : Nat → Bool} {B j : Nat} (hj : j < B) (ho : o j = true) : firstHit o B j = j := by417  rw [firstHit]; simp [hj, ho]418419theorem firstHit_miss {o : Nat → Bool} {B j : Nat} (hj : j < B) (ho : o j = false) :420    firstHit o B j = firstHit o B (j + 1) := by421  rw [firstHit]; simp [hj, ho]422423theorem firstHit_end {o : Nat → Bool} {B j : Nat} (hj : B ≤ j) : firstHit o B j = B := by424  rw [firstHit, dif_neg (by omega)]425426/-- RUN OF THE SHOOTOUT CONTROLLER from head j with k = B − j heads left: the decision is427    the OR of the queried outcomes; the number of queries is 1 + (first hit) − j, or the428    number of remaining heads if there is no hit. -/429theorem shootout_from {B : Nat} (o : Nat → Bool) : ∀ (k j : Nat), j + (k + 1) = B →430    (shootout B).run o (k + 2) j = (some ((List.range' j (k + 1)).any o), min (firstHit o B j) (B - 1) - j + 1) := by431  intro k432  induction k with433  | zero =>434    intro j h435    obtain rfl : B = j + 1 := by omega436    rw [run_query o (by omega)]437    cases ho : o j with438    | true => simp [run_yes, ho, firstHit_hit (show j < j + 1 by omega) ho]439    | false =>440      rw [if_neg (by simp), if_neg (by omega), run_no]441      simp [ho, firstHit_miss (show j < j + 1 by omega) ho, firstHit_end (o := o) (show j + 1 ≤ j + 1 by omega)]442  | succ k ih =>443    intro j h444    rw [run_query o (by omega)]445    cases ho : o j with446    | true =>447      simp only [if_true, run_yes, List.range'_succ, List.any_cons, ho, Bool.true_or, firstHit_hit (show j < B by omega) ho]448      simp; omega449    | false =>450      rw [if_neg (by simp), if_pos (by omega), ih (j + 1) (by omega)]451      have hge := firstHit_ge o B (j + 1) (by omega)452      simp only [List.range'_succ, List.any_cons, ho, Bool.false_or, firstHit_miss (show j < B by omega) ho,453        Prod.mk.injEq, true_and]454      omega455456/-- SHOOTOUT CONTROLLER THEOREM: started at head 0 with fuel B + 1 it outputs the OR of the457    B outcome bits, using at most B queries (one query if head 0 reports 1). -/458theorem shootout_spec {B : Nat} (hB : 1 ≤ B) (o : Nat → Bool) :459    ((shootout B).run o (B + 1) 0).1 = some ((List.range B).any o) ∧460    ((shootout B).run o (B + 1) 0).2 ≤ B ∧461    (o 0 = true → ((shootout B).run o (B + 1) 0).2 = 1) := by462  obtain ⟨k, rfl⟩ : ∃ k, B = k + 1 := ⟨B - 1, by omega⟩463  have h := shootout_from (B := k + 1) o k 0 (by omega)464  rw [show k + 1 + 1 = k + 2 by omega, h, List.range_eq_range']465  refine ⟨rfl, by simp; omega, fun h0 => ?_⟩466  simp [firstHit_hit (show 0 < k + 1 by omega) h0]467468/-- With the exact structured heads, the OR of the channel bits is (nim(P) ≠ 0). -/469theorem channels_or {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :470    (List.range B).any (fun j => rolloutWinner j P) = decide (nimSum P ≠ 0) := by471  have hσ := nimSum_lt hw472  apply Bool.eq_iff_iff.mpr473  simp only [List.any_eq_true, List.mem_range, decide_eq_true_iff, rolloutWinner_channel, channel]474  constructor475  · rintro ⟨j, hj, h⟩ h0476    rw [h0] at h; split at h <;> simp at h477  · intro h0478    by_cases h1 : (nimSum P).testBit 0 = true479    · exact ⟨0, by omega, by simp [h1]⟩480    · obtain ⟨k, hk, hbit⟩ := (pos_iff_bitLE hσ).1 (by omega)481      have hk0 : k ≠ 0 := by intro e; subst e; exact h1 hbit482      refine ⟨k, hk, ?_⟩483      simp [hk0, hbit, show (nimSum P).testBit 0 = false by simpa using h1]484485/-- The shootout over the exact structured heads decides whether P is an N-position. -/486theorem shootout_decides {B : Nat} (hB : 1 ≤ B) {P : List Nat} (hw : Width B P) :487    ((shootout B).run (fun j => rolloutWinner j P) (B + 1) 0).1 = some (decide (nimSum P ≠ 0)) ∧488    ((shootout B).run (fun j => rolloutWinner j P) (B + 1) 0).2 ≤ B := by489  obtain ⟨h1, h2, _⟩ := shootout_spec hB (fun j => rolloutWinner j P)490  exact ⟨by rw [h1, channels_or hB hw], h2⟩491492/-! ## C. Single-head baseline numbers -/493494theorem odd_count (n : Nat) : ((List.range (2 * n)).filter (fun σ => σ % 2 == 1)).length = n := by495  induction n with496  | zero => rfl497  | succ n ih =>498    rw [show 2 * (n + 1) = 2 * n + 1 + 1 by omega, List.range_succ, List.range_succ]499    simp only [List.filter_append, List.length_append, ih]500    simp <;> omega501502/-- Among the 2^B − 1 nonzero nim-sums of B ≥ 1 bits, exactly 2^{B−1} have σ₀ = 1, i.e.503    are detected by the classifier "declare N iff r₀ = 1" (r₀ = σ₀). -/504theorem detected_count {B : Nat} (hB : 1 ≤ B) :505    ((List.range (2 ^ B)).filter (fun σ => σ % 2 == 1)).length = 2 ^ (B - 1) ∧506    ((List.range (2 ^ B)).filter (fun σ => σ != 0)).length = 2 ^ B - 1 := by507  obtain ⟨k, rfl⟩ : ∃ k, B = k + 1 := ⟨B - 1, by omega⟩508  refine ⟨by rw [Nat.pow_succ, Nat.mul_comm, show k + 1 - 1 = k by omega]; exact odd_count _, ?_⟩509  have : ∀ n, ((List.range (n + 1)).filter (fun σ => σ != 0)).length = n := by510    intro n511    induction n with512    | zero => rfl513    | succ n ih => rw [List.range_succ, List.filter_append, List.length_append, ih]; simp514  have hp : 2 ^ (k + 1) = (2 ^ (k + 1) - 1) + 1 := by have := Nat.one_le_two_pow (n := k + 1); omega515  have h2 := this (2 ^ (k + 1) - 1)516  rw [← hp] at h2; exact h2517518theorem baseline_numbers :519    ((List.range (2 ^ 4)).filter (fun σ => σ % 2 == 1)).length = 8 ∧520    ((List.range (2 ^ 4)).filter (fun σ => σ != 0)).length = 15 ∧521    (1 / 2 : Rat) * 1 + 1 / 2 * (8 / 15) = 23 / 30 := by522  refine ⟨by decide, by decide, by grind⟩523524/-- The r₀ classifier never errs on P-positions: σ = 0 has σ₀ = 0. -/525theorem baseline_P (P : List Nat) (h : nimSum P = 0) : rolloutWinner 0 P = false := by526  rw [rolloutWinner_channel, h]; simp [channel]527528/-! ## D. Independent outcome flips -/529530/-- Product Bernoulli(ε) weight of a flip pattern. -/531def bw (ε : Rat) : List Bool → Rat532  | [] => 1533  | b :: e => (if b then ε else 1 - ε) * bw ε e534535theorem bw_total (ε : Rat) : ∀ L, rsum (bitvecs L) (bw ε) = 1536  | 0 => by simp [bitvecs, bw]537  | L + 1 => by538    rw [rsum_bitvecs_succ]539    simp only [bw, Bool.false_eq_true, if_false, if_true]540    rw [rsum_mul_left, rsum_mul_left, bw_total ε L]; grind541542theorem bw_sign (ε : Rat) : ∀ L, rsum (bitvecs L) (fun e => bw ε e * sgn (par e)) = (1 - 2 * ε) ^ L543  | 0 => by simp [bitvecs, bw, par, sgn]544  | L + 1 => by545    rw [rsum_bitvecs_succ]546    have e1 : rsum (bitvecs L) (fun v => bw ε (false :: v) * sgn (par (false :: v))) =547        (1 - ε) * rsum (bitvecs L) (fun v => bw ε v * sgn (par v)) := by548      rw [← rsum_mul_left]; apply rsum_congr; intro v _; simp [bw, par]; grind549    have e2 : rsum (bitvecs L) (fun v => bw ε (true :: v) * sgn (par (true :: v))) =550        (-ε) * rsum (bitvecs L) (fun v => bw ε v * sgn (par v)) := by551      rw [← rsum_mul_left]; apply rsum_congr; intro v _552      simp only [bw, if_true, par, Bool.true_xor]553      cases par v <;> simp [sgn] <;> grind554    rw [e1, e2, bw_sign ε L, Rat.pow_succ]; grind555556/-- OUTCOME-FLIP FORMULA: Pr[Y ⊕ E₁ ⊕ … ⊕ E_L = Y] = (1 + (1 − 2ε)^L)/2 for independent557    Bernoulli(ε) flips (exact, for every rational ε). -/558theorem flip_agree (ε : Rat) (L : Nat) :559    rsum (bitvecs L) (fun e => bw ε e * (if par e then 0 else 1)) = (1 + (1 - 2 * ε) ^ L) / 2 := by560  have h : ∀ e : List Bool, bw ε e * (if par e then 0 else 1) = (1 / 2) * bw ε e + (1 / 2) * (bw ε e * sgn (par e)) := by561    intro e; cases par e <;> simp [sgn] <;> grind562  rw [rsum_congr (fun e _ => h e), rsum_add, rsum_mul_left, rsum_mul_left, bw_total, bw_sign]; grind563564theorem flip_agree_noisy (ε : Rat) (L : Nat) (Y : Bool) :565    rsum (bitvecs L) (fun e => bw ε e * (if xor Y (par e) = Y then 1 else 0)) = (1 + (1 - 2 * ε) ^ L) / 2 := by566  rw [← flip_agree]; apply rsum_congr; intro e _; cases Y <;> cases par e <;> simp567568theorem par_append : ∀ x y : List Bool, par (x ++ y) = xor (par x) (par y)569  | [], y => by simp [par]570  | b :: x, y => by simp only [List.cons_append, par, par_append x y, Bool.xor_assoc]571572/-- CORRELATED FLIPS CAN CANCEL (Remark rem:noisy-rollout-decay): if the flips come in573    identical pairs, their XOR is always 0, so the observed bit always equals Y and there574    is no decay, whatever the flip probability. -/575theorem paired_flips_cancel (Y : Bool) (e : List Bool) : xor Y (par (e ++ e)) = Y := by576  rw [par_append]; cases par e <;> simp577578/-- Numerical example: ε = 1/100, L = 50 gives agreement in [0.682, 0.6822]. -/579theorem flip_example_nat : 364 * 50 ^ 50 ≤ 1000 * 49 ^ 50 ∧ 10000 * 49 ^ 50 ≤ 3644 * 50 ^ 50 := by580  constructor <;> decide581582/-! ## E. Spectral facts -/583584theorem pm_zipWith : ∀ (S T x : List Bool), S.length = T.length →585    pm (List.zipWith xor S T) x = xor (pm S x) (pm T x)586  | [], [], _, _ => by simp [pm]587  | s :: S, t :: T, [], _ => by simp [pm]588  | s :: S, t :: T, b :: x, h => by589    simp only [List.zipWith_cons_cons, pm]590    rw [pm_zipWith S T x (by simpa using h)]591    cases s <;> cases t <;> cases b <;> simp592  | [], _ :: _, _, h => by simp at h593  | _ :: _, [], _, h => by simp at h594595/-- Character sums: Σ_x (−1)^{⟨U,x⟩} = 2^n if U = 0, and 0 otherwise. -/596theorem char_sum : ∀ U : List Bool,597    rsum (bitvecs U.length) (fun x => sgn (pm U x)) = if U.all (fun b => b == false) then (2 : Rat) ^ U.length else 0598  | [] => by simp [bitvecs, pm, sgn]599  | u :: U => by600    simp only [List.length_cons]601    rw [rsum_bitvecs_succ]602    simp only [pm, Bool.and_false, Bool.false_xor, Bool.and_true]603    rw [char_sum U]604    cases u605    · simp only [Bool.false_xor, List.all_cons, beq_self_eq_true, Bool.true_and]606      have : rsum (bitvecs U.length) (fun v => sgn (pm U v)) = if U.all (fun b => b == false) then (2 : Rat) ^ U.length else 0 :=607        char_sum U608      rw [this]; split <;> simp [Rat.pow_succ] <;> grind609    · have e : rsum (bitvecs U.length) (fun v => sgn (xor true (pm U v))) =610          (-1) * rsum (bitvecs U.length) (fun v => sgn (pm U v)) := by611        rw [← rsum_mul_left]; apply rsum_congr; intro v _; cases pm U v <;> simp [sgn] <;> grind612      rw [e, char_sum U]613      simp only [List.all_cons]614      split <;> simp <;> grind615616theorem zipWith_xor_all_false : ∀ (S T : List Bool), S.length = T.length →617    ((List.zipWith xor S T).all (fun b => b == false) = true ↔ S = T)618  | [], [], _ => by simp619  | s :: S, t :: T, h => by620    simp only [List.zipWith_cons_cons, List.all_cons, Bool.and_eq_true, List.cons.injEq]621    rw [zipWith_xor_all_false S T (by simpa using h)]622    cases s <;> cases t <;> simp623  | [], _ :: _, h => by simp at h624  | _ :: _, [], h => by simp at h625626/-- ORTHONORMALITY of the characters χ_S(x) = (−1)^{⟨S,x⟩} on {0,1}^n. -/627theorem char_orth (S T : List Bool) (h : S.length = T.length) :628    rsum (bitvecs S.length) (fun x => sgn (pm S x) * sgn (pm T x)) / (2 : Rat) ^ S.length = if S = T then 1 else 0 := by629  have e : ∀ x, sgn (pm S x) * sgn (pm T x) = sgn (pm (List.zipWith xor S T) x) := by630    intro x; rw [pm_zipWith S T x h]; cases pm S x <;> cases pm T x <;> simp [sgn] <;> grind631  rw [rsum_congr (fun x _ => e x)]632  have hl : (List.zipWith xor S T).length = S.length := by simp [h]633  have hs := char_sum (List.zipWith xor S T)634  rw [hl] at hs635  rw [hs]636  have hpos := two_pow_pos' S.length637  have hne : (2 : Rat) ^ S.length ≠ 0 := Rat.ne_of_gt hpos638  by_cases hST : S = T639  · rw [if_pos ((zipWith_xor_all_false S T h).2 hST), if_pos hST]640    rw [Rat.div_def]; exact Rat.mul_inv_cancel _ hne641  · have : ¬ ((List.zipWith xor S T).all (fun b => b == false) = true) := fun h' => hST ((zipWith_xor_all_false S T h).1 h')642    rw [if_neg this, if_neg hST]643    rw [Rat.div_def, Rat.zero_mul]644645theorem dotB_low {j : Nat} (v : Nat) : ∀ B, B ≤ j → dotB B (2 ^ j) v = false646  | 0, _ => rfl647  | B + 1, h => by648    simp only [dotB, Nat.testBit_two_pow, dotB_low (j := j) v B (by omega)]649    simp; omega650651theorem dotB_pow {j : Nat} (v : Nat) : ∀ B, j < B → dotB B (2 ^ j) v = v.testBit j652  | 0, h => by omega653  | B + 1, h => by654    simp only [dotB, Nat.testBit_two_pow]655    by_cases hj : j = B656    · subst hj; rw [dotB_low v j (Nat.le_refl _)]; simp657    · rw [dotB_pow (j := j) v B (by omega)]; simp [hj]658659theorem count_eq_one (j : Nat) : ∀ B, ((List.range B).filter (fun k => decide (j = k))).length = if j < B then 1 else 0660  | 0 => by simp661  | B + 1 => by662    rw [List.range_succ, List.filter_append, List.length_append, count_eq_one j B]663    by_cases h1 : j < B664    · rw [if_pos h1, if_pos (by omega)]; simp; omega665    · by_cases h2 : j = B666      · subst h2; simp667      · rw [if_neg h1, if_neg (by omega)]; simp; omega668669theorem ones_toBitsBE_count : ∀ (B u : Nat), Bridge.ones (toBitsBE B u) = ((List.range B).filter (fun k => u.testBit k)).length670  | 0, u => by simp [toBitsBE, Bridge.ones]671  | B + 1, u => by672    simp only [toBitsBE, Bridge.ones, List.filter_cons, List.range_succ, List.filter_append, List.length_append]673    have := ones_toBitsBE_count B u674    unfold Bridge.ones at this675    cases h : u.testBit B <;> simp [h, this] <;> omega676677/-- NIM-SUM BITS ARE DEGREE-N CHARACTERS: bit j of nim(P) is the parity of the inputs on678    a mask with exactly N ones (one coordinate per heap). -/679theorem nimsum_bit_character {B N j : Nat} (hj : j < B) {x : List Bool} (hx : x ∈ bitvecs (B * N)) :680    (nimSum (decodeBoard B N x)).testBit j = pm (maskU B N (2 ^ j)) x ∧ Bridge.ones (maskU B N (2 ^ j)) = N := by681  refine ⟨by rw [← chi_parity B N (2 ^ j) hx]; exact (dotB_pow _ B hj).symm, ?_⟩682  rw [ones_maskU, ones_toBitsBE_count]683  have : (List.range B).filter (fun k => (2 ^ j).testBit k) = (List.range B).filter (fun k => decide (j = k)) := by684    apply List.filter_congr; intro k _; rw [Nat.testBit_two_pow]685  rw [this, count_eq_one, if_pos hj, Nat.mul_one]686687/-- DELTA BITS ARE TWO-COORDINATE CHARACTERS: across one legal move (heap value a → b),688    bit k of the difference is a_k ⊕ b_k. -/689theorem delta_bit_local {Q Q' : List Nat} (hm : Move Q Q') :690    ∃ pre a post b, Q = pre ++ a :: post ∧ Q' = pre ++ b :: post ∧691      ∀ k, (nimSum Q ^^^ nimSum Q').testBit k = xor (a.testBit k) (b.testBit k) := by692  obtain ⟨pre, a, post, b, h1, h2, _⟩ := hm693  refine ⟨pre, a, post, b, h1, h2, fun k => ?_⟩694  rw [h1, h2, one_heap_difference, Nat.testBit_xor]695696/-! ## F. The initialisation boundary -/697698/-- The matching-delta policy completed by "subtract one from the first nonempty heap"699    whenever there is no previous frame or no matching response. -/700def mdPolicy (prev : Option (List Nat)) (cur : List Nat) : Option (List Nat) :=701  match prev with702  | none => subFirstPos cur703  | some Q => match cancelFirst (nimSum Q ^^^ nimSum cur) cur with704    | some R => some R705    | none => subFirstPos cur706707/-- From the winning position (2) the completed matching-delta policy plays (2) → (1) and708    then (as the next mover, delta 2 ⊕ 1 = 3 is not realisable from (1)) (1) → (0): the709    first player loses although (2) is winning. -/710theorem init_counterexample :711    Win [2] ∧ mdPolicy none [2] = some [1] ∧ cancelFirst (nimSum [2] ^^^ nimSum [1]) [1] = none ∧712    mdPolicy (some [2]) [1] = some [0] ∧ Win [1] ∧ Lose [0] := by713  refine ⟨(win_iff _).2 (by decide), by decide, by decide, by decide, (win_iff _).2 (by decide),714    (lose_iff _).2 (by decide)⟩715716/-! ## G. Single-policy information bound (one-heap correction) -/717718theorem 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]721722723/-! ### Board-level recall and the numerical flip example -/724725theorem rsum_filter_count (l : List Nat) (p : Nat → Bool) (c : Rat) :726    rsum l (fun a => if p a then c else 0) = ((l.filter p).length : Rat) * c := by727  induction l with728  | nil => simp729  | cons a l ih =>730    simp only [rsum_cons, List.filter_cons]731    rw [ih]; cases p a <;> simp <;> grind732733/-- For uniform boards of N+1 heaps, the number of boards whose nim-sum satisfies a734    predicate p is (#values a < 2^B with p a) · (2^B)^N (nim-sum is exactly uniform). -/735theorem boards_count (B N : Nat) (p : Nat → Bool) :736    rsum (boards (2 ^ B) (N + 1)) (fun P => if p (nimSum P) then 1 else 0) =737      (((List.range (2 ^ B)).filter p).length : Rat) * ((2 ^ B : Nat) : Rat) ^ N := by738  have hexp : ∀ P ∈ boards (2 ^ B) (N + 1), (if p (nimSum P) then (1 : Rat) else 0) =739      rsum (List.range (2 ^ B)) (fun a => if a = nimSum P then (if p a then 1 else 0) else 0) := by740    intro P hP741    rw [rsum_range_ite (2 ^ B) (nimSum P) (fun a => if p a then 1 else 0), if_pos (sigma_lt hP)]742  rw [rsum_congr hexp, rsum_comm]743  have hin : ∀ a ∈ List.range (2 ^ B),744      rsum (boards (2 ^ B) (N + 1)) (fun P => if a = nimSum P then (if p a then (1 : Rat) else 0) else 0) =745        (if p a then ((2 ^ B : Nat) : Rat) ^ N else 0) := by746    intro a ha747    have hu := sigma_uniform B N a (List.mem_range.mp ha)748    cases hpa : p a749    · simp only [Bool.false_eq_true, if_false]; rw [rsum_congr (fun _ _ => by split <;> rfl)]; simp [rsum_zero]750    · simp only [if_true]751      rw [← hu]; apply rsum_congr; intro P _752      by_cases h : a = nimSum P753      · rw [if_pos h, if_pos h.symm]754      · rw [if_neg h, if_neg (Ne.symm h)]755  rw [rsum_congr hin, rsum_filter_count]756757/-- BOARD-LEVEL RECALL OF THE r₀ CLASSIFIER: among uniform boards with nonzero nim-sum the758    detected fraction is 2^{B−1}/(2^B − 1); for B = 4 it is 8/15. -/759theorem board_recall {B : Nat} (hB : 1 ≤ B) (N : Nat) :760    rsum (boards (2 ^ B) (N + 1)) (fun P => if (nimSum P % 2 == 1) then 1 else 0) =761      ((2 ^ (B - 1) : Nat) : Rat) * ((2 ^ B : Nat) : Rat) ^ N ∧762    rsum (boards (2 ^ B) (N + 1)) (fun P => if (nimSum P != 0) then 1 else 0) =763      ((2 ^ B - 1 : Nat) : Rat) * ((2 ^ B : Nat) : Rat) ^ N := by764  obtain ⟨h1, h2⟩ := detected_count hB765  refine ⟨?_, ?_⟩766  · rw [boards_count B N (fun σ => σ % 2 == 1), h1]767  · rw [boards_count B N (fun σ => σ != 0), h2]768769theorem pow_frac (a b : Nat) (hb : 0 < b) : ∀ n : Nat, ((a : Rat) / b) ^ n * (b : Rat) ^ n = (a : Rat) ^ n770  | 0 => by simp771  | n + 1 => by772    have hb' : (b : Rat) ≠ 0 := by exact_mod_cast (show b ≠ 0 by omega)773    have ih := pow_frac a b hb n774    rw [Rat.pow_succ, Rat.pow_succ, Rat.pow_succ]775    have e : ((a : Rat) / b) * b = a := by rw [Rat.div_def, Rat.mul_assoc, Rat.inv_mul_cancel _ hb', Rat.mul_one]776    calc ((a : Rat) / b) ^ n * (a / b) * ((b : Rat) ^ n * b) = (((a : Rat) / b) ^ n * (b : Rat) ^ n) * ((a / b) * b) := by777          grind778      _ = (a : Rat) ^ n * a := by rw [ih, e]779780theorem le_div_of_mul_le' {x y d : Rat} (hd : 0 < d) (h : y * d ≤ x) : y ≤ x / d := by781  apply Rat.le_of_mul_le_mul_right _ hd782  have e : x / d * d = x := by783    rw [Rat.div_def, Rat.mul_assoc, Rat.inv_mul_cancel _ (Rat.ne_of_gt hd), Rat.mul_one]784  rw [e]; exact h785786/-- NUMERICAL EXAMPLE of Remark rem:noisy-rollout-decay: for ε = 1/100 and L = 50 the787    agreement probability lies between 0.682 and 0.6822. -/788theorem flip_example :789    (682 / 1000 : Rat) ≤ (1 + (1 - 2 * (1 / 100 : Rat)) ^ 50) / 2 ∧790    (1 + (1 - 2 * (1 / 100 : Rat)) ^ 50) / 2 ≤ 6822 / 10000 := by791  have e1 : (1 - 2 * (1 / 100 : Rat)) = ((49 : Nat) : Rat) / ((50 : Nat) : Rat) := by grind792  rw [e1]793  have hq := pow_frac 49 50 (by decide) 50794  generalize (((49 : Nat) : Rat) / ((50 : Nat) : Rat)) ^ 50 = q at hq ⊢795  have hT : (0 : Rat) < ((50 : Nat) : Rat) ^ 50 := Rat.pow_pos (by decide)796  obtain ⟨n1, n2⟩ := flip_example_nat797  have c1 : (364 : Rat) * ((50 : Nat) : Rat) ^ 50 ≤ 1000 * ((49 : Nat) : Rat) ^ 50 := by exact_mod_cast n1798  have c2 : (10000 : Rat) * ((49 : Nat) : Rat) ^ 50 ≤ 3644 * ((50 : Nat) : Rat) ^ 50 := by exact_mod_cast n2799  rw [← hq] at c1 c2800  generalize ((50 : Nat) : Rat) ^ 50 = T at hT c1 c2801  have d1 : (364 : Rat) ≤ 1000 * q := by802    apply Rat.le_of_mul_le_mul_right _ hT803    have : 1000 * (q * T) = (1000 * q) * T := by grind804    rw [← this]; exact c1805  have d2 : 10000 * q ≤ (3644 : Rat) := by806    apply Rat.le_of_mul_le_mul_right _ hT807    have : 10000 * (q * T) = (10000 * q) * T := by grind808    rw [← this]; exact c2809  have two : (0 : Rat) < 2 := by decide810  constructor811  · have ea : (682 / 1000 : Rat) = (1364 / 1000) / 2 := by grind812    rw [ea]813    apply div_le_div_of_le two814    apply le_div_of_mul_le (by decide)815    have : (1 + q) * 1000 = 1000 + 1000 * q := by grind816    rw [this]; grind817  · have eb : (6822 / 10000 : Rat) = (13644 / 10000) / 2 := by grind818    rw [eb]819    apply div_le_div_of_le two820    apply le_div_of_mul_le' (by decide)821    have : (1 + q) * 10000 = 10000 + 10000 * q := by grind822    rw [this]; grind823824/-! ## H. Two small worked claims -/825826/-- FIGURE fig:restoration-example: from (3,5,6) (nim-sum 0) the opponent plays 5 → 4827    (nim-sum 1, δ = 1); the restoration rule answers 3 → 2, restoring nim-sum 0. -/828theorem restoration_figure :829    nimSum [3, 5, 6] = 0 ∧ Move [3, 5, 6] [3, 4, 6] ∧ nimSum [3, 4, 6] = 1 ∧ (5 ^^^ 4 : Nat) = 1 ∧830    restore [3, 5, 6] [3, 4, 6] = some [2, 4, 6] ∧ Move [3, 4, 6] [2, 4, 6] ∧ nimSum [2, 4, 6] = 0 := by831  refine ⟨by decide, ⟨[3], 5, [6], 4, rfl, rfl, by decide⟩, by decide, by decide, by decide,832    ⟨[], 3, [4, 6], 2, rfl, rfl, by decide⟩, by decide⟩833834theorem nimSum_bitBoard (k : Nat) : ∀ P : List Nat,835    (nimSum (P.map (fun h => if h.testBit k then 1 else 0))).testBit 0 = (nimSum P).testBit k836  | [] => by simp [nimSum]837  | h :: P => by838    have ih := nimSum_bitBoard k P839    simp only [List.map_cons, nimSum] at ih ⊢840    rw [Nat.testBit_xor, Nat.testBit_xor, ih]841    by_cases hb : h.testBit k <;> simp [hb]842843/-- WHY ARBITRARY START POSITIONS ARE EXCLUDED (Definition def:agent-types): a single844    rollout of π₀ on the board whose heaps are the k-th bits of P returns σ_k(P). -/845theorem bitBoard_query (k : Nat) (P : List Nat) :846    rolloutWinner 0 (P.map (fun h => if h.testBit k then 1 else 0)) = (nimSum P).testBit k := by847  rw [rolloutWinner_channel]; simp only [channel, if_true]; exact nimSum_bitBoard k P848849/-! ## Axiom audit -/850851#print axioms partner_partner852#print axioms partner_ne853#print axioms partner_lt854#print axioms secondWins_sound855#print axioms getD_set_ne'856#print axioms getD_set_eq'857#print axioms paired_move858#print axioms toNatBE_heap859#print axioms flagC_eval860#print axioms pairR_correct861#print axioms pairing_wins862#print axioms paired_lose863#print axioms pairR_reads864#print axioms valC_cmpR_res865#print axioms flagC_res866#print axioms pairR_res867#print axioms pairBin_bound868#print axioms firstHit_ge869#print axioms run_query870#print axioms run_yes871#print axioms run_no872#print axioms firstHit_hit873#print axioms firstHit_miss874#print axioms firstHit_end875#print axioms shootout_from876#print axioms shootout_spec877#print axioms channels_or878#print axioms shootout_decides879#print axioms odd_count880#print axioms detected_count881#print axioms baseline_numbers882#print axioms baseline_P883#print axioms bw_total884#print axioms bw_sign885#print axioms flip_agree886#print axioms flip_agree_noisy887#print axioms par_append888#print axioms paired_flips_cancel889#print axioms flip_example_nat890#print axioms pm_zipWith891#print axioms char_sum892#print axioms zipWith_xor_all_false893#print axioms char_orth894#print axioms dotB_low895#print axioms dotB_pow896#print axioms count_eq_one897#print axioms ones_toBitsBE_count898#print axioms nimsum_bit_character899#print axioms delta_bit_local900#print axioms init_counterexample901#print axioms single_policy_correction902#print axioms rsum_filter_count903#print axioms boards_count904#print axioms board_recall905#print axioms pow_frac906#print axioms le_div_of_mul_le'907#print axioms flip_example908#print axioms restoration_figure909#print axioms nimSum_bitBoard910#print axioms bitBoard_query911912