IID sequence: proving IID from the Bernoulli(1/3) cylinder product formula

Goal and scope

Let p=1/3, and let the cylinder certificate give each finite binary word w (length n, with k ones) the probability p^k(1−p)^{n−k}. Prove that this family is consistent with total mass 1 at every level; obtain from it (with the cited Kolmogorov existence theorem) a probability on {0,1}^ℕ; show that every X_i has the complete marginal Bernoulli(1/3) and that every finite subfamily is independent. Then use three contrasts to show that a checked prefix, pairwise independence and equal expectations are each insufficient for an infinite IID claim.

Works inside the MKO's scope: p is an exact rational in [0,1] (here 1/3), and cylinder words are finite binary sequences (assumption a1); the infinite IID claim rests on the explicit symbolic product-law certificate (assumption a2). Independence and identical distribution of every finite subfamily are proved in full; existence and uniqueness of the infinite product measure are cited from the Kolmogorov existence theorem and not proved here. Laws of large numbers and the central limit theorem are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• prob_axioms
• power_laws
• distributive
• finite_sum_rules
• nat_induction
• mul_comm

• G1 — p=1/3, an exact rational in [0,1] (MKO assumption a1); q(1)=p=1/3 and q(0)=1−p=2/3.
• G2 — Symbolic product-law certificate: for every n≥1 and every word w=(w_i)_{i=1}^{n}∈{0,1}^n, P(X_i=w_i for all 1≤i≤n)=c(w)=p^{k(w)}(1−p)^{n−k(w)}, where k(w) is the number of ones in w (MKO assumption a2).
• G3 — Definition: (X_i)_{i≥1} is IID if (a) identically distributed: all X_i have the same complete marginal law; and (b) independent: for every finite set J of distinct indices and values (a_j)_{j∈J}, P(X_j=a_j for all j∈J)=Π_{j∈J} P(X_j=a_j).

• p=\tfrac13 — the Bernoulli parameter
• q(1)=p,\ q(0)=1-p — the one-position probabilities
• c(w) — the cylinder probability p^{k}(1−p)^{n−k} of the word w
• k(w) — the number of ones in w
• J,\ a=(a_j)_{j\in J} — a finite index set and prescribed values

Rules and sources

• prob_axioms · prerequisite — Probability axioms: P(A)≥0; P(Ω)=1; the probability of a (countable) union of pairwise disjoint events is the sum of their probabilities. Hence P(∅)=0 and P(Aᶜ)=1−P(A).
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• mko_iid_def · cited — This slice uses a symbolic Bernoulli(p) infinite product-law cylinder certificate: each finite binary word has probability p raised to its number of ones times (1−p) raised to its number of zeros. A finite prefix can only certify a finite IID family; by itself it does not certify the infinite sequence. · mko-iid-sequence
• kolmogorov_ext · cited — If for every n a probability μ_n on {0,1}^n is given and the family is consistent (deleting the last coordinate maps μ_{n+1} to μ_n), then there is a unique probability on {0,1}^ℕ (with the product σ-algebra) whose law on the first n coordinates is μ_n. · Rick Durrett, Probability: Theory and Examples, 5th edition, Appendix A.3, Theorem A.3.1 and Example A.3.2
• L_product_form · lemma — c(w)=Π_{i=1}^{n} q(w_i).
• L_consistency · lemma — For every word w: c(w0)+c(w1)=c(w), where wa means w followed by a.
• L_marginal · lemma — For n≥1, J⊆{1, 2, up to n} and values (a_j)_{j∈J}: Σ_{w∈{0,1}^n, w_j=a_j (j∈J)} Π_{i=1}^{n} q(w_i)=Π_{j∈J} q(a_j).

Main derivation

c(101)

\left(\tfrac13\right)^2\left(\tfrac23\right)^1=\tfrac{2}{27}

c(w)=p^{k(w)}(1-p)^{n-k(w)}

c(w)=\prod_{i=1}^{n}q(w_i)

c(w0)+c(w1)

c(w)

\sum_{w\in\{0,1\}^n}c(w)

1\quad\text{for every}\ n\ge1

(\mu_n)_{n\ge1}\ \text{consistent, each a probability}

\exists!\ P\ \text{on}\ \{0,1\}^{\mathbb{N}}\ \text{with cylinder probabilities}\ c(w)

P(X_j=a_j\ \forall j\in J),\ n=\max J

\sum_{w\in\{0,1\}^n,\ w_j=a_j\ (j\in J)}c(w)

\sum_{w_J=a}\prod_{i=1}^{n}q(w_i)

\prod_{j\in J}q(a_j)

J=\{i\}

P(X_i=1)=\tfrac13,\ P(X_i=0)=\tfrac23\quad\text{for every}\ i

J\ \text{finite},\ (a_j)_{j\in J}

P(X_j=a_j\ \forall j\in J)=\prod_{j\in J}P(X_j=a_j)

P(X_2=1,\ X_5=0)

\tfrac13\cdot\tfrac23=\tfrac29

Z_1,Z_2\ \text{IID Bernoulli}(\tfrac13),\ Z_i=Z_1\ (i\ge3)

P(Z_1=1,Z_3=1)=\tfrac13\neq\tfrac19

U_1,U_2\ \text{IID Bernoulli}(\tfrac12),\ U_3=U_1\oplus U_2

\text{pairwise independent, but}\ P(U_1=U_2=U_3=1)=0\neq\tfrac18

V\equiv\tfrac13

E[V]=E[X_1]=\tfrac13,\ \text{but}\ P(V=1)=0\neq\tfrac13

\text{S05, S08, S09, S11 to S13}

(X_i)_{i\ge1}\ \text{IID Bernoulli}(\tfrac13)

Substeps and lemmas

\prod_{i=1}^{n}q(w_i)

p^{k(w)}(1-p)^{n-k(w)}

c(w)q(0)+c(w)q(1)

c(w)\big((1-p)+p\big)=c(w)

J=\{1,2,\text{up to }n\}

\sum=\prod_{i=1}^{n}q(a_i)

f\ \text{free positions},\ i\ \text{one of them}

\sum=\big(q(0)+q(1)\big)\cdot\big(\text{sum with}\ f-1\ \text{free positions}\big)=\prod_{j\in J}q(a_j)

Reverse audits

• S14 · sufficient_goal_reduction · S05, S08, S09, mko_iid_def — Goal G: (X_i) is IID Bernoulli(1/3). Sufficient condition H: the probability exists (S05, cited), (a) (S08) and (b) (S09); H⇒G by the definition G3. H is proved forwards from G1 and G2; only S05 relies on the cited theorem.
• S13 · premise_audit · S08, G3 — A single value with a different probability suffices to refute identical distribution.
• S12 · premise_audit · G3, quantifier_negation — All three pairs are checked; the failure is in the three-element subfamily, and (b) quantifies over every finite subfamily.
• S11 · premise_audit · G3, quantifier_negation — One failing finite subfamily refutes (b); it also shows why S09 must be proved for all J.
• S10 · premise_audit · S09, numeric_evaluation — One instance only; it does not replace the universal proof of S09.
• S09 · premise_audit · S06, S07, S08, forall_intro — The quantifier ranges over all finite J (MKO paragraph 1); the empty case uses probability 1 for Ω and product 1 for the empty family; only the nonempty case uses max J in S06, so the empty subfamily is not omitted.
• S08 · premise_audit · S06, S07, forall_intro — i is arbitrary and the proof puts no condition on it, so it holds for all i; this is not a check of finitely many i.
• S07.2 · premise_audit · S07.1, distributive, nat_induction — Pulling out the factor needs the product form (S02): q(w_i) does not depend on the other positions; without the product form this step fails (see S11).
• S07.1 · premise_audit · S02, nat_induction — A one-term sum; nothing else is needed.
• S07 · inverse_equivalence · L_marginal — The lemma is an equality, so the step holds both ways.
• S06 · inverse_equivalence · prob_axioms, set_operations_def — The decomposition of the event is a set equality, and additivity gives equal probabilities; both sides have the same value.
• S05 · premise_audit · S03, S04, kolmogorov_ext — The theorem needs each level to be a probability and the family to be consistent, both proved; the theorem itself is cited (citation_verified).
• S04 · premise_audit · S03, nat_induction, finite_sum_rules — The universal conclusion comes from induction, not from the numerical check at n=3; N2 is one instance only.
• S03.1 · inverse_equivalence · distributive, add_inverse, mul_one — Distributivity and (1−p)+p=1 are identities, so the step is two-way.
• S03 · inverse_equivalence · L_consistency — An identity, so it holds both ways.
• S02.1 · inverse_equivalence · mul_comm, mul_assoc, power_laws — Rearranging a finite product does not change its value; both directions are rearrangements.
• S02 · inverse_equivalence · L_product_form — The two expressions are equal for every w, so it holds both ways.
• S01 · inverse_equivalence · numeric_evaluation, G2 — An exact rational evaluation, independently recomputable; both sides are the same number.

Error controls and negative controls

A prefix does not certify the infinite sequence

The MKO's misconception: declaring an infinite IID sequence after checking a fixed prefix. The first two terms of the sequence Z in S11 match the product formula exactly, yet Z_3=Z_1 breaks independence for J={1,3} (1/3≠1/9). The certificate must hold symbolically for every length n and every word (G2).

Pairwise independence is not enough

Another MKO misconception. U_1, U_2, U_3 in S12 are pairwise independent and identically distributed, yet their joint probability is 0≠1/8. Independence must hold for every finite subfamily, which is what S09 proves for arbitrary finite J.

Equal expectations are not equal laws

MKO paragraph 0: identical distribution compares complete marginals, not just means. The constant 1/3 and Bernoulli(1/3) have the same mean, yet P(V=1)=0≠1/3 (S13).

• All words of length at most 2 satisfy the product formula, so the whole sequence is IID → reject — The sequence Z of S11 satisfies this, yet P(Z_1=1,Z_3=1)=1/3≠1/9.
• Pairwise independent, identically distributed random variables are IID → reject — The modulo-2 sum example of S12: P(U_1=U_2=U_3=1)=0≠1/8.
• Every X_i has mean 1/3, so they are identically distributed → reject — The constant 1/3 also has mean 1/3 but a different law (S13); identical distribution compares complete marginals.
• The words 110 and 101 have their ones in different places, so their probabilities differ → reject — The formula depends only on the number of ones: both are (1/3)^2(2/3)=2/27 (N9).

Result and limitations

The cylinder certificate c(w)=(1/3)^{k}(2/3)^{n−k} equals the product of the position probabilities, the family is consistent and has total mass 1 at every level; with the cited Kolmogorov existence theorem it determines a unique probability on {0,1}^ℕ. For every finite J, P(X_j=a_j, j∈J)=Π q(a_j), so every X_i has complete marginal Bernoulli(1/3) and every finite subfamily is independent: (X_i) is IID. A checked prefix, pairwise independence and equal expectations each have counterexamples and cannot replace the certificate.

• Existence and uniqueness of the measure on {0,1}^ℕ are cited from the checked Theorem A.3.1 and Example A.3.2 in Appendix A.3 of Durrett's Probability: Theory and Examples, fifth edition, specialized to countably many coordinates supported on {0,1}. The guide checks the hypotheses in S03 and S04, not the theorem's proof. The uninspected Billingsley edition is preserved separately as provenance. Laws of large numbers and the central limit theorem remain out of scope.

Verification and source binding

10 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: ba5654672fd1ce1b24fc7ce24c4d5916ec5632235207e7fb67cdc22967ffafa9
• original source SHA-256: 49bd8455452eda4395e6e1383315934f9e90e96eda5273f92b4fdc2148171d52
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)