Appendix F, paragraph 1Symmetric channel with agreement (1+a)/2; m*(a) is the least sample count with both errors ≤ 1/4

Checked definition or construction Lean contains the definition or construction, with checked properties.

1 Paper text

Remark 5.11 concerns a symmetric observation channel for an unknown bit $Y$ . Each observation agrees with $Y$ with probability $(1+a)/2$ , where $0<a\le1/2$ , and observations are independent conditional on $Y$ . A possibly randomised decision rule assigns a probability of outputting 1 to each observed bit vector. Let $m_*(a)$ be the least sample count for which such a rule has error at most $1/4$ for each possible value of $Y$ .

Generated from paper_jmlr.tex, lines 1605–1605.

2 Explain this

The appendix's setting: an unknown bit $Y$ is observed through a symmetric channel; each observation agrees with $Y$ with probability $(1+a)/2$ , and observations are independent given $Y$ . A decision rule (possibly randomised) maps the observed bits to a guess. $m_*(a)$ is the least number of observations for which some rule has error at most $1/4$ for each value of $Y$ .

3 How this is formalised

RealNoise.pOf is the agreement probability $(1+a)/2$ ; RealNoise.chan_law proves that the $m$ -sample channel law is a probability law; RealNoise.Ach $a\ m$ says some randomised rule on $m$ samples has both errors at most $1/4$ ; RealNoise.mMin is the least such $m$ (by convention $0$ when none exists). RealNoise.mMin_spec: for $0<a\le1$ the minimum exists, is attained and is minimal.

Coverage record
Paper anchor	`app:noise-samples-p1` (website anchor; the manuscript has no label here)
Displayed as	Appendix F, paragraph 1
Claim	Symmetric channel with agreement (1+a)/2; m*(a) is the least sample count with both errors ≤ 1/4
Coverage category	Checked definition or construction
Statement source	paper_jmlr.tex lines 1605–1605; SHA-256 of the normalised block source `58e52d25b7c88cb1…`
Lean declarations	`NimAudit.RealNoise.pOf` (RealNoise, lines 71–72, file `ff2ca55835de…`) `NimAudit.RealNoise.chan_law` (RealNoise, lines 79–82, file `ff2ca55835de…`) `NimAudit.RealNoise.Ach` (RealNoise, lines 129–130, file `ff2ca55835de…`) `NimAudit.RealNoise.mMin` (RealNoise, lines 139–141, file `ff2ca55835de…`) `NimAudit.RealNoise.mMin_spec` (RealNoise, lines 143–149, file `ff2ca55835de…`)
Audited correspondence rows	`app:noise-samples`
Explanations	`explain/c-noise-model`, `formal/c-noise-model`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

def `RealNoise.pOf`

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

Agreement probability for signed bias a.

Statement as elaborated and printed by Lean 4.26.0

ℝ → ℝ

Exact source text, lines 71–72

71/-- Agreement probability for signed bias a. -/72noncomputable def pOf (a : ℝ) : ℝ := (1 + a) / 2

Project declarations in the statement: none

Project declarations used by the proof or definition body

none

theorem `RealNoise.chan_law`

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

The m-sample channel law is a probability law (nonnegative, total mass 1).

Statement as elaborated and printed by Lean 4.26.0

∀ {a : ℝ},
  -1 ≤ a →
    a ≤ 1 →
      ∀ (Y : Bool) (m : ℕ),
        (∀ (o : List Bool), 0 ≤ NimAudit.Noise.chanW (NimAudit.RealNoise.pOf a) Y o) ∧
          NimAudit.Noise.gs (NimAudit.Bridge.bitvecs m)
              (NimAudit.Noise.chanW (NimAudit.RealNoise.pOf a) Y) =
            1

Exact source text, lines 79–82

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

Project declarations in the statement: Bridge.bitvecs, Noise.chanW, Noise.gs, RealNoise.pOf

Project declarations used by the proof or definition body

Bridge.bitvecs, Noise.chanW, Noise.chan_nonneg, Noise.chan_total, Noise.gs, RealNoise.pOf, RealNoise.pOf_bounds

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

theorem `RealNoise.mMin_spec`

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

EXISTENCE, ATTAINMENT AND MINIMALITY.

Statement as elaborated and printed by Lean 4.26.0

∀ {a : ℝ},
  0 < a →
    a ≤ 1 →
      NimAudit.RealNoise.Ach a (NimAudit.RealNoise.mMin a) ∧
        ∀ (m : ℕ), NimAudit.RealNoise.Ach a m → NimAudit.RealNoise.mMin a ≤ m

Exact source text, lines 143–149

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

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

Project declarations used by the proof or definition body

RealNoise.Ach, RealNoise.ach_exists, RealNoise.mMin

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

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 1Symmetric channel with agreement (1+a)/2; m*(a) is the least sample count with both errors ≤ 1/4

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

def RealNoise.pOf

theorem RealNoise.chan_law

def RealNoise.Ach

def RealNoise.mMin

theorem RealNoise.mMin_spec

Definitions these statements use

def Bridge.bitvecs

def Noise.chanW

def Noise.gs

Full modules

def `RealNoise.pOf`

theorem `RealNoise.chan_law`

def `RealNoise.Ach`

def `RealNoise.mMin`

theorem `RealNoise.mMin_spec`

def `Bridge.bitvecs`

def `Noise.chanW`

def `Noise.gs`