# Finite-state Markov chain: checking a row-stochastic matrix and computing two-step time laws and path probabilities

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-finite-markov-chain/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-finite-markov-chain-01 · production-20261019-adopted-96



## Goal and scope

The states are ordered 1, 2, 3; the transition matrix P has rows (1/2,1/2,0), (1/4,1/2,1/4), (0,1/3,2/3), and the initial law is μ_0=(1/2,1/2,0). (1) Check that P is row-stochastic and explain why column sums need not be 1; (2) prove the one-step formula μ_{n+1}=μ_nP and that the result is again a probability vector, and compute μ_1 and μ_2; (3) prove the path-probability formula and compute P(X_0=1,X_1=2,X_2=3) and P(X_0=2,X_1=3,X_2=3); (4) explain why P alone generally does not determine complete unconditional marginal and path laws.

Treats only the single time-homogeneous finite transition matrix and initial law of G1 to G3, computing finite-step outcomes only (MKO assumptions a1, a2). No stationary distribution, irreducibility, ergodicity or long-term convergence is asserted. The canonical MKO and its English edition are not changed.





## Givens and symbols


- prob_axioms
- finite_sum_rules
- matrix_product_def
- distributive
- numeric_evaluation


- G1 — State order (1,2,3). Rows of P: row 1 (1/2,1/2,0), row 2 (1/4,1/2,1/4), row 3 (0,1/3,2/3); rows are the current state and columns the next state (MKO assumption a1: exact rationals).
- G2 — (X_n) is a time-homogeneous Markov chain with kernel P and initial law μ_0=(1/2,1/2,0) (properties as in the prerequisite rule p_markov_property).
- G3 — Comparison initial law μ_0'=(0,0,1), with the same kernel.


- S=(1,2,3) — the states in fixed order
- P=(P_{ij}) — the transition matrix: rows current, columns next
- \mu_n — the law at time n (a row vector)
- \mu_0=(\tfrac12,\tfrac12,0) — the initial law
- (X_n) — the Markov chain
- \mu_0' — an alternative initial law (0,0,1) for comparison





## Rules and sources


- prob_axioms · prerequisite — Probability axioms: P(A)≥0; P(Ω)=1; the probability of a (countable) union of pairwise disjoint events is the sum of their probabilities. Hence P(∅)=0 and P(Aᶜ)=1−P(A).
- finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{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 — Matrix product: for A of size m×n and B of size n×p, (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}. Matrix multiplication is in general not commutative.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
- set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_markov_def · cited — Independent append-only source erratum (owner-adopted in this local revision; not merged or published): with a fixed state order, P is a prescribed transition kernel whose rows are nonnegative and sum exactly to 1. When Pr(X_n=i)>0, P_ij agrees with the ratio-defined Pr(X_(n+1)=j ∣ X_n=i). A kernel row at a null state can still be prescribed, but is not determined by 0/0. This slice uses a single finite time-homogeneous kernel; full unconditional marginal and path laws additionally require an initial distribution. The original citation and canonical MKO are retained. · mko-finite-markov-chain
- p_markov_property · prerequisite — A Markov chain with kernel P and initial law μ_0: P(X_0=i)=μ_0(i); for every n, every state j and every history event H, fixing the values of X_0 through X_n with X_n=i and P(H)>0, P(X_{n+1}=j∣H)=P_{ij}. In particular, P(X_{n+1}=j∣X_n=i)=P_{ij} whenever P(X_n=i)>0.
- p_cond_prob · prerequisite — Conditional probability: for P(B)>0, P(A∣B)=P(A∩B)/P(B), hence P(A∩B)=P(B)P(A∣B).
- L_one_step · lemma — For every n and state j: μ_{n+1}(j)=Σ_i μ_n(i)P_{ij}, that is μ_{n+1}=μ_nP (row vector times matrix).
- L_prob_vector · lemma — If μ is a probability vector and P is row-stochastic, then μP is nonnegative and its entries sum to 1.
- L_path · lemma — For all states 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}.





## Main derivation

S01 · definitionBefore

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

After

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)

Conditions: none

Rule: mko_markov_def · Uses: mko_markov_def, G1

Leaf basis: mko_markov_def + def_unfold

This adopted local revision fixes the state order (1,2,3) and treats P as the prescribed transition kernel: each row is nonnegative and sums exactly to 1. For a current state i of positive probability, row i can be identified with ratio-defined conditional probabilities. If Pr(X_n=i)=0 that ratio is undefined, although the model still prescribes the kernel row. Here μ_0(3)=0 and row 3 is fully supplied. The owner has adopted the definition correction in this append-only local revision, without rewriting the historical canonical MKO; the later S06 and S10 proofs already separate zero-mass cases.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: order_basics · Uses: G1, S01

Leaf basis: order_basics + numeric_evaluation

The nine entries take only the values 0, 1/4, 1/3, 1/2, 2/3, all nonnegative.



S03 · impliesBefore

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

After

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

Conditions: none

Rule: finite_sum_rules · Uses: G1, S01

Leaf basis: finite_sum_rules + numeric_evaluation

Sum the three rows one by one (S03.1 to S03.3); each equals 1 exactly. With S02, P is row-stochastic and may be used for step computations.



S04 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G1, S03

Leaf basis: numeric_evaluation + finite_sum_rules

The column sums are 1/2+1/4+0=3/4, 1/2+1/2+1/3=4/3 and 0+1/4+2/3=11/12 (N4 to N6), none equal to 1; their total 3 equals the number of rows. A column sum is not a conditional distribution and carries no requirement; P is still a valid transition matrix (merely not doubly stochastic).



S05 · impliesBefore

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

After

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

Conditions: none

Rule: prob_axioms · Uses: G2

Leaf basis: prob_axioms + numeric_evaluation

The three entries of the initial law are nonnegative and sum to 1 (N7), so μ_0 is a probability vector on {1,2,3}. The MKO notes that time laws and path probabilities need an initial law, so this is a required input for the computations from S08 on.



S06 · theorem_applicationBefore

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

After

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

Conditions: none

Rule: L_one_step · Uses: G2, L_one_step

Leaf basis: L_one_step + matrix_product_def

Lemma L_one_step (proved in S06.1, S06.2): the law at the next time is the current law (a row vector) multiplied on the right by P. This is the row-vector convention μP of MKO paragraph 1.



S07 · theorem_applicationBefore

\mu_n\ \text{probability vector}

After

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

Conditions: P\ \text{row-stochastic}

Rule: L_prob_vector · Uses: S03, S06, L_prob_vector

Leaf basis: L_prob_vector + finite_sum_rules

Lemma L_prob_vector (proved in S07.1): a probability vector times a row-stochastic matrix is again a probability vector. The proof uses row sums equal to 1, not column sums; this is why the qualification of S03 must precede any step computation.



S08 · equivalentBefore

\mu_1=\mu_0P

After

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

Conditions: none

Rule: L_one_step · Uses: S05, S06, G1

Leaf basis: L_one_step + numeric_evaluation

μ_1(1)=1/2·1/2+1/2·1/4+0·0=3/8 (N9); μ_1(2)=1/2·1/2+1/2·1/2+0·1/3=1/2 (N10); μ_1(3)=1/2·0+1/2·1/4+0·2/3=1/8 (N11). They sum to 1, consistent with S07.



S09 · equivalentBefore

\mu_2=\mu_1P

After

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

Conditions: none

Rule: L_one_step · Uses: S08, S06, G1

Leaf basis: L_one_step + numeric_evaluation + frac_rules

Apply L_one_step again: μ_2(1)=3/8·1/2+1/2·1/4+1/8·0=5/16 (N12); μ_2(2)=3/8·1/2+1/2·1/2+1/8·1/3=23/48 (N13); μ_2(3)=3/8·0+1/2·1/4+1/8·2/3=5/24 (N14). The sum is 15/48+23/48+10/48=1 (N15).



S10 · theorem_applicationBefore

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

After

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

Conditions: none

Rule: L_path · Uses: G2, L_path

Leaf basis: L_path + p_markov_property

Lemma L_path (proved in S10.1, S10.2): a finite path probability is the initial mass times the successive transition factors (MKO paragraph 2).



S11 · equivalentBefore

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

After

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

Conditions: none

Rule: L_path · Uses: S10, G1, G2

Leaf basis: L_path + numeric_evaluation

μ_0(1)=1/2, P_{12}=1/2, P_{23}=1/4, with product 1/16 (N16). Note that P_{23} is row 2, column 3 (from 2 to 3), not row 3, column 2.



S12 · equivalentBefore

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

After

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

Conditions: none

Rule: L_path · Uses: S10, G1, G2

Leaf basis: L_path + numeric_evaluation

μ_0(2)=1/2, P_{23}=1/4, P_{33}=2/3, with product 1/12 (N17).



S13 · impliesBefore

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

After

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

Conditions: none

Rule: L_path · Uses: S10, G1, G2

Leaf basis: L_path + mul_zero

P_{13}=0, so every path beginning 1→3 has probability 0; μ_0(3)=0, so every path starting at 3 has probability 0. A single zero factor in the product makes the path impossible.



S14 · equivalentBefore

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

After

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

Conditions: none

Rule: prob_axioms · Uses: S10, S09, G1

Leaf basis: prob_axioms + L_path + numeric_evaluation

Cross-check: {X_2=3} is partitioned by (X_0,X_1), so μ_2(3) is the sum of the probabilities of all paths ending at 3. The only nonzero ones are (1,2,3): 1/16, (2,2,3): 1/2·1/2·1/4=1/16, (2,3,3): 1/12; all others contain μ_0(3)=0 or P_{13}=0. The sum is 5/24 (N18), agreeing with S09. A check through P² also works: μ_2(3)=1/2·(P²)_{13}+1/2·(P²)_{23}=1/2·1/8+1/2·7/24=5/24 (N19).



S15 · impliesBefore

\mu_0'=(0,0,1)

After

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

Conditions: none

Rule: L_one_step · Uses: G3, S06, S08

Leaf basis: L_one_step + numeric_evaluation

With the same P but the initial law μ_0'=(0,0,1), the law after one step is row 3 of P, (0,1/3,2/3) (N20), which differs from μ_1 of S08. Thus P alone generally does not determine the complete unconditional marginal or path law. This does not make every individual probability undetermined: P_{13}=0 forces every path beginning 1→3 to have probability zero for all initial laws.



S16 · impliesBefore

\text{S03 to S15}

After

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

Conditions: none

Rule: and_intro_elim · Uses: S03, S08, S09, S11, S12, S15

Leaf basis: and_intro_elim

Summary: P is row-stochastic (column sums need not be 1); μ_1=(3/8,1/2,1/8) and μ_2=(5/16,23/48,5/24); the two path probabilities are 1/16 and 1/12; all of these need the initial law. No stationarity, irreducibility, ergodicity or long-term behaviour is asserted (MKO assumption a2).







## Substeps and lemmas

S03.1 · equivalentBefore

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

After

\tfrac12+\tfrac12+0=1

Conditions: none

Rule: numeric_evaluation · Uses: G1

Leaf basis: numeric_evaluation + frac_rules

Row 1: 1/2+1/2+0=1 (N1).



S03.2 · equivalentBefore

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

After

\tfrac14+\tfrac12+\tfrac14=1

Conditions: none

Rule: numeric_evaluation · Uses: G1

Leaf basis: numeric_evaluation + frac_rules

Row 2: 1/4+1/2+1/4=1 (N2).



S03.3 · equivalentBefore

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

After

0+\tfrac13+\tfrac23=1

Conditions: none

Rule: numeric_evaluation · Uses: G1

Leaf basis: numeric_evaluation + frac_rules

Row 3: 0+1/3+2/3=1 (N3).



S06.1 · equivalentBefore

P(X_{n+1}=j)

After

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

Conditions: none

Rule: prob_axioms · Uses: prob_axioms, finite_sum_rules

Leaf basis: prob_axioms + set_operations_def

The events {X_n=1}, {X_n=2}, {X_n=3} are pairwise disjoint with union the whole space, so {X_{n+1}=j} splits into three disjoint parts, and additivity of probability gives this sum.



S06.2 · equivalentBefore

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

After

\mu_n(i)P_{ij}

Conditions: none

Rule: p_cond_prob · Uses: S06.1, p_markov_property, p_cond_prob

Leaf basis: p_cond_prob + case_analysis + mul_zero

Two cases. If μ_n(i)>0: conditional probability gives P(X_n=i,X_{n+1}=j)=P(X_n=i)P(X_{n+1}=j∣X_n=i)=μ_n(i)P_{ij}. If μ_n(i)=0: the intersection lies inside {X_n=i}, so its probability is 0, and μ_n(i)P_{ij}=0 as well. Both cases give the same formula; substituting into S06.1 proves Lemma L_one_step.



S07.1 · equivalentBefore

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

After

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

Conditions: \sum_jP_{ij}=1

Rule: finite_sum_rules · Uses: finite_sum_rules, distributive

Leaf basis: finite_sum_rules + distributive + mul_one

A finite double sum may be summed in either order, and distributivity factors out μ(i): Σ_j Σ_i μ(i)P_{ij}=Σ_i μ(i)(Σ_j P_{ij}) (N8 checks this identity for this matrix). Each row sums to 1, so this equals Σ_i μ(i)=1. Nonnegativity: products and sums of nonnegative numbers are nonnegative. This proves Lemma L_prob_vector.



S10.1 · equivalentBefore

P(X_0=i_0,X_1=i_1)

After

\mu_0(i_0)P_{i_0i_1}

Conditions: none

Rule: p_cond_prob · Uses: p_markov_property, p_cond_prob

Leaf basis: p_cond_prob + case_analysis + mul_zero

If μ_0(i_0)>0: P(X_0=i_0,X_1=i_1)=P(X_0=i_0)P(X_1=i_1∣X_0=i_0)=μ_0(i_0)P_{i_0i_1}. If μ_0(i_0)=0: both sides are 0. This is the formula for two-point paths.



S10.2 · equivalentBefore

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

After

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}

Conditions: none

Rule: p_markov_property · Uses: S10.1, p_markov_property, p_cond_prob

Leaf basis: p_markov_property + p_cond_prob + case_analysis

Let H={X_0=i_0,X_1=i_1}. If P(H)>0: P(H∩{X_2=i_2})=P(H)P(X_2=i_2∣H), and the Markov property gives P(X_2=i_2∣H)=P_{i_1i_2} (depending only on the current state i_1). If P(H)=0: the three-point event lies inside H and has probability 0, and by S10.1 μ_0(i_0)P_{i_0i_1}=P(H)=0, so the formula also gives 0. Substituting S10.1 proves Lemma L_path.







## Reverse audits


- S16 · premise_audit · S03, S09, S11, S12 — Only conjoins finite-step conclusions already proved.
- S15 · premise_audit · L_one_step, G3 — One counterexample refutes 'P alone determines the time laws'.
- S14 · inverse_equivalence · prob_axioms, L_path, numeric_evaluation — Two methods (step-by-step laws and the path sum) give the same number; this is an independent consistency check, not a new assumption.
- S13 · premise_audit · L_path, mul_zero — A zero factor makes the product zero; the contrapositive (a nonzero product has nonzero factors) also holds but is not needed here.
- S12 · inverse_equivalence · L_path, numeric_evaluation — An exact computation substituting into the lemma.
- S11 · inverse_equivalence · L_path, numeric_evaluation — An exact computation substituting into the lemma.
- S10.2 · inverse_equivalence · p_markov_property, p_cond_prob, S10.1 — Both sides agree in both cases; the case P(H)=0 must be handled separately because the conditional probability is undefined.
- S10.1 · inverse_equivalence · p_cond_prob, case_analysis — The same two-case treatment as in S06.2.
- S10 · premise_audit · L_path — Needs the Markov property (G2); knowing each one-step conditional probability without independence from the past would not justify the product formula.
- S09 · inverse_equivalence · L_one_step, numeric_evaluation — Exact rational computation; the total of 1 is an independent check of S07.
- S08 · inverse_equivalence · L_one_step, numeric_evaluation — Each entry is an exact computation, recomputed by N9 to N11.
- S07.1 · inverse_equivalence · finite_sum_rules, distributive — Swapping finite sums and factoring are identities; the final step uses the row-sum condition.
- S07 · premise_audit · L_prob_vector, S03 — Needs row-stochasticity; column sums equal to 1 are neither necessary nor sufficient for this conclusion.
- S06.2 · inverse_equivalence · p_cond_prob, p_markov_property, case_analysis — Both sides are the same number in each case; the case μ_n(i)=0 cannot use conditional probability and is handled separately.
- S06.1 · inverse_equivalence · prob_axioms, set_operations_def — The partition and additivity are equalities, so the step holds both ways.
- S06 · premise_audit · L_one_step, matrix_product_def — By the definition of matrix product, (μP)_j=Σ_i μ(i)P_{ij}, which matches the sum in the lemma; writing Pμ (a column vector) by mistake would use columns instead of rows.
- S05 · premise_audit · prob_axioms, numeric_evaluation — The initial law and P are two independent pieces of data; a valid P does not mean the initial law is known (S15).
- S04 · premise_audit · numeric_evaluation, S03 — This step only shows that column sums are not among the obligations; mistaking column sums for row sums would wrongly reject this matrix (the misconception named by the MKO).
- S03.3 · inverse_equivalence · numeric_evaluation — Exact evaluation, independently recomputable.
- S03.2 · inverse_equivalence · numeric_evaluation — Exact evaluation, independently recomputable.
- S03.1 · inverse_equivalence · numeric_evaluation — Exact evaluation, independently recomputable.
- S03 · premise_audit · G1, finite_sum_rules, numeric_evaluation — Exact rational sums; being approximately 1 would not pass.
- S02 · premise_audit · G1, order_basics — All nine cells are enumerated; 0 is allowed (it marks an impossible transition).
- S01 · premise_audit · mko_markov_def — The row-stochastic requirements concern every prescribed kernel row, with no matching column requirement. Identification with a ratio conditional additionally needs Pr(X_n=i)>0; division at a null conditioning event is not allowed.





## Error controls and negative controls

Row sums, not column sumsOne misconception named by the MKO is to use column sums in place of row sums. Here the column sums are 3/4, 4/3, 11/12, so using them would wrongly reject this valid matrix; conversely, a matrix whose columns sum to 1 but some row does not is not a transition matrix. The proof of S07.1 shows that μP stays a probability vector precisely because rows sum to 1.

Initial laws and complete unconditional distributionsAnother misconception named by the MKO is to claim time laws and path probabilities without an initial law. In S15 the same P with initial laws (1/2,1/2,0) and (0,0,1) gives different one-step laws (3/8,1/2,1/8) and (0,1/3,2/3). P supplies the prescribed transition kernel. The full unconditional path law additionally needs initial mass, although some individual values are already fixed: every path product containing P_{13}=0 is zero for any initial law.

The row vector multiplies on the left; do not transpose indicesThe one-step law is μP: (μP)_j=Σ_i μ(i)P_{ij}, summing over the row index i. Computing Pμ^T by mistake sums along rows of P against μ, and the first entry would become 1/2·1/2+1/2·1/2+0·0=1/2 instead of 3/8. In a path, P_{23} means from 2 to 3, not P_{32}=1/3.


- The columns of P do not sum to 1, so P is not a transition matrix → reject — The qualification is nonnegative rows summing to 1 (S02, S03); there is no requirement on column sums (S04).
- Knowing P alone, one can compute P(X_1=2) → reject — The initial law (1/2,1/2,0) gives 1/2 while (0,0,1) gives 1/3 (S08, S15).
- P(X_0=1,X_1=2,X_2=3)=P_{12}P_{23}=1/8 → reject — The initial mass μ_0(1)=1/2 is missing; the correct value is 1/16 (S11). 1/8 is the conditional probability P(X_1=2,X_2=3∣X_0=1).
- μ_1≠μ_0 and μ_2≠μ_1, so μ_n must converge to some stationary distribution → reject — Finite-step computations do not imply long-term convergence; MKO assumption a2 explicitly asserts no stationarity, ergodicity or long-term convergence.





## Result and limitations

The three rows of P are nonnegative and sum to 1, so P is row-stochastic; the column sums 3/4, 4/3, 11/12 are unrestricted. From μ_{n+1}=μ_nP, μ_1=(3/8,1/2,1/8) and μ_2=(5/16,23/48,5/24); the path probabilities are P(X_0=1,X_1=2,X_2=3)=1/16 and P(X_0=2,X_1=3,X_2=3)=1/12, consistent with the path-sum cross-check. With the initial law (0,0,1) a different μ_1 results, so time laws require an initial law.


- The P² cross-check in S14 uses (μ_0P)P=μ_0(P²) (associativity of matrix multiplication), which is not proved here; the main conclusions do not depend on it.
- State classification, stationary distributions and first-passage times (the MKO's formal next) are out of scope.





## Verification and source binding

20 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-markov-chain-01.json)