# 兩次公平擲幣的完整鞅檢查

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

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

derivation-mko-martingale-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

在同一空間逐時核鞅的全部責任。

只處理時間0、1、2；不使用停止或收斂定理。





## 已知條件與符號


- work


- G1 — Ω={HH,HT,TH,TT}，每原子質量1/4，σ代數為冪集。
- G2 — P0={Ω}；P1={{HH,HT},{TH,TT}}；P2為四個singleton。F_t=σ(P_t)。
- G3 — 依上述原子順序，X0=(0,0,0,0)，X1=(1,1,-1,-1)，X2=(2,0,0,-2)。


- Ω — 完整樣本空間
- P_t — 資訊partition
- X_t — 時刻t值





## 規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。


- mko_definition · cited — 在共同有限機率空間上完整核filtration nesting、adaptedness、可積性及每個t的E[X_{t+1}|F_t]=X_t。零質量資訊block只a.s.決定；不推出獨立增量、Markov、optional stopping或收斂。 · mko-martingale
- work · prerequisite — 有限partition生成σ代數；適應表示在每時刻資訊塊上常數；正質量塊條件平均為加權和除塊質量。





## 逐步主鏈

S01 · implies操作前

p_\omega=1/4

操作後

\sum_{\omega\in\Omega}p_\omega=1

條件：無

規則：work · 依賴：G1, G2, G3, work

葉節點依據：work

四個非負質量總和一，三個變數共享這個law。



S02 · implies操作前

\mathcal P_0,\mathcal P_1,\mathcal P_2

操作後

\mathcal F_0\subseteq\mathcal F_1\subseteq\mathcal F_2

條件：無

規則：work · 依賴：G1, G2, G3, S01, work

葉節點依據：work

P1每塊包含於Ω，P2每singleton包含於一個P1塊，故資訊嵌套。



S03 · implies操作前

X_t\big|_B\quad(B\in\mathcal P_t)

操作後

X_t\text{ is }\mathcal F_t\text{-measurable}\quad(t=0,1,2)

條件：無

規則：work · 依賴：G1, G2, G3, S02, work

葉節點依據：work

X0全域常數，X1在兩塊各為1與-1，X2在singleton可測。



S04 · implies操作前

E|X_0|,E|X_1|,E|X_2|

操作後

(E|X_0|,E|X_1|,E|X_2|)=(0,1,1)

條件：無

規則：work · 依賴：G1, G2, G3, S03, work

葉節點依據：work

直接四原子加權，三個絕對期望有限。



S05 · implies操作前

E[X_1\mid\Omega]

操作後

(1+1-1-1)/4=0=X_0

條件：無

規則：work · 依賴：G1, G2, G3, S04, work

葉節點依據：work

t=0只有一個正質量資訊塊，下一值條件平均等於目前值。



S06 · implies操作前

E[X_2\mid\{HH,HT\}]

操作後

\frac{2/4+0/4}{1/2}=1=X_1\big|_{\{HH,HT\}}

條件：無

規則：work · 依賴：G1, G2, G3, S05, work

葉節點依據：work

在第一個P1塊，以該塊質量1/2重新正規化。



S07 · implies操作前

E[X_2\mid\{TH,TT\}]

操作後

\frac{0/4-2/4}{1/2}=-1=X_1\big|_{\{TH,TT\}}

條件：無

規則：work · 依賴：G1, G2, G3, S06, work

葉節點依據：work

第二塊也核對，不能只檢查正分支。



S08 · implies操作前

\text{nesting, adaptedness, integrability, both time equations}

操作後

(X_t,\mathcal F_t)_{t=0}^{2}\text{ is a martingale}

條件：無

規則：mko_definition · 依賴：G1, G2, G3, S07, mko_definition

葉節點依據：mko_definition

所有t=0、1的條件期望等式及前置資格均已完成。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, G2, G3, S07, mko_definition — 結論只綁這三時刻；零質量塊的一般值僅a.s.決定。
- S07 · premise_audit · G1, G2, G3, S06, work — 兩個P1塊互斥且覆蓋Ω，因此沒有遺漏條件情況。
- S06 · premise_audit · G1, G2, G3, S05, work — 直接用未除1/2的分子會錯得1/2。
- S05 · premise_audit · G1, G2, G3, S04, work — 分母是P(Ω)=1，且已使用全部四原子。
- S04 · premise_audit · G1, G2, G3, S03, work — 負值先取絕對值，不能用期望相消冒充可積。
- S03 · premise_audit · G1, G2, G3, S02, work — 若X1在HH與HT不同，這一步就失敗。
- S02 · premise_audit · G1, G2, G3, S01, work — 反查每個細塊都有唯一母塊，沒有交叉分割。
- S01 · premise_audit · G1, G2, G3, work — 不得把不同時刻的邊際law拼成共同空間。





## 錯誤控制與反例

共同空間每一表均使用HH、HT、TH、TT同順序。

逐塊檢查t=1兩塊都除以1/2；不以總期望代替。


- 只要三時刻期望都零就足夠。 → reject — 仍須核適應與每個資訊塊的條件平均。
- 第一塊條件平均為1/2。 → reject — 那是未正規化的分子，還須除塊質量1/2。
- 任意零質量塊必有唯一條件值。 → reject — 零分母不定義商；版本只在a.s.意義唯一。





## 結論與限制

此有限過程是相對F0⊆F1⊆F2的鞅。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 3e4962dc9cb35d34a2042159a6a6d4be004e5b0186957eb56a98adc6741ea543
- original source SHA-256: 641e4e51f6819b6df72016d7daa4b23f5fb3f6e935cefe065795b2f2fedfc3c4
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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