Proposition F.13/(32a²) ≤ m*(a) ≤ ⌈4/a²⌉ ≤ 17/(4a²); majority with ties declared 0 attains the middle bound

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

1 Paper text

Proposition F.1 (Repetitions needed for a weakly informative bit) The minimum $m_*(a)$ exists and satisfies $\frac{3}{32a^2}\le m_*(a)\le\left\lceil\frac{4}{a^2}\right\rceil \le\frac{17}{4a^2}.$ Majority voting, with ties declared 0, achieves the middle upper bound.

Generated from paper_jmlr.tex, lines 1607–1615.

2 Explain this

Statement. For $0<a\le1/2$ : $\;3/(32a^2)\le m_*(a)\le\lceil4/a^2\rceil\le17/(4a^2)$ , and majority vote with ties declared $0$ achieves the middle bound.

Upper bound idea. The number of correct observations has mean $m(1+a)/2$ and variance at most $m/4$ ; Chebyshev's inequality gives majority error at most $1/(ma^2)$ , which is at most $1/4$ once $m\ge4/a^2$ .

Lower bound idea. If $ma^2<3/32$ , the two possible observation laws are so close (chi-square divergence below $1$ , hence total variation below $1/2$ ) that no rule, randomised or not, can have both errors at most $1/4$ .

Example. $a=0.364$ (from $\varepsilon=0.01$ , $L=50$ ): $\lceil4/a^2\rceil=31$ observations suffice.

3 How this is formalised

RealNoise.majority_succeeds: for $0<a\le1$ majority (ties to $0$ ) has both errors at most $1/4$ for every $m\ge\lceil4/a^2\rceil$ (RealNoise.mUp).
RealNoise.any_rule_needs: for $0<a\le1/2$ every randomised rule with both errors at most $1/4$ uses at least $3/(32a^2)$ samples.
RealNoise.mMin_spec: existence, attainment and minimality of $m_*(a)$ .
RealNoise.mMin_bounds: $3/(32a^2)\le m_*(a)\le\lceil4/a^2\rceil<4/a^2+1$ .
RealNoise.mMin_theta: $\tfrac3{32}a^{-2}\le m_*(a)\le\tfrac{17}4a^{-2}$ .

All over Mathlib's reals; the adapters showing that the generic field operations are Mathlib's are part of the module.

Coverage record
Paper anchor	`prop:noise-samples` (manuscript label)
Displayed as	Proposition F.1
Claim	3/(32a²) ≤ m*(a) ≤ ⌈4/a²⌉ ≤ 17/(4a²); majority with ties declared 0 attains the middle bound
Coverage category	Checked theorem
Statement source	paper_jmlr.tex lines 1607–1615; SHA-256 of the normalised block source `31604b6f79fa704b…`
Lean declarations	`NimAudit.RealNoise.mMin_spec` (RealNoise, lines 143–149, file `ff2ca55835de…`) `NimAudit.RealNoise.mMin_bounds` (RealNoise, lines 151–157, file `ff2ca55835de…`) `NimAudit.RealNoise.mMin_theta` (RealNoise, lines 159–174, file `ff2ca55835de…`) `NimAudit.RealNoise.majority_succeeds` (RealNoise, lines 109–118, file `ff2ca55835de…`) `NimAudit.RealNoise.any_rule_needs` (RealNoise, lines 120–125, file `ff2ca55835de…`)
Assumptions and domain	$0<a\le1/2$ ; observations independent given $Y$ ; randomised decision rules allowed; error at most $1/4$ for each value of $Y$ .
Audited correspondence rows	`prop:noise-samples`, `app:noise-samples`
Explanations	`explain/prop:noise-samples`, `formal/prop:noise-samples`
Build evidence	fresh isolated rebuild, audit report

4 Lean statement and source

Principal declarations

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

theorem `RealNoise.mMin_bounds`

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

A3 TWO-SIDED BOUNDS: 3/(32a²) ≤ mMin a ≤ ⌈4/a²⌉₊ < 4/a² + 1.

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 ≤ NimAudit.RealNoise.mUp a ∧
          ↑(NimAudit.RealNoise.mUp a) < 4 / a ^ 2 + 1

Exact source text, lines 151–157

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

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

Project declarations used by the proof or definition body

Noise.Rule, Noise.err0, Noise.err1, RealNoise.Ach, RealNoise.ach_of_ge, RealNoise.any_rule_needs, RealNoise.mMin, RealNoise.mMin_spec, RealNoise.mUp, RealNoise.mUp_lt, RealNoise.pOf

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

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

A2 (UPPER BOUND, at ℝ): for 0 < a ≤ 1 the majority rule (ties declared 0) has both error probabilities at most 1/4 for EVERY m ≥ m(a), in particular at m = m(a).

Statement as elaborated and printed by Lean 4.26.0

∀ {a : ℝ},
  0 < a →
    a ≤ 1 →
      ∀ {m : ℕ},
        NimAudit.RealNoise.mUp a ≤ m →
          NimAudit.Noise.err0 (NimAudit.RealNoise.pOf a) m
                (NimAudit.Noise.detRule NimAudit.Noise.maj) ≤
              1 / 4 ∧
            NimAudit.Noise.err1 (NimAudit.RealNoise.pOf a) m
                (NimAudit.Noise.detRule NimAudit.Noise.maj) ≤
              1 / 4

Exact source text, lines 109–118

109/-- 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]

Project declarations in the statement: Noise.detRule, Noise.err0, Noise.err1, Noise.maj, RealNoise.mUp, RealNoise.pOf

Project declarations used by the proof or definition body

Noise.detRule, Noise.err0, Noise.err1, Noise.maj, Noise.maj_upper, RealNoise.mUp, RealNoise.mUp_spec, RealNoise.pOf, RealNoise.two_pOf

theorem `RealNoise.any_rule_needs`

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

A2 (LOWER BOUND, at ℝ): for 0 < a ≤ 1/2, EVERY randomized rule (acceptance probability φ(o) ∈ [0,1]) with both errors ≤ 1/4 uses at least 3/(32a²) samples.

Statement as elaborated and printed by Lean 4.26.0

∀ {a : ℝ},
  0 < a →
    a ≤ 1 / 2 →
      ∀ (m : ℕ) (φ : List Bool → ℝ),
        NimAudit.Noise.Rule m φ →
          NimAudit.Noise.err0 (NimAudit.RealNoise.pOf a) m φ ≤ 1 / 4 →
            NimAudit.Noise.err1 (NimAudit.RealNoise.pOf a) m φ ≤ 1 / 4 → 3 / (32 * a ^ 2) ≤ ↑m

Exact source text, lines 120–125

120/-- 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)]; linarith

Project declarations in the statement: Noise.Rule, Noise.err0, Noise.err1, RealNoise.pOf

Project declarations used by the proof or definition body

Noise.Rule, Noise.err0, Noise.err1, Noise.lower_bound, RealNoise.pOf, RealNoise.two_pOf

Definitions these statements use

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

def `Noise.detRule`

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

Statement as elaborated and printed by Lean 4.26.0

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

Exact source text, lines 345–345

345def detRule (δ : List Bool → Bool) : List Bool → R := fun o => ind (δ o)

Project declarations in the statement: none

Project declarations used by the proof or definition body

Noise.ind

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

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

THE MAJORITY RULE: declare 1 iff more than half of the m observations are 1; a tie (possible for even m) is declared 0.

Statement as elaborated and printed by Lean 4.26.0

List Bool → Bool

Exact source text, lines 355–357

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

Project declarations in the statement: none

Project declarations used by the proof or definition body

Noise.cnt

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

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

Full modules

Module	File	Lines	Imports
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).

Proposition F.13/(32a²) ≤ m*(a) ≤ ⌈4/a²⌉ ≤ 17/(4a²); majority with ties declared 0 attains the middle bound

1 Paper text

2 Explain this

3 How this is formalised

4 Lean statement and source

Principal declarations

theorem RealNoise.mMin_spec

theorem RealNoise.mMin_bounds

theorem RealNoise.mMin_theta

theorem RealNoise.majority_succeeds

theorem RealNoise.any_rule_needs

Definitions these statements use

def RealNoise.mUp

def RealNoise.Ach

def RealNoise.mMin

def Noise.detRule

def Noise.err0

def Noise.err1

def Noise.maj

def RealNoise.pOf

def Noise.Rule

Full modules

theorem `RealNoise.mMin_spec`

theorem `RealNoise.mMin_bounds`

theorem `RealNoise.mMin_theta`

theorem `RealNoise.majority_succeeds`

theorem `RealNoise.any_rule_needs`

def `RealNoise.mUp`

def `RealNoise.Ach`

def `RealNoise.mMin`

def `Noise.detRule`

def `Noise.err0`

def `Noise.err1`

def `Noise.maj`

def `RealNoise.pOf`

def `Noise.Rule`