Remark 5.11Independent outcome flips: agreement (1+(1−2ε)^L)/2 and Θ(a⁻²) repetitions with fresh randomness

Checked theorem Lean checks a formal statement corresponding to this claim.

1 Paper text

Remark 5.11 (An illustrative independent outcome-flip model) Suppose an ideal terminal bit $Y$ is corrupted as $\widetilde Y=Y\oplus E_1\oplus\cdots\oplus E_L$ , where the $E_i$ are independent Bernoulli variables of parameter $0\le\varepsilon<1/2$ . Then $\Pr[\widetilde Y=Y]=\frac{1+(1-2\varepsilon)^L}{2}.$ The formula follows by multiplying the expectations of $(-1)^{E_i}$ . With fresh independent flips for each repetition, the least number of observations needed to distinguish the two possible ideal bits with worst-case error at most $1/4$ grows as $a^{-2}$ , where $a=(1-2\varepsilon)^L$ . Appendix F states and proves explicit bounds over real parameters. Repeating one corrupted observation with the same randomness supplies no additional information. At $\varepsilon=0.01$ and $L=50$ , agreement is approximately $0.682$ , so this example is not yet close to a fair coin. This is a channel-noise illustration, not a theorem about erroneous game moves: a move error need not flip the terminal bit, and can change later states and rollout length. Correlated flips can cancel in pairs, eliminating the claimed decay. Exact structured rollouts have no such noise.

Generated from paper_jmlr.tex, lines 770–779.

2 Explain this

The model. Suppose the ideal outcome bit $Y$ reaches us flipped by $L$ independent coin flips, each with probability $\varepsilon<1/2$ . The observed bit agrees with $Y$ with probability $(1+a)/2$ where $a=(1-2\varepsilon)^L$ : each flip multiplies the bias by $1-2\varepsilon$ .

Example. $\varepsilon=0.01$ , $L=50$ : $a\approx0.364$ and agreement $\approx0.682$ , far from a fair coin.

Repetitions. With fresh independent flips each time (and $0\le\varepsilon<1/2$ ), about $1/a^2$ observations are needed to decide $Y$ with error at most $1/4$ for each value of $Y$ . When $0<a\le1/2$ , every (possibly randomised) decision rule needs at least $3/(32a^2)$ observations, while majority vote achieves the target with at most $17/(4a^2)$ . These bounds therefore enclose the minimum sufficient sample count. In the example, 31 fresh repetitions with majority vote (ties declared $0$ ) suffice.

Caveats.

Repeating the same corrupted observation (same randomness) gives no new information.
Correlated flips can cancel in pairs, so the decay is not automatic.
This models noise on the outcome channel, not erroneous game moves: a wrong move need not flip the outcome and can change everything that follows. Exact structured rollouts have no noise at all.

3 How this is formalised

All statements are checked over Mathlib's real numbers.

The flip law: RealNoise.flip_law (product Bernoulli $(\varepsilon)$ law on $\{0,1\}^L$ : nonnegative, total mass $1$ , marginals $\varepsilon$ ) and RealNoise.flip_agree_real (agreement $(1+(1-2\varepsilon)^L)/2$ ).
Fresh repetitions: RealNoise.flip_repeated (with fresh blocks the $m$ observations have the product channel law) and RealNoise.flip_mMin (for $0\le\varepsilon<1/2$ exactly the counts $m\ge m_*(a)$ suffice).
Growth: RealNoise.mMin_theta: $\tfrac{3}{32}a^{-2}\le m_*(a)\le\tfrac{17}{4}a^{-2}$ for $0<a\le1/2$ . The lower bound applies to every randomised decision rule; majority vote establishes the upper bound.
Reuse: RealNoise.reuse_any_rule: with one reused error block, every rule has total error at least $1-a$ .
Numbers: Misc.flip_example ( $0.682\le$ agreement $\le0.6822$ ) and RealNoise.remark_real ( $0.364\le a\le0.3644$ , $\lceil4/a^2\rceil=31$ ; optimality of 31 is not claimed).
Correlated flips: Misc.paired_flips_cancel.

The precise sample-count statement is Proposition F.1.

Coverage record
Paper anchor	`rem:noisy-rollout-decay` (manuscript label)
Displayed as	Remark 5.11
Claim	Independent outcome flips: agreement (1+(1−2ε)^L)/2 and Θ(a⁻²) repetitions with fresh randomness
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 770–779; SHA-256 of the normalised block source `90ba4a3ec1e63642…`
Lean declarations	`NimAudit.RealNoise.flip_agree_real` (RealNoise, lines 257–260, file `ff2ca55835de…`) `NimAudit.RealNoise.flip_law` (RealNoise, lines 248–251, file `ff2ca55835de…`) `NimAudit.RealNoise.flip_repeated` (RealNoise, lines 265–268, file `ff2ca55835de…`) `NimAudit.RealNoise.flip_mMin` (RealNoise, lines 316–320, file `ff2ca55835de…`) `NimAudit.RealNoise.mMin_theta` (RealNoise, lines 159–174, file `ff2ca55835de…`) `NimAudit.RealNoise.reuse_any_rule` (RealNoise, lines 382–404, file `ff2ca55835de…`) `NimAudit.RealNoise.remark_real` (RealNoise, lines 414–432, file `ff2ca55835de…`) `NimAudit.Misc.flip_example` (Misc, lines 786–822, file `07766c03566d…`) `NimAudit.Misc.paired_flips_cancel` (Misc, lines 572–576, file `07766c03566d…`)
Assumptions and domain	$0\le\varepsilon<1/2$ ; flips independent within a block and fresh for each repetition; worst-case error at most $1/4$ for both values of the ideal bit; for the explicit bounds $0<a\le1/2$ .
Prose-to-formal notes	This is a channel-noise model. Lean does not model erroneous game moves or learned heads, and neither does the remark.
Depends on	Proposition F.1
Audited correspondence rows	`rem:noisy-rollout-decay`
Explanations	`explain/rem:noisy-rollout-decay`, `formal/rem:noisy-rollout-decay`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

theorem `RealNoise.flip_agree_real`

Module RealNoise (lean/phase8/RealNoise.lean, lines 257–260) · file SHA-256 ff2ca55835deab85… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

The agreement formula of the remark, at ℝ.

Statement as elaborated and printed by Lean 4.26.0

∀ (ε : ℝ) (L : ℕ), NimAudit.Noise.agree ε L = (1 + (1 - 2 * ε) ^ L) / 2

Exact source text, lines 257–260

257/-- 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  linarith

Project declarations in the statement: Noise.agree

Project declarations used by the proof or definition body

Noise.agree, Noise.agree_formula

theorem `RealNoise.flip_law`

Module RealNoise (lean/phase8/RealNoise.lean, lines 248–251) · file SHA-256 ff2ca55835deab85… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

The product Bernoulli(ε) law on {0,1}^L: nonnegative, total mass 1, marginals ε.

Statement as elaborated and printed by Lean 4.26.0

∀ {ε : ℝ},
  0 ≤ ε →
    ε ≤ 1 →
      ∀ (L : ℕ),
        (∀ (e : List Bool), 0 ≤ NimAudit.Noise.fw ε e) ∧
          NimAudit.Noise.gs (NimAudit.Bridge.bitvecs L) (NimAudit.Noise.fw ε) = 1 ∧
            ∀ i < L, (NimAudit.Noise.prob ε L fun e => e.getD i false) = ε

Exact source text, lines 248–251

248/-- 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⟩

Project declarations in the statement: Bridge.bitvecs, Noise.fw, Noise.gs, Noise.prob

Project declarations used by the proof or definition body

Bridge.bitvecs, Noise.fw, Noise.fw_marginal, Noise.fw_nonneg, Noise.fw_total, Noise.gs, Noise.prob

theorem `RealNoise.flip_repeated`

Module RealNoise (lean/phase8/RealNoise.lean, lines 265–268) · file SHA-256 ff2ca55835deab85… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

Fresh blocks: the m observations have the product channel law with p = agree ε L.

Statement as elaborated and printed by Lean 4.26.0

∀ (ε : ℝ) (Y : Bool) (L m : ℕ) (o : List Bool),
  o.length = m →
    (NimAudit.Noise.gs (NimAudit.Bridge.bitvecs (m * L)) fun e =>
        NimAudit.Noise.fw ε e * NimAudit.Noise.ind (decide (NimAudit.Noise.obsOf Y L m e = o))) =
      NimAudit.Noise.chanW (NimAudit.Noise.agree ε L) Y o

Exact source text, lines 265–268

265/-- 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 ho

Project declarations in the statement: Bridge.bitvecs, Noise.agree, Noise.chanW, Noise.fw, Noise.gs, Noise.ind, Noise.obsOf

Project declarations used by the proof or definition body

Noise.repeated_law

theorem `RealNoise.flip_mMin`

Module RealNoise (lean/phase8/RealNoise.lean, lines 316–320) · file SHA-256 ff2ca55835deab85… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

For 0 ≤ ε < 1/2 the flip-space sample counts that suffice are exactly m ≥ mMin a.

Statement as elaborated and printed by Lean 4.26.0

∀ {ε : ℝ},
  0 ≤ ε →
    ε < 1 / 2 →
      ∀ (L m : ℕ), NimAudit.RealNoise.FlipAch ε L m ↔ NimAudit.RealNoise.mMin ((1 - 2 * ε) ^ L) ≤ m

Exact source text, lines 316–320

316/-- 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)) m

Project declarations in the statement: RealNoise.FlipAch, RealNoise.mMin

Project declarations used by the proof or definition body

RealNoise.Ach, RealNoise.FlipAch, RealNoise.ach_iff_ge, RealNoise.flipAch_iff, RealNoise.flip_bias_pos, RealNoise.mMin

theorem `RealNoise.mMin_theta`

Module RealNoise (lean/phase8/RealNoise.lean, lines 159–174) · file SHA-256 ff2ca55835deab85… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

UNIFORM Θ(a^{-2}) WITH EXPLICIT CONSTANTS: for all 0 < a ≤ 1/2, (3/32)·a^{-2} ≤ mMin a ≤ (17/4)·a^{-2}.

Statement as elaborated and printed by Lean 4.26.0

∀ {a : ℝ},
  0 < a →
    a ≤ 1 / 2 →
      3 / 32 * (a ^ 2)⁻¹ ≤ ↑(NimAudit.RealNoise.mMin a) ∧
        ↑(NimAudit.RealNoise.mMin a) ≤ 17 / 4 * (a ^ 2)⁻¹

Exact source text, lines 159–174

159/-- 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    linarith

Project declarations in the statement: RealNoise.mMin

Project declarations used by the proof or definition body

RealNoise.mMin, RealNoise.mMin_bounds, RealNoise.mUp

theorem `RealNoise.reuse_any_rule`

Module RealNoise (lean/phase8/RealNoise.lean, lines 382–404) · file SHA-256 ff2ca55835deab85… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

… and no rule does better: with one reused block, for EVERY m and every randomized rule, err₀ + err₁ ≥ 1 − a (a = (1 − 2ε)^L ≥ 0). So for a < 1/2 no number of repetitions of the same randomness reaches error ≤ 1/4.

Statement as elaborated and printed by Lean 4.26.0

∀ {ε : ℝ},
  ε ≤ 1 / 2 →
    ∀ (L m : ℕ) (φ : List Bool → ℝ),
      NimAudit.Noise.Rule m φ →
        1 - (1 - 2 * ε) ^ L ≤
          (NimAudit.Noise.gs (NimAudit.Bridge.bitvecs L) fun e =>
              NimAudit.Noise.fw ε e * φ (NimAudit.RealNoise.obsReuse false e m)) +
            NimAudit.Noise.gs (NimAudit.Bridge.bitvecs L) fun e =>
              NimAudit.Noise.fw ε e * (1 - φ (NimAudit.RealNoise.obsReuse true e m))

Exact source text, lines 382–404

382/-- … 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])]

Project declarations in the statement: Bridge.bitvecs, Noise.Rule, Noise.fw, Noise.gs, RealNoise.obsReuse

Project declarations used by the proof or definition body

Bridge.bitvecs, Bridge.mem_bitvecs_of_length, Bridge.par, Noise.Rule, Noise.agree, Noise.fw, Noise.fw_total, Noise.gs, Noise.gs_add, Noise.gs_congr, Noise.gs_mul_left, Noise.gs_sub, Noise.ind, RealNoise.flip_agree_real, RealNoise.obsReuse

theorem `RealNoise.remark_real`

Module RealNoise (lean/phase8/RealNoise.lean, lines 414–432) · file SHA-256 ff2ca55835deab85… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

THE REMARK'S NUMBERS AT ℝ: for ε = 1/100 and L = 50 the bias a = (1 − 2ε)^L satisfies 0.364 ≤ a ≤ 0.3644 (so the small-bias condition a ≤ 1/2 holds); the explicit count is m(a) = ⌈4/a²⌉₊ = 31, so 31 fresh repetitions with majority give both errors ≤ 1/4, and 1 ≤ mMin a ≤ 31. (Optimality of 31 is not claimed.)

Statement as elaborated and printed by Lean 4.26.0

0.364 ≤ (1 - 2 * (1 / 100)) ^ 50 ∧
  (1 - 2 * (1 / 100)) ^ 50 ≤ 0.3644 ∧
    NimAudit.RealNoise.mUp ((1 - 2 * (1 / 100)) ^ 50) = 31 ∧
      1 ≤ NimAudit.RealNoise.mMin ((1 - 2 * (1 / 100)) ^ 50) ∧
        NimAudit.RealNoise.mMin ((1 - 2 * (1 / 100)) ^ 50) ≤ 31

Exact source text, lines 414–432

414/-- 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⟩

Project declarations in the statement: RealNoise.mMin, RealNoise.mUp

Project declarations used by the proof or definition body

RealNoise.Ach, RealNoise.mMin, RealNoise.mMin_bounds, RealNoise.mMin_spec, RealNoise.mUp, RealNoise.zero_samples_never

theorem `Misc.flip_example`

Module Misc (lean/phase6/Misc.lean, lines 786–822) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

NUMERICAL EXAMPLE of Remark rem:noisy-rollout-decay: for ε = 1/100 and L = 50 the agreement probability lies between 0.682 and 0.6822.

Statement as elaborated and printed by Lean 4.26.0

682 / 1000 ≤ (1 + (1 - 2 * (1 / 100)) ^ 50) / 2 ∧ (1 + (1 - 2 * (1 / 100)) ^ 50) / 2 ≤ 6822 / 10000

Exact source text, lines 786–822

786/-- NUMERICAL EXAMPLE of Remark rem:noisy-rollout-decay: for ε = 1/100 and L = 50 the787    agreement probability lies between 0.682 and 0.6822. -/788theorem flip_example :789    (682 / 1000 : Rat) ≤ (1 + (1 - 2 * (1 / 100 : Rat)) ^ 50) / 2 ∧790    (1 + (1 - 2 * (1 / 100 : Rat)) ^ 50) / 2 ≤ 6822 / 10000 := by791  have e1 : (1 - 2 * (1 / 100 : Rat)) = ((49 : Nat) : Rat) / ((50 : Nat) : Rat) := by grind792  rw [e1]793  have hq := pow_frac 49 50 (by decide) 50794  generalize (((49 : Nat) : Rat) / ((50 : Nat) : Rat)) ^ 50 = q at hq ⊢795  have hT : (0 : Rat) < ((50 : Nat) : Rat) ^ 50 := Rat.pow_pos (by decide)796  obtain ⟨n1, n2⟩ := flip_example_nat797  have c1 : (364 : Rat) * ((50 : Nat) : Rat) ^ 50 ≤ 1000 * ((49 : Nat) : Rat) ^ 50 := by exact_mod_cast n1798  have c2 : (10000 : Rat) * ((49 : Nat) : Rat) ^ 50 ≤ 3644 * ((50 : Nat) : Rat) ^ 50 := by exact_mod_cast n2799  rw [← hq] at c1 c2800  generalize ((50 : Nat) : Rat) ^ 50 = T at hT c1 c2801  have d1 : (364 : Rat) ≤ 1000 * q := by802    apply Rat.le_of_mul_le_mul_right _ hT803    have : 1000 * (q * T) = (1000 * q) * T := by grind804    rw [← this]; exact c1805  have d2 : 10000 * q ≤ (3644 : Rat) := by806    apply Rat.le_of_mul_le_mul_right _ hT807    have : 10000 * (q * T) = (10000 * q) * T := by grind808    rw [← this]; exact c2809  have two : (0 : Rat) < 2 := by decide810  constructor811  · have ea : (682 / 1000 : Rat) = (1364 / 1000) / 2 := by grind812    rw [ea]813    apply div_le_div_of_le two814    apply le_div_of_mul_le (by decide)815    have : (1 + q) * 1000 = 1000 + 1000 * q := by grind816    rw [this]; grind817  · have eb : (6822 / 10000 : Rat) = (13644 / 10000) / 2 := by grind818    rw [eb]819    apply div_le_div_of_le two820    apply le_div_of_mul_le' (by decide)821    have : (1 + q) * 10000 = 10000 + 10000 * q := by grind822    rw [this]; grind

Project declarations in the statement: none

Project declarations used by the proof or definition body

Misc.flip_example_nat, Misc.le_div_of_mul_le', Misc.pow_frac, Prob.div_le_div_of_le, Prob.le_div_of_mul_le

theorem `Misc.paired_flips_cancel`

Module Misc (lean/phase6/Misc.lean, lines 572–576) · file SHA-256 07766c03566dbfca… Axioms reported by the fresh build: propext

CORRELATED FLIPS CAN CANCEL (Remark rem:noisy-rollout-decay): if the flips come in identical pairs, their XOR is always 0, so the observed bit always equals Y and there is no decay, whatever the flip probability.

Statement as elaborated and printed by Lean 4.26.0

∀ (Y : Bool) (e : List Bool), (Y ^^ NimAudit.Bridge.par (e ++ e)) = Y

Exact source text, lines 572–576

572/-- CORRELATED FLIPS CAN CANCEL (Remark rem:noisy-rollout-decay): if the flips come in573    identical pairs, their XOR is always 0, so the observed bit always equals Y and there574    is no decay, whatever the flip probability. -/575theorem paired_flips_cancel (Y : Bool) (e : List Bool) : xor Y (par (e ++ e)) = Y := by576  rw [par_append]; cases par e <;> simp

Project declarations in the statement: Bridge.par

Project declarations used by the proof or definition body

Bridge.par, Misc.par_append

Definitions these statements use

def `Noise.agree`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 239–240) · file SHA-256 bde0a1ff202682bd…

Probability that the observed bit Y ⊕ E₁ ⊕ … ⊕ E_L equals the ideal bit Y.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → R → ℕ → R

Exact source text, lines 239–240

239/-- 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)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.par, Noise.prob

def `Bridge.bitvecs`

Module BitBridge (lean/phase3/BitBridge.lean, lines 27–29) · file SHA-256 000644dc271d27f9…

Statement as elaborated and printed by Lean 4.26.0

ℕ → List (List Bool)

Exact source text, lines 27–29

27def bitvecs : Nat → List (List Bool)28  | 0 => [[]]29  | n + 1 => (bitvecs n).map (false :: ·) ++ (bitvecs n).map (true :: ·)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Noise.fw`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 118–121) · file SHA-256 bde0a1ff202682bd…

Weight of an error pattern e ∈ {0,1}^L: ∏ (ε if Eᵢ = 1, 1 − ε if Eᵢ = 0).

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → R → List Bool → R

Exact source text, lines 118–121

118/-- 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 ε e

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Noise.gs`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 48–49) · file SHA-256 bde0a1ff202682bd…

Finite sum Σ_{a ∈ l} f a.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → {α : Type} → List α → (α → R) → R

Exact source text, lines 48–49

48/-- Finite sum Σ_{a ∈ l} f a. -/49def gs {α : Type} (l : List α) (f : α → R) : R := l.foldr (fun a s => f a + s) 0

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Noise.prob`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 192–193) · file SHA-256 bde0a1ff202682bd…

Probability of an event A ⊆ {0,1}^L under the flip law.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → R → ℕ → (List Bool → Bool) → R

Exact source text, lines 192–193

192/-- 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))

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs, Noise.fw, Noise.gs, Noise.ind

def `Noise.chanW`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 291–294) · file SHA-256 bde0a1ff202682bd…

The m-sample symmetric channel law: each sample equals Y with probability p.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → R → Bool → List Bool → R

Exact source text, lines 291–294

291/-- 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 o

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Noise.ind`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 189–190) · file SHA-256 bde0a1ff202682bd…

Indicator of a Boolean in R.

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → Bool → R

Exact source text, lines 189–190

189/-- Indicator of a Boolean in R. -/190def ind (b : Bool) : R := if b then 1 else 0

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Noise.obsOf`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 286–289) · file SHA-256 bde0a1ff202682bd…

The observations of m repetitions, each using its own block of L error bits.

Statement as elaborated and printed by Lean 4.26.0

Bool → ℕ → ℕ → List Bool → List Bool

Exact source text, lines 286–289

286/-- 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)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.par

def `RealNoise.FlipAch`

Module RealNoise (lean/phase8/RealNoise.lean, lines 296–300) · file SHA-256 ff2ca55835deab85…

Achievability with errors computed on the space of m·L independent flips (fresh blocks).

Statement as elaborated and printed by Lean 4.26.0

ℝ → ℕ → ℕ → Prop

Exact source text, lines 296–300

296/-- 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 / 4

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs, Noise.Rule, Noise.fw, Noise.gs, Noise.obsOf

def `RealNoise.mMin`

Module RealNoise (lean/phase8/RealNoise.lean, lines 139–141) · file SHA-256 ff2ca55835deab85…

The least sufficient natural sample count; by convention 0 when no m suffices (e.g. at a = 0, `zero_signal_never`). Every theorem below assumes a > 0, where it exists.

Statement as elaborated and printed by Lean 4.26.0

ℝ → ℕ

Exact source text, lines 139–141

139/-- 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 0

Project declarations in the statement: none

Project declarations used by the proof or definition body

RealNoise.Ach

def `Noise.Rule`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 341–343) · file SHA-256 bde0a1ff202682bd…

A RANDOMIZED decision rule on m observations: φ o ∈ [0,1] is the probability of declaring Y = 1. Deterministic rules are the {0,1}-valued ones (detRule).

Statement as elaborated and printed by Lean 4.26.0

{R : Type} → [Grind.Field R] → [LE R] → ℕ → (List Bool → R) → Prop

Exact source text, lines 341–343

341/-- 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 ≤ 1

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs

def `RealNoise.obsReuse`

Module RealNoise (lean/phase8/RealNoise.lean, lines 355–358) · file SHA-256 ff2ca55835deab85…

NO FRESH RANDOMNESS, NO GAIN: if one error block e is reused for all m ≥ 1 repetitions (as when re-running the same deterministic rollout), the m observations are identical, majority returns the single observation, and its error stays (1 − a)/2.

Statement as elaborated and printed by Lean 4.26.0

Bool → List Bool → ℕ → List Bool

Exact source text, lines 355–358

355/-- 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))

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.par

def `RealNoise.mUp`

Module RealNoise (lean/phase8/RealNoise.lean, lines 84–85) · file SHA-256 ff2ca55835deab85…

The explicit integer sample count m(a) = ⌈4/a²⌉₊.

Statement as elaborated and printed by Lean 4.26.0

ℝ → ℕ

Exact source text, lines 84–85

84/-- The explicit integer sample count m(a) = ⌈4/a²⌉₊. -/85noncomputable def mUp (a : ℝ) : ℕ := ⌈4 / a ^ 2⌉₊

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

def `Bridge.par`

Module BitBridge (lean/phase3/BitBridge.lean, lines 348–351) · file SHA-256 000644dc271d27f9…

Parity of all bits.

Statement as elaborated and printed by Lean 4.26.0

List Bool → Bool

Exact source text, lines 348–351

348/-- Parity of all bits. -/349def par : List Bool → Bool350  | [] => false351  | b :: bs => xor b (par bs)

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

Full modules

Module	File	Lines	Imports
BitBridge	`lean/phase3/BitBridge.lean`	560	Circuit
Misc	`lean/phase6/Misc.lean`	912	Bypass
NoiseModel	`lean/phase7/NoiseModel.lean`	1008	Misc
RealNoise	`lean/phase8/RealNoise.lean`	483	`Mathlib.Data.Real.Archimedean`, `Mathlib.Tactic.Linarith`, `Mathlib.Tactic.Positivity`, `Mathlib.Tactic.FieldSimp`, `Mathlib.Tactic.NormNum`, `Mathlib.Tactic.Ring`, `Mathlib.Tactic.GCongr`, NoiseModel

Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).

Remark 5.11Independent outcome flips: agreement (1+(1−2ε)^L)/2 and Θ(a⁻²) repetitions with fresh randomness

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem RealNoise.flip_agree_real

theorem RealNoise.flip_law

theorem RealNoise.flip_repeated

theorem RealNoise.flip_mMin

theorem RealNoise.mMin_theta

theorem RealNoise.reuse_any_rule

theorem RealNoise.remark_real

theorem Misc.flip_example

theorem Misc.paired_flips_cancel

Definitions these statements use

def Noise.agree

def Bridge.bitvecs

def Noise.fw

def Noise.gs

def Noise.prob

def Noise.chanW

def Noise.ind

def Noise.obsOf

def RealNoise.FlipAch

def RealNoise.mMin

def Noise.Rule

def RealNoise.obsReuse

def RealNoise.mUp

def Bridge.par

Full modules

theorem `RealNoise.flip_agree_real`

theorem `RealNoise.flip_law`

theorem `RealNoise.flip_repeated`

theorem `RealNoise.flip_mMin`

theorem `RealNoise.mMin_theta`

theorem `RealNoise.reuse_any_rule`

theorem `RealNoise.remark_real`

theorem `Misc.flip_example`

theorem `Misc.paired_flips_cancel`

def `Noise.agree`

def `Bridge.bitvecs`

def `Noise.fw`

def `Noise.gs`

def `Noise.prob`

def `Noise.chanW`

def `Noise.ind`

def `Noise.obsOf`

def `RealNoise.FlipAch`

def `RealNoise.mMin`

def `Noise.Rule`

def `RealNoise.obsReuse`

def `RealNoise.mUp`

def `Bridge.par`