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

目標與範圍

給定支撐 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。

逐步主鏈

\text{table }(S,p)

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

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

\text{five pairwise distinct pairs}

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

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

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

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

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

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

C\subseteq\mathbb{Z}^2

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

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

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

\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

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

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

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

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

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)

P(X=2,\ Y=0)

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

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

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

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

局部子步與引理

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

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

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

\tfrac{12}{12}=1

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

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

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

\tfrac12,\ \tfrac13,\ \tfrac16

S\cap(A\times B)

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

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

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

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}

\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_{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)

逐步反向審查

• 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、反控制與修訂記錄）