Markov chain convergence in Lean via taboo matrices + renewal theorem (no eigenvalues)

For a finite stochastic Matrix S S ℝ, define the taboo matrix Q := Matrix.of fun i j ↦ if j = x then 0 else P i j. The first-entrance decomposition is a pure telescoping identity: P^n = Q^n + ∑ k ∈ range n, Q^k * (P - Q) * P^(n-1-k), via Finset.sum_range_sub' on h k = Q^k * P^(n-k). Since P - Q only has column x, (A * (P - Q) * B) y x = (A * P) y x * B x x, and (Q^(n+1)) i x = 0 (pow_succ, Matrix.mul_apply). Row sums g_n of Q^n telescope to the first-passage probabilities, and reachability gives a block N with all row sums of Q^N ≤ 1 - c, hence g_n ≤ (1-c)^(n/N); summability of r^(n/N) via rpow: r^(n/N) ≤ (r^(1/N))^n * r⁻¹ using Nat.lt_div_mul_add and Real.rpow_le_rpow_of_exponent_ge. Then the discrete renewal theorem gives P^n(x,x) → 1/m_x, and the key renewal theorem gives P^n(y,x) → 1/m_x. About 450 lines; most of it compiled on the first or second try.