Sharp spectral gaps for the switch and Curveball chains on every graphical degree sequence

Abstract

For every graphical degree vector on n ≥ 4 labeled vertices with more than one realization, the lazy chain that proposes switches uniformly on four vertices has spectral gap at least 1/(6 C(n,4)), and the chain that performs a uniform undirected Curveball trade on a uniformly chosen vertex pair has spectral gap at least 2/C(n,2); both constants are the worst case over all such degree vectors, for every n. Consequently the total-variation mixing times at distance 1/4 are at most n^6/4 + 1 for the switch chain and n^4/16 + 1 for the Curveball chain. Both gap bounds are kernel-checked in Lean 4, together with a total-variation bound for the switch chain whose prefactor is sqrt(M)/2, where M is the number of realizations, in place of the sqrt(M-1)/2 used in the paper. The result sharpens the pair-resampling argument of the OpenAI Math Release manuscript openai-math#131, which proves polynomial mixing for every graphical degree sequence. The deposit contains the manuscript (main.pdf). The companion repository, linked below at release v1.0.0, holds the Lean 4 verification against the pinned upstream definitions, the vendored upstream files with a blob-hash manifest, and the finite numerical checks.