# 四原子檢測模型的Bayes反轉 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-bayes-theorem/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-bayes-theorem-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 由完整joint law算prior、likelihood與posterior。 合成有限模型，不作醫療或因果推論。 ## 已知條件與符號 - work - G1 — Ω={D+,D-,N+,N-}的質量依序為1/20、1/20、9/100、81/100；D={D+,D-}，N為D補集，E={D+,N+}。 - D,N — 互斥假設事件 - E — evidence事件 ## 規則與來源 - mko_definition · cited — 完整有限原子law上用精確有理質量。二事件與partition形式都核正conditioning denominator；partition必須互斥且exhaustive，total probability得到的evidence mass也須正。Bayes不表示因果。 · mko-bayes-theorem - work · prerequisite — 正分母下P(A|B)=P(A∩B)/P(B)；完整互斥partition可用有限可加性求全機率。 ## 逐步主鏈 S01 · implies操作前 1/20+1/20+9/100+81/100 操作後 1 條件：無 規則：work · 依賴：G1, work 葉節點依據：work 先確認四原子law非負且歸一。 S02 · implies操作前 D\cap N=\varnothing,\quad D\cup N=\Omega 操作後 P(D)=1/10,\quad P(N)=9/10 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work D、N形成完整互斥partition，prior皆正。 S03 · implies操作前 P(E\cap D)=1/20 操作後 P(E\mid D)=(1/20)/(1/10)=1/2 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 以D質量正規化得到第一個likelihood。 S04 · implies操作前 P(E\cap N)=9/100 操作後 P(E\mid N)=(9/100)/(9/10)=1/10 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work 第二partition cell也算完likelihood。 S05 · implies操作前 P(E)=P(E\mid D)P(D)+P(E\mid N)P(N) 操作後 P(E)=1/20+9/100=7/50>0 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work 完整partition的全機率和給evidence分母。 S06 · implies操作前 P(D\mid E)=P(D\cap E)/P(E) 操作後 P(D\mid E)=(1/20)/(7/50)=5/14 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 同一intersection配上新的conditioning分母完成反轉。 S07 · implies操作前 P(N\mid E)=(9/100)/(7/50) 操作後 P(N\mid E)=9/14,\quad5/14+9/14=1 條件：無 規則：work · 依賴：G1, S06, work 葉節點依據：work 列完全部posterior並檢查歸一。 S08 · implies操作前 P(E\mid D)P(D)/P(E) 操作後 \frac{(1/2)(1/10)}{7/50}=5/14 條件：無 規則：work · 依賴：G1, S07, work 葉節點依據：work 以Bayes乘積形式交叉核對直接joint商。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S07, work — 結果只描述條件law，不識別因果效果。 - S07 · premise_audit · G1, S06, work — posterior總和核對依同一evidence事件。 - S06 · premise_audit · G1, S05, work — 5/14與likelihood1/2不同，方向沒有交換成等號。 - S05 · premise_audit · G1, S04, work — 兩項皆保留prior，且正性已核。 - S04 · premise_audit · G1, S03, work — N的prior是9/10，不能誤用D的1/10。 - S03 · premise_audit · G1, S02, work — 分母1/10嚴格正，商有定義。 - S02 · premise_audit · G1, S01, work — partition是由原子集合驗證，非假設獨立。 - S01 · premise_audit · G1, work — 不得只列陽性事件而漏陰性質量。 ## 錯誤控制與反例 完整partition先核D與N互斥且窮盡，再使用全機率。 方向以相同joint分子、不同正分母區分兩種條件機率。 - P(D|E)=P(E|D)=1/2。 → reject — 完整prior與evidence給5/14。 - posterior正比likelihood而不必prior。 → reject — 此處prior1/10與9/10不同，省略會改結果。 - 可在P(E)=0時照算Bayes商。 → reject — conditioning分母必須嚴格正。 ## 結論與限制 P(D|E)=5/14，P(N|E)=9/14；這不是因果結論。 ## 驗證及來源綁定 3 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 7e8ec8d8f62c0d717ec5d6930e0b5c893570e5fc01e96107d2673d7011ee5d2a - original source SHA-256: 74781eca7056072aa2c5331410f123e33209127243c5a4c6fb42825494c246dd - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-bayes-theorem-01.json)