RealNoise

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 Mathlib.Data.Real.Archimedean2import Mathlib.Tactic.Linarith3import Mathlib.Tactic.Positivity4import Mathlib.Tactic.FieldSimp5import Mathlib.Tactic.NormNum6import Mathlib.Tactic.Ring7import Mathlib.Tactic.GCongr8import NoiseModel910/- Phase 8, part A: the noise model at Mathlib's real numbers, an explicit integer sample11   count, the minimum sample count and its two-sided a^{-2} bounds, and the flip model.12   Written by Claude (10 October 2026).  Lean 4.26.0 with Mathlib v4.26.0 (commit 2df2f01),13   imported read-only from the pinned phase-8 Lake dependency.1415   Paper target: Remark rem:noisy-rollout-decay.1617   A1  The phase-7 theorems are stated for any type with Lean core's ordered-field18       interface.  At ℝ the six interfaces are Mathlib's instances (Field.toGrindField,19       the IsStrictOrderedRing → Lean.Grind.OrderedRing instance, LinearOrder →20       Std.IsLinearOrder, Preorder → Std.LawfulOrderLT); the adapters below show that the21       interface operations ARE Mathlib's (casts, inverses, powers: by rfl) and that the22       generic finite sum is List.sum.  Every theorem here applies the phase-7 theorem at ℝ.23   A2  The symmetric channel with p = (1 + a)/2; the integer m(a) = ⌈4/a²⌉₊ (Mathlib's24       Nat.ceil, available because ℝ is Archimedean); majority (ties declared 0) succeeds25       at every m ≥ m(a); every randomized rule with both errors ≤ 1/4 needs 32·m·a² ≥ 3.26   A3  mMin a = the least m for which SOME randomized rule has both errors ≤ 1/4: it exists,27       is attained and is minimal, and 3/(32a²) ≤ mMin a ≤ ⌈4/a²⌉₊ < 4/a² + 1 ≤ 17/(4a²)28       for 0 < a ≤ 1/2 (a uniform Θ(a^{-2}) statement with explicit constants).29       Boundaries: a = 0 (no m works), a = 1 (mMin = 1), m = 0 never works.30   A4  The flip model at ℝ: product law, agreement formula, fresh-block repetition law,31       and the sample-size conclusions for a = (1 − 2ε)^L with 0 ≤ ε < 1/2 in the32       small-bias regime a ≤ 1/2, which holds for every L ≥ ⌈1/(2ε)⌉₊ when ε > 0.33       ε = 0 or L = 0 give a = 1 (exact observations).  Reusing one error block for all34       repetitions (no fresh randomness) gives NO improvement: majority error stays35       (1 − a)/2. -/3637namespace NimAudit38namespace RealNoise3940open Noise41open Bridge (bitvecs par mem_bitvecs_length mem_bitvecs_of_length)4243attribute [local instance] Lean.Grind.Semiring.natCast4445/-! ## A1. The real interfaces and adapters -/4647/-- The interface cast is Mathlib's cast. -/48theorem natCast_real (m : ℕ) : (@Nat.cast ℝ Lean.Grind.Semiring.natCast m) = (m : ℝ) := rfl4950/-- The interface inverse is Mathlib's inverse. -/51theorem inv_real (x : ℝ) : (@Inv.inv ℝ (Lean.Grind.Field.toInv) x) = x⁻¹ := rfl5253/-- The interface power (Lean.Grind.Semiring.npow, used in every generic statement) is54    Mathlib's monoid power. -/55theorem pow_real (x : ℝ) (n : ℕ) : @HPow.hPow ℝ ℕ ℝ (@Lean.Grind.Semiring.npow ℝ inferInstance) x n = x ^ n := rfl5657/-- The interface addition, multiplication and numerals are Mathlib's. -/58theorem add_mul_real (x y : ℝ) :59    @HAdd.hAdd ℝ ℝ ℝ (@instHAdd ℝ (@Lean.Grind.Semiring.toAdd ℝ inferInstance)) x y = x + y ∧60    @HMul.hMul ℝ ℝ ℝ (@instHMul ℝ (@Lean.Grind.Semiring.toMul ℝ inferInstance)) x y = x * y ∧61    @OfNat.ofNat ℝ 2 (@Lean.Grind.Semiring.ofNat ℝ inferInstance 2) = (2 : ℝ) := ⟨rfl, rfl, rfl⟩6263/-- The generic finite sum at ℝ is Mathlib's List.sum. -/64theorem gs_real {α : Type} (l : List α) (f : α → ℝ) : gs l f = (l.map f).sum := by65  induction l with66  | nil => rfl67  | cons a l ih => rw [gs_cons, ih, List.map_cons, List.sum_cons]6869/-! ## A2. The symmetric observation channel over ℝ -/7071/-- Agreement probability for signed bias a. -/72noncomputable def pOf (a : ℝ) : ℝ := (1 + a) / 27374theorem two_pOf (a : ℝ) : 2 * pOf a = 1 + a := by unfold pOf; ring7576theorem pOf_bounds {a : ℝ} (h0 : -1 ≤ a) (h1 : a ≤ 1) : 0 ≤ pOf a ∧ pOf a ≤ 1 := by77  unfold pOf; constructor <;> linarith7879/-- The m-sample channel law is a probability law (nonnegative, total mass 1). -/80theorem chan_law {a : ℝ} (h0 : -1 ≤ a) (h1 : a ≤ 1) (Y : Bool) (m : ℕ) :81    (∀ o, 0 ≤ chanW (pOf a) Y o) ∧ gs (bitvecs m) (chanW (pOf a) Y) = 1 :=82  ⟨chan_nonneg (pOf_bounds h0 h1).1 (pOf_bounds h0 h1).2 Y, chan_total _ Y m⟩8384/-- The explicit integer sample count m(a) = ⌈4/a²⌉₊. -/85noncomputable def mUp (a : ℝ) : ℕ := ⌈4 / a ^ 2⌉₊8687/-- THE ARCHIMEDEAN STEP: m(a)·a² ≥ 4 for every real a > 0. -/88theorem mUp_spec {a : ℝ} (ha : 0 < a) : 4 ≤ (mUp a : ℝ) * a ^ 2 := by89  have h1 : 4 / a ^ 2 ≤ (mUp a : ℝ) := Nat.le_ceil _90  have h2 : 0 < a ^ 2 := by positivity91  calc (4 : ℝ) = 4 / a ^ 2 * a ^ 2 := by field_simp92    _ ≤ (mUp a : ℝ) * a ^ 2 := by gcongr9394theorem archimedean_step {a : ℝ} (ha : 0 < a) : ∃ m : ℕ, 4 ≤ (m : ℝ) * a ^ 2 := ⟨mUp a, mUp_spec ha⟩9596theorem mUp_pos {a : ℝ} (ha : 0 < a) : 1 ≤ mUp a := by97  unfold mUp; rw [Nat.one_le_ceil_iff]; positivity9899theorem mUp_lt {a : ℝ} (ha : 0 < a) : (mUp a : ℝ) < 4 / a ^ 2 + 1 :=100  Nat.ceil_lt_add_one (by positivity)101102/-- With a ≤ 1/2 at least 16 samples are used. -/103theorem mUp_ge_16 {a : ℝ} (ha : 0 < a) (ha1 : a ≤ 1 / 2) : 16 ≤ mUp a := by104  have h1 : (16 : ℝ) ≤ 4 / a ^ 2 := by105    rw [le_div_iff₀ (by positivity)]; nlinarith106  have h2 : 4 / a ^ 2 ≤ (mUp a : ℝ) := Nat.le_ceil _107  exact_mod_cast le_trans h1 h2108109/-- A2 (UPPER BOUND, at ℝ): for 0 < a ≤ 1 the majority rule (ties declared 0) has both error110    probabilities at most 1/4 for EVERY m ≥ m(a), in particular at m = m(a). -/111theorem majority_succeeds {a : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1) {m : ℕ} (hm : mUp a ≤ m) :112    err0 (pOf a) m (detRule maj) ≤ 1 / 4 ∧ err1 (pOf a) m (detRule maj) ≤ 1 / 4 := by113  have hmm : 4 ≤ (m : ℝ) * a ^ 2 := by114    have := mUp_spec ha0115    have h' : (mUp a : ℝ) ≤ m := by exact_mod_cast hm116    nlinarith [sq_nonneg a]117  have h := maj_upper (R := ℝ) (pOf a) a (two_pOf a) ha0 ha1 m hmm118  constructor <;> linarith [h.1, h.2]119120/-- A2 (LOWER BOUND, at ℝ): for 0 < a ≤ 1/2, EVERY randomized rule (acceptance probability121    φ(o) ∈ [0,1]) with both errors ≤ 1/4 uses at least 3/(32a²) samples. -/122theorem any_rule_needs {a : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1 / 2) (m : ℕ) (φ : List Bool → ℝ) (hφ : Rule m φ)123    (h0 : err0 (pOf a) m φ ≤ 1 / 4) (h1 : err1 (pOf a) m φ ≤ 1 / 4) : 3 / (32 * a ^ 2) ≤ (m : ℝ) := by124  have h := lower_bound (R := ℝ) (pOf a) a (two_pOf a) ha0 (by linarith) m φ hφ (by linarith) (by linarith)125  rw [div_le_iff₀ (by positivity)]; linarith126127/-! ## A3. The minimum sufficient sample count -/128129/-- Some randomized rule on m samples has both errors ≤ 1/4. -/130def Ach (a : ℝ) (m : ℕ) : Prop := Achievable (pOf a) m131132theorem ach_of_ge {a : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1) {m : ℕ} (hm : mUp a ≤ m) : Ach a m := by133  obtain ⟨h0, h1⟩ := majority_succeeds ha0 ha1 hm134  exact ⟨detRule maj, detRule_rule m maj, by linarith, by linarith⟩135136theorem ach_exists {a : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1) : ∃ m, Ach a m := ⟨mUp a, ach_of_ge ha0 ha1 le_rfl⟩137138open Classical in139/-- The least sufficient natural sample count; by convention 0 when no m suffices (e.g. at140    a = 0, `zero_signal_never`).  Every theorem below assumes a > 0, where it exists. -/141noncomputable def mMin (a : ℝ) : ℕ := if h : ∃ m, Ach a m then Nat.find h else 0142143/-- EXISTENCE, ATTAINMENT AND MINIMALITY. -/144theorem mMin_spec {a : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1) :145    Ach a (mMin a) ∧ ∀ m, Ach a m → mMin a ≤ m := by146  classical147  have h := ach_exists ha0 ha1148  unfold mMin; rw [dif_pos h]149  exact ⟨Nat.find_spec h, fun m hm => Nat.find_min' h hm⟩150151/-- A3 TWO-SIDED BOUNDS: 3/(32a²) ≤ mMin a ≤ ⌈4/a²⌉₊ < 4/a² + 1. -/152theorem mMin_bounds {a : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1 / 2) :153    3 / (32 * a ^ 2) ≤ (mMin a : ℝ) ∧ mMin a ≤ mUp a ∧ (mUp a : ℝ) < 4 / a ^ 2 + 1 := by154  obtain ⟨hach, hmin⟩ := mMin_spec ha0 (by linarith)155  obtain ⟨φ, hφ, h0, h1⟩ := hach156  refine ⟨any_rule_needs ha0 ha1 _ φ hφ (by linarith) (by linarith), hmin _ (ach_of_ge ha0 (by linarith) le_rfl),157    mUp_lt ha0⟩158159/-- UNIFORM Θ(a^{-2}) WITH EXPLICIT CONSTANTS: for all 0 < a ≤ 1/2,160      (3/32)·a^{-2} ≤ mMin a ≤ (17/4)·a^{-2}. -/161theorem mMin_theta {a : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1 / 2) :162    3 / 32 * (a ^ 2)⁻¹ ≤ (mMin a : ℝ) ∧ (mMin a : ℝ) ≤ 17 / 4 * (a ^ 2)⁻¹ := by163  obtain ⟨h1, h2, h3⟩ := mMin_bounds ha0 ha1164  have hpos : 0 < a ^ 2 := by positivity165  have hsq : a ^ 2 ≤ 1 / 4 := by nlinarith166  constructor167  · calc 3 / 32 * (a ^ 2)⁻¹ = 3 / (32 * a ^ 2) := by field_simp168      _ ≤ _ := h1169  · have h2' : (mMin a : ℝ) ≤ mUp a := by exact_mod_cast h2170    have h4 : 4 / a ^ 2 + 1 ≤ 17 / 4 * (a ^ 2)⁻¹ := by171      rw [show 17 / 4 * (a ^ 2)⁻¹ = 4 / a ^ 2 + 1 / (4 * a ^ 2) by field_simp; ring]172      have : (1 : ℝ) ≤ 1 / (4 * a ^ 2) := by rw [le_div_iff₀ (by positivity)]; linarith173      linarith174    linarith175176/-- The same in product form: 3/32 ≤ mMin a · a² ≤ 17/4. -/177theorem mMin_scaled {a : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1 / 2) :178    3 / 32 ≤ (mMin a : ℝ) * a ^ 2 ∧ (mMin a : ℝ) * a ^ 2 ≤ 17 / 4 := by179  obtain ⟨h1, h2⟩ := mMin_theta ha0 ha1180  have hpos : 0 < a ^ 2 := by positivity181  constructor182  · have := mul_le_mul_of_nonneg_right h1 hpos.le183    rwa [mul_assoc, inv_mul_cancel₀ hpos.ne', mul_one] at this184  · have := mul_le_mul_of_nonneg_right h2 hpos.le185    rwa [mul_assoc, inv_mul_cancel₀ hpos.ne', mul_one] at this186187/-- Zero samples never suffice (a constant rule has err₀ + err₁ = 1). -/188theorem zero_samples_never (a : ℝ) : ¬ Ach a 0 := by189  rintro ⟨φ, _, h0, h1⟩190  simp only [err0, err1, bitvecs, gs_cons, gs_nil, chanW] at h0 h1191  linarith192193/-- ZERO-SIGNAL BOUNDARY (a = 0, e.g. ε = 1/2 with L > 0): no sample count suffices. -/194theorem zero_signal_never (m : ℕ) : ¬ Ach 0 m := by195  rintro ⟨φ, _, h0, h1⟩196  have := no_signal (R := ℝ) (pOf 0) (by unfold pOf; ring) m φ197  linarith198199/-- EXACT OBSERVATIONS (a = 1): one sample suffices and is necessary. -/200theorem mMin_one : mMin 1 = 1 := by201  obtain ⟨hach, hmin⟩ := mMin_spec (a := 1) one_pos le_rfl202  have h1 : Ach 1 1 := by203    have := exact_channel (R := ℝ)204    refine ⟨fun o => ind (o.getD 0 false), fun o _ => ⟨?_, ?_⟩, ?_, ?_⟩205    · show (0 : ℝ) ≤ ind (o.getD 0 false); unfold ind; split <;> norm_num206    · show ind (o.getD 0 false) ≤ (1 : ℝ); unfold ind; split <;> norm_num207    · rw [show pOf 1 = 1 by unfold pOf; norm_num, this.1]; norm_num208    · rw [show pOf 1 = 1 by unfold pOf; norm_num, this.2]; norm_num209  have hle := hmin 1 h1210  have hne : mMin 1 ≠ 0 := fun h => zero_samples_never 1 (h ▸ hach)211  omega212213/-- An extra sample can be ignored: achievability is monotone in m. -/214theorem err_succ (p : ℝ) (m : ℕ) (φ : List Bool → ℝ) :215    err0 p (m + 1) (fun o => φ o.tail) = err0 p m φ ∧ err1 p (m + 1) (fun o => φ o.tail) = err1 p m φ := by216  unfold err0 err1217  rw [gs_bitvecs_succ, gs_bitvecs_succ]218  have a1 : ∀ v, chanW p false (false :: v) * φ (false :: v).tail = p * (chanW p false v * φ v) := by219    intro v; simp only [chanW, List.tail_cons, if_true]; ring220  have a2 : ∀ v, chanW p false (true :: v) * φ (true :: v).tail = (1 - p) * (chanW p false v * φ v) := by221    intro v; simp only [chanW, List.tail_cons, Bool.true_eq_false, if_false]; ring222  have b1 : ∀ v, chanW p true (false :: v) * (1 - φ (false :: v).tail) = (1 - p) * (chanW p true v * (1 - φ v)) := by223    intro v; simp only [chanW, List.tail_cons, Bool.false_eq_true, if_false]; ring224  have b2 : ∀ v, chanW p true (true :: v) * (1 - φ (true :: v).tail) = p * (chanW p true v * (1 - φ v)) := by225    intro v; simp only [chanW, List.tail_cons, if_true]; ring226  rw [gs_congr (fun v _ => a1 v), gs_congr (fun v _ => a2 v), gs_congr (fun v _ => b1 v), gs_congr (fun v _ => b2 v),227    gs_mul_left, gs_mul_left, gs_mul_left, gs_mul_left]228  constructor <;> ring229230theorem ach_succ {a : ℝ} {m : ℕ} (h : Ach a m) : Ach a (m + 1) := by231  obtain ⟨φ, hφ, h0, h1⟩ := h232  obtain ⟨e0, e1⟩ := err_succ (pOf a) m φ233  refine ⟨fun o => φ o.tail, fun o ho => ?_, by rw [e0]; exact h0, by rw [e1]; exact h1⟩234  have hl := mem_bitvecs_length ho235  exact hφ o.tail (mem_bitvecs_of_length (by simp [hl]))236237theorem ach_mono {a : ℝ} {m m' : ℕ} (h : Ach a m) (hm : m ≤ m') : Ach a m' := by238  induction hm with239  | refl => exact h240  | step _ ih => exact ach_succ ih241242/-- THE SUFFICIENT COUNTS FORM A RAY: for a > 0, m samples suffice iff m ≥ mMin a. -/243theorem ach_iff_ge {a : ℝ} (ha0 : 0 < a) (ha1 : a ≤ 1) (m : ℕ) : Ach a m ↔ mMin a ≤ m :=244  ⟨fun h => (mMin_spec ha0 ha1).2 m h, fun h => ach_mono (mMin_spec ha0 ha1).1 h⟩245246/-! ## A4. The flip model at ℝ -/247248/-- The product Bernoulli(ε) law on {0,1}^L: nonnegative, total mass 1, marginals ε. -/249theorem flip_law {ε : ℝ} (h0 : 0 ≤ ε) (h1 : ε ≤ 1) (L : ℕ) :250    (∀ e, 0 ≤ fw ε e) ∧ gs (bitvecs L) (fw ε) = 1 ∧ ∀ i, i < L → prob ε L (fun e => e.getD i false) = ε :=251  ⟨fw_nonneg h0 h1, fw_total ε L, fun _ hi => fw_marginal ε hi⟩252253/-- Independence (product rule) for the flip law at ℝ. -/254theorem flip_independent (ε : ℝ) (f : ℕ → Bool → ℝ) (L k : ℕ) :255    gs (bitvecs L) (fun e => fw ε e * pf f k e) = pe ε f k L := fw_product ε f L k256257/-- The agreement formula of the remark, at ℝ. -/258theorem flip_agree_real (ε : ℝ) (L : ℕ) : agree ε L = (1 + (1 - 2 * ε) ^ L) / 2 := by259  have := agree_formula (R := ℝ) ε L260  linarith261262theorem agree_eq_pOf (ε : ℝ) (L : ℕ) : agree ε L = pOf ((1 - 2 * ε) ^ L) := by263  rw [flip_agree_real]; rfl264265/-- Fresh blocks: the m observations have the product channel law with p = agree ε L. -/266theorem flip_repeated (ε : ℝ) (Y : Bool) (L m : ℕ) (o : List Bool) (ho : o.length = m) :267    gs (bitvecs (m * L)) (fun e => fw ε e * ind (decide (obsOf Y L m e = o))) = chanW (agree ε L) Y o :=268  repeated_law ε Y L m o ho269270/-- The bias is positive for ε < 1/2. -/271theorem flip_bias_pos {ε : ℝ} (h1 : ε < 1 / 2) (L : ℕ) : 0 < (1 - 2 * ε) ^ L := by272  apply pow_pos; linarith273274/-- A4 SAMPLE SIZES FOR THE FLIP MODEL: for 0 ≤ ε < 1/2 and a = (1 − 2ε)^L ≤ 1/2, with errors275    computed on the space of m·L independent flips (fresh blocks):276      majority succeeds for every m ≥ ⌈4/a²⌉₊;  every randomized rule with both errors ≤ 1/4277      needs 32·m·a² ≥ 3;  and the minimum sufficient m satisfies the Θ(a^{-2}) bounds. -/278theorem flip_samples {ε : ℝ} (h1 : ε < 1 / 2) (L : ℕ) (hsmall : (1 - 2 * ε) ^ L ≤ 1 / 2) :279    (∀ m, mUp ((1 - 2 * ε) ^ L) ≤ m →280      gs (bitvecs (m * L)) (fun e => fw ε e * detRule maj (obsOf false L m e)) ≤ 1 / 4 ∧281      gs (bitvecs (m * L)) (fun e => fw ε e * (1 - detRule maj (obsOf true L m e))) ≤ 1 / 4) ∧282    (∀ (m : ℕ) (φ : List Bool → ℝ), Rule m φ →283      gs (bitvecs (m * L)) (fun e => fw ε e * φ (obsOf false L m e)) ≤ 1 / 4 →284      gs (bitvecs (m * L)) (fun e => fw ε e * (1 - φ (obsOf true L m e))) ≤ 1 / 4 →285      3 / (32 * ((1 - 2 * ε) ^ L) ^ 2) ≤ (m : ℝ)) ∧286    3 / 32 * (((1 - 2 * ε) ^ L) ^ 2)⁻¹ ≤ (mMin ((1 - 2 * ε) ^ L) : ℝ) ∧287    (mMin ((1 - 2 * ε) ^ L) : ℝ) ≤ 17 / 4 * (((1 - 2 * ε) ^ L) ^ 2)⁻¹ := by288  have ha0 := flip_bias_pos h1 L289  refine ⟨fun m hm => ?_, fun m φ hφ e0 e1 => ?_, (mMin_theta ha0 hsmall).1, (mMin_theta ha0 hsmall).2⟩290  · rw [rep_expect ε false L m (detRule maj), rep_expect ε true L m (fun o => 1 - detRule maj o), agree_eq_pOf]291    exact majority_succeeds ha0 (by linarith) hm292  · rw [rep_expect ε false L m φ, agree_eq_pOf] at e0293    rw [rep_expect ε true L m (fun o => 1 - φ o), agree_eq_pOf] at e1294    exact any_rule_needs ha0 hsmall m φ hφ e0 e1295296/-- Achievability with errors computed on the space of m·L independent flips (fresh blocks). -/297def FlipAch (ε : ℝ) (L m : ℕ) : Prop :=298  ∃ φ : List Bool → ℝ, Rule m φ ∧299    gs (bitvecs (m * L)) (fun e => fw ε e * φ (obsOf false L m e)) ≤ 1 / 4 ∧300    gs (bitvecs (m * L)) (fun e => fw ε e * (1 - φ (obsOf true L m e))) ≤ 1 / 4301302/-- The flip-space problem and the channel problem with a = (1 − 2ε)^L have the same303    achievable sample counts; so mMin a is also the minimum for the flip model. -/304theorem flipAch_iff (ε : ℝ) (L m : ℕ) : FlipAch ε L m ↔ Ach ((1 - 2 * ε) ^ L) m := by305  unfold FlipAch Ach Achievable306  constructor307  · rintro ⟨φ, hφ, h0, h1⟩308    rw [rep_expect ε false L m φ, agree_eq_pOf] at h0309    rw [rep_expect ε true L m (fun o => 1 - φ o), agree_eq_pOf] at h1310    exact ⟨φ, hφ, by unfold err0; linarith, by unfold err1; linarith⟩311  · rintro ⟨φ, hφ, h0, h1⟩312    refine ⟨φ, hφ, ?_, ?_⟩313    · rw [rep_expect ε false L m φ, agree_eq_pOf]; unfold err0 at h0; linarith314    · rw [rep_expect ε true L m (fun o => 1 - φ o), agree_eq_pOf]; unfold err1 at h1; linarith315316/-- For 0 ≤ ε < 1/2 the flip-space sample counts that suffice are exactly m ≥ mMin a. -/317theorem flip_mMin {ε : ℝ} (h0 : 0 ≤ ε) (h1 : ε < 1 / 2) (L m : ℕ) :318    FlipAch ε L m ↔ mMin ((1 - 2 * ε) ^ L) ≤ m := by319  rw [flipAch_iff]320  exact ach_iff_ge (flip_bias_pos h1 L) (pow_le_one₀ (by linarith) (by linarith)) m321322/-- ε = 0 or L = 0: exact observations (a = 1, one sample suffices and is needed). -/323theorem flip_exact {ε : ℝ} {L : ℕ} (h : ε = 0 ∨ L = 0) : (1 - 2 * ε) ^ L = 1 ∧ mMin ((1 - 2 * ε) ^ L) = 1 := by324  have e : (1 - 2 * ε) ^ L = 1 := by325    rcases h with rfl | rfl326    · simp327    · simp328  exact ⟨e, by rw [e]; exact mMin_one⟩329330theorem bernoulli_real {x : ℝ} (hx : 0 ≤ x) : ∀ n : ℕ, 1 + (n : ℝ) * x ≤ (1 + x) ^ n331  | 0 => by simp332  | n + 1 => by333    have ih := bernoulli_real hx n334    push_cast335    rw [pow_succ]336    nlinarith [mul_nonneg (Nat.cast_nonneg n : (0 : ℝ) ≤ n) (mul_nonneg hx hx)]337338/-- THE SMALL-BIAS REGIME IS EVENTUALLY REACHED: for 0 < ε < 1/2,339    (1 − 2ε)^L ≤ 1/2 for every L ≥ ⌈1/(2ε)⌉₊ (via (1 − x)^L ≤ 1/(1 + Lx)). -/340theorem eventually_small {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1 / 2) {L : ℕ} (hL : ⌈1 / (2 * ε)⌉₊ ≤ L) :341    (1 - 2 * ε) ^ L ≤ 1 / 2 := by342  set x := 2 * ε with hx343  have hx0 : 0 < x := by positivity344  have hx1 : x < 1 := by linarith345  have hLx : 1 ≤ (L : ℝ) * x := by346    have h' : 1 / x ≤ (L : ℝ) := le_trans (Nat.le_ceil _) (by exact_mod_cast hL)347    rw [div_le_iff₀ hx0] at h'; linarith348  have hb := bernoulli_real hx0.le L349  have hprod : (1 - x) ^ L * (1 + x) ^ L ≤ 1 := by350    rw [← mul_pow]; apply pow_le_one₀ <;> nlinarith351  have hpos : 0 ≤ (1 - x) ^ L := pow_nonneg (by linarith) L352  have h2 : 2 ≤ (1 + x) ^ L := by linarith353  nlinarith354355/-- NO FRESH RANDOMNESS, NO GAIN: if one error block e is reused for all m ≥ 1 repetitions356    (as when re-running the same deterministic rollout), the m observations are identical,357    majority returns the single observation, and its error stays (1 − a)/2. -/358def obsReuse (Y : Bool) (e : List Bool) (m : ℕ) : List Bool := List.replicate m (xor Y (par e))359360theorem cnt_true_replicate (b : Bool) : ∀ m : ℕ, cnt true (List.replicate m b) = if b then m else 0361  | 0 => by cases b <;> rfl362  | m + 1 => by363    simp only [List.replicate_succ, cnt, cnt_true_replicate b m]364    cases b <;> simp; omega365366theorem maj_replicate {m : ℕ} (hm : 1 ≤ m) (b : Bool) : maj (List.replicate m b) = b := by367  unfold maj368  rw [cnt_true_replicate, List.length_replicate]369  cases b <;> simp <;> omega370371theorem reuse_no_gain (ε : ℝ) (L : ℕ) {m : ℕ} (hm : 1 ≤ m) :372    gs (bitvecs L) (fun e => fw ε e * detRule maj (obsReuse false e m)) = (1 - (1 - 2 * ε) ^ L) / 2 := by373  have e1 : ∀ e, fw ε e * detRule maj (obsReuse false e m) = fw ε e - fw ε e * ind (!par e) := by374    intro e375    simp only [obsReuse, detRule, Bool.false_xor, maj_replicate hm]376    cases par e <;> simp [ind]377  rw [gs_congr (fun e _ => e1 e), gs_sub, fw_total]378  have := flip_agree_real ε L379  unfold agree prob at this380  rw [this]; ring381382/-- … and no rule does better: with one reused block, for EVERY m and every randomized rule,383    err₀ + err₁ ≥ 1 − a (a = (1 − 2ε)^L ≥ 0).  So for a < 1/2 no number of repetitions of the384    same randomness reaches error ≤ 1/4. -/385theorem reuse_any_rule {ε : ℝ} (hε : ε ≤ 1 / 2) (L m : ℕ) (φ : List Bool → ℝ) (hφ : Rule m φ) :386    1 - (1 - 2 * ε) ^ L ≤ gs (bitvecs L) (fun e => fw ε e * φ (obsReuse false e m)) +387      gs (bitvecs L) (fun e => fw ε e * (1 - φ (obsReuse true e m))) := by388  set u := φ (List.replicate m false)389  set v := φ (List.replicate m true)390  have hu := hφ _ (mem_bitvecs_of_length (List.length_replicate (n := m) (a := false)))391  have hv := hφ _ (mem_bitvecs_of_length (List.length_replicate (n := m) (a := true)))392  set A := gs (bitvecs L) (fun e => fw ε e * ind (!par e)) with hA393  have e0 : ∀ e, fw ε e * φ (obsReuse false e m) = u * (fw ε e * ind (!par e)) + v * (fw ε e - fw ε e * ind (!par e)) := by394    intro e; cases h : par e <;> simp [obsReuse, h, ind, u, v] <;> ring395  have e1 : ∀ e, fw ε e * (1 - φ (obsReuse true e m)) =396      (1 - v) * (fw ε e * ind (!par e)) + (1 - u) * (fw ε e - fw ε e * ind (!par e)) := by397    intro e; cases h : par e <;> simp [obsReuse, h, ind, u, v] <;> ring398  rw [gs_congr (fun e _ => e0 e), gs_congr (fun e _ => e1 e), gs_add, gs_add, gs_mul_left, gs_mul_left,399    gs_mul_left, gs_mul_left, gs_sub, fw_total, ← hA]400  have hag := flip_agree_real ε L401  unfold agree prob at hag402  rw [← hA] at hag403  have ha : 0 ≤ (1 - 2 * ε) ^ L := pow_nonneg (by linarith) L404  nlinarith [mul_nonneg ha (show 0 ≤ u - v + 1 by linarith [hu.1, hv.2])]405406theorem reuse_never {ε : ℝ} (hε : ε ≤ 1 / 2) {L : ℕ} (hsmall : (1 - 2 * ε) ^ L < 1 / 2) (m : ℕ)407    (φ : List Bool → ℝ) (hφ : Rule m φ) :408    ¬ (gs (bitvecs L) (fun e => fw ε e * φ (obsReuse false e m)) ≤ 1 / 4 ∧409      gs (bitvecs L) (fun e => fw ε e * (1 - φ (obsReuse true e m))) ≤ 1 / 4) := by410  rintro ⟨h0, h1⟩411  have := reuse_any_rule hε L m φ hφ412  linarith413414/-- THE REMARK'S NUMBERS AT ℝ: for ε = 1/100 and L = 50 the bias a = (1 − 2ε)^L satisfies415    0.364 ≤ a ≤ 0.3644 (so the small-bias condition a ≤ 1/2 holds); the explicit count is416    m(a) = ⌈4/a²⌉₊ = 31, so 31 fresh repetitions with majority give both errors ≤ 1/4, and417    1 ≤ mMin a ≤ 31.  (Optimality of 31 is not claimed.) -/418theorem remark_real :419    (0.364 : ℝ) ≤ (1 - 2 * (1 / 100)) ^ 50 ∧ ((1 - 2 * (1 / 100)) ^ 50 : ℝ) ≤ 0.3644 ∧420    mUp ((1 - 2 * (1 / 100)) ^ 50) = 31 ∧ 1 ≤ mMin ((1 - 2 * (1 / 100)) ^ 50) ∧421    mMin ((1 - 2 * (1 / 100)) ^ 50) ≤ 31 := by422  have hb : (0.364 : ℝ) ≤ (1 - 2 * (1 / 100)) ^ 50 ∧ ((1 - 2 * (1 / 100)) ^ 50 : ℝ) ≤ 0.3644 := by norm_num423  have ha0 : (0 : ℝ) < (1 - 2 * (1 / 100)) ^ 50 := by linarith [hb.1]424  have ha1 : ((1 - 2 * (1 / 100)) ^ 50 : ℝ) ≤ 1 / 2 := by linarith [hb.2]425  have h31 : mUp ((1 - 2 * (1 / 100)) ^ 50) = 31 := by426    unfold mUp427    rw [Nat.ceil_eq_iff (by norm_num)]428    constructor <;> norm_num429  obtain ⟨hach, hmin⟩ := mMin_spec ha0 (by linarith)430  have hle := (mMin_bounds ha0 ha1).2.1431  have hne : mMin ((1 - 2 * (1 / 100)) ^ 50) ≠ 0 := fun h => zero_samples_never _ (h ▸ hach)432  exact ⟨hb.1, hb.2, h31, by omega, by rw [h31] at hle; exact hle⟩433434/-! ## Axiom checks -/435#print axioms natCast_real436#print axioms inv_real437#print axioms pow_real438#print axioms add_mul_real439#print axioms gs_real440#print axioms two_pOf441#print axioms pOf_bounds442#print axioms chan_law443#print axioms mUp_spec444#print axioms archimedean_step445#print axioms mUp_pos446#print axioms mUp_lt447#print axioms mUp_ge_16448#print axioms majority_succeeds449#print axioms any_rule_needs450#print axioms ach_of_ge451#print axioms ach_exists452#print axioms mMin_spec453#print axioms mMin_bounds454#print axioms mMin_theta455#print axioms mMin_scaled456#print axioms zero_samples_never457#print axioms zero_signal_never458#print axioms err_succ459#print axioms ach_succ460#print axioms ach_mono461#print axioms ach_iff_ge462#print axioms mMin_one463#print axioms flip_law464#print axioms flip_independent465#print axioms flip_agree_real466#print axioms agree_eq_pOf467#print axioms flip_repeated468#print axioms flip_bias_pos469#print axioms flip_samples470#print axioms flipAch_iff471#print axioms flip_mMin472#print axioms flip_exact473#print axioms bernoulli_real474#print axioms eventually_small475#print axioms cnt_true_replicate476#print axioms maj_replicate477#print axioms reuse_no_gain478#print axioms reuse_any_rule479#print axioms reuse_never480#print axioms remark_real481482end RealNoise483end NimAudit