No connected graph with at most ten vertices is an unweighted death-Birth amplifier of weak selection: an exhaustive census, and a Lean check that Richter's eleven-vertex graph is one

For death-Birth (dB) updating on a connected, simple, unweighted graph with N vertices, Allen et al. showed that the fixation probability of a single mutant of fitness 1 + δ is 1/N + δ(Neff − 2)/(2N) + O(δ2), and called the graph an amplifier of weak selection if Neff > N. We enumerated every connected graph with 3 ≤ N ≤ 10 (2, 6, 21, 112, 853, 11,117, 261,080 and 11,716,571 graphs) with nauty geng (counts equal to OEIS A001349) and found none with Neff > N: every regular graph has Neff = N exactly and every other graph has Neff < N; the closest non-regular graph at N = 10 lies at least 0.0207 below N, and the closest graphs are always nearly complete (KN minus an edge, or minus a maximum matching). In Lean 4 we check that on Richter's eleven-vertex graph every rational solution of Allen's coalescence system has Neff = 2668552698098/242579025123 ≈ 11.000756 > 11. Within the weak-selection criterion for unweighted graphs, the smallest dB amplifier therefore has exactly 11 vertices. The paper includes a step-by-step account for readers outside evolutionary graph theory. Tier split. Tier A (Lean 4.34.1, Mathlib; axioms within propext, Classical.choice, Quot.sound): the theorem R11_amplifier, the uniqueness theorem eq5_unique (a positive solution of the system is the only solution), the isothermal control P11_isothermal (Neff = 11 on the quartic parent), and kernel-decided negative controls (a perturbed certificate and a wrong graph are rejected; a planted sorry and a planted axiom are caught by the axiom audit). Tier L: Allen's criterion and coalescence equations, and the step from Neff > N to amplification near r = 1 (their eq. (8)); taken as stated, not re-proved. Tier C: the census (enumeration completeness rests on geng and the OEIS count; floating-point proposals are decided by an exact integer residual bound that uses the non-negativity of the inverse of I − M; the regular graphs are solved exactly with rational arithmetic) and exact-rational sign certificates for the fixation-probability difference against K11 at four values of r (and a certified sign change in [1.00082333, 1.00082349]); the census is not kernel-checked. Tier X: finite-r numerics beyond the certified points. Controls. Positive: complete graphs, cycles and all 1, 2, 2, 5, 4, 17, 22, 167 connected regular graphs (counts equal OEIS A005177) have Neff = N; stars have Neff = 4n/(n+1); the exact-chain slope equals (Neff − 2)/(2N) on all graphs with N ≤ 6; Richter's N = 11 and cubic N = 12 values reproduced to the printed digits. Negative: Allen's eq. (3) for the cycle as printed in arXiv v1 disagrees with the exact chain in 25 of 25 cases while three other sources agree with it; the published PLoS version prints the correct form, so this is a v1 misprint, not an open discrepancy; a planted wrong random walk and the complete graph are rejected. Two discrepancies with Richter remain unexplained: his printed τmax values (17.6997 vs 17.69069 here; the independent audit confirmed ours and ruled out the perturbed-graph explanation) and his rmax ≈ 1.00075, which is inconsistent with our certified signs (+ at 1.0007 to 1.0008125; bracket [1.00082333, 1.00082349]), while Neff agrees. What this is NOT. This is mathematics of graphs and of fixation probabilities in a Moran-type model. It is not a statement about real tumours, tissues, patients or any medical application, and nothing here bears on diagnosis or treatment. Limitations. To our knowledge there is no prior exhaustive N ≤ 10 death-Birth weak-selection statement: the auditor's alphaXiv searches and its reading of ten papers found none (Richter's ref. [6] is Allen et al. 2021, PLoS Comput. Biol. 17:e1008695, exhaustive for Birth-death only), but this is a search result, not a priority claim; unweighted graphs, dB updating, uniform initialisation and the first-order criterion only; the finite-r checks are not a proof for all r near 1; an independent AI audit (ACCEPT_WITH_CORRECTIONS) exists but no human audit and no statement lock; repository guards were not run; the tissue-like (r, d) plane of the preregistration was not attempted. Status. Produced by AI agents (Claude) under the author's direction; the author is responsible for the content. Independently audited by an AI audit agent (producer != verifier, 2026-10-27): verdict ACCEPT_WITH_CORRECTIONS, nothing blocking, corrections applied in this v1; the audit recompiled the Lean modules (oleans byte-identical), replayed the kernel with leanchecker on Core, DataR11, DataP11, Richter11 and Controls (rc 0), rechecked the census with a different exact method (all graphs N = 3..9, a 20,177-graph sample at N = 10) and reproduced the finite-r signs. No human audit; no statement lock. The Elenchus ledger gate exits with code 1 (0 blocking findings, 4 flags LEDGER_UNAUDITED_TIER_A, one per Tier A row).