有限 filtration：以分割細化核對資訊嵌套，並區分 adapted 與獨立

目標與範圍

在 Ω={0,1,2,3}（兩次擲幣：0=正正、1=正反、2=反正、3=反反）上，以分割編碼 P_0、P_1、P_2 表示時刻 0、1、2 的 σ 代數。證明「較晚分割細化較早分割 ⇔ σ 代數包含」，逐相鄰時刻完整核對，得出 (F_t) 是 filtration；給出不是 filtration 的分割序列；並證明 filtration 既不使每個過程 adapted，也不推出獨立。

只在 MKO 範圍內工作：所有分割使用同一樣本載體 0 到 3，每行的 label 只表示區塊等價（假設 a1）；細化逐相鄰時刻完整核對（假設 a2）。不宣稱 natural filtration、獨立或 Markov 性質；不處理 martingale；不改動 canonical MKO 或英文 edition。

已知條件與符號

• set_operations_def
• subset_def
• set_extensionality
• prob_axioms

• G1 — Ω={0,1,2,3}；結果的意義：0=正正、1=正反、2=反正、3=反反（只作說明，不影響分割的定義）。
• G2 — 分割編碼（依結果 0、1、2、3 給 label）：P_0=(a,a,a,a)、P_1=(a,a,b,b)、P_2=(a,b,c,d)；同一 label 表示同一區塊（MKO 假設 a1）。
• G3 — 定義：F_t=σ(P_t)；(F_t)_{t=0,1,2} 是 filtration，若 s≤t ⇒ F_s⊆F_t。P' 細化 P（記 P'⪯P），若 P' 的每個區塊都含於 P 的某個區塊。
• G4 — 對照序列：Q_0=(a,a,b,b)、Q_1=(a,b,a,b)。過程：X_1(ω)=1 若 ω∈{0,1}（第一次為正），否則 0；Y_1(ω)=1 若 ω∈{0,2}（第二次為正），否則 0。

• P_t — 時刻 t 的分割
• F_t=\sigma(P_t) — P_t 生成的 σ 代數（區塊的聯集）
• P'\preceq P — P' 細化 P：P' 的每個區塊含於 P 的某個區塊
• X_1,\ Y_1 — 第一次、第二次擲幣是否為正的指示函數
• Q_0,Q_1 — 不構成 filtration 的分割序列

規則與來源

• 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。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• 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_filtration_def · cited — 以同一有限樣本空間上的 partition 表示各時刻 sigma 代數。F_s 包含於 F_t 等價於較晚 partition 細化較早 partition。filtration 只表資訊嵌套，不自動使過程 adapted，也不宣稱 natural filtration、獨立或 Markov 性。 · mko-finite-filtration
• sigma_partition · prerequisite — 有限集合 Ω 的分割 𝒫 生成的 σ 代數 σ(𝒫) 恰由區塊的聯集組成（含 ∅）；共有 2^{|𝒫|} 個事件。
• meas_const · prerequisite — Ω 上的實函數為 σ(𝒫) 可測，當且僅當它在 𝒫 的每個區塊上為常數。
• L_refine_iff · lemma — 對同一有限 Ω 的分割 P、P'：P'⪯P ⇔ σ(P)⊆σ(P')。

逐步主鏈

P_0=(a,a,a,a),\ P_1=(a,a,b,b),\ P_2=(a,b,c,d)

P_0=\{\Omega\},\ P_1=\{\{0,1\},\{2,3\}\},\ P_2=\{\{0\},\{1\},\{2\},\{3\}\}

F_t=\sigma(P_t)

F_0=\{\varnothing,\Omega\},\ F_1=\{\varnothing,\{0,1\},\{2,3\},\Omega\},\ F_2=2^{\Omega}

P'\preceq P

\sigma(P)\subseteq\sigma(P')

P_1\ \text{vs}\ P_0

\{0,1\}\subseteq\Omega,\ \{2,3\}\subseteq\Omega:\ P_1\preceq P_0

P_2\ \text{vs}\ P_1

\{0\},\{1\}\subseteq\{0,1\},\ \{2\},\{3\}\subseteq\{2,3\}:\ P_2\preceq P_1

P_1\preceq P_0,\ P_2\preceq P_1

F_0\subseteq F_1\subseteq F_2,\ \text{so}\ (F_t)_{t=0,1,2}\ \text{is a filtration}

A=\{0,1,2\}

A\in F_2,\ A\notin F_1

Q_0=\{\{0,1\},\{2,3\}\},\ Q_1=\{\{0,2\},\{1,3\}\}

Q_1\not\preceq Q_0,\ \text{so}\ \sigma(Q_0)\not\subseteq\sigma(Q_1)

X_1=(1,1,0,0)\ \text{on}\ (0,1,2,3)

X_1\ F_1\text{-measurable}

Y_1=(1,0,1,0)\ \text{on}\ (0,1,2,3)

Y_1\ \text{not}\ F_1\text{-measurable}

P(\{0\})=P(\{3\})=\tfrac12,\ P(\{1\})=P(\{2\})=0

P(X_1=1,\,Y_1=1)=\tfrac12\neq\tfrac14=P(X_1=1)P(Y_1=1)

\text{S06, S08, S10, S11}

(F_t)\ \text{filtration};\ (\sigma(Q_t))\ \text{not};\ \text{adaptedness and independence not implied}

局部子步與引理

P'\preceq P,\ B\in P

B=\bigcup\{C\in P'\mid C\cap B\neq\varnothing\},\ \text{hence}\ \sigma(P)\subseteq\sigma(P')

\sigma(P)\subseteq\sigma(P'),\ C\in P',\ \omega\in C

C\subseteq B\ \text{for the block}\ B\in P\ \text{containing}\ \omega

逐步反向審查

• S12 · sufficient_goal_reduction · S06, S08, S10, S11 — 目標 G：本稿目標的四個結論。足夠條件 H：S06、S08、S10、S11；H⇒G 由合取。H 由 G1 到 G4 正向證成，沒有把 G 當作前提。
• S11 · premise_audit · S06, prob_axioms — 一個反例就足以否定「filtration 推出獨立」；不宣稱在其他機率下也不獨立。
• S10 · premise_audit · meas_const, S06 — adapted 是過程與 filtration 之間的另一個條件，必須另核（MKO 段落 2）；filtration 的存在不提供它。
• S09 · premise_audit · meas_const, S01 — 要逐區塊核對常數，這裡 2 個區塊都通過。
• S08 · premise_audit · G4, L_refine_iff — 一個不通過的區塊就足以否定細化；見證事件獨立地確認包含失敗。
• S07 · premise_audit · S02, sigma_partition — 只需找到一個被切開的區塊 {2,3}；不宣稱反向。
• S06 · premise_audit · S03, S04, S05, subset_def — 需要每一對相鄰時刻都通過；不宣稱這個 filtration 是某個過程的 natural filtration。
• S05 · premise_audit · S01, subset_def — 4 個區塊全部通過；任一失敗就不是細化。
• S04 · premise_audit · S01, subset_def — 細化要求 P_1 的每個區塊都通過；這裡 2 個都通過。
• S03.2 · premise_audit · G3, sigma_partition, subset_def — 關鍵是 P' 的區塊互斥，使 ω 所在的 P' 區塊唯一。
• S03.1 · premise_audit · G3, set_extensionality, sigma_partition — 用到 P' 覆蓋 Ω 與 P 的區塊互斥；只證一個方向。
• S03 · inverse_equivalence · L_refine_iff — 兩個方向分別在 S03.1、S03.2 證明；兩個分割必須在同一 Ω 上。
• S02 · inverse_equivalence · sigma_partition — 列出的集合正是區塊的全部聯集；雙向成立。
• S01 · inverse_equivalence · set_builder, G2 — 由區塊可重建一行 label（每區塊給一個新 label），且只差 label 改名；兩種表示決定同一分割。

錯誤控制與反例

任意分割序列不一定是 filtration

MKO 指出的誤解：把任意 partition 序列叫 filtration。Q_0、Q_1 都是同一 Ω 上的分割，但 Q_1 不細化 Q_0，{0,1} 在時刻 0 可判定、在時刻 1 卻不可判定（S08）。必須逐相鄰時刻完整核對每個區塊。

filtration 不推出 adapted、獨立或 Markov

MKO 的第二個誤解。S06 證明 (F_t) 是 filtration，但 Y_1 不是 F_1 可測（S10），且在 P({0})=P({3})=1/2 下擲幣不獨立（S11）。adapted 要逐過程另核；獨立與 Markov 依賴機率，filtration 的定義不含機率。

抽查事件不能證明包含

MKO 假設 a2：有限抽樣事件不足以證 σ 代數包含。對 Q 序列，事件 ∅ 與 Ω 都同時在 σ(Q_0) 與 σ(Q_1) 中，只抽這兩個會誤判包含成立；完整的區塊細化核對（S03 的引理）才是證書。

• σ(Q_0)、σ(Q_1) 都是同一 Ω 上的 σ 代數，所以 (σ(Q_0),σ(Q_1)) 是 filtration → reject — {0,1}∈σ(Q_0) 但不在 σ(Q_1)（S08）。
• (F_t) 是 filtration，所以第二次擲幣 Y_1 是 F_1 可測 → reject — Y_1 在區塊 {0,1} 上取 1 與 0（S10）。
• (F_t) 是 filtration，所以兩次擲幣獨立 → reject — P({0})=P({3})=1/2 時 P(兩次皆正)=1/2≠1/4（S11）。
• ∅、Ω 都屬於 σ(Q_1)，所以 σ(Q_0)⊆σ(Q_1) → reject — 包含要對 σ(Q_0) 的每個事件成立；{0,1} 失敗。
• 把 P_1 改寫成 (b,b,a,a) 就得到不同的分割與不同的 F_1 → reject — label 只表示區塊等價；區塊仍是 {0,1}、{2,3}（S01）。

結論與限制

對同一有限 Ω 的分割，較晚分割細化較早分割當且僅當 σ 代數包含。P_1 的 2 個區塊含於 Ω，P_2 的 4 個單點含於 P_1 的區塊，所以 F_0⊆F_1⊆F_2，(F_t) 是 filtration；Q_1 的區塊 {0,2} 不含於任何 Q_0 區塊，{0,1}∈σ(Q_0)∖σ(Q_1)，不是 filtration。第一次擲幣 X_1 是 F_1 可測，第二次擲幣 Y_1 不是；在 P({0})=P({3})=1/2 下兩次擲幣不獨立。filtration 只表示資訊嵌套。

• 本稿不宣稱 (F_t) 是某個過程的 natural filtration，也不處理 martingale（MKO 的下一步，需與條件期望一起加入）。

驗證及來源綁定

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

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

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