The spectral gap of random Markov generators

Let L = X − D be the generator of a continuous-time Markov chain on n states. Its off-diagonal rates X_ij are i.i.d. and nonnegative, with mean m, variance σ² > 0 and a finite fourth moment, and D is the diagonal matrix of row sums. In 2012 Bordenave, Caputo and Chafaï proved that the spectral gap κ satisfies κ ≥ mn − σ√(2n log n)(1 + o(1)) almost surely. They conjectured equality and stated that they had no proof of the upper bound. We prove three facts that hold with probability tending to one: the rightmost nonzero eigenvalue of L is real and unique; it is separated from the rest of the spectrum by at least g₀/(2 log n), where g₀ = σ√n/√(2 log n); κ = D_min + m + O_P(1), where D_min is the smallest row sum. This proves the conjecture in probability, under the hypotheses of Bordenave, Caputo and Chafaï. Since D_min fluctuates on the scale g₀, the spectral gap has Gumbel fluctuations, with the same centring as the smallest row sum. This contrasts with random symmetric Laplacians, where the centring of the largest eigenvalue is known to be shifted. The proof combines two Schur complements with a contraction mapping. The self-energy is bounded by a second-moment estimate for a row given its sum. That estimate rests on the exchangeability of the row’s entries given their total, and the area mean-value property for analytic functions makes it uniform in the spectral parameter. The same estimate bounds the second-order term. The deterministic propositions are verified in Lean 4 with Mathlib, including the inequality for exchangeable quadratic forms. That covers 27 declarations, with no sorry; for the deflation step, the verified part is the determinant identity. The Lean source files are included.