Interchange graphs of (0,1)-matrices are maximally Hamiltonian

Abstract

For integer vectors R,S let A(R,S) denote the class of (0,1)-matrices with row sum vector R and column sum vector S. Its interchange graph G(R,S) has A(R,S) as its vertex set, two matrices being adjacent when they differ by a single 2 x 2 interchange. Brualdi asked whether G(R,S) is Hamiltonian for every R,S. We prove the stronger statement that G(R,S) is maximally Hamiltonian: Hamilton-laceable when bipartite, and Hamilton-connected when not. The proof is a structural induction on the number of matrices in the class, organized by the structure theory of interchange graphs. Deleting inactive lines and splitting invariant positions expresses any class as a Cartesian product, reducing the argument to the prime factors. The bipartite classes are products of complete transposition graphs; we settle them together, without induction, by proving they are paired 2-disjoint-path-coverable and hence Hamilton-laceable, using a recent theorem of Coleman, Fischberg, Gong, Harrington and Wong on paired disjoint path covers. The non-bipartite classes divide into three cases: products assembled from smaller factors, a base of Johnson graphs and small classes, and the large prime classes, treated by a pivot-and-fiber construction whose line quotients are matroid base-exchange graphs. The complete argument has been machine-checked in the Lean 4 proof assistant from first principles together with seven cited results of the literature; the disjoint-path-cover results it imports are themselves proved within the formalization.

Disclosure

“e result independently of the argument: the SAT sweep tests its instances, the mechanization its deductions. Acknowledgments The computational search and verification programs and the Lean 4 formaliza- tion (Section 9) were developed with AI-assisted tools (Anthropic Claude; Ope- nAI GPT/Codex) under author direction. All mathematical content was veri- fied independently of any model’s assertions: the argument is machine-checked in Lean 4 (Section 9) and validated computationally on al”

PDF page 43

Classification

Proof ideas or individual proof-step assistance

Multiplier

8

Verified

2026-08-23T18:53:37.287942Z

Structural counts