Fixation probabilities as absorption limits of matrix powers, kernel-checked: neutral Wright-Fisher, the Moran model with selection, the Price equation, and a fail-closed CVODE certificate

For a stochastic kernel P on {0,…,N} with absorbing ends we prove in Lean 4 that the n-step probability Pn(i,N) converges to h(i), and Pn(i,0) to 1−h(i), whenever h is harmonic at the interior states with boundary values 0 and 1 and the one-step variance of h is positive at every interior state (a second-moment argument; uniqueness of h follows from uniqueness of limits). One theorem covers two models: neutral Wright–Fisher, Pn(i,N) → i/N (closing a gap recorded in an earlier module, which proved only uniqueness of the harmonic function), and the Moran process with fitness r > 0, Pn(i,N) → Si/SN with Sn = ∑k