← All Papers · Formal Verification

Spectral Bridges in Population Genetics

Tamás Nagy, Ph.D. Short Draft Formal Verification Lean-Verified
Mathematics verified. Core theorems are machine-checked in Lean 4. Prose and presentation may not have been human-reviewed.
View in Graph BibTeX

Abstract

We establish precise spectral relationships between three foundational models in population genetics: the Wright-Fisher diffusion (forward-time allele frequency dynamics), the coalescent process (backward-time genealogical structure), and gene regulatory networks (equilibrium stability analysis). Our central result is a spectral duality theorem: the Wright-Fisher generator eigenvalues at zero mutation exactly equal the coalescent merger rates. Mutation shifts this spectrum by a linear term. When Wright-Fisher and GRN spectral gaps are matched, the Wright-Fisher eigenvalues exceed the GRN eigenvalues by precisely \((n-1)(n-2)/2\) for \(n \geq 3\), revealing a quadratic-versus-linear growth dichotomy. This dichotomy has implications for spectral truncation accuracy: Wright-Fisher and coalescent processes (quadratic eigenvalue growth) require \(O(\sqrt{L})\) modes for accuracy \(L\), while GRN dynamics (linear growth) require \(O(L)\) modes. All results are formally verified in the Platonic proof system (24 theorems, 0 axioms). The framework provides a unified spectral language for comparing models across population genetics.

Keywords: Wright-Fisher diffusion, coalescent theory, gene regulatory networks, spectral analysis, eigenvalue duality, formal verification

MSC 2020: 92D10, 92D25, 60J70, 15A18

Length
1,832 words
Claims
9 theorems
Status
draft
Target
Journal of Mathematical Biology

Browse all Formal Verification papers →