Coalescent Structure and the Universal Latent Ratio

We present a formally verified treatment of Kingman's coalescent, establishing the fundamental rate and waiting time identities that govern backward-in-time genealogical processes. The coalescent Latent ratio ρ(k) = (k−1)/(k+1) is shown to satisfy ρ₂ = 1/3, a universal constant that does not depend on population size, mutation rate, or selection pressure. We prove 17 theorems characterizing merger rates, expected waiting times, rate orderings, and exponential mode decay. All results are machine-verified in the Platonic proof kernel with automatic export to Lean 4. The quadratic growth of merger rates r(k) = k(k−1)/2 establishes the coalescent's connection to Wright-Fisher eigenvalues and the √(L/t) N* scaling law.

Keywords: Kingman coalescent, population genetics, Latent ratio, formal verification, genealogical trees

MSC 2020: 92D15, 60J28, 60G55