Spectral Gap for the Binary Fixed-Margin Swap Chain

We prove an explicit spectral-gap lower bound for the lazy swap chain on binary matrices with prescribed row and column sums. This chain is a standard sampler for fixed-margin null models in ecology, statistics, and network analysis. Kannan, Tetali, and Vempala (KTV) conjectured that it mixes rapidly for all feasible margins citepkannan1997simple. We show that for every feasible set of margins on an m× n binary matrix, the lazy swap chain has spectral gap at least binomm2-1binomn2-1. The bound is tight in the worst case. Thus, our result proves this KTV conjecture in a stronger quantitative form. The same spectral-gap bound also verifies the Mihail--Vazirani conjecture for fixed-margin 0/1-matrix polytopes. The proof gives a new route to fixed-margin sampling that avoids stability assumptions and canonical-path constructions. We compare the swap chain with a two-row heat-bath chain and use a local-to-global spectral reduction to reduce the analysis from arbitrary m× n matrices to a three-row problem. The remaining three-row inequality is then proved by separating the scalar column-count sector from the non-scalar Johnson harmonic sectors. The proof itself was generated by ChatGPT 5.5 Pro. The author's role was to pose the problem, guide the search direction, evaluate the AI-generated arguments, rewrite the proof, and take responsibility for the final form and validity of the result. The full proof of the main theorem has been formalized in Lean, and the accompanying formalization is available at the anonymous repository https://github.com/guanyangwang/ktv-swap-lean.