A complete structural proof that interchange graphs of (0,1)-matrices are maximally Hamiltonian is machine-checked in Lean 4 from first principles.
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 conjectured that 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.
Problem
For classes A(R,S) of (0,1)-matrices with fixed row and column sums, the interchange graph G(R,S) connects matrices differing by a single 2x2 interchange. Brualdi conjectured G(R,S) is Hamiltonian for all R,S.
Approach
A stronger statement is proved: G(R,S) is Hamilton-laceable when bipartite and Hamilton-connected otherwise. The proof uses structural induction on class size, decomposing classes as Cartesian products via deleting inactive lines and splitting invariant positions. Bipartite classes reduce to products of complete transposition graphs handled via paired disjoint path covers; non-bipartite classes are treated by product assembly, a Johnson-graph base, and a pivot-and-fiber construction over matroid base-exchange graphs.
Figure 1: The doubled-layer device. G=A\,\square\,B is drawn as copies of A (“layers”) indexed by V(B) , with layers over adjacent B -vertices joined by the identity matching on the A -coordinate. A spanning walk W of B visits one vertex twice; here the layers are drawn in walk order, so the doubled layer appears twice. Since A is bipartite, traversing a layer by a Hamilton path of A flips the A -Figure 2: The construction of this section, on the class R=(2,2,1) , S=(2,1,1,1) . All twelve matrices of \mathcal{A}(R,S) and all thirty-three edges of G(R,S) are drawn. Fixing the buffer line L= row 3 partitions the class into four fibers, which sit below their vertices in the quotient Q_{L}=K_{4} (dotted). Three fibers are constrained ( K_{2} : bipartite, so a traversal’s exit is forced); the f
Results
The full argument, including seven cited literature results and the imported disjoint-path-cover results, is formalized and machine-checked in the Lean 4 proof assistant from first principles.
