# 獨立同分布序列：由 Bernoulli(1/3) 柱集乘積公式證明 IID

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-iid-sequence/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-iid-sequence-01 · production-20261019-adopted-96



## 目標與範圍

設 p=1/3，柱集證書規定每個有限 0-1 word w（長度 n、含 k 個 1）的機率為 p^k(1−p)^{n−k}。證明：此族一致且每層總和為 1；由此（配合引用的 Kolmogorov 存在定理）得到 {0,1}^ℕ 上的機率；每個 X_i 的完整邊際都是 Bernoulli(1/3)；每個有限子族都獨立。再以三個對照說明：檢查過的 prefix、pairwise 獨立與相同期望都不足以宣稱無限 IID。

只在 MKO 範圍內工作：p 為 [0,1] 中的精確有理數（此處 1/3），cylinder word 為有限 0-1 序列（假設 a1）；無限 IID 的宣稱以明示的符號乘積律證書為依據（假設 a2）。對每個有限子族的獨立性與同分布給出完整證明；無限乘積測度的存在與唯一性引用 Kolmogorov 存在定理，本稿不證明。不處理大數律或中心極限定理；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- prob_axioms
- power_laws
- distributive
- finite_sum_rules
- nat_induction
- mul_comm


- G1 — p=1/3，為 [0,1] 中的精確有理數（MKO 假設 a1）；q(1)=p=1/3、q(0)=1−p=2/3。
- G2 — 符號乘積律證書：對每個 n≥1 與每個 word w=(w_i)_{i=1}^{n}∈{0,1}^n，P(X_i=w_i 對所有 1≤i≤n)=c(w)=p^{k(w)}(1−p)^{n−k(w)}，k(w) 為 w 中 1 的個數（MKO 假設 a2）。
- G3 — 定義：(X_i)_{i≥1} 是 IID，若 (a) 同分布：所有 X_i 有相同的完整邊際分布；(b) 獨立：對每個有限的相異指標集 J 與值 (a_j)_{j∈J}，P(X_j=a_j 對所有 j∈J)=Π_{j∈J} P(X_j=a_j)。


- p=\tfrac13 — Bernoulli 參數
- q(1)=p,\ q(0)=1-p — 單一位置的機率
- c(w) — word w 的柱集機率 p^{k}(1−p)^{n−k}
- k(w) — w 中 1 的個數
- J,\ a=(a_j)_{j\in J} — 有限指標集與指定值





## 規則與來源


- prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{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 — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- mko_iid_def · cited — 本輪用 Bernoulli(p) 無限 product-law／cylinder symbolic certificate 建立 IID 序列：任意有限 0-1 word 的機率為 p 的一數次方乘 (1-p) 的零數次方。有限 prefix 只能稱 finite IID family，不能獨自證無限序列。 · mko-iid-sequence
- kolmogorov_ext · cited — 若對每個 n 給定 {0,1}^n 上的機率 μ_n，且族一致（刪去最後一個座標時 μ_{n+1} 的像是 μ_n），則 {0,1}^ℕ（配乘積 σ 代數）上存在唯一的機率，其前 n 個座標的分布為 μ_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 — 對每個 word w：c(w0)+c(w1)=c(w)，其中 wa 表示在 w 後面接上 a。
- L_marginal · lemma — 對 n≥1、J⊆{1,2,直到 n} 與值 (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)。





## 逐步主鏈

S01 · equivalent操作前

c(101)

操作後

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

條件：無

規則：numeric_evaluation · 依賴：G1, G2

葉節點依據：numeric_evaluation + power_laws

先讀懂證書：w=101 長度 n=3，含 k=2 個 1，所以 c(101)=p^2(1−p)^1=(1/3)^2(2/3)=2/27（N1）。公式只依賴 1 的個數，所以 110、011 也是 2/27（N9）。



S02 · equivalent操作前

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

操作後

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

條件：無

規則：L_product_form · 依賴：G1, G2

葉節點依據：mul_comm + mul_assoc + power_laws

依引理 L_product_form（在 S02.1 證明），柱集機率是各位置機率 q(w_i) 的乘積。這個乘積形式是之後一致性與邊際計算的關鍵。



S03 · equivalent操作前

c(w0)+c(w1)

操作後

c(w)

條件：無

規則：L_consistency · 依賴：S02

葉節點依據：distributive + add_comm + mul_one

依引理 L_consistency（在 S03.1 證明），把長度 n+1 的 word 對最後一個位置求和，回到長度 n 的機率。這正是 Kolmogorov 存在定理要求的一致性。



S04 · induction_step操作前

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

操作後

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

條件：無

規則：nat_induction · 依賴：S03, G1

葉節點依據：nat_induction + finite_sum_rules + numeric_evaluation

對 n 歸納。基底 n=1：c(0)+c(1)=2/3+1/3=1（N8）。歸納步：長度 n+1 的 word 恰是長度 n 的 w 接上 0 或 1，所以 Σ_{|v|=n+1} c(v)=Σ_{|w|=n}(c(w0)+c(w1))=Σ_{|w|=n} c(w)=1（S03 與歸納假設）。例 n=3：8 個 word 的總和 8/27+12/27+6/27+1/27=1（N2、N10）。所以每一層都是機率分布。



S05 · theorem_application操作前

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

操作後

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

條件：\text{consistency (S03)}; \text{total mass 1 (S04)}

規則：kolmogorov_ext · 依賴：S03, S04

葉節點依據：kolmogorov_ext

令 μ_n(w)=c(w)。S04 給出每個 μ_n 是 {0,1}^n 上的機率，S03 給出一致性。依引用的 Kolmogorov 存在定理，{0,1}^ℕ 上存在唯一機率使柱集機率為 c(w)；X_i 是第 i 個座標。本稿只核對定理的前提，不證明定理本身。



S06 · equivalent操作前

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)

條件：J\ \text{finite, nonempty}

規則：prob_axioms · 依賴：S05, G2, prob_axioms

葉節點依據：prob_axioms + set_operations_def + finite_sum_rules

取 n=max J。事件「X_j=a_j 對所有 j∈J」是長度 n、在 J 上取指定值的 word 的柱集之聯集；不同 word 的柱集互斥。依機率的有限可加性，其機率等於這些 c(w) 之和。



S07 · equivalent操作前

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

操作後

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

條件：無

規則：L_marginal · 依賴：S06, S02

葉節點依據：distributive + finite_sum_rules + nat_induction

用乘積形式（S02）改寫和中的 c(w)，再依引理 L_marginal（在 S07.1、S07.2 證明）：自由位置的和全部化為因子 q(0)+q(1)=1，只剩指定位置的因子。



S08 · implies操作前

J=\{i\}

操作後

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

條件：無

規則：forall_intro · 依賴：S06, S07, G1

葉節點依據：forall_intro + forall_elim

取 J={i}：P(X_i=a)=q(a)，即 P(X_i=1)=1/3、P(X_i=0)=2/3，對任意 i 相同；1/3+2/3=1（N8）。這是完整的邊際分布（兩個值的機率），不只是期望 E[X_i]=1/3。所以 (a) 同分布成立。



S09 · implies操作前

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)

條件：無

規則：forall_intro · 依賴：S06, S07, S08, G3

葉節點依據：forall_intro + eq_replace

先分情況。若 J=∅，沒有座標限制的事件是整個 Ω，機率為 1；右邊依空乘積慣例也為 1，所以獨立性等式成立，不取 max∅。若 J 為非空有限集，才依 S06 取 n=max J；由 S06、S07 左邊等於 Π_{j∈J} q(a_j)，再由 S08 每個 q(a_j)=P(X_j=a_j)，所以聯合機率等於邊際之積。兩個分支涵蓋所有有限 J，因此 (b) 對每個有限子族成立，不只是成對。



S10 · implies操作前

P(X_2=1,\ X_5=0)

操作後

\tfrac13\cdot\tfrac23=\tfrac29

條件：無

規則：forall_elim · 依賴：S09, S08

葉節點依據：forall_elim + numeric_evaluation

實例：J={2,5}、a_2=1、a_5=0。由 S09 得 (1/3)(2/3)=2/9。直接由 S06 驗算：n=5，自由位置 1、3、4 共 2^3=8 個 word，和為 (1/3)(2/3)((2/3)+(1/3))^3=2/9（N4）。



S11 · implies操作前

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

操作後

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

條件：無

規則：quantifier_negation · 依賴：G3

葉節點依據：quantifier_negation + numeric_evaluation

對照（prefix）：令 Z_1、Z_2 為獨立 Bernoulli(1/3)，其後每個 Z_i 都等於 Z_1。長度 2 的 prefix 滿足乘積公式，每個 Z_i 的邊際也是 Bernoulli(1/3)；但 P(Z_1=1,Z_3=1)=P(Z_1=1)=1/3，而 P(Z_1=1)P(Z_3=1)=1/9（N5），所以 J={1,3} 的獨立性失敗。檢查過的有限 prefix 不能證明無限序列 IID。



S12 · implies操作前

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

條件：無

規則：quantifier_negation · 依賴：G3

葉節點依據：quantifier_negation + prob_axioms + numeric_evaluation

對照（pairwise）：U_3 是 U_1、U_2 的模 2 和。四種 (U_1,U_2) 各有機率 1/4。對任意 a、b，P(U_1=a,U_3=b)=P(U_1=a,U_2=a⊕b)=1/4=(1/2)(1/2)（N7），(U_2,U_3) 同理，且三者邊際都是 Bernoulli(1/2)。但 U_1=U_2=1 推出 U_3=0，所以 P(U_1=U_2=U_3=1)=0≠1/8（N6）。pairwise 獨立加同分布仍不是 IID。



S13 · implies操作前

V\equiv\tfrac13

操作後

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

條件：無

規則：quantifier_negation · 依賴：S08, G3

葉節點依據：quantifier_negation + numeric_evaluation

對照（相同期望）：常數 V≡1/3 的期望與 X_1 相同，都是 1/3，但 P(V=1)=0，而 P(X_1=1)=1/3。所以期望相同不推出分布相同；(a) 要比較完整邊際（S08）。



S14 · implies操作前

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

操作後

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

條件：無

規則：mko_iid_def · 依賴：S05, S08, S09, S11, S12, S13

葉節點依據：and_intro_elim + def_unfold

在 S05 的機率下，每個 X_i 的完整邊際都是 Bernoulli(1/3)（S08），每個有限子族都獨立（S09），所以 (X_i) 是 IID；這依賴的是對所有 n 與所有 word 成立的符號證書，而不是某段 prefix。三個對照（S11 到 S13）說明較弱的檢查都不足夠。







## 局部子步與引理

S02.1 · equivalent操作前

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

操作後

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

條件：無

規則：power_laws · 依賴：G1, mul_comm, power_laws

葉節點依據：mul_comm + mul_assoc + power_laws

乘積中 w_i=1 的 k(w) 個位置各貢獻 q(1)=p，w_i=0 的 n−k(w) 個位置各貢獻 q(0)=1−p。依乘法交換與結合律把相同因子集中，得 p^{k(w)}(1−p)^{n−k(w)}。S02.1 證得引理 L_product_form。



S03.1 · equivalent操作前

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

操作後

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

條件：無

規則：distributive · 依賴：S02, distributive

葉節點依據：distributive + add_inverse + add_comm + mul_one

由乘積形式（S02），c(wa)=c(w)q(a)。所以 c(w0)+c(w1)=c(w)(1−p)+c(w)p=c(w)((1−p)+p)=c(w)·1=c(w)（N3 以多項式恆等式核對）。S03.1 證得引理 L_consistency。



S07.1 · induction_base操作前

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

操作後

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

條件：無

規則：nat_induction · 依賴：S02

葉節點依據：nat_induction + finite_sum_rules

對自由位置的個數 f=n−|J| 歸納。基底 f=0：所有位置都被指定，和中只有一個 word w=a，其值為 Π_{i=1}^{n} q(a_i)=Π_{j∈J} q(a_j)。



S07.2 · induction_step操作前

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)

條件：無

規則：nat_induction · 依賴：S07.1, S02, distributive

葉節點依據：nat_induction + distributive + finite_sum_rules + add_inverse

歸納步：設 f≥1，取一個自由位置 i。按 w_i 的值把和分成兩組；每項含因子 q(w_i)，依分配律提出：和=Σ_{b∈{0,1}} q(b)·T=(q(0)+q(1))T=T，其中 T 是去掉位置 i 後、其餘位置的乘積在同樣約束下的和，只有 f−1 個自由位置。依歸納假設 T=Π_{j∈J} q(a_j)。S07.1 與 S07.2 合起來證得引理 L_marginal。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S05, S08, S09, mko_iid_def — 目標 G：(X_i) 是 IID Bernoulli(1/3)。足夠條件 H：機率存在（S05，引用）、(a)（S08）、(b)（S09）；H⇒G 由定義 G3。H 由 G1、G2 正向證成，只有 S05 依賴引用的定理。
- S13 · premise_audit · S08, G3 — 一個值的機率不同就足以否定同分布。
- S12 · premise_audit · G3, quantifier_negation — 三個成對都核對了，失敗的是三元子族；(b) 量化每個有限子族。
- S11 · premise_audit · G3, quantifier_negation — 一個失敗的有限子族就否定 (b)；這也顯示 S09 必須對所有 J 證明。
- S10 · premise_audit · S09, numeric_evaluation — 只是一個實例，不取代 S09 的全稱證明。
- S09 · premise_audit · S06, S07, S08, forall_intro — 量化範圍是所有有限 J（MKO 段落 1）；空集由 Ω 的機率與空乘積均為 1 的分支處理；非空集才用 S06 的 max J 論證，所以沒有遺漏空子族。
- S08 · premise_audit · S06, S07, forall_intro — i 是任意的，證明沒有對 i 加條件，所以對所有 i 成立；不是逐一核對有限多個 i。
- S07.2 · premise_audit · S07.1, distributive, nat_induction — 提出因子需要乘積形式（S02）：q(w_i) 不依賴其他位置；若機率不是乘積形式，這一步就失敗（見 S11）。
- S07.1 · premise_audit · S02, nat_induction — 只是單項和，無需其他前提。
- S07 · inverse_equivalence · L_marginal — 引理是等式，雙向成立。
- S06 · inverse_equivalence · prob_axioms, set_operations_def — 事件分解是集合等式，可加性給出機率相等；兩邊同值。
- S05 · premise_audit · S03, S04, kolmogorov_ext — 定理需要每層是機率且族一致，兩者都已證；定理本身是引用（citation_verified）。
- S04 · premise_audit · S03, nat_induction, finite_sum_rules — 全稱結論來自歸納法，不是來自 n=3 的數值核對；N2 只是一個實例。
- S03.1 · inverse_equivalence · distributive, add_inverse, mul_one — 分配律與 (1−p)+p=1 都是恆等式，雙向成立。
- S03 · inverse_equivalence · L_consistency — 恆等式，雙向成立。
- S02.1 · inverse_equivalence · mul_comm, mul_assoc, power_laws — 重排有限乘積不改變其值；兩向都只是重排。
- S02 · inverse_equivalence · L_product_form — 兩式對每個 w 相等，雙向成立。
- S01 · inverse_equivalence · numeric_evaluation, G2 — 精確有理數求值，可獨立重算；兩邊是同一數。





## 錯誤控制與反例

prefix 不能證無限序列MKO 指出的誤解：檢查固定 prefix 就宣稱無限 IID。S11 的 Z 序列前兩項完全符合乘積公式，但 Z_3=Z_1 使 J={1,3} 的獨立性失敗（1/3≠1/9）。證書必須對所有長度 n 與所有 word 以符號形式成立（G2）。

pairwise 獨立不夠MKO 的另一個誤解。S12 的 U_1、U_2、U_3 兩兩獨立且同分布，但三者的聯合機率 0≠1/8。獨立性要對每個有限子族核對，S09 正是對任意有限 J 證明。

相同期望不是同分布MKO 段落 0：同分布要核完整邊際，不是只看平均。常數 1/3 與 Bernoulli(1/3) 期望相同，但 P(V=1)=0≠1/3（S13）。


- 長度至多 2 的 word 都符合乘積公式，所以整個序列是 IID → reject — S11 的 Z 序列滿足此條件，但 P(Z_1=1,Z_3=1)=1/3≠1/9。
- 兩兩獨立且同分布的隨機變數就是 IID → reject — S12 的模 2 和例子：P(U_1=U_2=U_3=1)=0≠1/8。
- 每個 X_i 的期望都是 1/3，所以它們同分布 → reject — 常數 1/3 的期望也是 1/3，但分布不同（S13）；同分布要比較完整邊際。
- word 110 與 101 的 1 位置不同，所以機率不同 → reject — 公式只依賴 1 的個數：兩者都是 (1/3)^2(2/3)=2/27（N9）。





## 結論與限制

柱集證書 c(w)=(1/3)^{k}(2/3)^{n−k} 等於各位置機率之積，族一致且每層總和為 1；配合引用的 Kolmogorov 存在定理，它在 {0,1}^ℕ 上定出唯一機率。對任何有限 J，P(X_j=a_j, j∈J)=Π q(a_j)，所以每個 X_i 的完整邊際是 Bernoulli(1/3)，每個有限子族獨立：(X_i) 是 IID。檢查過的 prefix、pairwise 獨立與相同期望各有反例，不能代替證書。


- {0,1}^ℕ 上乘積測度的存在與唯一性引用已核對的 Durrett《Probability: Theory and Examples》第 5 版附錄 A.3 定理 A.3.1 及例 A.3.2，取支撐於 {0,1} 的可數座標特例；本稿核對其前提（S03、S04），不重證定理。原 Billingsley 版次未查閱，已另存沿革。大數律與中心極限定理仍不在範圍內。





## 驗證及來源綁定

10 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-iid-sequence-01.json)