# 有限聯合分布：驗證聯合質量表並由同一 joint law 聚合邊際與事件

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

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

derivation-mko-finite-joint-distribution-01 · production-20261019-adopted-96



## 目標與範圍

給定支撐 S={(0,0),(0,1),(1,0),(1,1),(2,1)} 與質量 p(0,0)=1/6、p(0,1)=1/3、p(1,0)=1/4、p(1,1)=1/12、p(2,1)=1/6。驗證 (S,p) 是二維有限聯合分布；由同一個 joint law 算出 X 與 Y 的邊際、矩形事件 P(X∈{1,2}, Y=1) 與單點質量 P(X=2, Y=0)；最後構造一個邊際相同但不同的 joint law，說明兩個邊際一般不能反推聯合分布。

只在 MKO 的範圍內：支撐為互異整數對、質量為精確有理數的有限 joint law（假設 a1），視為數學模型而非資料配適或連續密度（假設 a2）。本稿驗證一張具體的表，並一般地證明「乘積律」引理；不處理獨立性、協方差或條件期望（MKO 的後續節點），不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- cartesian_product_def
- frac_rules
- finite_sum_rules
- order_basics
- numeric_evaluation
- finite_sum_regroup


- G1 — 表：S={(0,0),(0,1),(1,0),(1,1),(2,1)}，p(0,0)=1/6、p(0,1)=1/3、p(1,0)=1/4、p(1,1)=1/12、p(2,1)=1/6，皆為精確有理數。
- G2 — X 與 Y 是同一個值對的兩個座標：在 (x,y) 上 X=x、Y=y。所有事件機率都由這同一張表聚合。
- G3 — A={1,2}，B={1}。


- S — 支撐：列出的互異整數對
- p(x,y) — 值對 (x,y) 的精確質量；不在 S 中的值對質量為 0
- X,\ Y — 座標投影：在值對 (x,y) 上 X=x、Y=y
- p_X,\ p_Y — X 與 Y 的邊際質量
- A\times B — 矩形事件：第一座標在 A 且第二座標在 B
- Q — 兩個邊際相乘得到的另一個 joint law





## 規則與來源


- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- 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）。
- 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。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。
- 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。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_joint_def · cited — 二維有限聯合分布列出互異值對(x,y)及非負精確質量，總和恰為1。邊際、矩形事件及單點質量都從同一joint law聚合。 · mko-finite-joint-distribution
- joint_event_sum · prerequisite — 有限 joint law (S,p) 給出事件機率：對 C⊆ℤ²，P((X,Y)∈C)=Σ_{s∈S∩C} p(s)；不在 S 中的值對質量為 0。這是機率公理對互斥單點事件的可加性。
- marginal_def · prerequisite — 邊際：p_X(x)=P(X=x)=Σ_{y:(x,y)∈S} p(x,y)，p_Y(y)=P(Y=y)=Σ_{x:(x,y)∈S} p(x,y)，即事件 {x}×ℤ 與 ℤ×{y} 的機率。
- finite_sum_regroup · prerequisite — 有限和重組：若有限集合 S 分割成兩兩不交的子集 S_1、S_2 等（每個元素恰屬其中一個），則 Σ_{s∈S} f(s) 等於各子集上的和再相加。
- L_product_law · lemma — 設 p_X 定義在有限整數集 S_X 上、p_Y 定義在有限整數集 S_Y 上，都是非負精確有理質量且各自總和恰為 1。則 Q(x,y)=p_X(x)p_Y(y) 在 S_X×S_Y 上是有限 joint law，且其兩個邊際恰為 p_X 與 p_Y。





## 逐步主鏈

S01 · definition操作前

\text{table }(S,p)

操作後

\text{(i) distinct pairs, (ii) } p(s)\ge 0 \text{ exact, (iii) } \sum_{s\in S}p(s)=1

條件：無

規則：mko_joint_def · 依賴：G1, G2

葉節點依據：mko_joint_def + def_unfold

依 MKO，一張表要成為二維有限聯合分布，必須同時滿足三項資格：(i) 列出的值對互異；(ii) 每個質量是非負的精確數；(iii) 質量總和恰好等於 1，不是近似等於 1。之後每一項都逐一核對，三項都通過之前不計算任何邊際或事件。



S02 · implies操作前

(0,0),\ (0,1),\ (1,0),\ (1,1),\ (2,1)

操作後

\text{five pairwise distinct pairs}

條件：無

規則：cartesian_product_def · 依賴：S01, G1, cartesian_product_def

葉節點依據：cartesian_product_def + case_analysis

兩個有序對相等必須兩個座標都相等。依第一座標分組：第一座標不同的兩對必然不同；第一座標為 0 的 (0,0)、(0,1) 第二座標不同；第一座標為 1 的 (1,0)、(1,1) 第二座標不同；第一座標為 2 的只有 (2,1)。所以 C(5,2)=10 組比較全部得到「不相等」，資格 (i) 成立。



S03 · implies操作前

p=\tfrac16,\ \tfrac13,\ \tfrac14,\ \tfrac1{12},\ \tfrac16

操作後

p(s)>0\ \text{for every } s\in S

條件：無

規則：order_basics · 依賴：S01, G1

葉節點依據：order_basics + frac_rules

每個質量都是兩個正整數的商，所以是正的精確有理數，特別是非負。資格 (ii) 成立；精確有理數也符合 MKO 假設 a1。



S04 · equivalent操作前

\sum_{s\in S}p(s)=\tfrac16+\tfrac13+\tfrac14+\tfrac1{12}+\tfrac16

操作後

\sum_{s\in S}p(s)=1

條件：無

規則：frac_rules · 依賴：S01, G1

葉節點依據：frac_rules + numeric_evaluation

用精確分數運算求總和（細節見 S04.1、S04.2）：結果恰為 1，資格 (iii) 成立。不能用四捨五入的小數代替。



S05 · implies操作前

\text{(i), (ii), (iii) checked}

操作後

(S,p)\ \text{is a finite joint law}

條件：無

規則：and_intro_elim · 依賴：S01, S02, S03, S04

葉節點依據：mko_joint_def + and_intro_elim

三項資格分別在 S02、S03、S04 成立，合取後依 S01 的定義，(S,p) 是二維有限聯合分布。從此可以由這一張表聚合任何事件的機率。



S06 · definition操作前

C\subseteq\mathbb{Z}^2

操作後

P((X,Y)\in C)=\sum_{s\in S\cap C}p(s)

條件：(S,p)\ \text{valid}

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

葉節點依據：joint_event_sum + prob_axioms

有效的 joint law 決定每個事件的機率：把事件中屬於支撐的值對質量相加；不在 S 中的值對貢獻 0。這是互斥單點事件的可加性。例如 C=ℤ² 時得到 S04 的總和 1，與 P(Ω)=1 一致。



S07 · implies操作前

p_X(x)=\sum_{y:(x,y)\in S}p(x,y)

操作後

p_X(0)=\tfrac12,\ p_X(1)=\tfrac13,\ p_X(2)=\tfrac16

條件：無

規則：marginal_def · 依賴：S06, marginal_def, G1

葉節點依據：marginal_def + joint_event_sum + frac_rules

X 的邊際是事件 {X=x}={x}×ℤ 的機率，依 S06 把該事件中支撐值對的質量相加。先列出每個 x 的值對（S07.1），再相加（S07.2）。



S08 · equivalent操作前

\sum_{x}p_X(x)=\sum_{x}\sum_{y:(x,y)\in S}p(x,y)

操作後

\sum_{x}p_X(x)=\sum_{s\in S}p(s)=1

條件：\text{the fibres }S\cap(\{x\}\times\mathbb{Z})\text{ partition }S

規則：finite_sum_regroup · 依賴：S04, S07.1, S07.2, finite_sum_regroup

葉節點依據：finite_sum_regroup + numeric_evaluation

S07.1 的三個集合分割 S，依有限和重組，三個邊際值相加等於整個支撐的質量和，即 1。這對任何有效的有限 joint law 都成立，不只這張表；本例的數值核對是 1/2+1/3+1/6=1。



S09 · implies操作前

p_Y(y)=\sum_{x:(x,y)\in S}p(x,y)

操作後

p_Y(0)=\tfrac{5}{12},\ p_Y(1)=\tfrac{7}{12}

條件：無

規則：marginal_def · 依賴：S06, marginal_def, G1

葉節點依據：marginal_def + joint_event_sum + frac_rules

依第二座標分組：Y=0 的值對是 (0,0)、(1,0)，質量和 2/12+3/12=5/12；Y=1 的值對是 (0,1)、(1,1)、(2,1)，質量和 4/12+1/12+2/12=7/12。兩者相加為 1，與 S08 同理的重組一致。



S10 · implies操作前

P(X\in A,\ Y\in B)=P((X,Y)\in A\times B)

操作後

P(X\in A,\ Y\in B)=\tfrac14

條件：無

規則：joint_event_sum · 依賴：S06, G3

葉節點依據：joint_event_sum + cartesian_product_def

矩形事件要求兩個座標同時落入指定集合，所以它是 A×B 這個值對集合的事件。依 S06，先求 S∩(A×B)（S10.1），再把質量相加（S10.2）。



S11 · implies操作前

P(X\in A)\,P(Y\in B)=\left(\tfrac13+\tfrac16\right)\tfrac{7}{12}

操作後

\tfrac{7}{24}\neq\tfrac{6}{24}=P(X\in A,\ Y\in B)

條件：無

規則：numeric_evaluation · 依賴：S07, S09, S10

葉節點依據：numeric_evaluation + frac_rules + prob_axioms

P(X∈A)=p_X(1)+p_X(2)=1/3+1/6=1/2（{X=1} 與 {X=2} 互斥），P(Y∈B)=p_Y(1)=7/12，乘積為 7/24；但 S10 算得的矩形機率是 1/4=6/24。所以對這個 joint law，矩形機率不是兩個邊際機率的乘積，必須由聯合表本身聚合。



S12 · implies操作前

P(X=2,\ Y=0)

操作後

0\neq\tfrac{5}{72}=p_X(2)\,p_Y(0)

條件：無

規則：joint_event_sum · 依賴：S06, S07, S09, G1

葉節點依據：joint_event_sum + finite_sum_rules + frac_rules

S 中第一座標為 2 的只有 (2,1)，所以 (2,0)∉S，事件 {(2,0)} 不含支撐值對，依 S06 其機率是空和 0。另一方面 p_X(2)p_Y(0)=(1/6)(5/12)=5/72>0。單點質量必須直接讀 joint law，不能由邊際相乘得到。



S13 · theorem_application操作前

p_X\ \text{on}\ \{0,1,2\},\ p_Y\ \text{on}\ \{0,1\}

操作後

Q(x,y)=p_X(x)\,p_Y(y)\ \text{is a finite joint law with marginals}\ p_X,\ p_Y

條件：p_X\ge 0,\ \sum_x p_X(x)=1; p_Y\ge 0,\ \sum_y p_Y(y)=1

規則：L_product_law · 依賴：S07, S08, S09

葉節點依據：L_product_law + numeric_evaluation

把引理 L_product_law 用在 S_X={0,1,2}、S_Y={0,1} 上；引理的前提由 S07、S08、S09 提供。Q 的六個質量是 Q(0,0)=5/24、Q(0,1)=7/24、Q(1,0)=5/36、Q(1,1)=7/36、Q(2,0)=5/72、Q(2,1)=7/72。引理本身在 S13.1 到 S13.3 一般地證明。



S14 · implies操作前

J(2,0)=0,\ Q(2,0)=\tfrac{5}{72}

操作後

J\neq Q\ \text{while}\ J,\ Q\ \text{have the same marginals}

條件：無

規則：function_def · 依賴：S07, S09, S12, S13

葉節點依據：function_def + exists_intro + quantifier_negation

把兩個 joint law 看成 ℤ² 上的質量函數（支撐外為 0）。原表 J 在 (2,0) 的質量是 0（S12），Q 在 (2,0) 的質量是 5/72，兩個函數在一點不同，所以 J≠Q。但兩者的邊際都是 p_X 與 p_Y（J 由 S07、S09，Q 由 S13）。一個反例就否定「兩個邊際決定聯合分布」這個全稱命題。







## 局部子步與引理

S04.1 · equivalent操作前

\tfrac16+\tfrac13+\tfrac14+\tfrac1{12}+\tfrac16

操作後

\tfrac{2}{12}+\tfrac{4}{12}+\tfrac{3}{12}+\tfrac{1}{12}+\tfrac{2}{12}

條件：k\neq 0

規則：frac_rules · 依賴：G1

葉節點依據：frac_rules

依 a/b=(ak)/(bk)（k≠0）把每個分數改寫成分母 12：1/6 取 k=2，1/3 取 k=4，1/4 取 k=3，1/12 取 k=1。每一項的值不變。



S04.2 · equivalent操作前

\tfrac{2}{12}+\tfrac{4}{12}+\tfrac{3}{12}+\tfrac{1}{12}+\tfrac{2}{12}

操作後

\tfrac{12}{12}=1

條件：12\neq 0

規則：frac_rules · 依賴：S04.1

葉節點依據：frac_rules + numeric_evaluation

同分母相加：a/c+b/c=(a+b)/c，分子 2+4+3+1+2=12，所以總和是 12/12=1。



S07.1 · equivalent操作前

S\cap(\{x\}\times\mathbb{Z}),\ x=0,1,2

操作後

\{(0,0),(0,1)\},\ \{(1,0),(1,1)\},\ \{(2,1)\}

條件：無

規則：set_operations_def · 依賴：G1, set_operations_def

葉節點依據：set_operations_def + set_extensionality

逐一檢查 S 的五個值對的第一座標，把它們放進對應的集合。每個值對恰屬一個集合，三個集合兩兩不交且聯集是 S。



S07.2 · equivalent操作前

p(0,0)+p(0,1),\ p(1,0)+p(1,1),\ p(2,1)

操作後

\tfrac12,\ \tfrac13,\ \tfrac16

條件：無

規則：frac_rules · 依賴：S07.1, G1

葉節點依據：frac_rules + numeric_evaluation

1/6+1/3=1/6+2/6=3/6=1/2；1/4+1/12=3/12+1/12=4/12=1/3；p(2,1)=1/6。



S10.1 · equivalent操作前

S\cap(A\times B)

操作後

\{(1,1),\ (2,1)\}

條件：無

規則：cartesian_product_def · 依賴：G1, G3, cartesian_product_def

葉節點依據：cartesian_product_def + set_operations_def + set_extensionality

逐一檢查：(0,0) 與 (0,1) 的 x=0∉A；(1,0) 的 y=0∉B；(1,1) 的 1∈A 且 1∈B；(2,1) 的 2∈A 且 1∈B。所以交集恰為 {(1,1),(2,1)}。



S10.2 · equivalent操作前

p(1,1)+p(2,1)

操作後

\tfrac{1}{12}+\tfrac{2}{12}=\tfrac14

條件：無

規則：frac_rules · 依賴：S10.1, G1

葉節點依據：frac_rules + numeric_evaluation

1/12+1/6=1/12+2/12=3/12=1/4。



S13.1 · implies操作前

Q(x,y)=p_X(x)\,p_Y(y),\ (x,y)\in S_X\times S_Y

操作後

\text{distinct pairs},\ Q(x,y)\ge 0\ \text{exact rational}

條件：p_X(x)\ge 0; p_Y(y)\ge 0

規則：cartesian_product_def · 依賴：cartesian_product_def, order_basics

葉節點依據：cartesian_product_def + order_basics + frac_rules

S_X×S_Y 的元素依第一、第二座標的選擇逐一列出，每個選擇給出一個不同的有序對，所以值對互異。兩個非負精確有理數的乘積仍是非負精確有理數。這給出 joint law 的資格 (i) 與 (ii)。



S13.2 · equivalent操作前

\sum_{x\in S_X}\sum_{y\in S_Y}p_X(x)\,p_Y(y)

操作後

\sum_{x\in S_X}p_X(x)\cdot\sum_{y\in S_Y}p_Y(y)=1\cdot 1=1

條件：\sum_x p_X(x)=1; \sum_y p_Y(y)=1

規則：distributive · 依賴：S13.1, finite_sum_rules, distributive, finite_sum_regroup

葉節點依據：distributive + finite_sum_rules + finite_sum_regroup + mul_one

依第一座標把 S_X×S_Y 上的和重組成兩層和；內層 Σ_y p_X(x)p_Y(y) 中 p_X(x) 是常數，可提出得 p_X(x)Σ_y p_Y(y)=p_X(x)·1；外層再相加得 Σ_x p_X(x)=1。資格 (iii) 成立。



S13.3 · equivalent操作前

\sum_{y\in S_Y}Q(x,y),\ \sum_{x\in S_X}Q(x,y)

操作後

p_X(x)\sum_{y}p_Y(y)=p_X(x),\ p_Y(y)\sum_{x}p_X(x)=p_Y(y)

條件：\sum_x p_X(x)=1; \sum_y p_Y(y)=1

規則：finite_sum_rules · 依賴：S13.1, finite_sum_rules, marginal_def

葉節點依據：finite_sum_rules + mul_one + marginal_def

Q 的 X 邊際是固定 x 後對 y 求和：常數 p_X(x) 提出，剩下 Σ_y p_Y(y)=1，所以等於 p_X(x)；Y 邊際同理等於 p_Y(y)。S13.1 到 S13.3 合起來證得引理 L_product_law。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S12, S13, function_def, exists_intro — 目標 G：邊際一般不能反推 joint law。足夠條件 H：存在兩個不同 joint law 有相同邊際；H⇒G 因為否定全稱只需一個反例。H 由 S12、S13 正向構造，沒有把 G 當作前提。
- S13.3 · inverse_equivalence · finite_sum_rules, mul_one — Σ c·a_i=c·Σ a_i 與乘以 1 都是等值改寫，雙向成立。此子步不使用 L_product_law。
- S13.2 · inverse_equivalence · distributive, finite_sum_rules, finite_sum_regroup — 提出常數因子與重組有限和都是等值改寫，可倒推；所用條件是兩個邊際各自總和為 1。此子步不使用 L_product_law。
- S13.1 · premise_audit · cartesian_product_def, order_basics — 非負乘非負得非負；不宣稱反向。此子步不使用 L_product_law。
- S13 · premise_audit · S07, S08, S09, L_product_law — 引理需要兩個邊際各自非負且總和為 1；S07 到 S09 已逐項確認。此步只建構 Q，不宣稱 Q 等於原來的 joint law。
- S12 · premise_audit · S06, S07, S09, G1 — 需要支撐列表完整（假設 a1）：正因為 (2,0) 沒被列出，它的質量才是 0。
- S11 · premise_audit · S07, S09, S10, numeric_evaluation — 只比較兩個精確數；此步只說這張表上兩者不等，不宣稱任何 joint law 都如此（乘積律 Q 上兩者相等）。
- S10.2 · inverse_equivalence · frac_rules, numeric_evaluation — 精確分數運算的等值改寫，雙向成立。
- S10.1 · inverse_equivalence · cartesian_product_def, set_extensionality — S 的五個值對都判定過，兩邊是同一個集合，雙向成立。
- S10 · premise_audit · S06, G3, cartesian_product_def — 需要「同時」：(x,y)∈A×B 當且僅當 x∈A 且 y∈B。若改成「或」就是另一個事件，結果也不同。
- S09 · premise_audit · S06, marginal_def — 要求每個 y 的值對列表完整：S 中第二座標為 0 的恰有兩對，為 1 的恰有三對，共五對，與 S 的大小相符。
- S08 · inverse_equivalence · finite_sum_regroup, S07.1 — 重組只改變有限和的分組，不改變其值；兩邊是同一個數，雙向成立。條件是分割：每個值對恰被算一次。
- S07.2 · inverse_equivalence · frac_rules, numeric_evaluation — 精確分數運算是等值改寫，左右兩邊是同樣的三個有理數。
- S07.1 · inverse_equivalence · set_operations_def, set_extensionality — 五個值對都已逐一判定，兩邊是同一個集合（逐元素相同），雙向成立。
- S07 · premise_audit · S06, marginal_def — 要求列出的值對是 S 與 {x}×ℤ 的完整交集；漏掉一對就會得到錯的邊際。不宣稱反向：由邊際不能還原這些值對的個別質量。
- S06 · premise_audit · S05, joint_event_sum, prob_axioms — 需要 S05：若質量和不是 1 或有負質量，所得的數就不是機率。此步是定義的使用，不推出其他事實。
- S05 · sufficient_goal_reduction · S01, S02, S03, S04, and_intro_elim — 目標 G：(S,p) 是有限 joint law。足夠條件 H：資格 (i)(ii)(iii) 同時成立；H⇒G 由定義。H 由 S02 到 S04 正向證成，沒有把 G 當作前提。
- S04.2 · inverse_equivalence · frac_rules, numeric_evaluation — 整數加法與同分母合併都是等值改寫，可逐步倒推。
- S04.1 · inverse_equivalence · frac_rules — 反向是約去同一個非零因數 k，回到原分數；兩邊逐項相等。
- S04 · inverse_equivalence · frac_rules, numeric_evaluation — 左右兩式表示同一個有理數，可由 S04.2 倒推回 S04.1 的形式，雙向成立。
- S03 · premise_audit · G1, order_basics — 只需逐一看五個質量的符號；正推出非負，反向不宣稱。
- S02 · premise_audit · G1, cartesian_product_def — 分組涵蓋全部 10 組比較，沒有遺漏；一個座標不同就足以推出兩對不同，不需要反向。
- S01 · premise_audit · G1, mko_joint_def — 此步只展開定義、列出要核的三項，不推出新事實。





## 錯誤控制與反例

兩張邊際表不是聯合分布MKO 指出的常見誤解是把兩個邊際表直接當聯合分布。本稿的 J 與 Q 有完全相同的邊際（1/2、1/3、1/6 與 5/12、7/12），但在 (2,0) 的質量一個是 0、一個是 5/72（S14）。邊際只是聯合表的聚合結果，聚合會丟失資訊，所以不能反推。

總和必須恰為 1若把質量換成三位小數 0.166、0.333、0.25、0.083、0.166，這些有限小數本身仍是精確有理數，但總和是 0.998，不是 1，所以這張表不合 MKO 的資格（iii）；若它們只是原質量的截斷近似，也不能當作原來的精確質量。S04 用原給定分數計算得到恰好 12/12=1。

矩形事件要兩座標同時成立P(X∈A, Y∈B) 是兩座標同時成立的事件，本例為 1/4。把它算成 P(X∈A)+P(Y∈B)−P(X∈A, Y∈B)=1/2+7/12−1/4=5/6 是「或」事件；算成 P(X∈A)P(Y∈B)=7/24 則是把邊際當成 joint law。兩者都不是矩形機率（S10、S11）。


- 兩個邊際相乘就得到聯合分布：P(X=x,Y=y)=p_X(x)p_Y(y) 對本表成立 → reject — 在 (2,0)：J 的質量是 0，而 p_X(2)p_Y(0)=5/72。
- 質量 0.166、0.333、0.25、0.083、0.166 的表是有效的有限聯合分布 → reject — 總和是 0.998≠1；MKO 要求總和恰為 1。
- P(X∈{1,2}, Y=1)=P(X∈{1,2})·P(Y=1)=7/24 → reject — 由 joint law 聚合得 1/12+1/6=1/4=6/24≠7/24。
- 把 (0,1) 列兩次、各給質量 1/6，仍是符合 MKO 的聯合表 → reject — MKO 要求支撐列出互異值對；重複列出的值對必須合併成一筆（質量 1/3）後才是合格的表。





## 結論與限制

(S,p) 是有效的二維有限聯合分布（值對互異、質量為正的精確有理數、總和恰為 1）。由同一 joint law 得 p_X(0)=1/2、p_X(1)=1/3、p_X(2)=1/6，p_Y(0)=5/12、p_Y(1)=7/12，矩形事件 P(X∈{1,2}, Y=1)=1/4，單點質量 P(X=2,Y=0)=0。乘積律 Q=p_X p_Y 有相同邊際但 Q(2,0)=5/72≠0，所以兩個邊際不能反推聯合分布。


- 有限和重組（finite_sum_regroup）與 joint_event_sum 是本稿的前提，不在本稿中由更基本的公理推出。
- N14、N15 是錯誤控制中反例數值的核對，只對這些數字有效。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 5b995a039b001aab1d5b78c71b0b7780f68598a4f9bf05748dd25e86da4430d9
- original source SHA-256: 5b995a039b001aab1d5b78c71b0b7780f68598a4f9bf05748dd25e86da4430d9
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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