NoiseModel

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 Misc23/- Phase 7, Part B: the independent outcome-flip model of Remark rem:noisy-rollout-decay as4   a genuine finite probability law, and the two-sided order-a^{-2} repetition bound.5   Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.67   PARAMETER SCOPE.  Everything in the generic section is proved for an arbitrary type R8   carrying Lean core's ordered-field interface9       [Lean.Grind.Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R]10       [Lean.Grind.OrderedRing R],11   i.e. a linearly ordered field.  Core Lean supplies these instances for ℚ, and the12   ℚ-instantiation is checked below and tied to the phase-6 identities Misc.bw_total,13   Misc.bw_sign and Misc.flip_agree.  The real numbers are not available in this core-only14   environment, so instantiation at ℝ (which needs the same five instances, e.g. from15   Mathlib) is NOT checked here.1617   B1  fw ε: the product Bernoulli(ε) law on error patterns e ∈ {0,1}^L; nonnegative for18       0 ≤ ε ≤ 1, total mass 1, block factorisation, full product/independence formula19       for coordinate functions, coordinate marginals ε.20   B2  agreement probability: 2·P[Y ⊕ E₁ ⊕ … ⊕ E_L = Y] = 1 + (1 − 2ε)^L; the m-fold law21       of the observations with FRESH independent error blocks is the product channel law22       chanW p Y with p the agreement probability.23   B3  the testing problem: hypotheses Y ∈ {0,1}, m observations from chanW p Y, arbitrary24       randomized rules φ (acceptance probabilities in [0,1]), error probabilities err0,25       err1, the majority rule with ties declared 0.26   B4  upper bound: bias a = 2p − 1, 0 < a ≤ 1, m·a² ≥ 4 ⇒ majority has both errors ≤ 1/427       (finite second-moment / Chebyshev argument).28   B5  lower bound: 0 < a ≤ 1/2 and both errors ≤ 1/4 for ANY randomized rule ⇒29       32·m·a² ≥ 3 (finite χ²/Cauchy–Schwarz argument plus a Bernoulli-type inequality).30   B6  packaging and the specialisation a = (1 − 2ε)^L.31   Nothing here concerns erroneous game moves, learned heads or training dynamics. -/3233namespace NimAudit34namespace Noise3536set_option linter.unusedSectionVars false3738open Lean.Grind Std Bridge3940section Generic4142variable {R : Type} [Field R] [LE R] [LT R] [LawfulOrderLT R] [IsLinearOrder R] [OrderedRing R]4344attribute [local instance] Semiring.natCast4546/-! ## Finite sums over lists -/4748/-- Finite sum Σ_{a ∈ l} f a. -/49def gs {α : Type} (l : List α) (f : α → R) : R := l.foldr (fun a s => f a + s) 05051@[simp] theorem gs_nil {α : Type} (f : α → R) : gs [] f = 0 := rfl52@[simp] theorem gs_cons {α : Type} (a : α) (l : List α) (f : α → R) : gs (a :: l) f = f a + gs l f := rfl5354theorem gs_append {α : Type} (l m : List α) (f : α → R) : gs (l ++ m) f = gs l f + gs m f := by55  induction l with56  | nil => simp only [List.nil_append, gs_nil]; grind57  | cons a l ih => simp only [List.cons_append, gs_cons, ih]; grind5859theorem gs_map {α β : Type} (g : α → β) (l : List α) (f : β → R) : gs (l.map g) f = gs l (fun a => f (g a)) := by60  induction l with61  | nil => rfl62  | cons a l ih => simp only [List.map_cons, gs_cons, ih]6364theorem gs_congr {α : Type} {l : List α} {f g : α → R} (h : ∀ a ∈ l, f a = g a) : gs l f = gs l g := by65  induction l with66  | nil => rfl67  | cons a l ih =>68    simp only [gs_cons]69    rw [h a (by simp), ih (fun x hx => h x (List.mem_cons_of_mem _ hx))]7071theorem gs_add {α : Type} (l : List α) (f g : α → R) : gs l (fun a => f a + g a) = gs l f + gs l g := by72  induction l with73  | nil => simp only [gs_nil]; grind74  | cons a l ih => simp only [gs_cons, ih]; grind7576theorem gs_sub {α : Type} (l : List α) (f g : α → R) : gs l (fun a => f a - g a) = gs l f - gs l g := by77  induction l with78  | nil => simp only [gs_nil]; grind79  | cons a l ih => simp only [gs_cons, ih]; grind8081theorem gs_mul_left {α : Type} (l : List α) (c : R) (f : α → R) : gs l (fun a => c * f a) = c * gs l f := by82  induction l with83  | nil => simp only [gs_nil]; grind84  | cons a l ih => simp only [gs_cons, ih]; grind8586theorem gs_zero {α : Type} (l : List α) : gs l (fun _ => (0 : R)) = 0 := by87  induction l with88  | nil => rfl89  | cons a l ih => simp only [gs_cons, ih]; grind9091theorem gs_le {α : Type} {l : List α} {f g : α → R} (h : ∀ a ∈ l, f a ≤ g a) : gs l f ≤ gs l g := by92  induction l with93  | nil => simp only [gs_nil]; grind94  | cons a l ih =>95    simp only [gs_cons]96    have h1 := h a (by simp)97    have h2 := ih (fun x hx => h x (List.mem_cons_of_mem _ hx))98    grind99100theorem gs_nonneg {α : Type} {l : List α} {f : α → R} (h : ∀ a ∈ l, 0 ≤ f a) : 0 ≤ gs l f := by101  have := gs_le (l := l) (f := fun _ => (0 : R)) (g := f) h102  rw [gs_zero] at this; exact this103104theorem gs_bitvecs_succ (n : Nat) (f : List Bool → R) :105    gs (bitvecs (n + 1)) f = gs (bitvecs n) (fun v => f (false :: v)) + gs (bitvecs n) (fun v => f (true :: v)) := by106  simp only [bitvecs, gs_append, gs_map]107108theorem gs_bitvecs_add (m n : Nat) (f : List Bool → R) :109    gs (bitvecs (m + n)) f = gs (bitvecs m) (fun v => gs (bitvecs n) (fun w => f (v ++ w))) := by110  induction m generalizing f with111  | zero => simp only [Nat.zero_add, bitvecs, gs_cons, gs_nil, List.nil_append]; grind112  | succ m ih =>113    rw [show m + 1 + n = (m + n) + 1 by omega, gs_bitvecs_succ, gs_bitvecs_succ, ih, ih]114    rfl115116/-! ## B1. The product Bernoulli(ε) law on error patterns -/117118/-- Weight of an error pattern e ∈ {0,1}^L: ∏ (ε if Eᵢ = 1, 1 − ε if Eᵢ = 0). -/119def fw (ε : R) : List Bool → R120  | [] => 1121  | b :: e => (if b then ε else 1 - ε) * fw ε e122123/-- NONNEGATIVITY on the domain 0 ≤ ε ≤ 1. -/124theorem fw_nonneg {ε : R} (h0 : 0 ≤ ε) (h1 : ε ≤ 1) : ∀ e, 0 ≤ fw ε e125  | [] => by simp only [fw]; exact OrderedRing.zero_le_one126  | b :: e => by127    simp only [fw]128    apply OrderedRing.mul_nonneg _ (fw_nonneg h0 h1 e)129    cases b130    · simp only [Bool.false_eq_true, if_false]; grind131    · simp only [if_true]; exact h0132133/-- NORMALISATION (for every ε). -/134theorem fw_total (ε : R) : ∀ L, gs (bitvecs L) (fw ε) = 1135  | 0 => by simp only [bitvecs, gs_cons, gs_nil, fw]; grind136  | L + 1 => by137    rw [gs_bitvecs_succ]138    simp only [fw, Bool.false_eq_true, if_false, if_true]139    rw [gs_mul_left, gs_mul_left, fw_total ε L]; grind140141/-- BLOCK FACTORISATION: the weight of a concatenation is the product of the weights. -/142theorem fw_append (ε : R) : ∀ e f : List Bool, fw ε (e ++ f) = fw ε e * fw ε f143  | [], f => by simp only [List.nil_append, fw]; grind144  | b :: e, f => by simp only [List.cons_append, fw, fw_append ε e f]; grind145146/-- Product of coordinate functions: pf f k (e₀ … e_{L−1}) = ∏ f (k+i) eᵢ. -/147def pf (f : Nat → Bool → R) : Nat → List Bool → R148  | _, [] => 1149  | k, b :: e => f k b * pf f (k + 1) e150151/-- Product of the coordinate expectations: ∏_{i<L} (ε·f (k+i) 1 + (1−ε)·f (k+i) 0). -/152def pe (ε : R) (f : Nat → Bool → R) : Nat → Nat → R153  | _, 0 => 1154  | k, L + 1 => (ε * f k true + (1 - ε) * f k false) * pe ε f (k + 1) L155156/-- INDEPENDENCE (product formula): the expectation of a product of functions of distinct157    coordinates is the product of their expectations.  With indicator functions this is158    P[∀ i, Eᵢ ∈ Aᵢ] = ∏ P[Eᵢ ∈ Aᵢ]: the coordinates are mutually independent. -/159theorem fw_product (ε : R) (f : Nat → Bool → R) : ∀ L k,160    gs (bitvecs L) (fun e => fw ε e * pf f k e) = pe ε f k L161  | 0, k => by simp only [bitvecs, gs_cons, gs_nil, fw, pf, pe]; grind162  | L + 1, k => by163    rw [gs_bitvecs_succ]164    have e0 : ∀ v, fw ε (false :: v) * pf f k (false :: v) = ((1 - ε) * f k false) * (fw ε v * pf f (k + 1) v) := by165      intro v; simp only [fw, pf, Bool.false_eq_true, if_false]; grind166    have e1 : ∀ v, fw ε (true :: v) * pf f k (true :: v) = (ε * f k true) * (fw ε v * pf f (k + 1) v) := by167      intro v; simp only [fw, pf, if_true]; grind168    rw [gs_congr (fun v _ => e0 v), gs_congr (fun v _ => e1 v), gs_mul_left, gs_mul_left, fw_product ε f L (k + 1)]169    simp only [pe]; grind170171/-- BLOCK INDEPENDENCE: events on disjoint blocks of coordinates multiply. -/172theorem fw_blocks (ε : R) (m n : Nat) (g h : List Bool → R) :173    gs (bitvecs (m + n)) (fun e => fw ε e * (g (e.take m) * h (e.drop m))) =174      gs (bitvecs m) (fun v => fw ε v * g v) * gs (bitvecs n) (fun w => fw ε w * h w) := by175  rw [gs_bitvecs_add]176  have e1 : ∀ v ∈ bitvecs m, gs (bitvecs n) (fun w => fw ε (v ++ w) * (g ((v ++ w).take m) * h ((v ++ w).drop m))) =177      (fw ε v * g v) * gs (bitvecs n) (fun w => fw ε w * h w) := by178    intro v hv179    have hl := mem_bitvecs_length hv180    rw [← gs_mul_left]181    apply gs_congr; intro w _182    rw [fw_append, List.take_left' hl, List.drop_left' hl]; grind183  rw [gs_congr e1]184  have e2 := gs_mul_left (bitvecs m) (gs (bitvecs n) (fun w => fw ε w * h w)) (fun v => fw ε v * g v)185  rw [show (fun v => fw ε v * g v * gs (bitvecs n) (fun w => fw ε w * h w)) =186      (fun v => gs (bitvecs n) (fun w => fw ε w * h w) * (fw ε v * g v)) by funext v; grind, e2]187  grind188189/-- Indicator of a Boolean in R. -/190def ind (b : Bool) : R := if b then 1 else 0191192/-- Probability of an event A ⊆ {0,1}^L under the flip law. -/193def prob (ε : R) (L : Nat) (A : List Bool → Bool) : R := gs (bitvecs L) (fun e => fw ε e * ind (A e))194195theorem getD_drop' (e : List Bool) (i : Nat) : e.getD i false = (e.drop i).getD 0 false := by196  simp only [List.getD_eq_getElem?_getD, List.getElem?_drop, Nat.add_zero]197198theorem gs_fw_one (ε : R) (i : Nat) : gs (bitvecs i) (fun v => fw ε v * (1 : R)) = 1 := by199  rw [show (fun v => fw ε v * (1 : R)) = fw ε by funext v; grind]; exact fw_total ε i200201theorem gs_fw_head (ε : R) (n : Nat) : gs (bitvecs (n + 1)) (fun w => fw ε w * ind (w.getD 0 false)) = ε := by202  rw [gs_bitvecs_succ]203  simp only [fw, ind, List.getD_cons_zero, Bool.false_eq_true, if_false, if_true]204  have h0 : gs (bitvecs n) (fun v => (1 - ε) * fw ε v * (0 : R)) = 0 := by205    rw [show (fun v => (1 - ε) * fw ε v * (0 : R)) = (fun _ => (0 : R)) by funext v; grind, gs_zero]206  have h1 : gs (bitvecs n) (fun v => ε * fw ε v * (1 : R)) = ε * gs (bitvecs n) (fw ε) := by207    rw [← gs_mul_left]; apply gs_congr; intro v _; grind208  rw [h0, h1, fw_total]; grind209210/-- COORDINATE MARGINALS: every coordinate is 1 with probability ε. -/211theorem fw_marginal (ε : R) {i L : Nat} (hi : i < L) : prob ε L (fun e => e.getD i false) = ε := by212  obtain ⟨n, rfl⟩ : ∃ n, L = i + (n + 1) := ⟨L - i - 1, by omega⟩213  unfold prob214  have hb := fw_blocks ε i (n + 1) (fun _ => (1 : R)) (fun w => ind (w.getD 0 false))215  simp only at hb216  have e1 : ∀ e : List Bool, fw ε e * ind (e.getD i false) = fw ε e * (1 * ind ((e.drop i).getD 0 false)) := by217    intro e; rw [getD_drop' e i, Semiring.one_mul]218  rw [gs_congr (fun e _ => e1 e), hb, gs_fw_one, gs_fw_head, Semiring.one_mul]219220/-! ## B2. The corrupted observation and fresh repetitions -/221222/-- ±1 encoding of a bit. -/223def sg (b : Bool) : R := if b then -1 else 1224225/-- SIGN IDENTITY: E[(−1)^{E₁ ⊕ … ⊕ E_L}] = (1 − 2ε)^L. -/226theorem fw_sign (ε : R) : ∀ L, gs (bitvecs L) (fun e => fw ε e * sg (par e)) = (1 - 2 * ε) ^ L227  | 0 => by simp only [bitvecs, gs_cons, gs_nil, fw, par, sg, Bool.false_eq_true, if_false]; grind228  | L + 1 => by229    rw [gs_bitvecs_succ]230    have e0 : ∀ v, fw ε (false :: v) * sg (par (false :: v)) = (1 - ε) * (fw ε v * sg (par v)) := by231      intro v; simp only [fw, par, Bool.false_xor, Bool.false_eq_true, if_false]; grind232    have e1 : ∀ v, fw ε (true :: v) * sg (par (true :: v)) = (-ε) * (fw ε v * sg (par v)) := by233      intro v; simp only [fw, par, Bool.true_xor, if_true]; cases par v <;> simp only [sg, Bool.not_false,234        Bool.not_true, Bool.false_eq_true, if_false, if_true] <;> grind235    rw [gs_congr (fun v _ => e0 v), gs_congr (fun v _ => e1 v), gs_mul_left, gs_mul_left, fw_sign ε L,236      Semiring.pow_succ]237    grind238239/-- Probability that the observed bit Y ⊕ E₁ ⊕ … ⊕ E_L equals the ideal bit Y. -/240def agree (ε : R) (L : Nat) : R := prob ε L (fun e => !par e)241242/-- THE REMARK'S FORMULA: P[Ỹ = Y] = (1 + (1 − 2ε)^L)/2, stated without division. -/243theorem agree_formula (ε : R) (L : Nat) : 2 * agree ε L = 1 + (1 - 2 * ε) ^ L := by244  unfold agree prob245  have h : ∀ e : List Bool, 2 * (fw ε e * ind (!par e)) = fw ε e + fw ε e * sg (par e) := by246    intro e; cases par e <;> simp only [ind, sg, Bool.not_false, Bool.not_true, Bool.false_eq_true,247      if_false, if_true] <;> grind248  rw [← gs_mul_left, gs_congr (fun e _ => h e), gs_add, fw_total, fw_sign]249250/-- The observed bit's law given the ideal bit Y. -/251theorem observe_law (ε : R) (L : Nat) (Y b : Bool) :252    prob ε L (fun e => decide (xor Y (par e) = b)) = if b = Y then agree ε L else 1 - agree ε L := by253  unfold agree prob254  by_cases hb : b = Y255  · subst hb; rw [if_pos rfl]; apply gs_congr; intro e _256    simp only; cases b <;> cases par e <;> simp257  · rw [if_neg hb]258    have h : ∀ e : List Bool, fw ε e * ind (decide (xor Y (par e) = b)) = fw ε e - fw ε e * ind (!par e) := by259      intro e260      have hb' : b = !Y := by cases b <;> cases Y <;> simp_all261      subst hb'262      cases Y <;> cases par e <;> simp only [ind, Bool.not_false, Bool.not_true, Bool.false_xor, Bool.true_xor,263        decide_eq_true_eq, decide_eq_false_iff_not, Bool.false_eq_true, if_false, if_true, decide_true,264        decide_false] <;> grind265    rw [gs_congr (fun e _ => h e), gs_sub, fw_total]266267theorem one_pow' : ∀ L : Nat, (1 : R) ^ L = 1268  | 0 => Semiring.pow_zero _269  | L + 1 => by rw [Semiring.pow_succ, one_pow' L]; grind270271/-- EDGE CASES of the agreement probability. -/272theorem agree_edges (ε : R) (L : Nat) :273    agree ε 0 = 1 ∧ agree (0 : R) L = 1 ∧ (2 * ε = 1 → 0 < L → 2 * agree ε L = 1) := by274  refine ⟨?_, ?_, fun h hL => ?_⟩275  · have := agree_formula ε 0; rw [Semiring.pow_zero] at this; grind276  · have := agree_formula (0 : R) L277    have e : (1 - 2 * (0 : R)) = 1 := by grind278    rw [e, one_pow'] at this279    grind280  · have hf := agree_formula ε L281    have e : 1 - 2 * ε = 0 := by grind282    rw [e] at hf283    obtain ⟨k, rfl⟩ : ∃ k, L = k + 1 := ⟨L - 1, by omega⟩284    rw [Semiring.pow_succ] at hf; grind285286/-- The observations of m repetitions, each using its own block of L error bits. -/287def obsOf (Y : Bool) (L : Nat) : Nat → List Bool → List Bool288  | 0, _ => []289  | m + 1, e => xor Y (par (e.take L)) :: obsOf Y L m (e.drop L)290291/-- The m-sample symmetric channel law: each sample equals Y with probability p. -/292def chanW (p : R) (Y : Bool) : List Bool → R293  | [] => 1294  | b :: o => (if b = Y then p else 1 - p) * chanW p Y o295296theorem ind_and (a b : Bool) : ind (a && b) = (ind a : R) * ind b := by297  cases a <;> cases b <;> simp only [ind, Bool.and_true, Bool.and_false, Bool.true_and, Bool.false_and,298    Bool.false_eq_true, if_false, if_true] <;> grind299300/-- REPEATED OBSERVATIONS WITH FRESH ERRORS: the law of the m observations, when the error301    pattern of length m·L has the product law (independent fresh blocks), is the product302    channel law with agreement probability agree ε L. -/303theorem repeated_law (ε : R) (Y : Bool) (L : Nat) : ∀ (m : Nat) (o : List Bool), o.length = m →304    gs (bitvecs (m * L)) (fun e => fw ε e * ind (decide (obsOf Y L m e = o))) = chanW (agree ε L) Y o305  | 0, o, ho => by306    have : o = [] := List.eq_nil_of_length_eq_zero ho307    subst this308    simp only [Nat.zero_mul, bitvecs, gs_cons, gs_nil, fw, obsOf, decide_true, ind, if_true, chanW]; grind309  | m + 1, o, ho => by310    obtain ⟨b, o', rfl⟩ : ∃ b o', o = b :: o' := by311      cases o with312      | nil => simp at ho313      | cons b o' => exact ⟨b, o', rfl⟩314    have ho' : o'.length = m := by simpa using ho315    rw [show (m + 1) * L = L + m * L by rw [Nat.succ_mul, Nat.add_comm]]316    have hb := fw_blocks ε L (m * L) (fun v => ind (decide (xor Y (par v) = b)))317      (fun w => ind (decide (obsOf Y L m w = o')))318    simp only at hb319    have e1 : ∀ e : List Bool, fw ε e * ind (decide (obsOf Y L (m + 1) e = b :: o')) =320        fw ε e * (ind (decide (xor Y (par (e.take L)) = b)) * ind (decide (obsOf Y L m (e.drop L) = o'))) := by321      intro e322      simp only [obsOf, List.cons.injEq]323      rw [← ind_and]; congr 2324      by_cases h1 : (xor Y (par (List.take L e)) = b) <;> by_cases h2 : obsOf Y L m (List.drop L e) = o' <;> simp [h1, h2]325    rw [gs_congr (fun e _ => e1 e), hb, repeated_law ε Y L m o' ho']326    have hq := observe_law ε L Y b327    unfold prob at hq328    rw [hq]; simp only [chanW]329330/-! ## B3. The testing problem -/331332/-- Number of observations equal to b. -/333def cnt (b : Bool) : List Bool → Nat334  | [] => 0335  | c :: o => (if c = b then 1 else 0) + cnt b o336337theorem cnt_add : ∀ o : List Bool, cnt true o + cnt false o = o.length338  | [] => rfl339  | c :: o => by have := cnt_add o; cases c <;> simp only [cnt, List.length_cons] <;> simp <;> omega340341/-- A RANDOMIZED decision rule on m observations: φ o ∈ [0,1] is the probability of342    declaring Y = 1.  Deterministic rules are the {0,1}-valued ones (detRule). -/343def Rule (m : Nat) (φ : List Bool → R) : Prop := ∀ o ∈ bitvecs m, 0 ≤ φ o ∧ φ o ≤ 1344345def detRule (δ : List Bool → Bool) : List Bool → R := fun o => ind (δ o)346347theorem detRule_rule (m : Nat) (δ : List Bool → Bool) : Rule m (detRule (R := R) δ) := by348  intro o _; unfold detRule ind; cases δ o <;> simp only [Bool.false_eq_true, if_false, if_true] <;>349    exact ⟨by grind, by grind⟩350351/-- Error under Y = 0 (declaring 1) and under Y = 1 (declaring 0). -/352def err0 (p : R) (m : Nat) (φ : List Bool → R) : R := gs (bitvecs m) (fun o => chanW p false o * φ o)353def err1 (p : R) (m : Nat) (φ : List Bool → R) : R := gs (bitvecs m) (fun o => chanW p true o * (1 - φ o))354355/-- THE MAJORITY RULE: declare 1 iff more than half of the m observations are 1; a tie356    (possible for even m) is declared 0. -/357def maj (o : List Bool) : Bool := decide (o.length < 2 * cnt true o)358359/-! ## Moments of the channel law -/360361def qY (p : R) (Y b : Bool) : R := if b = Y then p else 1 - p362363def prodF (f : Bool → R) : List Bool → R364  | [] => 1365  | b :: o => f b * prodF f o366367/-- Product formula for the channel law. -/368theorem chan_prod (p : R) (Y : Bool) (f : Bool → R) : ∀ m,369    gs (bitvecs m) (fun o => chanW p Y o * prodF f o) = (qY p Y true * f true + qY p Y false * f false) ^ m370  | 0 => by simp only [bitvecs, gs_cons, gs_nil, chanW, prodF, Semiring.pow_zero]; grind371  | m + 1 => by372    rw [gs_bitvecs_succ]373    have e0 : ∀ v, chanW p Y (false :: v) * prodF f (false :: v) = (qY p Y false * f false) * (chanW p Y v * prodF f v) := by374      intro v; simp only [chanW, prodF, qY]; grind375    have e1 : ∀ v, chanW p Y (true :: v) * prodF f (true :: v) = (qY p Y true * f true) * (chanW p Y v * prodF f v) := by376      intro v; simp only [chanW, prodF, qY]; grind377    rw [gs_congr (fun v _ => e0 v), gs_congr (fun v _ => e1 v), gs_mul_left, gs_mul_left, chan_prod p Y f m,378      Semiring.pow_succ]379    grind380381theorem prodF_one : ∀ o : List Bool, prodF (fun _ => (1 : R)) o = 1382  | [] => rfl383  | b :: o => by simp only [prodF, prodF_one o]; grind384385/-- NORMALISATION of the channel law (every p). -/386theorem chan_total (p : R) (Y : Bool) (m : Nat) : gs (bitvecs m) (chanW p Y) = 1 := by387  have h := chan_prod p Y (fun _ => 1) m388  rw [show (fun o => chanW p Y o * prodF (fun _ => (1 : R)) o) = chanW p Y by funext o; rw [prodF_one]; grind] at h389  rw [h]390  have : qY p Y true * 1 + qY p Y false * 1 = 1 := by cases Y <;> simp only [qY] <;> simp <;> grind391  rw [this, one_pow']392393theorem chan_nonneg {p : R} (h0 : 0 ≤ p) (h1 : p ≤ 1) (Y : Bool) : ∀ o, 0 ≤ chanW p Y o394  | [] => by simp only [chanW]; exact OrderedRing.zero_le_one395  | b :: o => by396    simp only [chanW]397    apply OrderedRing.mul_nonneg _ (chan_nonneg h0 h1 Y o)398    split <;> grind399400/-- Centred agreement count D(o) = #{j : oⱼ = Y} − m·p. -/401def dev (p : R) (Y : Bool) (o : List Bool) : R := (cnt Y o : R) - (o.length : R) * p402403theorem sum3 {α : Type} (l : List α) (A B C : R) (W y : α → R) :404    gs l (fun v => A * W v + B * (W v * y v) + C * (W v * y v ^ 2)) =405      A * gs l W + B * gs l (fun v => W v * y v) + C * gs l (fun v => W v * y v ^ 2) := by406  rw [gs_add, gs_add, gs_mul_left, gs_mul_left, gs_mul_left]407408theorem dev_cons (p : R) (Y b : Bool) (v : List Bool) :409    dev p Y (b :: v) = ((if b = Y then 1 else 0) - p) + dev p Y v := by410  unfold dev; simp only [cnt, List.length_cons]; split <;> grind411412/-- FIRST AND SECOND MOMENTS: E[D] = 0 and E[D²] = m·p·(1 − p). -/413theorem chan_moments (p : R) (Y : Bool) : ∀ m,414    gs (bitvecs m) (fun o => chanW p Y o * dev p Y o) = 0 ∧415    gs (bitvecs m) (fun o => chanW p Y o * dev p Y o ^ 2) = (m : R) * p * (1 - p)416  | 0 => by417    simp only [bitvecs, gs_cons, gs_nil, chanW, dev, cnt, List.length_nil]418    constructor <;> grind419  | m + 1 => by420    obtain ⟨ih1, ih2⟩ := chan_moments p Y m421    have ht := chan_total p Y m422    have hv : ∀ v ∈ bitvecs m, v.length = m := fun v hv => mem_bitvecs_length hv423    have br : ∀ b : Bool,424        gs (bitvecs m) (fun v => chanW p Y (b :: v) * dev p Y (b :: v)) =425          qY p Y b * ((if b = Y then 1 else 0) - p) ∧426        gs (bitvecs m) (fun v => chanW p Y (b :: v) * dev p Y (b :: v) ^ 2) =427          qY p Y b * (((if b = Y then 1 else 0) - p) ^ 2 + (m : R) * p * (1 - p)) := by428      intro b429      have hc : ∀ v, chanW p Y (b :: v) = qY p Y b * chanW p Y v := fun v => rfl430      generalize hx : ((if b = Y then 1 else 0) - p : R) = x431      have hd : ∀ v, dev p Y (b :: v) = x + dev p Y v := fun v => by rw [dev_cons, hx]432      generalize qY p Y b = q at hc433      constructor434      · have e : ∀ v, chanW p Y (b :: v) * dev p Y (b :: v) =435            (q * x) * chanW p Y v + q * (chanW p Y v * dev p Y v) + 0 * (chanW p Y v * dev p Y v ^ 2) := by436          intro v; rw [hc, hd]; grind437        rw [gs_congr (fun v _ => e v), sum3, ht, ih1, ih2]; grind438      · have e : ∀ v, chanW p Y (b :: v) * dev p Y (b :: v) ^ 2 =439            (q * x ^ 2) * chanW p Y v + (2 * q * x) * (chanW p Y v * dev p Y v) + q * (chanW p Y v * dev p Y v ^ 2) := by440          intro v; rw [hc, hd]; grind441        rw [gs_congr (fun v _ => e v), sum3, ht, ih1, ih2]; grind442    obtain ⟨f0, s0⟩ := br false443    obtain ⟨f1, s1⟩ := br true444    rw [gs_bitvecs_succ, gs_bitvecs_succ, f0, f1, s0, s1]445    cases Y <;> simp only [qY, Bool.false_eq_true, Bool.true_eq_false, if_false, if_true] <;> constructor <;> grind446447/-! ## B4. Upper bound for the majority rule (finite Chebyshev) -/448449theorem sq_le_sq' {x y : R} (h0 : 0 ≤ x) (h : x ≤ y) : x ^ 2 ≤ y ^ 2 := by450  have h1 : x * x ≤ x * y := OrderedRing.mul_le_mul_of_nonneg_left h h0451  have h2 : x * y ≤ y * y := OrderedRing.mul_le_mul_of_nonneg_right h (by grind)452  have e1 : x ^ 2 = x * x := by grind453  have e2 : y ^ 2 = y * y := by grind454  rw [e1, e2]; grind455456/-- Pointwise Chebyshev: on the event 2·#agreements ≤ m the centred count is at least m·a/2457    in absolute value. -/458theorem cheb_point {p a : R} (hap : 2 * p = 1 + a) (ha : 0 ≤ a) (Y : Bool) (o : List Bool) :459    ind (decide (2 * cnt Y o ≤ o.length)) * ((o.length : R) * a) ^ 2 ≤ 4 * dev p Y o ^ 2 := by460  unfold ind dev461  by_cases h : 2 * cnt Y o ≤ o.length462  · rw [_root_.decide_eq_true h, if_pos rfl]463    have hc : 2 * (cnt Y o : R) ≤ (o.length : R) := by464      have := OrderedRing.natCast_le_natCast_of_le (R := R) _ _ h; grind465    have hm : (0 : R) ≤ (o.length : R) * a := OrderedRing.mul_nonneg (by466      have := OrderedRing.natCast_le_natCast_of_le (R := R) 0 o.length (Nat.zero_le _); grind) ha467    have hmp : (o.length : R) * (2 * p) = (o.length : R) * (1 + a) := by rw [hap]468    have key : (o.length : R) * a ≤ 2 * ((o.length : R) * p - (cnt Y o : R)) := by grind469    have := sq_le_sq' hm key470    grind471  · rw [_root_.decide_eq_false h, if_neg (by simp)]472    have : (0 : R) ≤ ((cnt Y o : R) - (o.length : R) * p) ^ 2 := OrderedRing.sq_nonneg473    grind474475/-- CHEBYSHEV: P_Y[2·#agreements ≤ m] · (m a)² ≤ 4 m p (1 − p). -/476theorem cheb (p a : R) (hap : 2 * p = 1 + a) (ha : 0 ≤ a) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (Y : Bool) (m : Nat) :477    gs (bitvecs m) (fun o => chanW p Y o * ind (decide (2 * cnt Y o ≤ m))) * ((m : R) * a) ^ 2 ≤478      4 * ((m : R) * p * (1 - p)) := by479  rw [← (chan_moments p Y m).2, ← gs_mul_left]480  have e : gs (bitvecs m) (fun o => chanW p Y o * ind (decide (2 * cnt Y o ≤ m))) * ((m : R) * a) ^ 2 =481      gs (bitvecs m) (fun o => chanW p Y o * (ind (decide (2 * cnt Y o ≤ o.length)) * ((o.length : R) * a) ^ 2)) := by482    rw [show gs (bitvecs m) (fun o => chanW p Y o * ind (decide (2 * cnt Y o ≤ m))) * ((m : R) * a) ^ 2 =483        ((m : R) * a) ^ 2 * gs (bitvecs m) (fun o => chanW p Y o * ind (decide (2 * cnt Y o ≤ m))) by grind,484      ← gs_mul_left]485    apply gs_congr; intro o ho; rw [mem_bitvecs_length ho]; grind486  rw [e]487  apply gs_le; intro o _488  have hw := chan_nonneg hp0 hp1 Y o489  have := OrderedRing.mul_le_mul_of_nonneg_left (cheb_point hap ha Y o) hw490  grind491492theorem nat_cast_nonneg' (n : Nat) : (0 : R) ≤ (n : R) := by493  have := OrderedRing.natCast_le_natCast_of_le (R := R) 0 n (Nat.zero_le _); grind494495/-- From the Chebyshev bound to error ≤ 1/4 once m·a² ≥ 4. -/496theorem quarter_of_cheb {p a E : R} {m : Nat} (hap : 2 * p = 1 + a) (hE : 0 ≤ E)497    (hc : E * ((m : R) * a) ^ 2 ≤ 4 * ((m : R) * p * (1 - p))) (hm : 4 ≤ (m : R) * a ^ 2) : 4 * E ≤ 1 := by498  have hm0 := nat_cast_nonneg' (R := R) m499  have hEm : 0 ≤ E * (m : R) := OrderedRing.mul_nonneg hE hm0500  have h1 : E * (m : R) * 4 ≤ E * (m : R) * ((m : R) * a ^ 2) := OrderedRing.mul_le_mul_of_nonneg_left hm hEm501  have h2 : 4 * ((m : R) * p * (1 - p)) = (m : R) * (1 - a ^ 2) := by502    have : 4 * (p * (1 - p)) = 1 - a ^ 2 := by503      have e : 4 * (p * (1 - p)) = (2 * p) * (2 - 2 * p) := by grind504      rw [e, hap]; grind505    grind506  have h3 : (m : R) * (1 - a ^ 2) ≤ (m : R) := by507    have : 0 ≤ (m : R) * a ^ 2 := OrderedRing.mul_nonneg hm0 OrderedRing.sq_nonneg508    grind509  have hpos : (0 : R) < (m : R) := by510    rcases Nat.eq_zero_or_pos m with h | h511    · subst h; exfalso512      have : ((0 : Nat) : R) = 0 := by grind513      rw [this] at hm; grind514    · have := OrderedRing.natCast_le_natCast_of_le (R := R) 1 m h; grind515  have h4 : (4 * E) * (m : R) ≤ 1 * (m : R) := by grind516  exact (Field.IsOrdered.mul_le_mul_iff_of_pos_right hpos).1 h4517518/-- B4. UPPER BOUND (constructive): for bias 0 < a ≤ 1 (p = (1 + a)/2) and every m with519    m·a² ≥ 4, the majority rule (ties declared 0) has error at most 1/4 under BOTH520    hypotheses. -/521theorem maj_upper (p a : R) (hap : 2 * p = 1 + a) (ha0 : 0 < a) (ha1 : a ≤ 1) (m : Nat)522    (hm : 4 ≤ (m : R) * a ^ 2) :523    4 * err0 p m (detRule maj) ≤ 1 ∧ 4 * err1 p m (detRule maj) ≤ 1 := by524  have hp0 : 0 ≤ p := by grind525  have hp1 : p ≤ 1 := by grind526  constructor527  · have hle : err0 p m (detRule maj) ≤ gs (bitvecs m) (fun o => chanW p false o * ind (decide (2 * cnt false o ≤ m))) := by528      apply gs_le; intro o ho529      have hl := mem_bitvecs_length ho530      apply OrderedRing.mul_le_mul_of_nonneg_left _ (chan_nonneg hp0 hp1 false o)531      unfold detRule maj ind532      have hc := cnt_add o533      by_cases h : o.length < 2 * cnt true o534      · rw [_root_.decide_eq_true h, if_pos rfl, _root_.decide_eq_true (by omega), if_pos rfl]; grind535      · rw [_root_.decide_eq_false h, if_neg (by simp)]; split <;> grind536    have hE := gs_nonneg (l := bitvecs m) (f := fun o => chanW p false o * ind (decide (2 * cnt false o ≤ m)))537      (fun o _ => OrderedRing.mul_nonneg (chan_nonneg hp0 hp1 false o) (by unfold ind; split <;> grind))538    have := quarter_of_cheb hap hE (cheb p a hap (by grind) hp0 hp1 false m) hm539    grind540  · have he : err1 p m (detRule maj) = gs (bitvecs m) (fun o => chanW p true o * ind (decide (2 * cnt true o ≤ m))) := by541      apply gs_congr; intro o ho542      have hl := mem_bitvecs_length ho543      unfold detRule maj ind544      by_cases h : o.length < 2 * cnt true o545      · rw [_root_.decide_eq_true h, if_pos rfl, _root_.decide_eq_false (by omega), if_neg (by simp)]; grind546      · rw [_root_.decide_eq_false h, if_neg (by simp), _root_.decide_eq_true (by omega), if_pos rfl]; grind547    have hE := gs_nonneg (l := bitvecs m) (f := fun o => chanW p true o * ind (decide (2 * cnt true o ≤ m)))548      (fun o _ => OrderedRing.mul_nonneg (chan_nonneg hp0 hp1 true o) (by unfold ind; split <;> grind))549    rw [he]550    exact quarter_of_cheb hap hE (cheb p a hap (by grind) hp0 hp1 true m) hm551552/-! ## B5. Lower bound for arbitrary randomized rules (finite χ² argument) -/553554/-- Per-observation likelihood ratio P₁(b)/P₀(b) (P₀ = law under Y = 0, P₁ under Y = 1). -/555def rr (p : R) (b : Bool) : R := if b then p * (1 - p)⁻¹ else (1 - p) * p⁻¹556557/-- The single-observation χ² factor: Σ_b P₁(b)²/P₀(b). -/558def chiG (p : R) : R := p * (p * (1 - p)⁻¹) + (1 - p) * ((1 - p) * p⁻¹)559560theorem lr_mul {p : R} (hp : p * p⁻¹ = 1) (hq : (1 - p) * (1 - p)⁻¹ = 1) :561    ∀ o, chanW p false o * prodF (rr p) o = chanW p true o562  | [] => by simp only [chanW, prodF]; grind563  | b :: o => by564    have ih := lr_mul hp hq o565    simp only [chanW, prodF]566    generalize chanW p false o = W0 at ih ⊢567    generalize prodF (rr p) o = Lr at ih ⊢568    generalize chanW p true o = W1 at ih ⊢569    subst ih570    cases b571    · simp only [rr, Bool.false_eq_true, if_false, if_true]572      have : p * W0 * ((1 - p) * p⁻¹ * Lr) = (p * p⁻¹) * ((1 - p) * (W0 * Lr)) := by grind573      rw [this, hp]; grind574    · simp only [rr, Bool.true_eq_false, if_false, if_true]575      have : (1 - p) * W0 * (p * (1 - p)⁻¹ * Lr) = ((1 - p) * (1 - p)⁻¹) * (p * (W0 * Lr)) := by grind576      rw [this, hq]; grind577578/-- Σ_o P₀(o)·LR(o)² = G^m (the χ² identity for the product law). -/579theorem chi_identity {p : R} (hp : p * p⁻¹ = 1) (hq : (1 - p) * (1 - p)⁻¹ = 1) (m : Nat) :580    gs (bitvecs m) (fun o => chanW p false o * prodF (rr p) o ^ 2) = chiG p ^ m := by581  have e : ∀ o, chanW p false o * prodF (rr p) o ^ 2 = chanW p true o * prodF (rr p) o := by582    intro o; rw [← lr_mul hp hq o]; grind583  rw [gs_congr (fun o _ => e o), chan_prod]584  simp only [qY, rr, chiG, if_true, Bool.false_eq_true, Bool.true_eq_false, if_false]585586/-- The χ² factor in terms of the bias: (G − 1)(1 − a²) = 4a². -/587theorem chiG_bias {p a : R} (hap : 2 * p = 1 + a) (hp : p * p⁻¹ = 1) (hq : (1 - p) * (1 - p)⁻¹ = 1) :588    (chiG p - 1) * (1 - a ^ 2) = 4 * a ^ 2 := by589  have hG : chiG p * (p * (1 - p)) = p ^ 3 + (1 - p) ^ 3 := by590    unfold chiG591    have e : (p * (p * (1 - p)⁻¹) + (1 - p) * ((1 - p) * p⁻¹)) * (p * (1 - p)) =592        p ^ 3 * ((1 - p) * (1 - p)⁻¹) + (1 - p) ^ 3 * (p * p⁻¹) := by grind593    rw [e, hp, hq]; grind594  have h4 : 4 * (p * (1 - p)) = 1 - a ^ 2 := by595    have e : 4 * (p * (1 - p)) = (2 * p) * (2 - 2 * p) := by grind596    rw [e, hap]; grind597  have e2 : (chiG p - 1) * (1 - a ^ 2) = 4 * (chiG p * (p * (1 - p))) - 4 * (p * (1 - p)) := by rw [← h4]; grind598  rw [e2, hG]599  have e3 : p ^ 3 + (1 - p) ^ 3 = 1 - 3 * (p * (1 - p)) := by grind600  rw [e3]; grind601602/-- A Bernoulli-type inequality: (1 + x)^m (1 − m x) ≤ 1 for x ≥ 0. -/603theorem bernoulli_le (x : R) (hx : 0 ≤ x) : ∀ m : Nat, (1 + x) ^ m * (1 - (m : R) * x) ≤ 1604  | 0 => by rw [Semiring.pow_zero]; grind605  | m + 1 => by606    have ih := bernoulli_le x hx m607    have hpow : 0 ≤ (1 + x) ^ m := by608      clear ih609      induction m with610      | zero => rw [Semiring.pow_zero]; exact OrderedRing.zero_le_one611      | succ k ihk => rw [Semiring.pow_succ]; exact OrderedRing.mul_nonneg ihk (by grind)612    have hm := nat_cast_nonneg' (R := R) m613    have h2 : 0 ≤ (1 + x) ^ m * (((m : R) + 1) * x ^ 2) :=614      OrderedRing.mul_nonneg hpow (OrderedRing.mul_nonneg (by grind) OrderedRing.sq_nonneg)615    have e : (1 + x) ^ (m + 1) * (1 - ((m + 1 : Nat) : R) * x) =616        (1 + x) ^ m * (1 - (m : R) * x) - (1 + x) ^ m * (((m : R) + 1) * x ^ 2) := by617      rw [Semiring.pow_succ]; grind618    rw [e]; grind619620/-- The quadratic (Cauchy–Schwarz) step: Σ P₀ (LR − 1)² ≥ (Σ (P₁ − P₀)(2φ − 1))² whenever621    0 ≤ φ ≤ 1. -/622theorem sum3' {α : Type} (l : List α) (A B C : R) (f g h : α → R) :623    gs l (fun v => A * f v + B * g v + C * h v) = A * gs l f + B * gs l g + C * gs l h := by624  rw [gs_add, gs_add, gs_mul_left, gs_mul_left, gs_mul_left]625626/-- Sum of the two errors of any rule: err₀ + err₁ = 1 − Σ (P₁ − P₀) φ. -/627theorem err_sum (p : R) (m : Nat) (φ : List Bool → R) :628    err0 p m φ + err1 p m φ = 1 - gs (bitvecs m) (fun o => (chanW p true o - chanW p false o) * φ o) := by629  unfold err0 err1630  have e : ∀ o, chanW p true o * (1 - φ o) = chanW p true o - chanW p true o * φ o := fun o => by grind631  have e2 : ∀ o, (chanW p true o - chanW p false o) * φ o = chanW p true o * φ o - chanW p false o * φ o :=632    fun o => by grind633  rw [gs_congr (fun o _ => e o), gs_congr (fun o _ => e2 o), gs_sub, gs_sub, chan_total]; grind634635theorem sq_unit {φ : R} (hl : 0 ≤ φ) (hu : φ ≤ 1) : (2 * φ - 1) ^ 2 ≤ 1 := by636  have : 0 ≤ (1 - (2 * φ - 1)) * (1 + (2 * φ - 1)) := OrderedRing.mul_nonneg (by grind) (by grind)637  grind638639theorem final_arith (A D G : R) (hq0 : 0 ≤ D ^ 2 * A + (-2 * D) * D + 1 * (G - 1)) (hA : D ^ 2 * A ≤ D ^ 2 * 1)640    (h1 : 1 ≤ D ^ 2) : 2 ≤ G := by grind641642/-- B5 core: if both errors are at most 1/4 then G^m ≥ 2. -/643theorem chi_ge_two {p : R} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hp : p * p⁻¹ = 1) (hq : (1 - p) * (1 - p)⁻¹ = 1)644    (m : Nat) (φ : List Bool → R) (hφ : Rule m φ) (h0 : 4 * err0 p m φ ≤ 1) (h1 : 4 * err1 p m φ ≤ 1) :645    2 ≤ chiG p ^ m := by646  -- Δ := Σ (P₁ − P₀) φ ≥ 1/2647  have hs := err_sum p m φ648  generalize hΔ : gs (bitvecs m) (fun o => (chanW p true o - chanW p false o) * φ o) = Δ at hs649  have hΔ2 : 1 ≤ 2 * Δ := by grind650  -- the quadratic form at t = 2Δ651  let P0 := chanW p false652  let LR := prodF (rr p)653  have hlr : ∀ o, P0 o * LR o = chanW p true o := lr_mul hp hq654  have hq0 : 0 ≤ gs (bitvecs m) (fun o => P0 o * ((2 * Δ) * (2 * φ o - 1) - (LR o - 1)) ^ 2) :=655    gs_nonneg (fun o _ => OrderedRing.mul_nonneg (chan_nonneg hp0 hp1 false o) OrderedRing.sq_nonneg)656  have expand : ∀ o, P0 o * ((2 * Δ) * (2 * φ o - 1) - (LR o - 1)) ^ 2 =657      (2 * Δ) ^ 2 * (P0 o * (2 * φ o - 1) ^ 2) + (-2 * (2 * Δ)) * ((2 * φ o - 1) * (chanW p true o - P0 o)) +658        1 * (P0 o * LR o ^ 2 - 2 * chanW p true o + P0 o) := by659    intro o; rw [← hlr o]; grind660  rw [gs_congr (fun o _ => expand o), sum3'] at hq0661  -- A = Σ P₀ (2φ − 1)² ≤ 1662  have hA : gs (bitvecs m) (fun o => P0 o * (2 * φ o - 1) ^ 2) ≤ 1 := by663    have h := gs_le (l := bitvecs m) (f := fun o => P0 o * (2 * φ o - 1) ^ 2) (g := chanW p false) (by664      intro o ho665      obtain ⟨hl, hu⟩ := hφ o ho666      have hw : (2 * φ o - 1) ^ 2 ≤ 1 := sq_unit hl hu667      have := OrderedRing.mul_le_mul_of_nonneg_left hw (chan_nonneg hp0 hp1 false o)668      simp only [P0]; grind)669    rw [chan_total] at h; exact h670  -- B = Σ (2φ − 1)(P₁ − P₀) = 2Δ671  have hB : gs (bitvecs m) (fun o => (2 * φ o - 1) * (chanW p true o - P0 o)) = 2 * Δ := by672    have e : ∀ o, (2 * φ o - 1) * (chanW p true o - P0 o) =673        2 * ((chanW p true o - chanW p false o) * φ o) - (chanW p true o - chanW p false o) := by674      intro o; simp only [P0]; grind675    rw [gs_congr (fun o _ => e o), gs_sub, gs_mul_left, hΔ, gs_sub, chan_total, chan_total]; grind676  -- C = G^m − 1677  have hC : gs (bitvecs m) (fun o => P0 o * LR o ^ 2 - 2 * chanW p true o + P0 o) = chiG p ^ m - 1 := by678    rw [gs_add, gs_sub, gs_mul_left, chi_identity hp hq, chan_total, chan_total]; grind679  rw [hB, hC] at hq0680  have hsq : 0 ≤ (2 * Δ) ^ 2 := OrderedRing.sq_nonneg681  have hAm := OrderedRing.mul_le_mul_of_nonneg_left hA hsq682  have h1' : (1 : R) ≤ (2 * Δ) ^ 2 := by683    have := sq_le_sq' (by grind : (0 : R) ≤ 1) hΔ2; grind684  exact final_arith _ _ _ hq0 hAm h1'685686/-- From G^m ≥ 2 and (G − 1)(1 − a²) = 4a² to 8·m·a² ≥ 1 − a². -/687theorem samples_from_chi {a x : R} {m : Nat} (hx : x * (1 - a ^ 2) = 4 * a ^ 2) (ha : a ^ 2 < 1)688    (hG : 2 ≤ (1 + x) ^ m) : 1 - a ^ 2 ≤ 8 * ((m : R) * a ^ 2) := by689  have hpos : 0 < 1 - a ^ 2 := by grind690  have hx0 : 0 ≤ x := by691    rcases IsLinearPreorder.le_total 0 x with h | h692    · exact h693    · by_cases hz : x = 0694      · grind695      · have hneg : x < 0 := by grind696        have := OrderedRing.mul_neg_of_neg_of_pos hneg hpos697        have : 0 ≤ a ^ 2 := OrderedRing.sq_nonneg698        grind699  have hb := bernoulli_le x hx0 m700  have h2 : 1 ≤ 2 * ((m : R) * x) := by701    rcases IsLinearPreorder.le_total (1 - (m : R) * x) 0 with h | h702    · grind703    · have := OrderedRing.mul_le_mul_of_nonneg_right hG h704      grind705  have e : (2 * ((m : R) * x)) * (1 - a ^ 2) = 8 * ((m : R) * a ^ 2) := by706    rw [show (2 * ((m : R) * x)) * (1 - a ^ 2) = 2 * (m : R) * (x * (1 - a ^ 2)) by grind, hx]; grind707  have h3 := OrderedRing.mul_le_mul_of_nonneg_right h2 (Preorder.le_of_lt hpos)708  grind709710/-- B5 (general bias 0 < a < 1): any rule with both errors ≤ 1/4 needs 8·m·a² ≥ 1 − a². -/711theorem lower_bound_general (p a : R) (hap : 2 * p = 1 + a) (ha0 : 0 < a) (ha1 : a < 1) (m : Nat)712    (φ : List Bool → R) (hφ : Rule m φ) (h0 : 4 * err0 p m φ ≤ 1) (h1 : 4 * err1 p m φ ≤ 1) :713    1 - a ^ 2 ≤ 8 * ((m : R) * a ^ 2) := by714  have hp0 : 0 ≤ p := by grind715  have hp1 : p ≤ 1 := by grind716  have hpne : p ≠ 0 := by intro h; rw [h] at hap; grind717  have hqne : 1 - p ≠ 0 := by intro h; grind718  have hp : p * p⁻¹ = 1 := Field.mul_inv_cancel hpne719  have hq : (1 - p) * (1 - p)⁻¹ = 1 := Field.mul_inv_cancel hqne720  have hG := chi_ge_two hp0 hp1 hp hq m φ hφ h0 h1721  have hx := chiG_bias hap hp hq722  have ha2 : a ^ 2 < 1 := by723    have : a * a < 1 * 1 := by724      have h1' : a * a < a * 1 := OrderedRing.mul_lt_mul_of_pos_left ha1 ha0725      grind726    grind727  have hG' : 2 ≤ (1 + (chiG p - 1)) ^ m := by rw [show 1 + (chiG p - 1) = chiG p by grind]; exact hG728  exact samples_from_chi hx ha2 hG'729730/-- B5. LOWER BOUND for ARBITRARY (randomized, hence also deterministic) rules: with bias731    0 < a ≤ 1/2, if both error probabilities are at most 1/4 then 32·m·a² ≥ 3. -/732theorem lower_bound (p a : R) (hap : 2 * p = 1 + a) (ha0 : 0 < a) (ha1 : 2 * a ≤ 1) (m : Nat)733    (φ : List Bool → R) (hφ : Rule m φ) (h0 : 4 * err0 p m φ ≤ 1) (h1 : 4 * err1 p m φ ≤ 1) :734    3 ≤ 32 * ((m : R) * a ^ 2) := by735  have h := lower_bound_general p a hap ha0 (by grind) m φ hφ h0 h1736  have h4 : 4 * a ^ 2 ≤ 1 := by737    have := sq_le_sq' (by grind : (0 : R) ≤ 2 * a) ha1738    grind739  grind740741/-! ## B3 edge cases -/742743/-- NO SIGNAL (a = 0, e.g. ε = 1/2 with L > 0): the two hypotheses give the same law, so744    every rule has err₀ + err₁ = 1 and worst-case error at least 1/2. -/745theorem no_signal (p : R) (hp : 2 * p = 1) (m : Nat) (φ : List Bool → R) :746    err0 p m φ + err1 p m φ = 1 := by747  have e : ∀ o, chanW p true o = chanW p false o := by748    intro o; induction o with749    | nil => rfl750    | cons b o ih =>751      simp only [chanW, ih]752      have : 1 - p = p := by grind753      cases b <;> simp only [Bool.false_eq_true, Bool.true_eq_false, if_true, if_false, this]754  rw [err_sum]755  have : gs (bitvecs m) (fun o => (chanW p true o - chanW p false o) * φ o) = 0 := by756    rw [show (fun o => (chanW p true o - chanW p false o) * φ o) = (fun _ => (0 : R)) by757      funext o; rw [e o]; grind, gs_zero]758  rw [this]; grind759760/-- EXACT OBSERVATIONS (a = 1, e.g. ε = 0 or L = 0): one sample and the identity rule give761    zero error under both hypotheses. -/762theorem exact_channel : err0 (1 : R) 1 (fun o => ind (o.getD 0 false)) = 0 ∧763    err1 (1 : R) 1 (fun o => ind (o.getD 0 false)) = 0 := by764  simp only [err0, err1, bitvecs, List.map_cons, List.map_nil, List.cons_append, List.nil_append,765    gs_cons, gs_nil, chanW, ind, List.getD_cons_zero, Bool.false_eq_true, Bool.true_eq_false, if_true, if_false]766  constructor <;> grind767768/-! ## B6. Packaging: the precise meaning of "order a^{-2} repetitions" -/769770/-- m samples suffice for worst-case error ≤ 1/4 (some randomized rule achieves it). -/771def Achievable (p : R) (m : Nat) : Prop :=772  ∃ φ : List Bool → R, Rule m φ ∧ 4 * err0 p m φ ≤ 1 ∧ 4 * err1 p m φ ≤ 1773774/-- ORDER a^{-2}, TWO-SIDED: for bias 0 < a ≤ 1/2,775      m·a² ≥ 4  ⇒  achievable (by the majority rule), and776      achievable (by ANY randomized rule) ⇒ 32·m·a² ≥ 3.777    So the least sufficient m lies between 3/(32a²) and the least m with m·a² ≥ 4. -/778theorem order_inv_sq (p a : R) (hap : 2 * p = 1 + a) (ha0 : 0 < a) (ha1 : 2 * a ≤ 1) :779    (∀ m : Nat, 4 ≤ (m : R) * a ^ 2 → Achievable p m) ∧780    (∀ m : Nat, Achievable p m → 3 ≤ 32 * ((m : R) * a ^ 2)) := by781  refine ⟨fun m hm => ⟨detRule maj, detRule_rule m maj, maj_upper p a hap ha0 (by grind) m hm⟩,782    fun m ⟨φ, hφ, h0, h1⟩ => lower_bound p a hap ha0 ha1 m φ hφ h0 h1⟩783784/-! ## Errors computed on the underlying error space (fresh repetitions) -/785786theorem gs_comm {α β : Type} (l : List α) (k : List β) (f : α → β → R) :787    gs l (fun a => gs k (fun b => f a b)) = gs k (fun b => gs l (fun a => f a b)) := by788  induction l with789  | nil => simp only [gs_nil]; rw [gs_zero]790  | cons a l ih => simp only [gs_cons]; rw [ih, ← gs_add]791792theorem gs_point : ∀ (m : Nat) (x : List Bool), x.length = m → ∀ g : List Bool → R,793    gs (bitvecs m) (fun o => ind (decide (x = o)) * g o) = g x794  | 0, x, hx, g => by795    have : x = [] := List.eq_nil_of_length_eq_zero hx796    subst this; simp only [bitvecs, gs_cons, gs_nil, decide_true, ind, if_true]; grind797  | m + 1, x, hx, g => by798    obtain ⟨b, x', rfl⟩ : ∃ b x', x = b :: x' := by799      cases x with800      | nil => simp at hx801      | cons b x' => exact ⟨b, x', rfl⟩802    have hx' : x'.length = m := by simpa using hx803    rw [gs_bitvecs_succ]804    have hf : ∀ c v, ind (decide (b :: x' = c :: v)) * g (c :: v) =805        (if b = c then 1 else 0) * (ind (decide (x' = v)) * g (c :: v)) := by806      intro c v807      by_cases hbc : b = c <;> by_cases hxv : x' = v <;> simp only [hbc, hxv, List.cons.injEq, and_self,808        and_true, true_and, and_false, false_and, decide_true, decide_false, ind, if_true, if_false,809        Bool.false_eq_true] <;> grind810    rw [gs_congr (fun v _ => hf false v), gs_congr (fun v _ => hf true v), gs_mul_left, gs_mul_left,811      gs_point m x' hx' (fun o => g (false :: o)), gs_point m x' hx' (fun o => g (true :: o))]812    cases b <;> simp only [Bool.false_eq_true, Bool.true_eq_false, if_true, if_false] <;> grind813814theorem obsOf_length (Y : Bool) (L : Nat) : ∀ m e, (obsOf Y L m e).length = m815  | 0, _ => rfl816  | m + 1, e => by simp [obsOf, obsOf_length Y L m]817818/-- TRANSFER TO THE ERROR SPACE: averaging a function of the m observations over the819    fresh-error law equals averaging it over the channel law chanW (agree ε L) Y. -/820theorem rep_expect (ε : R) (Y : Bool) (L m : Nat) (g : List Bool → R) :821    gs (bitvecs (m * L)) (fun e => fw ε e * g (obsOf Y L m e)) =822      gs (bitvecs m) (fun o => chanW (agree ε L) Y o * g o) := by823  have e1 : ∀ e, fw ε e * g (obsOf Y L m e) =824      gs (bitvecs m) (fun o => (fw ε e * ind (decide (obsOf Y L m e = o))) * g o) := by825    intro e826    rw [← gs_point m (obsOf Y L m e) (obsOf_length Y L m e) g, ← gs_mul_left]827    apply gs_congr; intro o _; grind828  rw [gs_congr (fun e _ => e1 e), gs_comm]829  apply gs_congr; intro o ho830  have := repeated_law ε Y L m o (mem_bitvecs_length ho)831  rw [show (fun e => fw ε e * ind (decide (obsOf Y L m e = o)) * g o) =832      (fun e => g o * (fw ε e * ind (decide (obsOf Y L m e = o)))) by funext e; grind, gs_mul_left, this]833  grind834835/-- B6, SPECIALISED to the flip model: a = (1 − 2ε)^L, p = P[Ỹ = Y].  If 0 ≤ ε, 2ε < 1836    and (1 − 2ε)^L ≤ 1/2, then for m fresh repetitions (error space of m·L independent837    flips): m·a² ≥ 4 suffices (majority), and any randomized rule with both errors ≤ 1/4838    needs 32·m·a² ≥ 3.  Errors are computed directly on the error space.  (0 ≤ ε is not839    needed as a hypothesis: the regime condition 2a ≤ 1 with a > 0 is what is used; the840    error law is a probability law when 0 ≤ ε ≤ 1, fw_nonneg.) -/841theorem flip_order_inv_sq (ε : R) (L : Nat) (hε1 : 2 * ε < 1)842    (hsmall : 2 * (1 - 2 * ε) ^ L ≤ 1) :843    (∀ m : Nat, 4 ≤ (m : R) * ((1 - 2 * ε) ^ L) ^ 2 →844      4 * gs (bitvecs (m * L)) (fun e => fw ε e * detRule maj (obsOf false L m e)) ≤ 1 ∧845      4 * gs (bitvecs (m * L)) (fun e => fw ε e * (1 - detRule maj (obsOf true L m e))) ≤ 1) ∧846    (∀ (m : Nat) (φ : List Bool → R), Rule m φ →847      4 * gs (bitvecs (m * L)) (fun e => fw ε e * φ (obsOf false L m e)) ≤ 1 →848      4 * gs (bitvecs (m * L)) (fun e => fw ε e * (1 - φ (obsOf true L m e))) ≤ 1 →849      3 ≤ 32 * ((m : R) * ((1 - 2 * ε) ^ L) ^ 2)) := by850  have hap := agree_formula ε L851  have ha0 : 0 < (1 - 2 * ε) ^ L := by852    have hb : 0 < 1 - 2 * ε := by grind853    clear hsmall hap854    induction L with855    | zero => rw [Semiring.pow_zero]; exact OrderedRing.zero_lt_one856    | succ L ih => rw [Semiring.pow_succ]; exact OrderedRing.mul_pos ih hb857  have hle1 : (1 - 2 * ε) ^ L ≤ 1 := by858    have h1 := hsmall; have h2 := ha0859    generalize (1 - 2 * ε) ^ L = a at h1 h2 ⊢; grind860  refine ⟨fun m hm => ?_, fun m φ hφ h0 h1 => ?_⟩861  · rw [rep_expect ε false L m (detRule maj), rep_expect ε true L m (fun o => 1 - detRule maj o)]862    exact maj_upper (agree ε L) ((1 - 2 * ε) ^ L) hap ha0 hle1 m hm863  · rw [rep_expect ε false L m φ] at h0864    rw [rep_expect ε true L m (fun o => 1 - φ o)] at h1865    exact lower_bound (agree ε L) ((1 - 2 * ε) ^ L) hap ha0 hsmall m φ hφ h0 h1866867end Generic868869/-! ## The rational instantiation, tied to the phase-6 identities -/870871section RatInst872873open Prob874875theorem gs_rat {α : Type} (l : List α) (f : α → Rat) : gs l f = rsum l f := by876  induction l with877  | nil => rfl878  | cons a l ih => rw [gs_cons, rsum_cons, ih]879880/-- The law fw at R = ℚ is exactly the phase-6 weight Misc.bw. -/881theorem fw_rat (ε : Rat) : ∀ e, fw ε e = Misc.bw ε e882  | [] => rfl883  | b :: e => by simp only [fw, Misc.bw, fw_rat ε e]884885/-- Misc.bw IS a probability law on the domain 0 ≤ ε ≤ 1 (nonnegative, total mass 1), and886    the phase-6 agreement identity Misc.flip_agree is the event probability agree ε L. -/887theorem bw_probability (ε : Rat) (h0 : 0 ≤ ε) (h1 : ε ≤ 1) (L : Nat) :888    (∀ e, 0 ≤ Misc.bw ε e) ∧ rsum (bitvecs L) (Misc.bw ε) = 1 ∧889    agree ε L = rsum (bitvecs L) (fun e => Misc.bw ε e * (if par e then 0 else 1)) ∧890    agree ε L = (1 + (1 - 2 * ε) ^ L) / 2 := by891  have hag : agree ε L = rsum (bitvecs L) (fun e => Misc.bw ε e * (if par e then 0 else 1)) := by892    unfold agree prob; rw [gs_rat]; apply rsum_congr; intro e _893    rw [fw_rat]; simp only; cases par e <;> simp [ind]894  refine ⟨fun e => by rw [← fw_rat]; exact fw_nonneg h0 h1 e, ?_, hag, by rw [hag]; exact Misc.flip_agree ε L⟩895  rw [← gs_rat, show (Misc.bw ε) = fw ε by funext e; rw [fw_rat]]; exact fw_total ε L896897theorem q_bounds (q T : Rat) (hT : 0 < T) (c1 : 364 * T ≤ 1000 * (q * T)) (c2 : 10000 * (q * T) ≤ 3644 * T) :898    2 * q ≤ 1 ∧ 4 ≤ ((31 : Nat) : Rat) * q ^ 2 ∧ 364 ≤ 1000 * q ∧ 10000 * q ≤ 3644 := by899  have d1 : (364 : Rat) ≤ 1000 * q := by900    apply Rat.le_of_mul_le_mul_right _ hT901    have : 1000 * (q * T) = (1000 * q) * T := by grind902    rw [← this]; exact c1903  have d2 : 10000 * q ≤ (3644 : Rat) := by904    apply Rat.le_of_mul_le_mul_right _ hT905    have : 10000 * (q * T) = (10000 * q) * T := by grind906    rw [← this]; exact c2907  refine ⟨by grind, ?_, d1, d2⟩908  have := sq_le_sq' (R := Rat) (by grind : (0 : Rat) ≤ 364) d1909  have e31 : ((31 : Nat) : Rat) = 31 := by grind910  rw [e31]; grind911912/-- WORKED INSTANCE of the remark's numbers ε = 1/100, L = 50: a = (49/50)^50 lies in913    [0.364, 0.3644], the small-bias condition 2a ≤ 1 holds, 31·a² ≥ 4, and therefore 31914    fresh repetitions with the majority rule give both error probabilities ≤ 1/4 (errors915    computed on the error space of 31·50 independent flips). -/916theorem remark_instance :917    364 ≤ 1000 * (1 - 2 * (1 / 100 : Rat)) ^ 50 ∧ 10000 * (1 - 2 * (1 / 100 : Rat)) ^ 50 ≤ 3644 ∧918    2 * (1 - 2 * (1 / 100 : Rat)) ^ 50 ≤ 1 ∧919    4 ≤ ((31 : Nat) : Rat) * ((1 - 2 * (1 / 100 : Rat)) ^ 50) ^ 2 ∧920    4 * gs (bitvecs (31 * 50)) (fun e => fw (1 / 100 : Rat) e * detRule maj (obsOf false 50 31 e)) ≤ 1 ∧921    4 * gs (bitvecs (31 * 50)) (fun e => fw (1 / 100 : Rat) e * (1 - detRule maj (obsOf true 50 31 e))) ≤ 1 := by922  have e1 : (1 - 2 * (1 / 100 : Rat)) = ((49 : Nat) : Rat) / ((50 : Nat) : Rat) := by grind923  have hq := Misc.pow_frac 49 50 (by decide) 50924  obtain ⟨n1, n2⟩ := Misc.flip_example_nat925  have c1 : (364 : Rat) * ((50 : Nat) : Rat) ^ 50 ≤ 1000 * ((49 : Nat) : Rat) ^ 50 := by exact_mod_cast n1926  have c2 : (10000 : Rat) * ((49 : Nat) : Rat) ^ 50 ≤ 3644 * ((50 : Nat) : Rat) ^ 50 := by exact_mod_cast n2927  have hT : (0 : Rat) < ((50 : Nat) : Rat) ^ 50 := Rat.pow_pos (by decide)928  rw [← hq] at c1 c2929  obtain ⟨hsmall, hm, hlo, hhi⟩ := q_bounds _ _ hT c1 c2930  rw [← e1] at hsmall hm hlo hhi931  have hf := flip_order_inv_sq (R := Rat) (1 / 100) 50 (by grind) hsmall932  exact ⟨hlo, hhi, hsmall, hm, hf.1 31 hm⟩933934/-! ## Axiom audit -/935936#print axioms gs_nil937#print axioms gs_cons938#print axioms gs_append939#print axioms gs_map940#print axioms gs_congr941#print axioms gs_add942#print axioms gs_sub943#print axioms gs_mul_left944#print axioms gs_zero945#print axioms gs_le946#print axioms gs_nonneg947#print axioms gs_bitvecs_succ948#print axioms gs_bitvecs_add949#print axioms fw_nonneg950#print axioms fw_total951#print axioms fw_append952#print axioms fw_product953#print axioms fw_blocks954#print axioms getD_drop'955#print axioms gs_fw_one956#print axioms gs_fw_head957#print axioms fw_marginal958#print axioms fw_sign959#print axioms agree_formula960#print axioms observe_law961#print axioms one_pow'962#print axioms agree_edges963#print axioms ind_and964#print axioms repeated_law965#print axioms cnt_add966#print axioms detRule_rule967#print axioms chan_prod968#print axioms prodF_one969#print axioms chan_total970#print axioms chan_nonneg971#print axioms sum3972#print axioms dev_cons973#print axioms chan_moments974#print axioms sq_le_sq'975#print axioms cheb_point976#print axioms cheb977#print axioms nat_cast_nonneg'978#print axioms quarter_of_cheb979#print axioms maj_upper980#print axioms lr_mul981#print axioms chi_identity982#print axioms chiG_bias983#print axioms bernoulli_le984#print axioms sum3'985#print axioms err_sum986#print axioms sq_unit987#print axioms final_arith988#print axioms chi_ge_two989#print axioms samples_from_chi990#print axioms lower_bound_general991#print axioms lower_bound992#print axioms no_signal993#print axioms exact_channel994#print axioms order_inv_sq995#print axioms gs_comm996#print axioms gs_point997#print axioms obsOf_length998#print axioms rep_expect999#print axioms flip_order_inv_sq1000#print axioms gs_rat1001#print axioms fw_rat1002#print axioms bw_probability1003#print axioms q_bounds1004#print axioms remark_instance10051006end RatInst1007end Noise1008end NimAudit