隨機變數獨立：完整核對有限聯合表，零協方差只是後果

目標與範圍

（一）聯合表 J₁：X∈{0,1}、Y∈{0,1,2}，P(0,0)=1/12、P(0,1)=1/12、P(0,2)=1/6、P(1,0)=1/6、P(1,1)=1/6、P(1,2)=1/3。由聯合表聚合兩個邊際，核對全部 6 個值對的乘積式，判定 X、Y 是否獨立；並證明獨立推出任意座標事件 {X∈S} 與 {Y∈T} 獨立與 E[XY]=E[X]E[Y]。（二）聯合表 J₂：X 在 {−1,0,1} 上均勻、Y=X²。證明 Cov(X,Y)=0 但 X、Y 不獨立。（三）聯合表 J₃ 說明只核一個值對不夠。

在 MKO 的範圍內工作：完整的有限聯合支撐與精確有理質量屬於同一機率模型（假設 a1）；主要處理兩個變數，三個以上變數只在負向控制中說明兩兩獨立不推出相互獨立（假設 a2）。零協方差只作必要後果，不作反向證書。不處理連續分布或獨立同分布序列（下一節點），不改動 canonical MKO 或英文 edition。

已知條件與符號

• prob_axioms
• frac_rules
• distributive
• finite_sum_rules
• numeric_evaluation

• G1 — J₁：值集合 X∈{0,1}、Y∈{0,1,2}；p(0,0)=1/12、p(0,1)=1/12、p(0,2)=1/6、p(1,0)=1/6、p(1,1)=1/6、p(1,2)=1/3。
• G2 — J₂：值集合 X∈{−1,0,1}、Y∈{0,1}；p(−1,1)=1/3、p(0,0)=1/3、p(1,1)=1/3，其餘值對 (−1,0)、(0,1)、(1,0) 的質量為 0（即 Y=X²）。
• G3 — J₃：值集合 X∈{0,1}、Y∈{0,1,2}；p(0,0)=1/4、p(0,1)=1/4、p(0,2)=0、p(1,0)=1/4、p(1,1)=0、p(1,2)=1/4。

• p(x,y)=P(X=x,Y=y) — 聯合質量
• P(X=x),\ P(Y=y) — 由聯合表聚合的邊際
• J_1,J_2,J_3 — 三個聯合表
• E[\cdot] — 期望，對聯合表加權求和
• \operatorname{Cov}(X,Y)=E[XY]-E[X]E[Y] — 協方差
• S,T — X 與 Y 的值集合子集（矩形事件）

規則與來源

• prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• 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。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• 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。
• mko_rv_indep_def · cited — 有限值隨機變數 X,Y 獨立，若對每個值對 (x,y) 皆有 P(X=x,Y=y)=P(X=x)P(Y=y)。等價地，所有值事件逆像獨立。本輪完整核有限 joint table；零協方差只作必要後果而非反向證書。 · mko-random-variable-independence
• mko_joint_def · cited — 二維有限聯合分布列出互異值對 (x,y) 及非負精確質量，總和恰為 1。邊際、矩形事件及單點質量都從同一 joint law 聚合。 · mko-finite-joint-distribution
• expectation_def · prerequisite — 對有限聯合表，E[g(X,Y)]=Σ_{(x,y)} g(x,y)p(x,y)；特別地 E[X]=Σ_x x P(X=x)，Cov(X,Y)=E[XY]−E[X]E[Y]。
• L_rect · lemma — 若對所有值對 p(x,y)=P(X=x)P(Y=y)，則對值集合的任意子集 S、T：P(X∈S, Y∈T)=P(X∈S)P(Y∈T)。
• L_EXY · lemma — 若對所有值對 p(x,y)=P(X=x)P(Y=y)，則 E[XY]=E[X]E[Y]，所以 Cov(X,Y)=0。

逐步主鏈

J_1:\ p(x,y)\ge0

\sum_{(x,y)}p(x,y)=\tfrac1{12}+\tfrac1{12}+\tfrac16+\tfrac16+\tfrac16+\tfrac13=1

P(X=0)=\sum_{y}p(0,y),\ P(X=1)=\sum_{y}p(1,y)

P(X=0)=\tfrac1{12}+\tfrac1{12}+\tfrac16=\tfrac13,\ \ P(X=1)=\tfrac16+\tfrac16+\tfrac13=\tfrac23

P(Y=y)=\sum_{x}p(x,y)

P(Y=0)=\tfrac1{12}+\tfrac16=\tfrac14,\ P(Y=1)=\tfrac1{12}+\tfrac16=\tfrac14,\ P(Y=2)=\tfrac16+\tfrac13=\tfrac12

X,Y\ \text{independent}

\forall x\in\{0,1\}\ \forall y\in\{0,1,2\}:\ p(x,y)=P(X=x)P(Y=y)

x=0:\ P(X=0)=\tfrac13

\tfrac13\cdot\tfrac14=\tfrac1{12}=p(0,0),\ \tfrac13\cdot\tfrac14=\tfrac1{12}=p(0,1),\ \tfrac13\cdot\tfrac12=\tfrac16=p(0,2)

x=1:\ P(X=1)=\tfrac23

\tfrac23\cdot\tfrac14=\tfrac16=p(1,0),\ \tfrac23\cdot\tfrac14=\tfrac16=p(1,1),\ \tfrac23\cdot\tfrac12=\tfrac13=p(1,2)

6\ \text{of}\ 6\ \text{value pairs factor}

X,Y\ \text{independent under}\ J_1

S=\{1\},\ T=\{1,2\}

P(X\in S,Y\in T)=\tfrac16+\tfrac13=\tfrac12=\tfrac23\cdot\tfrac34=P(X\in S)P(Y\in T)

X,Y\ \text{independent}

E[XY]=E[X]E[Y],\ \ \operatorname{Cov}(X,Y)=0

E[X]=\tfrac23,\ E[Y]=0\cdot\tfrac14+1\cdot\tfrac14+2\cdot\tfrac12=\tfrac54

E[XY]=1\cdot1\cdot\tfrac16+1\cdot2\cdot\tfrac13=\tfrac56=\tfrac23\cdot\tfrac54

J_2:\ P(X=x)=\tfrac13\ (x=-1,0,1),\ P(Y=0)=\tfrac13,\ P(Y=1)=\tfrac23

E[X]=0,\ E[XY]=(-1)(1)\tfrac13+0+(1)(1)\tfrac13=0\ \Rightarrow\ \operatorname{Cov}(X,Y)=0-0\cdot\tfrac23=0

p(0,1)=0,\ P(X=0)P(Y=1)=\tfrac13\cdot\tfrac23=\tfrac29

0\neq\tfrac29\ \Rightarrow\ X,Y\ \text{not independent, although}\ \operatorname{Cov}=0

J_3:\ P(X=0)=\tfrac12,\ P(Y=0)=\tfrac12,\ P(Y=1)=\tfrac14

p(0,0)=\tfrac14=\tfrac12\cdot\tfrac12\ \text{but}\ p(0,1)=\tfrac14\neq\tfrac18=\tfrac12\cdot\tfrac14

\text{S07},\ \text{S08},\ \text{S09},\ \text{S12},\ \text{S13}

J_1:\ X\perp Y;\ J_2:\ \operatorname{Cov}=0,\ X\not\perp Y;\ J_3:\ X\not\perp Y

局部子步與引理

P(X\in S,Y\in T)

\sum_{x\in S}\sum_{y\in T}p(x,y)

\sum_{x\in S}\sum_{y\in T}P(X=x)P(Y=y)

\Big(\sum_{x\in S}P(X=x)\Big)\Big(\sum_{y\in T}P(Y=y)\Big)=P(X\in S)P(Y\in T)

E[XY]=\sum_{x}\sum_{y}xy\,p(x,y)

E[XY]=\sum_{x}\sum_{y}\big(xP(X=x)\big)\big(yP(Y=y)\big)

\sum_{x}\sum_{y}\big(xP(X=x)\big)\big(yP(Y=y)\big)

\Big(\sum_{x}xP(X=x)\Big)\Big(\sum_{y}yP(Y=y)\Big)=E[X]E[Y]

逐步反向審查

• S14 · sufficient_goal_reduction · S07, S08, S09, S12, S13, and_intro_elim — 目標是三個任務的合取；各部分由所列步驟正向證得，H⇒G 由合取引入。
• S13 · premise_audit · quantifier_negation, prob_axioms, numeric_evaluation — 一個值對通過不推出全稱（N11），一個值對失敗就否定全稱（N12）。
• S12 · premise_audit · mko_rv_indep_def, quantifier_negation, numeric_evaluation — 否定全稱只需一個失敗的值對（N10）；質量 0 的值對也必須核對。
• S11 · premise_audit · expectation_def, prob_axioms, numeric_evaluation — 精確計算（N9）；零協方差在此只是一個事實，尚未推出任何獨立性結論。
• S10 · premise_audit · S09, numeric_evaluation — 這是對 J₁ 的獨立重算（N8），不是引理的證明。
• S09.2 · inverse_equivalence · finite_sum_rules, distributive — 有限和的分配律是等式，雙向成立。
• S09.1 · premise_audit · expectation_def, mul_comm, mul_assoc — 代入需要全部值對的乘積式。
• S09 · premise_audit · S07, L_EXY — 只宣稱獨立 ⇒ 零協方差；反向由 J₂ 否定。
• S08.2 · premise_audit · S08.1, finite_sum_rules, distributive, prob_axioms — 需要全部值對的乘積式；只有部分值對成立時，代入不合法。
• S08.1 · inverse_equivalence · prob_axioms, mko_joint_def — 可加性是等式，雙向成立；值對互異保證不重複計算。
• S08 · premise_audit · S07, L_rect, numeric_evaluation — 反向（矩形事件獨立 ⇒ 值對獨立）取 S={x}、T={y} 即得，但本步不需要；數字由 N7 核對。
• S07 · sufficient_goal_reduction · S04, S05, S06, case_analysis — 目標：獨立。足夠條件：6 對全部通過；H⇒G 由定義，H 由已知正向證得。
• S06 · premise_audit · frac_rules, numeric_evaluation — 精確比較（N5、N6）。
• S05 · premise_audit · frac_rules, numeric_evaluation — 每個等式都是精確有理數比較（N4、N13）。
• S04 · premise_audit · mko_rv_indep_def — 只展開定義；量化範圍是完整的值對集合，不是幾個樣本。
• S03 · inverse_equivalence · prob_axioms, frac_rules — 精確計算，兩邊同值（N3）。
• S02 · inverse_equivalence · prob_axioms, frac_rules — 精確有理數相加，兩邊同值（N2）。
• S01 · premise_audit · mko_joint_def, G1 — 只核資格（N1）；若總和不是 1，就不是機率模型，之後的判定無意義。

錯誤控制與反例

零協方差不是獨立證書

MKO 指出的誤解是由零協方差直接宣稱獨立。S09 證明獨立 ⇒ Cov=0，但 J₂ 中 Y 完全由 X 決定（Y=X²），Cov 卻為 0。零協方差只排除「線性」關聯，不排除其他依賴。

只核一個值對不夠

J₃ 中值對 (0,0) 滿足 1/4=(1/2)(1/2)，但 (0,1) 不滿足。獨立量化所有值對，包括質量為 0 的值對（J₂ 的 (0,1) 正是質量 0 的值對失敗）。

只看邊際不夠

J₃ 的邊際是 X：(1/2,1/2)、Y：(1/2,1/4,1/4)。具有相同邊際的獨立表是 (1/4,1/8,1/8; 1/4,1/8,1/8)，與 J₃ 不同。邊際不決定聯合分布，所以必須由聯合表逐對比較。

• J₂ 中 Cov(X,Y)=0，所以 X 與 Y 獨立 → reject — p(0,1)=0，但 P(X=0)P(Y=1)=2/9。
• J₃ 中 P(X=0,Y=0)=P(X=0)P(Y=0)，所以 X 與 Y 獨立 → reject — (0,1) 失敗：1/4≠(1/2)(1/4)=1/8。
• J₃ 與某個獨立表有相同的邊際，所以 J₃ 下 X、Y 獨立 → reject — 邊際不決定聯合表；J₃ 的 p(0,1)=1/4，獨立表的是 1/8。
• X、Y 為獨立的公平 0/1 變數，Z=(X+Y) mod 2；X、Y、Z 兩兩獨立，所以三者相互獨立 → reject — P(X=0,Y=0,Z=1)=0，但 (1/2)³=1/8；兩兩獨立不推出相互獨立。

結論與限制

J₁ 的邊際為 P(X=0)=1/3、P(X=1)=2/3、P(Y=0)=1/4、P(Y=1)=1/4、P(Y=2)=1/2，全部 6 個值對都滿足 p(x,y)=P(X=x)P(Y=y)，所以 X 與 Y 獨立；因此任意座標事件 {X∈S} 與 {Y∈T} 也獨立（例：1/2=(2/3)(3/4)），且 E[XY]=5/6=E[X]E[Y]。J₂（Y=X²）中 Cov(X,Y)=0，但 p(0,1)=0≠2/9，所以不獨立。J₃ 中 (0,0) 通過而 (0,1) 失敗，不獨立。

• 第四個負向控制中「X、Y、Z 兩兩獨立」只作說明，未在本稿逐對核對。
• L_EXY 只用於有限值變數；無限值或連續變數需要可積性條件，不在本稿範圍內。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 7bf7621a002b7bd6ae4231f260d2c52de04b8a76aece92b976ea6093d4b8e054
• original source SHA-256: 7bf7621a002b7bd6ae4231f260d2c52de04b8a76aece92b976ea6093d4b8e054
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）