Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Independent majority repetition reduces bounded error

Lax253009.MajorityAmplification · concepts/Lax253009/MajorityAmplification.lean · lax-253009

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Three independent executions followed by majority vote transform an error probability pp into 3p2−2p33p^2-2p^3. Three rounds of this construction reduce error at most 1/31/3 to at most 1/121/12, using 27 independent executions.

    Concept map
    2 concepts
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 majority_error proven

    2 three_rounds proven

    Lean source view on GitHub

    1import Lax253009.FiniteProbability
    2
    3/-!
    4---
    5title: Independent majority repetition reduces bounded error
    6type: theorem
    7---
    8Three independent executions followed by majority vote transform an error
    9probability pp into 3p2−2p33p^2-2p^3. Three rounds of this construction reduce
    10error at most 1/31/3 to at most 1/121/12, using 27 independent executions.
    11-/
    12
    13namespace Lax253009.MajorityAmplification
    14
    15open FiniteProbability
    16
    17def vote (a b c : Bool) : Bool := (a && b) || (a && c) || (b && c)
    18
    19def errorMap (p : ℝ) : ℝ := 3 * p ^ 2 - 2 * p ^ 3
    20
    21axiom majority_error {α : Type} [Fintype α] [Nonempty α]
    22 (answer : α → Bool) (b : Bool) :
    23 probability (fun r : α × α × α ↦
    24 vote (answer r.1) (answer r.2.1) (answer r.2.2) ≠ b) =
    25 errorMap (probability (fun r ↦ answer r ≠ b))
    26
    27axiom three_rounds (p : ℝ) (hp : 0 ≤ p) (hp' : p ≤ 1 / 3) :
    28 errorMap (errorMap (errorMap p)) ≤ 1 / 12
    29
    30end Lax253009.MajorityAmplification
    31
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…