有限狀態 Markov 鏈：核對行隨機矩陣，計算兩步時刻律與路徑機率

目標與範圍

狀態依序為 1、2、3，轉移矩陣 P 的行為 (1/2,1/2,0)、(1/4,1/2,1/4)、(0,1/3,2/3)，初始律 μ_0=(1/2,1/2,0)。(1) 核對 P 是行隨機矩陣，並說明列和不必為 1；(2) 證明一步公式 μ_{n+1}=μ_nP 且結果仍是機率向量，算出 μ_1 與 μ_2；(3) 證明路徑機率公式並計算 P(X_0=1,X_1=2,X_2=3)、P(X_0=2,X_1=3,X_2=3)；(4) 說明 P 單獨一般不能決定完整的無條件時刻律與路徑律。

只處理 G1 到 G3 指定的單一時間齊次有限轉移矩陣與初始律，只算有限步結果（MKO 假設 a1、a2）。不宣稱平穩分布、不可約、遍歷或長期收斂。不改動 canonical MKO 或其英文 edition。

已知條件與符號

• prob_axioms
• finite_sum_rules
• matrix_product_def
• distributive
• numeric_evaluation

• G1 — 狀態次序 (1,2,3)。P 的行：第 1 行 (1/2,1/2,0)、第 2 行 (1/4,1/2,1/4)、第 3 行 (0,1/3,2/3)；行為現在狀態、列為下一步狀態（MKO 假設 a1：精確有理數）。
• G2 — (X_n) 是以 P 為核、以 μ_0=(1/2,1/2,0) 為初始律的時間齊次 Markov 鏈（性質見前提規則 p_markov_property）。
• G3 — 比較用初始律 μ_0'=(0,0,1)，核不變。

• S=(1,2,3) — 固定次序的狀態
• P=(P_{ij}) — 轉移矩陣：行為現在、列為下一步
• \mu_n — 時刻 n 的分布（行向量）
• \mu_0=(\tfrac12,\tfrac12,0) — 初始律
• (X_n) — Markov 鏈
• \mu_0' — 比較用的另一個初始律 (0,0,1)

規則與來源

• prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。
• 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。
• matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• 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。
• 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）。
• 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。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_markov_def · cited — 獨立來源追加式勘誤（使用者已採用於本地修訂；未合併或發布）：固定狀態次序後，P 是每行非負且精確和為 1 的指定轉移核。在 Pr(X_n=i)>0 時，P_{ij} 才與比值定義的 Pr(X_{n+1}=j∣X_n=i) 相同；零機率狀態的核行仍可指定，但不由 0/0 決定。本輪只處理單一時間齊次有限轉移核；完整的無條件時刻律與路徑律另需初始分布。原始引文與 canonical MKO 保留。 · mko-finite-markov-chain
• p_markov_property · prerequisite — 以 P 為核、μ_0 為初始律的 Markov 鏈：P(X_0=i)=μ_0(i)；對每個 n、每個狀態 j，以及每個由 X_0 到 X_n 的取值所定義、機率為正且 X_n=i 的歷史事件 H，P(X_{n+1}=j∣H)=P_{ij}。特別地，P(X_n=i)>0 時 P(X_{n+1}=j∣X_n=i)=P_{ij}。
• p_cond_prob · prerequisite — 條件機率：P(B)>0 時 P(A∣B)=P(A∩B)/P(B)，因此 P(A∩B)=P(B)P(A∣B)。
• L_one_step · lemma — 對每個 n 與狀態 j：μ_{n+1}(j)=Σ_i μ_n(i)P_{ij}，即 μ_{n+1}=μ_nP（行向量乘矩陣）。
• L_prob_vector · lemma — 若 μ 是機率向量且 P 行隨機，則 μP 非負且分量和為 1。
• L_path · lemma — 對所有狀態 i_0、i_1、i_2：P(X_0=i_0,X_1=i_1,X_2=i_2)=μ_0(i_0)P_{i_0i_1}P_{i_1i_2}。

逐步主鏈

P=(P_{ij})_{i,j\in\{1,2,3\}}

P_{ij}\ge0,\quad \sum_jP_{ij}=1;\quad \Pr(X_n=i)>0\ \Longrightarrow\ P_{ij}=\Pr(X_{n+1}=j\mid X_n=i)

P_{ij}\in\{0,\tfrac14,\tfrac13,\tfrac12,\tfrac23\}

P_{ij}\ge0\ \text{for all nine entries}

\sum_jP_{1j},\ \sum_jP_{2j},\ \sum_jP_{3j}

1,\ 1,\ 1:\ P\ \text{is row-stochastic}

\sum_iP_{i1},\ \sum_iP_{i2},\ \sum_iP_{i3}

\tfrac34,\ \tfrac43,\ \tfrac{11}{12}\ \ (\text{not required to be}\ 1)

\mu_0=(\tfrac12,\tfrac12,0)

\mu_0\ge0,\ \ \tfrac12+\tfrac12+0=1

\mu_{n+1}(j)=P(X_{n+1}=j)

\sum_{i}\mu_n(i)P_{ij}\ \ (\mu_{n+1}=\mu_nP)

\mu_n\ \text{probability vector}

\mu_{n+1}=\mu_nP\ \text{probability vector}

\mu_1=\mu_0P

\mu_1=(\tfrac38,\ \tfrac12,\ \tfrac18)

\mu_2=\mu_1P

\mu_2=(\tfrac{5}{16},\ \tfrac{23}{48},\ \tfrac{5}{24})

P(X_0=i_0,X_1=i_1,X_2=i_2)

\mu_0(i_0)P_{i_0i_1}P_{i_1i_2}

P(X_0=1,X_1=2,X_2=3)

\tfrac12\cdot\tfrac12\cdot\tfrac14=\tfrac{1}{16}

P(X_0=2,X_1=3,X_2=3)

\tfrac12\cdot\tfrac14\cdot\tfrac23=\tfrac{1}{12}

P(X_0=1,X_1=3,X_2=j),\ P(X_0=3,X_1=i,X_2=j)

0\ \ (P_{13}=0,\ \mu_0(3)=0)

\mu_2(3)=\sum_{i_0,i_1}\mu_0(i_0)P_{i_0i_1}P_{i_13}

\tfrac{1}{16}+\tfrac{1}{16}+\tfrac{1}{12}=\tfrac{5}{24}

\mu_0'=(0,0,1)

\mu_0'P=(0,\tfrac13,\tfrac23)\neq\mu_1=(\tfrac38,\tfrac12,\tfrac18)

\text{S03 to S15}

P\ \text{row-stochastic};\ \mu_1,\mu_2;\ \text{path probabilities}\ \tfrac1{16},\ \tfrac1{12};\ \mu_0\ \text{required}

局部子步與引理

P_{11}+P_{12}+P_{13}

\tfrac12+\tfrac12+0=1

P_{21}+P_{22}+P_{23}

\tfrac14+\tfrac12+\tfrac14=1

P_{31}+P_{32}+P_{33}

0+\tfrac13+\tfrac23=1

P(X_{n+1}=j)

\sum_{i=1}^{3}P(X_n=i,\ X_{n+1}=j)

P(X_n=i,\ X_{n+1}=j)

\mu_n(i)P_{ij}

\sum_j\sum_i\mu(i)P_{ij}

\sum_i\mu(i)\sum_jP_{ij}=\sum_i\mu(i)\cdot1=1

P(X_0=i_0,X_1=i_1)

\mu_0(i_0)P_{i_0i_1}

P(X_0=i_0,X_1=i_1,X_2=i_2)

P(X_0=i_0,X_1=i_1)\,P_{i_1i_2}=\mu_0(i_0)P_{i_0i_1}P_{i_1i_2}

逐步反向審查

• S16 · premise_audit · S03, S09, S11, S12 — 只合取已證的有限步結論。
• S15 · premise_audit · L_one_step, G3 — 一個反例就否定「P 單獨決定時刻律」。
• S14 · inverse_equivalence · prob_axioms, L_path, numeric_evaluation — 兩種算法（逐步分布與路徑求和）給出同一個數；這是獨立的一致性核對，不是新的假設。
• S13 · premise_audit · L_path, mul_zero — 零因子推出乘積為零；逆否命題（乘積非零推出每個因子非零）也成立但此處不需要。
• S12 · inverse_equivalence · L_path, numeric_evaluation — 代入引理的精確計算。
• S11 · inverse_equivalence · L_path, numeric_evaluation — 代入引理的精確計算。
• S10.2 · inverse_equivalence · p_markov_property, p_cond_prob, S10.1 — 兩種情況下兩邊同值；P(H)=0 的情況必須單獨處理，因為條件機率不定義。
• S10.1 · inverse_equivalence · p_cond_prob, case_analysis — 與 S06.2 相同的兩種情況處理。
• S10 · premise_audit · L_path — 需要 Markov 性（G2）；若只知道每步的條件機率而不知歷史無關，乘法公式沒有根據。
• S09 · inverse_equivalence · L_one_step, numeric_evaluation — 精確有理數計算；總和為 1 是 S07 的獨立核對。
• S08 · inverse_equivalence · L_one_step, numeric_evaluation — 每個分量都是精確計算，可由 N9 到 N11 重算。
• S07.1 · inverse_equivalence · finite_sum_rules, distributive — 交換有限和與提出公因子都是恆等變形；最後一步用到行和條件。
• S07 · premise_audit · L_prob_vector, S03 — 需要行隨機；列和為 1 對這個結論既不必要也不充分。
• S06.2 · inverse_equivalence · p_cond_prob, p_markov_property, case_analysis — 兩邊在每種情況下都是同一個數；μ_n(i)=0 的情況不能用條件機率，必須另外處理。
• S06.1 · inverse_equivalence · prob_axioms, set_operations_def — 分割與可加性都是等式，雙向成立。
• S06 · premise_audit · L_one_step, matrix_product_def — 依矩陣乘法定義，(μP)_j=Σ_i μ(i)P_{ij}，與引理的和式一致；若誤寫成 Pμ（列向量），會用到列而不是行。
• S05 · premise_audit · prob_axioms, numeric_evaluation — 初始律與 P 是兩份獨立資料；P 合格不代表初始律已知（S15）。
• S04 · premise_audit · numeric_evaluation, S03 — 這一步只說明列和不在責任清單上；若把列和當行和，會誤判本矩陣不合格（MKO 指出的誤解）。
• S03.3 · inverse_equivalence · numeric_evaluation — 精確求值，可獨立重算。
• S03.2 · inverse_equivalence · numeric_evaluation — 精確求值，可獨立重算。
• S03.1 · inverse_equivalence · numeric_evaluation — 精確求值，可獨立重算。
• S03 · premise_audit · G1, finite_sum_rules, numeric_evaluation — 精確有理數求和；近似為 1 不算通過。
• S02 · premise_audit · G1, order_basics — 九格完整列舉；0 是允許的（表示不可能的轉移）。
• S01 · premise_audit · mko_markov_def — 行隨機要求作用於指定轉移核的每一行，列沒有對應要求。與比值條件機率的等同另需 Pr(X_n=i)>0；不能在零機率條件事件上作除法。

錯誤控制與反例

行和，不是列和

MKO 指出的誤解之一是把列和當行和。本例列和為 3/4、4/3、11/12，若誤用列和會錯誤地拒絕這個合法矩陣；反過來，一個列和都為 1 而某行和不為 1 的矩陣不是轉移矩陣。S07.1 的證明顯示，μP 仍是機率向量靠的正是行和為 1。

初始律與完整的無條件分布

MKO 的另一個誤解是在沒有初始律時聲稱時刻分布與路徑機率。S15 中同一個 P 配上 (1/2,1/2,0) 與 (0,0,1) 兩個初始律，得到不同的一步分布 (3/8,1/2,1/8) 與 (0,1/3,2/3)。P 給指定轉移核；完整無條件路徑律還要初始質量，但某些個別值可先確定，例如含 P_{13}=0 的路徑機率對任意初始律都是 0。

行向量乘在左邊，索引不要倒置

一步律是 μP：(μP)_j=Σ_i μ(i)P_{ij}，對行索引 i 求和。若誤算成 Pμ^T，就變成對列求和，例如第 1 分量會變成 1/2·1/2+1/2·1/2+0·0=1/2 而不是 3/8。路徑中的 P_{23} 是從 2 到 3，不是 P_{32}=1/3。

• P 的列和不是 1，所以 P 不是轉移矩陣 → reject — 資格條件是行非負且行和為 1（S02、S03）；列和沒有要求（S04）。
• 只要知道 P，就能算出 P(X_1=2) → reject — 初始律 (1/2,1/2,0) 給 1/2，初始律 (0,0,1) 給 1/3（S08、S15）。
• P(X_0=1,X_1=2,X_2=3)=P_{12}P_{23}=1/8 → reject — 漏了初始質量 μ_0(1)=1/2；正確值是 1/16（S11）。1/8 是條件機率 P(X_1=2,X_2=3∣X_0=1)。
• μ_1≠μ_0 且 μ_2≠μ_1，所以 μ_n 一定收斂到某個平穩分布 → reject — 有限步計算不能推出長期收斂；MKO 假設 a2 明示不宣稱平穩、遍歷或長期收斂。

結論與限制

P 的三行和皆為 1、元素非負，是行隨機矩陣；列和 3/4、4/3、11/12 不受限制。由 μ_{n+1}=μ_nP 得 μ_1=(3/8,1/2,1/8)、μ_2=(5/16,23/48,5/24)；路徑機率 P(X_0=1,X_1=2,X_2=3)=1/16、P(X_0=2,X_1=3,X_2=3)=1/12，與路徑求和交叉核對一致。換成初始律 (0,0,1) 會得到不同的 μ_1，所以時刻律需要初始律。

• S14 的 P² 交叉核對用到 (μ_0P)P=μ_0(P²)（矩陣乘法結合律），本稿未證明結合律；主要結論不依賴它。
• 狀態分類、平穩分布與首達時間（MKO 的 formal next）不在範圍內。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 6f5cd3a61fc98aa7b2e492e044393761f66e3b4905bd398b1b0096fd7ef4ca68
• original source SHA-256: 7bf7d81f8e1bef72de3c74bbacf391a9a6ee30e2667b8069d65cf1aa1f8f28c7
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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