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
- 1SocrateAI Lab
Abstract
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<n r−k, i.e. (1−r−i)/(1−r−N) for r ≠ 1 and i/N for r = 1; the limit r → 1 of the closed form is proved as well. We also prove the Price equation for a finite population as an exact identity over any field and its haploid corollary Δw̄ = Varn(w)/w̄ (constant type fitnesses, no transmission bias). Every claim is filed in an Elenchus claim ledger with tiers A (kernel-checked Lean), L (cited literature, pinned to a page), C (human argument, not machine-checked) and X (floating-point exploration, which never supports a claim). Tier A (Lean 4.34.1, Mathlib only; axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls caught; kernel-checked positive and negative controls, including a Markov kernel that is absorbing and has a harmonic function yet never absorbs). The statements are limits of the n-step matrix power defined by the Chapman–Kolmogorov recursion. The identification of Pn(i,N) with the probability of reaching N by time n for a path measure is the standard definition of the n-step law and is not formalised (Tier C). The preregistered goal ‘Fisher’s theorem in the Price/Ewens partial-change reading’ was not achieved; only the haploid constant-fitness special case is proved. All results are classical textbook facts; no novelty or priority is claimed, and the novelty search was limited. Nothing depends on openai/math results (only Mathlib is used). Tier X: a new rusty-SUNDIALS crate (qf-popgen, not pushed) integrates the uniformised Kolmogorov equation with CVODE (BDF, exact Jacobian) behind a fail-closed absorption certificate (valid absorbing kernel, mass conservation, every component non-negative, decay of the interior mass, agreement with the target). 106 accepted runs (Moran N = 2–30, Wright–Fisher N = 10, 20) agree with the closed forms to at most 3.1e-10 and with scipy expm to at most 1.0e-13; 9 of 9 negative controls (flipped exponent, neutral value under selection, identity kernel, too-short horizon, corrupted row sum) are refused, and the smallest probability component seen in any accepted run is -4.6e-18. A small Lean module checks the arithmetic of the decimal literals against the exact closed form; it does not certify CVODE. Status: the Lean files were compiled by their producer agents, re-compiled at the paper stage by the same AI pipeline, and then recompiled from source in a separate build directory by an independent AI auditor with its own axiom audit and planted controls (verdict ACCEPT_WITH_CORRECTIONS, no blocking issue; the audit and the list of corrections applied are in the paper directory as AUDIT.md and REVISION.md). The auditor is an AI of the same model family as the producer, so this is not a human audit: no human has audited the statements or the hand proofs. The Elenchus ledger gate reports 0 blocking findings and 14 flags (exit code 1), one for each Tier A row whose statement adequacy no human has audited. The work was produced by AI agents (Claude) under the author's direction; the author is responsible for the content. Not peer reviewed.
Related
- Absorption probabilities of random walks without symmetry or general position
- Ornstein--Uhlenbeck spirals: Absorption Probabilities and Conic Intrinsic Volumes
- Absorption Probabilities for Brownian Convex Hulls in Arbitrary Dimension
- Sharp regularity and small ball probabilities for the stochastic heat equation on bounded domains
- Classification of radially symmetric solutions to a Hardy-Hénon equation with sublinear absorption and applications
BibTeX
@misc{callens2026fixation,
title = {{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}},
author = {Xavier Callens},
howpublished = {Zenodo (CERN European Organization for Nuclear Research)},
year = {2026},
month = oct,
doi = {10.5281/zenodo.23653849},
url = {https://doi.org/10.5281/zenodo.23653849},
note = {CC BY},
}
RIS
TY - UNPB
TI - 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
AU - Xavier Callens
PY - 2026
DA - 2026/10/26
PB - Zenodo (CERN European Organization for Nuclear Research)
DO - 10.5281/zenodo.23653849
UR - https://doi.org/10.5281/zenodo.23653849
AB - 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<n r−k, i.e. (1−r−i)/(1−r−N) for r ≠ 1 and i/N for r = 1; the limit r → 1 of the closed form is proved as well. We also prove the Price equation for a finite population as an exact identity over any field and its haploid corollary Δw̄ = Varn(w)/w̄ (constant type fitnesses, no transmission bias). Every claim is filed in an Elenchus claim ledger with tiers A (kernel-checked Lean), L (cited literature, pinned to a page), C (human argument, not machine-checked) and X (floating-point exploration, which never supports a claim). Tier A (Lean 4.34.1, Mathlib only; axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls caught; kernel-checked positive and negative controls, including a Markov kernel that is absorbing and has a harmonic function yet never absorbs). The statements are limits of the n-step matrix power defined by the Chapman–Kolmogorov recursion. The identification of Pn(i,N) with the probability of reaching N by time n for a path measure is the standard definition of the n-step law and is not formalised (Tier C). The preregistered goal ‘Fisher’s theorem in the Price/Ewens partial-change reading’ was not achieved; only the haploid constant-fitness special case is proved. All results are classical textbook facts; no novelty or priority is claimed, and the novelty search was limited. Nothing depends on openai/math results (only Mathlib is used). Tier X: a new rusty-SUNDIALS crate (qf-popgen, not pushed) integrates the uniformised Kolmogorov equation with CVODE (BDF, exact Jacobian) behind a fail-closed absorption certificate (valid absorbing kernel, mass conservation, every component non-negative, decay of the interior mass, agreement with the target). 106 accepted runs (Moran N = 2–30, Wright–Fisher N = 10, 20) agree with the closed forms to at most 3.1e-10 and with scipy expm to at most 1.0e-13; 9 of 9 negative controls (flipped exponent, neutral value under selection, identity kernel, too-short horizon, corrupted row sum) are refused, and the smallest probability component seen in any accepted run is -4.6e-18. A small Lean module checks the arithmetic of the decimal literals against the exact closed form; it does not certify CVODE. Status: the Lean files were compiled by their producer agents, re-compiled at the paper stage by the same AI pipeline, and then recompiled from source in a separate build directory by an independent AI auditor with its own axiom audit and planted controls (verdict ACCEPT_WITH_CORRECTIONS, no blocking issue; the audit and the list of corrections applied are in the paper directory as AUDIT.md and REVISION.md). The auditor is an AI of the same model family as the producer, so this is not a human audit: no human has audited the statements or the hand proofs. The Elenchus ledger gate reports 0 blocking findings and 14 flags (exit code 1), one for each Tier A row whose statement adequacy no human has audited. The work was produced by AI agents (Claude) under the author's direction; the author is responsible for the content. Not peer reviewed.
ER -