Appendix F, paragraph 2The flip model gives a=(1−2ε)^L; small bias eventually; ε=0 or L=0 exact; a=0 hopeless; reuse gives nothing

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

1 Paper text

For the flip model, $a=(1-2\varepsilon)^L$ . Fresh independent blocks of $L$ flips produce exactly the product observation law used above. When $0<\varepsilon<1/2$ , the small-bias condition holds for every $L\ge\lceil1/(2\varepsilon)\rceil$ ; one elementary bound is $(1-2\varepsilon)^L\le(1+2\varepsilon L)^{-1}$ . If $\varepsilon=0$ or $L=0$ , one observation is exact. If $a=0$ , no number of observations permits error below $1/2$ for both ideal bits. Reusing the same corrupted bit leaves the information content unchanged. The finite product laws, real-parameter bounds, minimum sample count and these boundary cases are checked in Lean.

Generated from paper_jmlr.tex, lines 1625–1625.

2 Explain this

How the flip model of Remark 5.11 fits this setting, and its boundary cases:

with fresh independent blocks of $L$ flips, the observations follow exactly the channel law above with $a=(1-2\varepsilon)^L$ ;
for $0<\varepsilon<1/2$ the small-bias condition $a\le1/2$ holds for every $L\ge\lceil1/(2\varepsilon)\rceil$ ;
if $\varepsilon=0$ or $L=0$ , one observation is exact;
if $a=0$ , no number of observations gets both errors below $1/2$ ;
reusing the same corrupted bit adds no information.

3 How this is formalised

RealNoise.flip_repeated (fresh blocks give the product channel law), RealNoise.flip_mMin (the sufficient counts in flip space are exactly $m\ge m_*(a)$ ), RealNoise.eventually_small ( $(1-2\varepsilon)^L\le1/2$ for $L\ge\lceil1/(2\varepsilon)\rceil$ , via $(1-x)^L\le1/(1+Lx)$ ), RealNoise.flip_exact ( $\varepsilon=0$ or $L=0$ : $a=1$ and $m_*=1$ ), RealNoise.zero_signal_never ( $a=0$ : no $m$ suffices), Noise.no_signal ( $a=0$ : every rule has $\mathrm{err}_0+\mathrm{err}_1=1$ , so worst-case error at least $1/2$ ) and RealNoise.reuse_any_rule (with one reused block every rule has total error at least $1-a$ ).

Coverage record
Paper anchor	`app:noise-samples-p2` (website anchor; the manuscript has no label here)
Displayed as	Appendix F, paragraph 2
Claim	The flip model gives a=(1−2ε)^L; small bias eventually; ε=0 or L=0 exact; a=0 hopeless; reuse gives nothing
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1625–1625; SHA-256 of the normalised block source `1c8c7d52ef64b0b2…`
Lean declarations	`NimAudit.RealNoise.flip_repeated` (RealNoise, lines 265–268, file `ff2ca55835de…`) `NimAudit.RealNoise.flip_mMin` (RealNoise, lines 316–320, file `ff2ca55835de…`) `NimAudit.RealNoise.eventually_small` (RealNoise, lines 338–353, file `ff2ca55835de…`) `NimAudit.RealNoise.flip_exact` (RealNoise, lines 322–328, file `ff2ca55835de…`) `NimAudit.RealNoise.zero_signal_never` (RealNoise, lines 193–197, file `ff2ca55835de…`) `NimAudit.Noise.no_signal` (NoiseModel, lines 743–758, file `bde0a1ff2026…`) `NimAudit.RealNoise.reuse_any_rule` (RealNoise, lines 382–404, file `ff2ca55835de…`)
Audited correspondence rows	`app:noise-samples`
Explanations	`explain/c-flip-cases`, `formal/c-flip-cases`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

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.eventually_small`

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

THE SMALL-BIAS REGIME IS EVENTUALLY REACHED: for 0 < ε < 1/2, (1 − 2ε)^L ≤ 1/2 for every L ≥ ⌈1/(2ε)⌉₊ (via (1 − x)^L ≤ 1/(1 + Lx)).

Statement as elaborated and printed by Lean 4.26.0

∀ {ε : ℝ}, 0 < ε → ε < 1 / 2 → ∀ {L : ℕ}, ⌈1 / (2 * ε)⌉₊ ≤ L → (1 - 2 * ε) ^ L ≤ 1 / 2

Exact source text, lines 338–353

338/-- 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  nlinarith

Project declarations in the statement: none

Project declarations used by the proof or definition body

RealNoise.bernoulli_real

theorem `RealNoise.flip_exact`

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

ε = 0 or L = 0: exact observations (a = 1, one sample suffices and is needed).

Statement as elaborated and printed by Lean 4.26.0

∀ {ε : ℝ} {L : ℕ},
  ε = 0 ∨ L = 0 → (1 - 2 * ε) ^ L = 1 ∧ NimAudit.RealNoise.mMin ((1 - 2 * ε) ^ L) = 1

Exact source text, lines 322–328

322/-- ε = 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⟩

Project declarations in the statement: RealNoise.mMin

Project declarations used by the proof or definition body

RealNoise.mMin, RealNoise.mMin_one

theorem `RealNoise.zero_signal_never`

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

ZERO-SIGNAL BOUNDARY (a = 0, e.g. ε = 1/2 with L > 0): no sample count suffices.

Statement as elaborated and printed by Lean 4.26.0

∀ (m : ℕ), ¬NimAudit.RealNoise.Ach 0 m

Exact source text, lines 193–197

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

Project declarations in the statement: RealNoise.Ach

Project declarations used by the proof or definition body

Noise.Rule, Noise.err0, Noise.err1, Noise.no_signal, RealNoise.Ach, RealNoise.pOf

theorem `Noise.no_signal`

Module NoiseModel (lean/phase7/NoiseModel.lean, lines 743–758) · file SHA-256 bde0a1ff202682bd… Axioms reported by the fresh build: propext, Classical.choice, Quot.sound

NO SIGNAL (a = 0, e.g. ε = 1/2 with L > 0): the two hypotheses give the same law, so every rule has err₀ + err₁ = 1 and worst-case error at least 1/2.

Statement as elaborated and printed by Lean 4.26.0

∀ {R : Type} [inst : Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Grind.OrderedRing R] (p : R),
  2 * p = 1 →
    ∀ (m : ℕ) (φ : List Bool → R), NimAudit.Noise.err0 p m φ + NimAudit.Noise.err1 p m φ = 1

Exact source text, lines 743–758

743/-- 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]; grind

Project declarations in the statement: Noise.err0, Noise.err1

Project declarations used by the proof or definition body

Bridge.bitvecs, Noise.chanW, Noise.err0, Noise.err1, Noise.err_sum, Noise.gs, Noise.gs_zero

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

Definitions these statements use

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.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 `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.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.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 `RealNoise.Ach`

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

Some randomized rule on m samples has both errors ≤ 1/4.

Statement as elaborated and printed by Lean 4.26.0

ℝ → ℕ → Prop

Exact source text, lines 129–130

129/-- Some randomized rule on m samples has both errors ≤ 1/4. -/130def Ach (a : ℝ) (m : ℕ) : Prop := Achievable (pOf a) m

Project declarations in the statement: none

Project declarations used by the proof or definition body

Noise.Achievable, RealNoise.pOf

def `Noise.err0`

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

Error under Y = 0 (declaring 1) and under Y = 1 (declaring 0).

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 351–352

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

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs, Noise.chanW, Noise.gs

def `Noise.err1`

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

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 353–353

353def err1 (p : R) (m : Nat) (φ : List Bool → R) : R := gs (bitvecs m) (fun o => chanW p true o * (1 - φ o))

Project declarations in the statement: none

Project declarations used by the proof or definition body

Bridge.bitvecs, Noise.chanW, Noise.gs

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

Full modules

Module	File	Lines	Imports
BitBridge	`lean/phase3/BitBridge.lean`	560	Circuit
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).

Appendix F, paragraph 2The flip model gives a=(1−2ε)^L; small bias eventually; ε=0 or L=0 exact; a=0 hopeless; reuse gives nothing

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem RealNoise.flip_repeated

theorem RealNoise.flip_mMin

theorem RealNoise.eventually_small

theorem RealNoise.flip_exact

theorem RealNoise.zero_signal_never

theorem Noise.no_signal

theorem RealNoise.reuse_any_rule

Definitions these statements use

def Bridge.bitvecs

def Noise.agree

def Noise.chanW

def Noise.fw

def Noise.gs

def Noise.ind

def Noise.obsOf

def RealNoise.FlipAch

def RealNoise.mMin

def RealNoise.Ach

def Noise.err0

def Noise.err1

def Noise.Rule

def RealNoise.obsReuse

Full modules

theorem `RealNoise.flip_repeated`

theorem `RealNoise.flip_mMin`

theorem `RealNoise.eventually_small`

theorem `RealNoise.flip_exact`

theorem `RealNoise.zero_signal_never`

theorem `Noise.no_signal`

theorem `RealNoise.reuse_any_rule`

def `Bridge.bitvecs`

def `Noise.agree`

def `Noise.chanW`

def `Noise.fw`

def `Noise.gs`

def `Noise.ind`

def `Noise.obsOf`

def `RealNoise.FlipAch`

def `RealNoise.mMin`

def `RealNoise.Ach`

def `Noise.err0`

def `Noise.err1`

def `Noise.Rule`

def `RealNoise.obsReuse`