Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Chebyshev bounds the majority error of repeated Bernoulli trials

Statement

Let k1, let X1,,Xk be independent Bernoulli random variables with P(Xi=1)2/3 for every i, and put S:=X1++Xk. Then

P ⁣(Sk2)9k.

Thus the probability that a majority vote is wrong decays like O(1/k).

Facts & Assumptions

Given: an integer k1 and independent Bernoulli variables X1,,Xk with P(Xi=1)2/3.

[L2]

Bernoulli mean and variance satisfy E[Xi]=pi and Var(Xi)=pi(1pi)1/4 (A Bernoulli(p) variable has mean p and variance p(1p); a binomial(n,p) variable has mean np and variance np(1p)).

[L3]

Variance adds for pairwise-independent finite families (Variance adds for every finite pairwise-independent family).

[L4]

Chebyshev's inequality bounds P(YE[Y]t) by Var(Y)/t2 (Chebyshev's inequality on a finite probability space).

Proof

technique · direct
1.1

Let μ:=E[S]. By [L1] and [L2], μ=i=1kE[Xi]2k/3. Also [L2] and [L3] give Var(S)=i=1kVar(Xi)k/4.

L1L2L3given
2.1

If Sk/2, then since μ2k/3 we have μSk/6, so {Sk/2}{Sμk/6}. Applying [L4] with Y=S and t=k/6 yields P(Sk/2)Var(S)/(k/6)2(k/4)/(k2/36)=9/k.

L4step 1.1algebra
3.1

The event Sk/2 is exactly the event that at most half the trials are correct, so the same bound controls majority-vote error.

step 2.1

Depends on

Used by

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources