NimProbability

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 NimGame23/- Phase 2, target 3.  Written by Claude for the independent review4   (9 October 2026).  Lean 4.26.0, core/Std only (core `Rat`).56   Paper Appendix G(i) as a finite rational-probability theorem.7   Model: q = 2^B, N independent uniform B-bit heaps.  The uniform product8   distribution is the counting measure on `boards q N` (all q^N boards), so9   E[f] = (sum over boards of f) / q^N.1011   EXTERNAL INPUT.  `CorrHyp B N F η` is the parity-correlation premise, stated as12   a theorem hypothesis: for every observed bit b, every value a < q and every13   nonzero u < q,  |E[H_{b,a}(P) * chi_u(P)]| <= η.  It is NOT an axiom, and it14   is NOT proved here.  The paper justifies it by AC0 membership of the fixed-b15   readout indicators together with the classical AC0 parity-correlation bound16   (Hastad); that circuit-to-correlation bridge is outside this file.1718   Everything else is proved: uniformity of sigma, character orthogonality on19   F_2^B, the exact-value indicator expansion, the per-value error bound,20   disjointness, conditioning on sigma ≠ 0, and the link between legal success21   and g_{ell(sigma)} = sigma. -/2223namespace NimAudit24namespace Prob2526open Game Rollout2728attribute [local simp] Rat.add_zero Rat.zero_add Rat.zero_mul Rat.mul_zero Rat.one_mul29  Rat.neg_mul Rat.mul_neg3031/-! ## Finite sums over Rat -/3233def rsum {α : Type} (l : List α) (f : α → Rat) : Rat := (l.map f).sum3435@[simp] theorem rsum_nil {α : Type} (f : α → Rat) : rsum [] f = 0 := rfl3637@[simp] theorem rsum_cons {α : Type} (a : α) (l : List α) (f : α → Rat) :38    rsum (a :: l) f = f a + rsum l f := by39  simp [rsum]4041theorem rsum_append {α : Type} (l m : List α) (f : α → Rat) :42    rsum (l ++ m) f = rsum l f + rsum m f := by43  induction l with44  | nil => simp45  | cons a l ih => simp only [List.cons_append, rsum_cons, ih]; grind4647theorem rsum_congr {α : Type} {l : List α} {f g : α → Rat} (h : ∀ x ∈ l, f x = g x) :48    rsum l f = rsum l g := by49  induction l with50  | nil => rfl51  | cons a l ih =>52    simp only [rsum_cons]53    rw [h a (by simp), ih (fun x hx => h x (List.mem_cons_of_mem _ hx))]5455theorem rsum_zero {α : Type} (l : List α) : rsum l (fun _ => 0) = 0 := by56  induction l with57  | nil => rfl58  | cons a l ih => simp [ih]5960theorem rsum_add {α : Type} (l : List α) (f g : α → Rat) :61    rsum l (fun x => f x + g x) = rsum l f + rsum l g := by62  induction l with63  | nil => simp64  | cons a l ih => simp only [rsum_cons, ih]; grind6566theorem rsum_mul_left {α : Type} (l : List α) (c : Rat) (f : α → Rat) :67    rsum l (fun x => c * f x) = c * rsum l f := by68  induction l with69  | nil => simp70  | cons a l ih => simp only [rsum_cons, ih]; grind7172theorem rsum_le {α : Type} {l : List α} {f g : α → Rat} (h : ∀ x ∈ l, f x ≤ g x) :73    rsum l f ≤ rsum l g := by74  induction l with75  | nil => exact Rat.le_refl76  | cons a l ih =>77    simp only [rsum_cons]78    have h1 := h a (by simp)79    have h2 := ih (fun x hx => h x (List.mem_cons_of_mem _ hx))80    grind8182theorem rsum_const {α : Type} (l : List α) (c : Rat) :83    rsum l (fun _ => c) = (l.length : Rat) * c := by84  induction l with85  | nil => simp86  | cons a l ih => simp only [rsum_cons, ih, List.length_cons]; grind8788theorem rsum_comm {α β : Type} (l : List α) (m : List β) (f : α → β → Rat) :89    rsum l (fun x => rsum m (f x)) = rsum m (fun y => rsum l (fun x => f x y)) := by90  induction l with91  | nil => simp [rsum_zero]92  | cons a l ih => simp only [rsum_cons, ih, rsum_add]9394theorem rsum_map {α β : Type} (l : List α) (g : α → β) (f : β → Rat) :95    rsum (l.map g) f = rsum l (fun x => f (g x)) := by96  simp only [rsum, List.map_map]; rfl9798theorem rsum_flatMap {α β : Type} (l : List α) (g : α → List β) (f : β → Rat) :99    rsum (l.flatMap g) f = rsum l (fun x => rsum (g x) f) := by100  induction l with101  | nil => simp [rsum]102  | cons a l ih => simp only [List.flatMap_cons, rsum_append, rsum_cons, ih]103104theorem rsum_bound {α : Type} {l : List α} {f : α → Rat} {e : Rat}105    (h : ∀ x ∈ l, -e ≤ f x ∧ f x ≤ e) :106    -((l.length : Rat) * e) ≤ rsum l f ∧ rsum l f ≤ (l.length : Rat) * e := by107  induction l with108  | nil => simp only [rsum_nil, List.length_nil]; constructor <;> grind109  | cons a l ih =>110    simp only [rsum_cons, List.length_cons]111    have h1 := h a (by simp)112    have h2 := ih (fun x hx => h x (List.mem_cons_of_mem _ hx))113    constructor <;> grind114115theorem rsum_range_ite (q c : Nat) (v : Nat → Rat) :116    rsum (List.range q) (fun a => if a = c then v a else 0) = if c < q then v c else 0 := by117  induction q with118  | zero => simp119  | succ q ih =>120    rw [List.range_succ, rsum_append, ih]121    simp only [rsum_cons, rsum_nil]122    by_cases h1 : c < q123    · have : q ≠ c := by omega124      simp [h1, this, show c < q + 1 by omega]125    · by_cases h2 : c = q126      · subst h2; simp127      · have : q ≠ c := fun e => h2 e.symm128        simp [h1, this, show ¬ c < q + 1 by omega]129130/-- Sum over u ≠ 0 of g u, written over `range q` with the u = 0 term removed. -/131def offZero (g : Nat → Rat) (u : Nat) : Rat := if u = 0 then 0 else g u132133theorem rsum_range_split0 {q : Nat} (hq : 0 < q) (g : Nat → Rat) :134    rsum (List.range q) g = g 0 + rsum (List.range q) (offZero g) := by135  have e : rsum (List.range q) g =136      rsum (List.range q) (fun u => (if u = 0 then g u else 0) + offZero g u) := by137    apply rsum_congr138    intro u _139    by_cases hu : u = 0 <;> simp [offZero, hu]140  rw [e, rsum_add, rsum_range_ite q 0 g]141  simp [hq]142143theorem range_one_add (q : Nat) (hq : 0 < q) :144    List.range q = List.range 1 ++ (List.range (q - 1)).map (1 + ·) := by145  have : q = 1 + (q - 1) := by omega146  conv => lhs; rw [this]147  exact List.range_add148149theorem rsum_offZero_bound {q : Nat} (hq : 0 < q) (g : Nat → Rat) (e : Rat)150    (h : ∀ u, 0 < u → u < q → -e ≤ g u ∧ g u ≤ e) :151    -(((q - 1 : Nat) : Rat) * e) ≤ rsum (List.range q) (offZero g) ∧152      rsum (List.range q) (offZero g) ≤ ((q - 1 : Nat) : Rat) * e := by153  rw [range_one_add q hq, rsum_append, rsum_map]154  have h0 : rsum (List.range 1) (offZero g) = 0 := by simp [offZero]155  rw [h0]156  have hb := rsum_bound (l := List.range (q - 1)) (f := fun x => offZero g (1 + x)) (e := e)157    (by158      intro x hx159      have hx' := List.mem_range.mp hx160      simp only [offZero, show 1 + x ≠ 0 by omega, if_false]161      exact h (1 + x) (by omega) (by omega))162  rw [List.length_range] at hb163  constructor <;> grind164165theorem rsum_offZero_const {q : Nat} (hq : 0 < q) (c : Rat) :166    rsum (List.range q) (offZero (fun _ => c)) = ((q - 1 : Nat) : Rat) * c := by167  rw [range_one_add q hq, rsum_append, rsum_map]168  have h0 : rsum (List.range 1) (offZero (fun _ => c)) = 0 := by simp [offZero]169  rw [h0]170  have : rsum (List.range (q - 1)) (fun x => offZero (fun _ => c) (1 + x)) =171      rsum (List.range (q - 1)) (fun _ => c) := by172    apply rsum_congr; intro x _; simp [offZero]173  rw [this, rsum_const, List.length_range]174  grind175176theorem rsum_offZero_add (q : Nat) (f g : Nat → Rat) :177    rsum (List.range q) (offZero (fun u => f u + g u)) =178      rsum (List.range q) (offZero f) + rsum (List.range q) (offZero g) := by179  rw [← rsum_add]180  apply rsum_congr; intro u _181  by_cases hu : u = 0 <;> simp [offZero, hu]182183theorem rsum_offZero_le {q : Nat} {f g : Nat → Rat} (h : ∀ u, 0 < u → u < q → f u ≤ g u) :184    rsum (List.range q) (offZero f) ≤ rsum (List.range q) (offZero g) := by185  apply rsum_le186  intro u hu187  have hu' := List.mem_range.mp hu188  by_cases h0 : u = 0189  · simp [offZero, h0]; exact Rat.le_refl190  · simp only [offZero, h0, if_false]; exact h u (by omega) hu'191192/-! ## The uniform model on boards -/193194/-- All boards of N heaps with values below q (each exactly once). -/195def boards (q : Nat) : Nat → List (List Nat)196  | 0 => [[]]197  | N + 1 => (List.range q).flatMap (fun h => (boards q N).map (h :: ·))198199theorem mem_boards {q N : Nat} {P : List Nat} (h : P ∈ boards q N) :200    P.length = N ∧ ∀ x ∈ P, x < q := by201  induction N generalizing P with202  | zero => simp [boards] at h; subst h; simp203  | succ N ih =>204    simp only [boards, List.mem_flatMap, List.mem_range, List.mem_map] at h205    obtain ⟨x, hx, P', hP', rfl⟩ := h206    obtain ⟨h1, h2⟩ := ih hP'207    refine ⟨by simp [h1], ?_⟩208    intro y hy209    rcases List.mem_cons.mp hy with rfl | hy210    · exact hx211    · exact h2 y hy212213theorem rsum_boards_succ (q N : Nat) (f : List Nat → Rat) :214    rsum (boards q (N + 1)) f =215      rsum (List.range q) (fun h => rsum (boards q N) (fun P => f (h :: P))) := by216  simp only [boards, rsum_flatMap, rsum_map]217218/-- There are q^N boards. -/219theorem count_boards (q N : Nat) : rsum (boards q N) (fun _ => 1) = (q : Rat) ^ N := by220  induction N with221  | zero => simp [boards]222  | succ N ih =>223    rw [rsum_boards_succ, rsum_congr (g := fun _ => (q : Rat) ^ N) (fun h _ => ih),224      rsum_const, List.length_range]225    grind226227theorem xor_eq_iff (h s a : Nat) : (h ^^^ s = a) ↔ (s = h ^^^ a) := by228  constructor229  · intro e; rw [← e, xor_cancel_left]230  · intro e; rw [e, xor_cancel_left]231232/-- UNIFORMITY OF SIGMA: for N ≥ 1 (written N + 1) and every a < 2^B, exactly233    q^N of the q^(N+1) boards have nim-sum a. -/234theorem sigma_uniform (B N a : Nat) (ha : a < 2 ^ B) :235    rsum (boards (2 ^ B) (N + 1)) (fun P => if nimSum P = a then 1 else 0) =236      ((2 ^ B : Nat) : Rat) ^ N := by237  induction N generalizing a with238  | zero =>239    rw [rsum_boards_succ]240    simp only [boards, rsum_cons, rsum_nil, nimSum, Nat.xor_zero, Rat.add_zero]241    rw [rsum_range_ite (2 ^ B) a (fun _ => 1)]242    simp [ha]243  | succ N ih =>244    rw [rsum_boards_succ]245    have : ∀ h ∈ List.range (2 ^ B),246        rsum (boards (2 ^ B) (N + 1)) (fun P => if nimSum (h :: P) = a then 1 else 0) =247          ((2 ^ B : Nat) : Rat) ^ N := by248      intro h hh249      have hlt : h ^^^ a < 2 ^ B := Nat.xor_lt_two_pow (List.mem_range.mp hh) ha250      rw [← ih (h ^^^ a) hlt]251      apply rsum_congr252      intro P _253      simp only [nimSum, xor_eq_iff]254    rw [rsum_congr this, rsum_const, List.length_range]255    grind256257/-! ## Characters on F_2^B -/258259/-- The F_2 inner product of the first B bits of u and v. -/260def dotB : Nat → Nat → Nat → Bool261  | 0, _, _ => false262  | B + 1, u, v => xor (dotB B u v) (u.testBit B && v.testBit B)263264/-- chi_u(v) = (-1)^<u,v>. -/265def chi (B u v : Nat) : Rat := if dotB B u v then -1 else 1266267theorem dotB_xor_right (B u v w : Nat) :268    dotB B u (v ^^^ w) = xor (dotB B u v) (dotB B u w) := by269  induction B with270  | zero => rfl271  | succ B ih =>272    simp only [dotB, ih, Nat.testBit_xor]273    cases dotB B u v <;> cases dotB B u w <;> cases u.testBit B <;>274      cases v.testBit B <;> cases w.testBit B <;> rfl275276theorem dotB_xor_left (B u w v : Nat) :277    dotB B (u ^^^ w) v = xor (dotB B u v) (dotB B w v) := by278  induction B with279  | zero => rfl280  | succ B ih =>281    simp only [dotB, ih, Nat.testBit_xor]282    cases dotB B u v <;> cases dotB B w v <;> cases u.testBit B <;>283      cases w.testBit B <;> cases v.testBit B <;> rfl284285theorem dotB_zero_left (B v : Nat) : dotB B 0 v = false := by286  induction B with287  | zero => rfl288  | succ B ih => simp [dotB, ih]289290theorem dotB_congr_left {B u u' : Nat} (v : Nat) (h : ∀ i < B, u.testBit i = u'.testBit i) :291    dotB B u v = dotB B u' v := by292  induction B with293  | zero => rfl294  | succ B ih =>295    simp only [dotB]296    rw [ih (fun i hi => h i (by omega)), h B (by omega)]297298theorem chi_xor_right (B u v w : Nat) : chi B u (v ^^^ w) = chi B u v * chi B u w := by299  unfold chi300  rw [dotB_xor_right]301  cases dotB B u v <;> cases dotB B u w <;> simp <;> grind302303theorem chi_zero_left (B v : Nat) : chi B 0 v = 1 := by304  simp [chi, dotB_zero_left]305306theorem chi_cases (B u v : Nat) : chi B u v = 1 ∨ chi B u v = -1 := by307  unfold chi; split <;> simp308309/-- Bits 0..B-1 of v are all zero. -/310def lowZero : Nat → Nat → Bool311  | 0, _ => true312  | B + 1, v => lowZero B v && !v.testBit B313314theorem lowZero_spec (B v : Nat) : lowZero B v = true ↔ ∀ i < B, v.testBit i = false := by315  induction B with316  | zero => simp [lowZero]317  | succ B ih =>318    show (lowZero B v && !v.testBit B) = true ↔ _319    cases h2 : v.testBit B320    · simp only [Bool.not_false, Bool.and_true]321      rw [ih]322      constructor323      · intro h i hi324        by_cases hiB : i = B325        · subst hiB; exact h2326        · exact h i (by omega)327      · intro h i hi; exact h i (by omega)328    · simp only [Bool.not_true, Bool.and_false]329      constructor330      · intro h; cases h331      · intro h; have := h B (by omega); rw [h2] at this; cases this332333theorem lowZero_iff {B v : Nat} (hv : v < 2 ^ B) : lowZero B v = true ↔ v = 0 := by334  rw [lowZero_spec]335  constructor336  · intro h337    apply Nat.eq_of_testBit_eq338    intro i339    rw [Nat.zero_testBit]340    by_cases hi : i < B341    · exact h i hi342    · exact Nat.testBit_lt_two_pow343        (Nat.lt_of_lt_of_le hv (Nat.pow_le_pow_right (by decide) (by omega)))344  · rintro rfl i _; exact Nat.zero_testBit i345346/-- CHARACTER ORTHOGONALITY on F_2^B. -/347theorem orthogonality (B v : Nat) :348    rsum (List.range (2 ^ B)) (fun u => chi B u v) =349      if lowZero B v then ((2 ^ B : Nat) : Rat) else 0 := by350  induction B with351  | zero => simp [chi, dotB, lowZero]352  | succ B ih =>353    have hsplit : List.range (2 ^ (B + 1)) =354        List.range (2 ^ B) ++ (List.range (2 ^ B)).map (2 ^ B + ·) := by355      rw [show 2 ^ (B + 1) = 2 ^ B + 2 ^ B by rw [Nat.pow_succ]; omega]356      exact List.range_add357    rw [hsplit, rsum_append, rsum_map]358    have e1 : rsum (List.range (2 ^ B)) (fun u => chi (B + 1) u v) =359        rsum (List.range (2 ^ B)) (fun u => chi B u v) := by360      apply rsum_congr361      intro u hu362      have hu' : u.testBit B = false := Nat.testBit_lt_two_pow (List.mem_range.mp hu)363      simp [chi, dotB, hu']364    have e2 : rsum (List.range (2 ^ B)) (fun u => chi (B + 1) (2 ^ B + u) v) =365        rsum (List.range (2 ^ B)) (fun u => (if v.testBit B then -1 else 1) * chi B u v) := by366      apply rsum_congr367      intro u hu368      have hu' : u.testBit B = false := Nat.testBit_lt_two_pow (List.mem_range.mp hu)369      have hc : dotB B (2 ^ B + u) v = dotB B u v :=370        dotB_congr_left v (fun i hi => Nat.testBit_two_pow_add_gt hi u)371      have ht : (2 ^ B + u).testBit B = true := by372        rw [Nat.testBit_two_pow_add_eq, hu']; rfl373      simp only [chi, dotB, hc, ht, Bool.true_and]374      cases dotB B u v <;> cases v.testBit B <;> simp <;> grind375    rw [e1, e2, rsum_mul_left, ih]376    show _ = if (lowZero B v && !v.testBit B) = true then _ else _377    by_cases hb : v.testBit B = true <;> by_cases hl : lowZero B v = true <;>378      simp [hb, hl, Nat.pow_succ] <;> grind379380/-- EXACT-VALUE INDICATOR EXPANSION: q * 1[s = a] = sum_u chi_u(a) chi_u(s). -/381theorem indicator_expansion {B a s : Nat} (ha : a < 2 ^ B) (hs : s < 2 ^ B) :382    rsum (List.range (2 ^ B)) (fun u => chi B u a * chi B u s) =383      if s = a then ((2 ^ B : Nat) : Rat) else 0 := by384  rw [rsum_congr (g := fun u => chi B u (a ^^^ s)) (fun u _ => (chi_xor_right B u a s).symm),385    orthogonality]386  have hlt : a ^^^ s < 2 ^ B := Nat.xor_lt_two_pow ha hs387  by_cases h : s = a388  · subst h389    have h0 : lowZero B 0 = true := (lowZero_iff (Nat.two_pow_pos B)).2 rfl390    simp [h0]391  · have : lowZero B (a ^^^ s) = false := by392      cases hl : lowZero B (a ^^^ s)393      · rfl394      · exact absurd ((xor_eq_zero_imp ((lowZero_iff hlt).1 hl)).symm) h395    simp [this, h]396397/-! ## Readouts, legal success and g_b -/398399/-- A readout: from board P and observed bit b, a proposed move (heap index i, new400    value v), or `none` (invalid output).  No circuit restriction is imposed here;401    the only property ever used is the correlation premise `CorrHyp`. -/402abbrev Readout := List Nat → Bool → Option (Nat × Nat)403404/-- g_b(P): old heap XOR new value for a legal proposed move; 0 for invalid output. -/405def gval (F : Readout) (b : Bool) (P : List Nat) : Nat :=406  match F P b with407  | some (i, v) =>408    match P[i]? with409    | some x => if v < x then x ^^^ v else 0410    | none => 0411  | none => 0412413/-- H_{b,a}(P) = 1[g_b(P) = a]. -/414def H (F : Readout) (b : Bool) (a : Nat) (P : List Nat) : Rat :=415  if gval F b P = a then 1 else 0416417/-- Legal success: the proposed move is legal and leaves nim-sum zero. -/418def Success (F : Readout) (b : Bool) (P : List Nat) : Prop :=419  ∃ i v x, F P b = some (i, v) ∧ P[i]? = some x ∧ v < x ∧ nimSum (P.set i v) = 0420421/-- Decidable form of `Success`. -/422def successB (F : Readout) (b : Bool) (P : List Nat) : Bool :=423  match F P b with424  | some (i, v) =>425    match P[i]? with426    | some x => decide (v < x) && decide (nimSum (P.set i v) = 0)427    | none => false428  | none => false429430theorem successB_iff (F : Readout) (b : Bool) (P : List Nat) :431    successB F b P = true ↔ Success F b P := by432  unfold successB Success433  cases hF : F P b with434  | none => simp435  | some iv =>436    obtain ⟨i, v⟩ := iv437    cases hx : P[i]? with438    | none =>439      simp only [hx]440      constructor441      · intro h; cases h442      · rintro ⟨i', v', x', h1, h2, _⟩443        simp only [Option.some.injEq, Prod.mk.injEq] at h1444        obtain ⟨rfl, rfl⟩ := h1445        rw [hx] at h2; cases h2446    | some x =>447      simp only [hx, Bool.and_eq_true, decide_eq_true_eq]448      constructor449      · rintro ⟨h1, h2⟩; exact ⟨i, v, x, rfl, hx, h1, h2⟩450      · rintro ⟨i', v', x', h1, h2, h3, h4⟩451        simp only [Option.some.injEq, Prod.mk.injEq] at h1452        obtain ⟨rfl, rfl⟩ := h1453        rw [hx, Option.some.injEq] at h2454        subst h2455        exact ⟨h3, h4⟩456457theorem nimSum_set {P : List Nat} {i x : Nat} (v : Nat) (h : P[i]? = some x) :458    nimSum (P.set i v) = nimSum P ^^^ x ^^^ v := by459  induction P generalizing i with460  | nil => simp at h461  | cons y t ih =>462    cases i with463    | zero =>464      simp only [List.getElem?_cons_zero, Option.some.injEq] at h465      subst h466      simpa using one_heap_update [] t y v467    | succ k =>468      simp only [List.getElem?_cons_succ] at h469      simp only [List.set_cons_succ, nimSum, ih h, Nat.xor_assoc]470471/-- A legally proposed (index, value) is an ordinary legal Nim move. -/472theorem set_move {P : List Nat} {i x v : Nat} (h : P[i]? = some x) (hv : v < x) :473    Move P (P.set i v) := by474  induction P generalizing i with475  | nil => simp at h476  | cons y t ih =>477    cases i with478    | zero =>479      simp only [List.getElem?_cons_zero, Option.some.injEq] at h480      subst h481      exact ⟨[], y, t, v, rfl, rfl, hv⟩482    | succ k =>483      simp only [List.getElem?_cons_succ] at h484      obtain ⟨pre, z, post, w, h1, h2, h3⟩ := ih h485      refine ⟨y :: pre, z, post, w, by simp [h1], ?_, h3⟩486      simp [h2]487488/-- Success is a legal Nim move to a zero-nim-sum board. -/489theorem success_legal {F : Readout} {b : Bool} {P : List Nat} (h : Success F b P) :490    ∃ Q, Move P Q ∧ nimSum Q = 0 := by491  obtain ⟨i, v, x, _, hx, hv, hz⟩ := h492  exact ⟨_, set_move hx hv, hz⟩493494/-- Invalid outputs are never successes and have g = 0. -/495theorem invalid_output {F : Readout} {b : Bool} {P : List Nat} (h : F P b = none) :496    successB F b P = false ∧ gval F b P = 0 := by497  simp [successB, gval, h]498499/-- SUCCESS ↔ g_b(P) = sigma(P), on boards with sigma ≠ 0. -/500theorem success_iff_gval {F : Readout} {b : Bool} {P : List Nat} (hs : nimSum P ≠ 0) :501    successB F b P = true ↔ gval F b P = nimSum P := by502  unfold successB gval503  cases hF : F P b with504  | none =>505    constructor506    · intro h; cases h507    · intro h; exact absurd h.symm hs508  | some iv =>509    obtain ⟨i, v⟩ := iv510    cases hx : P[i]? with511    | none =>512      simp only [hx]513      constructor514      · intro h; cases h515      · intro h; exact absurd h.symm hs516    | some x =>517      simp only [hx]518      by_cases hv : v < x519      · simp only [hv, decide_true, Bool.true_and, if_true, decide_eq_true_eq]520        rw [nimSum_set v hx, Nat.xor_assoc]521        constructor522        · intro h; exact (xor_eq_zero_imp h).symm523        · intro h; rw [h]; exact Nat.xor_self _524      · simp only [hv, decide_false, Bool.false_and, if_false]525        constructor526        · intro h; cases h527        · intro h; exact absurd h.symm hs528529/-! ## Expectations and the correlation premise -/530531/-- Number of boards, q^N. -/532def T (B N : Nat) : Rat := ((2 ^ B : Nat) : Rat) ^ N533534/-- Expectation under N independent uniform B-bit heaps. -/535def expect (B N : Nat) (f : List Nat → Rat) : Rat := rsum (boards (2 ^ B) N) f / T B N536537/-- E[H_{b,a}(P) chi_u(P)], where chi_u(P) = (-1)^<u, sigma(P)>. -/538def corr (B N : Nat) (F : Readout) (b : Bool) (a u : Nat) : Rat :=539  expect B N (fun P => H F b a P * chi B u (nimSum P))540541/-- THE IMPORTED PARITY-CORRELATION PREMISE, as a predicate used only as a theorem542    hypothesis: |E[H_{b,a} chi_u]| ≤ η for every b, every a < q and every nonzero543    u < q.  (Not an axiom; not proved here.) -/544def CorrHyp (B N : Nat) (F : Readout) (η : Rat) : Prop :=545  ∀ (b : Bool) (a u : Nat), a < 2 ^ B → 0 < u → u < 2 ^ B →546    -η ≤ corr B N F b a u ∧ corr B N F b a u ≤ η547548theorem q_pos (B : Nat) : (0 : Rat) < ((2 ^ B : Nat) : Rat) :=549  Rat.natCast_pos.mpr (Nat.two_pow_pos B)550551theorem T_eq (B N : Nat) : T B N = (((2 ^ B) ^ N : Nat) : Rat) := by552  simp [T]553554theorem T_pos (B N : Nat) : 0 < T B N := by555  rw [T_eq]; exact Rat.natCast_pos.mpr (Nat.pow_pos (Nat.two_pow_pos B))556557theorem rsum_boards_eq_T (B N : Nat) : rsum (boards (2 ^ B) N) (fun _ => 1) = T B N := by558  rw [count_boards]; rfl559560theorem div_mul_cancel' {x d : Rat} (hd : d ≠ 0) : x / d * d = x := by grind561562theorem div_le_div_of_le {x y d : Rat} (hd : 0 < d) (h : x ≤ y) : x / d ≤ y / d := by563  have hd' : d ≠ 0 := by grind564  apply Rat.le_of_mul_le_mul_right _ hd565  rw [div_mul_cancel' hd', div_mul_cancel' hd']566  exact h567568theorem le_div_of_mul_le {x y d : Rat} (hd : 0 < d) (h : x ≤ y * d) : x / d ≤ y := by569  have hd' : d ≠ 0 := by grind570  apply Rat.le_of_mul_le_mul_right _ hd571  rw [div_mul_cancel' hd']572  exact h573574theorem sigma_lt {B N : Nat} {P : List Nat} (h : P ∈ boards (2 ^ B) N) : nimSum P < 2 ^ B :=575  nimSum_lt (mem_boards h).2576577/-- Raw character sums C_{b,a,u} = sum_P H_{b,a}(P) chi_u(P). -/578def Csum (B N : Nat) (F : Readout) (b : Bool) (a u : Nat) : Rat :=579  rsum (boards (2 ^ B) N) (fun P => H F b a P * chi B u (nimSum P))580581theorem Csum_bound {B N : Nat} {F : Readout} {η : Rat} (hyp : CorrHyp B N F η)582    (b : Bool) {a u : Nat} (ha : a < 2 ^ B) (hu0 : 0 < u) (hu : u < 2 ^ B) :583    -(η * T B N) ≤ Csum B N F b a u ∧ Csum B N F b a u ≤ η * T B N := by584  obtain ⟨h1, h2⟩ := hyp b a u ha hu0 hu585  have hT := T_pos B N586  have hT' : T B N ≠ 0 := by grind587  have e : corr B N F b a u * T B N = Csum B N F b a u := by588    unfold corr expect Csum; exact div_mul_cancel' hT'589  have k1 := Rat.mul_le_mul_of_nonneg_right h1 (Rat.le_of_lt hT)590  have k2 := Rat.mul_le_mul_of_nonneg_right h2 (Rat.le_of_lt hT)591  rw [e] at k1 k2592  constructor <;> grind593594/-- A_{b,a} = sum_P H_{b,a}(P) 1[sigma(P) = a]. -/595def Aval (B N : Nat) (F : Readout) (b : Bool) (a : Nat) : Rat :=596  rsum (boards (2 ^ B) N) (fun P => H F b a P * (if nimSum P = a then 1 else 0))597598/-- C0_{b,a} = sum_P H_{b,a}(P). -/599def C0val (B N : Nat) (F : Readout) (b : Bool) (a : Nat) : Rat :=600  rsum (boards (2 ^ B) N) (fun P => H F b a P)601602theorem natCast_pred (B : Nat) : (((2 ^ B - 1 : Nat) : Rat)) = ((2 ^ B : Nat) : Rat) - 1 := by603  have h : 2 ^ B - 1 + 1 = 2 ^ B := by have := Nat.two_pow_pos B; omega604  have h' : (((2 ^ B - 1 + 1 : Nat)) : Rat) = ((2 ^ B : Nat) : Rat) := by rw [h]605  rw [Rat.natCast_add] at h'606  grind607608/-- EXACT-VALUE ERROR (counting form):609    |q * A_{b,a} - C0_{b,a}| ≤ (q-1) * η * q^N. -/610theorem exact_value_count {B N : Nat} {F : Readout} {η : Rat} (hyp : CorrHyp B N F η)611    (b : Bool) {a : Nat} (ha : a < 2 ^ B) :612    -(((2 ^ B - 1 : Nat) : Rat) * (η * T B N)) ≤613        ((2 ^ B : Nat) : Rat) * Aval B N F b a - C0val B N F b a ∧614      ((2 ^ B : Nat) : Rat) * Aval B N F b a - C0val B N F b a ≤615        ((2 ^ B - 1 : Nat) : Rat) * (η * T B N) := by616  have hq : 0 < 2 ^ B := Nat.two_pow_pos B617  -- step 1: expand the exact-value indicator into characters618  have step1 : ((2 ^ B : Nat) : Rat) * Aval B N F b a =619      rsum (boards (2 ^ B) N) (fun P => rsum (List.range (2 ^ B))620        (fun u => chi B u a * (H F b a P * chi B u (nimSum P)))) := by621    unfold Aval622    rw [← rsum_mul_left]623    apply rsum_congr624    intro P hP625    have hexp := indicator_expansion ha (sigma_lt hP)626    have e : rsum (List.range (2 ^ B)) (fun u => chi B u a * (H F b a P * chi B u (nimSum P))) =627        H F b a P * rsum (List.range (2 ^ B)) (fun u => chi B u a * chi B u (nimSum P)) := by628      rw [← rsum_mul_left]; apply rsum_congr; intro u _; grind629    rw [e, hexp]630    by_cases h : nimSum P = a <;> simp [h] <;> grind631  -- step 2: swap sums632  have step2 : ((2 ^ B : Nat) : Rat) * Aval B N F b a =633      rsum (List.range (2 ^ B)) (fun u => chi B u a * Csum B N F b a u) := by634    rw [step1, rsum_comm]635    apply rsum_congr; intro u _636    unfold Csum; rw [rsum_mul_left]637  -- step 3: separate u = 0638  have hC0 : Csum B N F b a 0 = C0val B N F b a := by639    unfold Csum C0val; apply rsum_congr; intro P _; simp [chi_zero_left]640  rw [step2, rsum_range_split0 hq, chi_zero_left, hC0]641  -- step 4: bound the nonzero characters642  have hb := rsum_offZero_bound hq (fun u => chi B u a * Csum B N F b a u) (η * T B N)643    (by644      intro u hu0 hu645      obtain ⟨k1, k2⟩ := Csum_bound hyp b ha hu0 hu646      show -(η * T B N) ≤ chi B u a * Csum B N F b a u ∧ chi B u a * Csum B N F b a u ≤ η * T B N647      rcases chi_cases B u a with hc | hc <;> rw [hc] <;> constructor <;> grind)648  constructor <;> grind649650/-- EXACT-VALUE ERROR (expectation form, as in the brief), with q = 2^B:651    |E[H_{b,a} 1[sigma = a]] - (1/q) E[H_{b,a}]| ≤ ((q-1)/q) η. -/652theorem exact_value_error {B N : Nat} {F : Readout} {η : Rat} (hyp : CorrHyp B N F η)653    (b : Bool) {a : Nat} (ha : a < 2 ^ B) :654    -((((2 ^ B : Nat) : Rat) - 1) / ((2 ^ B : Nat) : Rat) * η) ≤655        expect B N (fun P => H F b a P * (if nimSum P = a then 1 else 0)) -656          (1 / ((2 ^ B : Nat) : Rat)) * expect B N (fun P => H F b a P) ∧657      expect B N (fun P => H F b a P * (if nimSum P = a then 1 else 0)) -658          (1 / ((2 ^ B : Nat) : Rat)) * expect B N (fun P => H F b a P) ≤659        (((2 ^ B : Nat) : Rat) - 1) / ((2 ^ B : Nat) : Rat) * η := by660  obtain ⟨k1, k2⟩ := exact_value_count hyp b ha661  rw [natCast_pred] at k1 k2662  have hq := q_pos B663  have hT := T_pos B N664  have hqT : 0 < ((2 ^ B : Nat) : Rat) * T B N := Rat.mul_pos hq hT665  have hq' : ((2 ^ B : Nat) : Rat) ≠ 0 := Rat.ne_of_gt hq666  have hT' : T B N ≠ 0 := Rat.ne_of_gt hT667  have d1 := div_le_div_of_le hqT k1668  have d2 := div_le_div_of_le hqT k2669  unfold expect670  unfold Aval C0val at d1 d2671  generalize rsum (boards (2 ^ B) N) (fun P => H F b a P * (if nimSum P = a then 1 else 0)) = A672    at d1 d2 ⊢673  generalize rsum (boards (2 ^ B) N) (fun P => H F b a P) = C at d1 d2 ⊢674  generalize T B N = t at *675  generalize ((2 ^ B : Nat) : Rat) = q at *676  have e1 : (q * A - C) / (q * t) = A / t - 1 / q * (C / t) := by grind677  have e2 : (q - 1) * (η * t) / (q * t) = (q - 1) / q * η := by grind678  have e3 : -((q - 1) * (η * t)) / (q * t) = -((q - 1) / q * η) := by grind679  rw [e1, e2] at d2680  rw [e1, e3] at d1681  exact ⟨d1, d2⟩682683/-! ## Success, disjointness and conditioning -/684685/-- Number of boards with sigma ≠ 0 on which the readout, fed b = ell_w(sigma),686    makes a legal move to nim-sum zero. -/687def succCount (B N : Nat) (F : Readout) (w : Nat) : Rat :=688  rsum (boards (2 ^ B) N)689    (fun P => if nimSum P ≠ 0 ∧ successB F (dotB B w (nimSum P)) P = true then 1 else 0)690691/-- Number of boards with sigma ≠ 0. -/692def nonzeroCount (B N : Nat) : Rat :=693  rsum (boards (2 ^ B) N) (fun P => if nimSum P ≠ 0 then 1 else 0)694695theorem offZero_rsum {α : Type} (l : List α) (X : Nat → α → Rat) (a : Nat) :696    offZero (fun a => rsum l (X a)) a = rsum l (fun P => offZero (fun a => X a P) a) := by697  by_cases h : a = 0698  · simp [offZero, h, rsum_zero]699  · simp [offZero, h]700701theorem rsum_offZero_indicator {q σ : Nat} (hσ : σ < q) (f : Nat → Rat) :702    rsum (List.range q) (offZero (fun a => f a * (if σ = a then 1 else 0))) = offZero f σ := by703  rw [rsum_congr (g := fun a => if a = σ then offZero f a else 0)]704  · rw [rsum_range_ite]; simp [hσ]705  · intro a _706    by_cases h : a = σ707    · subst h; by_cases h0 : a = 0 <;> simp [offZero, h0]708    · have : σ ≠ a := fun e => h e.symm709      by_cases h0 : a = 0 <;> simp [offZero, h0, h, this]710711theorem rsum_range_indicator_le (q c : Nat) :712    rsum (List.range q) (fun a => if a = c then 1 else 0) ≤ 1 := by713  rw [rsum_range_ite q c (fun _ => 1)]714  split <;> grind715716/-- (S1) The success count as a sum of exact-value terms. -/717theorem succCount_eq (B N : Nat) (F : Readout) (w : Nat) :718    succCount B N F w =719      rsum (List.range (2 ^ B)) (offZero (fun a => Aval B N F (dotB B w a) a)) := by720  unfold Aval721  rw [rsum_congr (fun a _ => offZero_rsum _ _ a), ← rsum_comm]722  unfold succCount723  apply rsum_congr724  intro P hP725  have hσ := sigma_lt hP726  have e := rsum_offZero_indicator hσ (fun a => H F (dotB B w a) a P)727  have e' : rsum (List.range (2 ^ B))728        (fun a => offZero (fun a => H F (dotB B w a) a P *729          (if nimSum P = a then 1 else 0)) a) =730      rsum (List.range (2 ^ B))731        (offZero (fun a => H F (dotB B w a) a P * (if nimSum P = a then 1 else 0))) := rfl732  rw [e', e]733  by_cases h0 : nimSum P = 0734  · simp [offZero, h0]735  · have hs := success_iff_gval (F := F) (b := dotB B w (nimSum P)) h0736    simp only [offZero, h0, if_false, H, ne_eq, not_false_eq_true, true_and]737    by_cases hg : gval F (dotB B w (nimSum P)) P = nimSum P738    · simp [hg, hs.2 hg]739    · have : ¬ successB F (dotB B w (nimSum P)) P = true := fun h => hg (hs.1 h)740      simp [hg, this]741742/-- (S3) Disjointness: for each board, at most two values a ≠ 0 satisfy743    g_{ell(a)}(P) = a (one for each observed bit). -/744theorem disjoint_le_two (B : Nat) (F : Readout) (w : Nat) (P : List Nat) :745    rsum (List.range (2 ^ B)) (offZero (fun a => H F (dotB B w a) a P)) ≤ 2 := by746  have hle : rsum (List.range (2 ^ B)) (offZero (fun a => H F (dotB B w a) a P)) ≤747      rsum (List.range (2 ^ B)) (fun a => (if a = gval F false P then 1 else 0) +748        (if a = gval F true P then 1 else 0)) := by749    apply rsum_le750    intro a _751    have n1 : (0 : Rat) ≤ if a = gval F false P then 1 else 0 := by split <;> grind752    have n2 : (0 : Rat) ≤ if a = gval F true P then 1 else 0 := by split <;> grind753    by_cases h0 : a = 0754    · simp only [offZero, h0, if_true]; grind755    · simp only [offZero, h0, if_false, H]756      by_cases hg : gval F (dotB B w a) P = a757      · simp only [hg, if_true]758        cases hd : dotB B w a759        · rw [hd] at hg; simp [hg.symm]; grind760        · rw [hd] at hg; simp [hg.symm]; grind761      · simp only [hg, if_false]; grind762  rw [rsum_add] at hle763  have h1 := rsum_range_indicator_le (2 ^ B) (gval F false P)764  have h2 := rsum_range_indicator_le (2 ^ B) (gval F true P)765  grind766767theorem C0_sum_le (B N : Nat) (F : Readout) (w : Nat) :768    rsum (List.range (2 ^ B)) (offZero (fun a => C0val B N F (dotB B w a) a)) ≤ 2 * T B N := by769  unfold C0val770  rw [rsum_congr (fun a _ => offZero_rsum _ _ a), ← rsum_comm]771  have : rsum (boards (2 ^ B) N) (fun P => rsum (List.range (2 ^ B))772      (fun a => offZero (fun a => H F (dotB B w a) a P) a)) ≤773      rsum (boards (2 ^ B) N) (fun _ => 2 * 1) := by774    apply rsum_le; intro P _775    have := disjoint_le_two B F w P776    show rsum (List.range (2 ^ B)) (offZero (fun a => H F (dotB B w a) a P)) ≤ 2 * 1777    grind778  rw [rsum_mul_left, rsum_boards_eq_T] at this779  exact this780781/-- JOINT BOUND (counting form): q * #success ≤ 2 q^N + (q-1)^2 η q^N. -/782theorem succCount_bound {B N : Nat} (F : Readout) (w : Nat) {η : Rat}783    (hyp : CorrHyp B N F η) :784    ((2 ^ B : Nat) : Rat) * succCount B N F w ≤785      2 * T B N + ((2 ^ B - 1 : Nat) : Rat) * (((2 ^ B - 1 : Nat) : Rat) * (η * T B N)) := by786  have hq : 0 < 2 ^ B := Nat.two_pow_pos B787  rw [succCount_eq, ← rsum_mul_left]788  have e : rsum (List.range (2 ^ B))789        (fun a => ((2 ^ B : Nat) : Rat) * offZero (fun a => Aval B N F (dotB B w a) a) a) =790      rsum (List.range (2 ^ B))791        (offZero (fun a => ((2 ^ B : Nat) : Rat) * Aval B N F (dotB B w a) a)) := by792    apply rsum_congr; intro a _; by_cases h : a = 0 <;> simp [offZero, h]793  rw [e]794  have hle := rsum_offZero_le (q := 2 ^ B)795    (f := fun a => ((2 ^ B : Nat) : Rat) * Aval B N F (dotB B w a) a)796    (g := fun a => C0val B N F (dotB B w a) a + ((2 ^ B - 1 : Nat) : Rat) * (η * T B N))797    (by798      intro a _ ha799      have := (exact_value_count hyp (dotB B w a) ha).2800      grind)801  rw [rsum_offZero_add, rsum_offZero_const hq] at hle802  have h2 := C0_sum_le B N F w803  grind804805/-- Pr[sigma ≠ 0] = (q-1)/q, in counting form, for N ≥ 1. -/806theorem nonzeroCount_eq (B N : Nat) :807    nonzeroCount B (N + 1) = T B (N + 1) - ((2 ^ B : Nat) : Rat) ^ N := by808  unfold nonzeroCount809  have e : rsum (boards (2 ^ B) (N + 1)) (fun P => if nimSum P ≠ 0 then 1 else 0) =810      rsum (boards (2 ^ B) (N + 1)) (fun _ => 1) -811        rsum (boards (2 ^ B) (N + 1)) (fun P => if nimSum P = 0 then 1 else 0) := by812    have := rsum_add (boards (2 ^ B) (N + 1)) (fun P => if nimSum P ≠ 0 then (1 : Rat) else 0)813      (fun P => if nimSum P = 0 then 1 else 0)814    rw [rsum_congr (g := fun _ => (1 : Rat)) (by815      intro P _; by_cases h : nimSum P = 0 <;> simp [h])] at this816    grind817  rw [e, rsum_boards_eq_T, sigma_uniform B N 0 (Nat.two_pow_pos B)]818819theorem prob_sigma_ne_zero (B N : Nat) :820    nonzeroCount B (N + 1) / T B (N + 1) =821      (((2 ^ B : Nat) : Rat) - 1) / ((2 ^ B : Nat) : Rat) := by822  rw [nonzeroCount_eq]823  have hq := q_pos B824  have hq' : ((2 ^ B : Nat) : Rat) ≠ 0 := Rat.ne_of_gt hq825  have ht : (0 : Rat) < ((2 ^ B : Nat) : Rat) ^ N := by826    rw [← Rat.natCast_pow]; exact Rat.natCast_pos.mpr (Nat.pow_pos (Nat.two_pow_pos B))827  have ht' : ((2 ^ B : Nat) : Rat) ^ N ≠ 0 := Rat.ne_of_gt ht828  unfold T829  rw [Rat.pow_succ]830  generalize ((2 ^ B : Nat) : Rat) ^ N = t at *831  generalize ((2 ^ B : Nat) : Rat) = q at *832  grind833834/-- MAIN THEOREM (Appendix G(i), finite form).  For every B ≥ 1, N ≥ 1 (written835    N + 1), every readout F, every vector w (the head's linear functional836    ell(sigma) = <w, sigma>), and every η, the parity-correlation premise implies837      Pr[legal winning move | sigma ≠ 0] ≤ 2/(q-1) + (q-1) η,   q = 2^B. -/838theorem success_bound {B N : Nat} (hB : 1 ≤ B) (F : Readout) (w : Nat) {η : Rat}839    (hyp : CorrHyp B (N + 1) F η) :840    succCount B (N + 1) F w / nonzeroCount B (N + 1) ≤841      2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * η := by842  have hqge : 2 ≤ 2 ^ B := by843    have := Nat.pow_le_pow_right (show 0 < 2 by decide) hB; simpa using this844  have hq2 : (2 : Rat) ≤ ((2 ^ B : Nat) : Rat) := by845    have := Rat.natCast_le_natCast.mpr hqge; simpa using this846  have hjoint := succCount_bound F w hyp847  rw [natCast_pred] at hjoint848  have ht : (0 : Rat) < ((2 ^ B : Nat) : Rat) ^ N := by849    rw [← Rat.natCast_pow]; exact Rat.natCast_pos.mpr (Nat.pow_pos (Nat.two_pow_pos B))850  have hT : T B (N + 1) = ((2 ^ B : Nat) : Rat) * ((2 ^ B : Nat) : Rat) ^ N := by851    unfold T; rw [Rat.pow_succ]; grind852  have hZ : nonzeroCount B (N + 1) =853      (((2 ^ B : Nat) : Rat) - 1) * ((2 ^ B : Nat) : Rat) ^ N := by854    rw [nonzeroCount_eq, hT]; grind855  rw [hT] at hjoint856  rw [hZ]857  generalize succCount B (N + 1) F w = S at *858  generalize ((2 ^ B : Nat) : Rat) ^ N = t at *859  generalize ((2 ^ B : Nat) : Rat) = q at *860  have h1 : (0 : Rat) < q - 1 := by grind861  have hZpos : 0 < (q - 1) * t := Rat.mul_pos h1 ht862  apply le_div_of_mul_le hZpos863  have hqpos : (0 : Rat) < q := by grind864  have hS : S ≤ 2 * t + (q - 1) * ((q - 1) * (η * t)) := by865    apply Rat.le_of_mul_le_mul_left _ hqpos866    grind867  have hq1 : q - 1 ≠ 0 := Rat.ne_of_gt h1868  have eR : (2 / (q - 1) + (q - 1) * η) * ((q - 1) * t) =869      2 * t + (q - 1) * ((q - 1) * (η * t)) := by grind870  rw [eR]871  exact hS872873/-! ## The structured heads are nonzero linear functionals -/874875/-- The vector w_j with RO_{pi_j}(P) = <w_j, sigma(P)>: w_0 = 1, w_j = 2^j XOR 1. -/876def headVec (j : Nat) : Nat := if j = 0 then 1 else 2 ^ j ^^^ 1877878theorem dotB_two_pow (B j v : Nat) : dotB B (2 ^ j) v = (decide (j < B) && v.testBit j) := by879  induction B with880  | zero => simp [dotB]881  | succ B ih =>882    simp only [dotB, ih, Nat.testBit_two_pow]883    by_cases h1 : j < B884    · have : ¬ j = B := by omega885      simp [h1, this, show j < B + 1 by omega]886    · by_cases h2 : j = B887      · subst h2; simp888      · have : ¬ j < B + 1 := by omega889        simp [h1, h2, this]890891theorem head_linear {B j : Nat} (hj : j < B) (v : Nat) :892    channel j v = dotB B (headVec j) v := by893  unfold headVec channel894  by_cases h0 : j = 0895  · subst h0896    have : (1 : Nat) = 2 ^ 0 := rfl897    simp only [if_true]898    rw [this, dotB_two_pow]; simp [hj]899  · simp only [h0, if_false]900    rw [dotB_xor_left, show (1 : Nat) = 2 ^ 0 from rfl, dotB_two_pow, dotB_two_pow]901    simp [hj, show 0 < B by omega]902903theorem headVec_ne_zero (j : Nat) : headVec j ≠ 0 := by904  unfold headVec905  by_cases h0 : j = 0906  · simp [h0]907  · simp only [h0, if_false]908    intro h909    have := xor_eq_zero_imp h910    have := Nat.one_lt_two_pow h0911    omega912913theorem headVec_lt {B j : Nat} (hj : j < B) : headVec j < 2 ^ B := by914  unfold headVec915  by_cases h0 : j = 0916  · simp only [h0, if_true]; exact Nat.one_lt_two_pow (by omega)917  · simp only [h0, if_false]918    exact Nat.xor_lt_two_pow (Nat.pow_lt_pow_right (by decide) hj) (Nat.one_lt_two_pow (by omega))919920/-- RO_{pi_j}(P), the executed rollout outcome, is the linear functional <w_j, sigma(P)>. -/921theorem rollout_outcome_linear {B j : Nat} (hj : j < B) (P : List Nat) :922    rolloutWinner j P = dotB B (headVec j) (nimSum P) := by923  rw [rolloutWinner_channel, head_linear hj]924925/-- SINGLE-POLICY INFORMATION BOUND (paper Prop. single-policy-bound): if P' differs926    from P in one heap h -> h', then RO_{pi_j}(P') = RO_{pi_j}(P) XOR <w_j, h XOR h'>,927    a correction bit computable from the known heap values. -/928theorem single_policy_affine {B j : Nat} (hj : j < B) (pre post : List Nat) (h h' : Nat) :929    rolloutWinner j (pre ++ h' :: post) =930      xor (rolloutWinner j (pre ++ h :: post)) (dotB B (headVec j) (h ^^^ h')) := by931  rw [rollout_outcome_linear hj, rollout_outcome_linear hj, nimSum_move, dotB_xor_right]932933/-- Success count when the readout is fed the ACTUAL rollout outcome RO_{pi_j}(P). -/934def succCountRO (B N : Nat) (F : Readout) (j : Nat) : Rat :=935  rsum (boards (2 ^ B) N)936    (fun P => if nimSum P ≠ 0 ∧ successB F (rolloutWinner j P) P = true then 1 else 0)937938/-- MAIN THEOREM FOR ONE STRUCTURED HEAD: a readout F_N(P, RO_{pi_j}(P)) that939    satisfies the correlation premise wins with conditional probability at most940    2/(q-1) + (q-1) η. -/941theorem structured_head_bound {B N j : Nat} (hj : j < B) (F : Readout) {η : Rat}942    (hyp : CorrHyp B (N + 1) F η) :943    succCountRO B (N + 1) F j / nonzeroCount B (N + 1) ≤944      2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * η := by945  have e : succCountRO B (N + 1) F j = succCount B (N + 1) F (headVec j) := by946    unfold succCountRO succCount947    apply rsum_congr; intro P _948    rw [rollout_outcome_linear hj]949  rw [e]950  exact success_bound (by omega) F (headVec j) hyp951952/-! ## Asymptotic corollary for fixed B -/953954/-- f is negligible: below every inverse polynomial eventually (N+1 avoids 1/0). -/955def Negligible (f : Nat → Rat) : Prop :=956  ∀ c : Nat, ∃ N0 : Nat, ∀ N ≥ N0, f N ≤ 1 / (((N + 1 : Nat) : Rat)) ^ c957958theorem negligible_const_mul (K : Nat) {f : Nat → Rat} (hf : Negligible f) :959    Negligible (fun N => (K : Rat) * f N) := by960  intro c961  obtain ⟨N0, hN0⟩ := hf (c + 1)962  refine ⟨max N0 K, fun N hN => ?_⟩963  have h1 := hN0 N (by omega)964  show (K : Rat) * f N ≤ 1 / (((N + 1 : Nat) : Rat)) ^ c965  have hXpos : (0 : Rat) < ((N + 1 : Nat) : Rat) := Rat.natCast_pos.mpr (by omega)966  have hXc : (0 : Rat) < ((N + 1 : Nat) : Rat) ^ c := by967    rw [← Rat.natCast_pow]; exact Rat.natCast_pos.mpr (Nat.pow_pos (by omega))968  have hKX : (K : Rat) ≤ ((N + 1 : Nat) : Rat) := Rat.natCast_le_natCast.mpr (by omega)969  have hK0 : (0 : Rat) ≤ K := Rat.natCast_nonneg970  rw [Rat.pow_succ] at h1971  generalize f N = y at *972  generalize ((N + 1 : Nat) : Rat) ^ c = Y at *973  generalize ((N + 1 : Nat) : Rat) = X at *974  have k1 := Rat.mul_le_mul_of_nonneg_left h1 hK0975  have hY' : Y ≠ 0 := Rat.ne_of_gt hXc976  have hX' : X ≠ 0 := Rat.ne_of_gt hXpos977  have hd : 0 < Y * X := Rat.mul_pos hXc hXpos978  have k2 : (K : Rat) * (1 / (Y * X)) ≤ 1 / Y := by979    apply Rat.le_of_mul_le_mul_right _ hd980    have e1 : (K : Rat) * (1 / (Y * X)) * (Y * X) = K := by grind981    have e2 : 1 / Y * (Y * X) = X := by grind982    rw [e1, e2]; exact hKX983  exact Rat.le_trans k1 k2984985/-- ASYMPTOTIC COROLLARY: for fixed B ≥ 1 and readouts F_N satisfying the986    correlation premise with negligible η_N, the conditional success probability987    is at most 2/(q-1) + ε_N with ε_N negligible. -/988theorem asymptotic_bound {B : Nat} (hB : 1 ≤ B) (F : Nat → Readout) (w : Nat)989    (η : Nat → Rat) (hη : Negligible η) (hyp : ∀ N, CorrHyp B (N + 1) (F N) (η N)) :990    ∃ ε : Nat → Rat, Negligible ε ∧ ∀ N,991      succCount B (N + 1) (F N) w / nonzeroCount B (N + 1) ≤992        2 / (((2 ^ B : Nat) : Rat) - 1) + ε N := by993  refine ⟨fun N => ((2 ^ B - 1 : Nat) : Rat) * η N, negligible_const_mul _ hη, fun N => ?_⟩994  have := success_bound hB (F N) w (hyp N)995  rw [natCast_pred]996  exact this997998999#print axioms rsum_nil1000#print axioms rsum_cons1001#print axioms rsum_append1002#print axioms rsum_congr1003#print axioms rsum_zero1004#print axioms rsum_add1005#print axioms rsum_mul_left1006#print axioms rsum_le1007#print axioms rsum_const1008#print axioms rsum_comm1009#print axioms rsum_map1010#print axioms rsum_flatMap1011#print axioms rsum_bound1012#print axioms rsum_range_ite1013#print axioms rsum_range_split01014#print axioms range_one_add1015#print axioms rsum_offZero_bound1016#print axioms rsum_offZero_const1017#print axioms rsum_offZero_add1018#print axioms rsum_offZero_le1019#print axioms mem_boards1020#print axioms rsum_boards_succ1021#print axioms count_boards1022#print axioms xor_eq_iff1023#print axioms sigma_uniform1024#print axioms dotB_xor_right1025#print axioms dotB_xor_left1026#print axioms dotB_zero_left1027#print axioms dotB_congr_left1028#print axioms chi_xor_right1029#print axioms chi_zero_left1030#print axioms chi_cases1031#print axioms lowZero_spec1032#print axioms lowZero_iff1033#print axioms orthogonality1034#print axioms indicator_expansion1035#print axioms successB_iff1036#print axioms nimSum_set1037#print axioms set_move1038#print axioms success_legal1039#print axioms invalid_output1040#print axioms success_iff_gval1041#print axioms q_pos1042#print axioms T_eq1043#print axioms T_pos1044#print axioms rsum_boards_eq_T1045#print axioms div_mul_cancel'1046#print axioms div_le_div_of_le1047#print axioms le_div_of_mul_le1048#print axioms sigma_lt1049#print axioms Csum_bound1050#print axioms natCast_pred1051#print axioms exact_value_count1052#print axioms exact_value_error1053#print axioms offZero_rsum1054#print axioms rsum_offZero_indicator1055#print axioms rsum_range_indicator_le1056#print axioms succCount_eq1057#print axioms disjoint_le_two1058#print axioms C0_sum_le1059#print axioms succCount_bound1060#print axioms nonzeroCount_eq1061#print axioms prob_sigma_ne_zero1062#print axioms success_bound1063#print axioms dotB_two_pow1064#print axioms head_linear1065#print axioms headVec_ne_zero1066#print axioms headVec_lt1067#print axioms rollout_outcome_linear1068#print axioms single_policy_affine1069#print axioms structured_head_bound1070#print axioms negligible_const_mul1071#print axioms asymptotic_bound10721073end Prob1074end NimAudit