The isothermal theorem of evolutionary graph theory for birth-death updating, kernel-checked in Lean 4: Moran fixation on strongly connected isothermal graphs and its stationary-selection generalization

We prove in Lean 4 (Mathlib) the sufficiency direction of the isothermal theorem of evolutionary graph theory for birth–death updating. A population sits on the nodes of a row-stochastic replacement matrix W; mutants have fitness r > 0, residents 1; a node is chosen to reproduce with probability proportional to its fitness (times a selection weight μi > 0) and its offspring replaces node j with probability Wij. If W is doubly stochastic (isothermal) and strongly connected and μ ≡ 1, then from every initial mutant set S the t-step probability of reaching the all-mutant configuration converges to the Moran value (1 − r−|S|)/(1 − r−n) (|S|/n if r = 1); for a single mutant at any node this is (1 − r−1)/(1 − r−n). The same limit is proved whenever μW = μ (stationary selection) and every proper non-empty set has an outgoing edge. Preregistration deviation. The preregistered wording ‘the number of mutants is a birth–death chain with ratio r’ is false as a Markov statement for the chain with holding. A kernel-checked counterexample on the isothermal 4-cycle (r = 2) shows that two configurations with two mutants each have increase probabilities 1/3 and 2/3. What is proved instead is the per-configuration forward bias P+(S) = r P−(S), from which S ↦ ρn(|S|) is harmonic for the configuration chain; the absorption limit follows from the kernel-checked absorption theorem of the earlier preprint doi:10.5281/zenodo.23653850 (P7), transported to the configuration space. Keller and Uğurlu (arXiv:2403.12598) state that the count of the Lieberman–Hauert–Nowak argument need not be Markovian; the per-configuration forward-bias route is that of Pattni, Broom, Rychtař and Silvers (arXiv:1505.06021, Lemma 1). Both citations were read through alphaXiv; Lieberman, Hauert and Nowak (Nature 433:312–316, 2005) was not read. Tier A (Lean 4.34.1, Mathlib; axioms within propext, Classical.choice, Quot.sound, together with a kernel replay (leanchecker) by an independent auditor and a grep for skipKernelTC/addDecl/native_decide/implemented_by, because #print axioms alone can be fooled by debug.skipKernelTC; planted sorry and planted-axiom controls caught). Kernel-checked controls: the complete graph lumps exactly onto the Moran chain; the star with stationary selection gives 4/7; the star with n = 3, r = 2 gives 5/12 (centre), 2/3 (leaf), 7/12 (uniform start), none equal to 4/7; the 4-cycle is not lumpable; the identity matrix (doubly stochastic but disconnected) never fixes. Not proved: the converse (Moran for all r implies isothermal), death–birth or other updating rules, non-row-stochastic weights, a path-measure formulation (‘fixation probability’ means the limit of the t-step kernel), and exact star values for n ≥ 4 (exact-rational Python numerics only, Tier X). No novelty is claimed for the mathematics (known results of 2005, 2015 and 2024); we are not aware of an earlier machine-checked formalization, but no systematic search was made. Biological relevance (amplifiers and suppressors of selection, structured tissues) is stated as interpretation only (Tier C); no biological data are used. Status. The Lean files were compiled by their producer AI agent and re-compiled at the paper stage by the same AI pipeline. An independent adversarial AI auditor (producer != verifier; not a human) then recompiled the EvoGraph and reused P7 modules from source into its own olean directory, re-ran #print axioms, ran a leanchecker kernel replay (rc 0, with a debug.skipKernelTC forgery control rejected), recomputed the star and 4-cycle values with an independent exact-rational script, and checked both cited sources; verdict ACCEPT_WITH_CORRECTIONS (papers/p3_isothermal_theorem/AUDIT.md; statement lock results/proposal3/2026-10-26/N4/STATEMENT_LOCK.json). There has been no human audit. The Elenchus ledger gate reports 0 blocking findings and 11 flags (exit code 1), one for each Tier A row whose statement adequacy no human has audited. Produced by AI agents (Claude) under the author's direction; the author is responsible for the content. Not peer reviewed.