arXiv++ Combinatorics

We prove that the realization graph of every graphical degree sequence is maximally Hamiltonian: it is Hamilton-laceable when bipartite on more than one vertex, and Hamilton-connected otherwise. This answers Problem P59 of Mütze's survey of combinatorial Gray codes, and the Hamiltonicity question recorded as open by Barrus, in the strongest form either admits. The argument is an induction on the number of ground vertices, cutting the realization graph at a single ground vertex into fibers and the quotient they lie over. The proof is formalized in Lean 4 and checked by its kernel, with seven results cited from the literature and nothing else assumed. Its engine is a classification. The realizable neighborhoods of a ground vertex form a shifted family -- one closed under replacing an element by a smaller one -- and the quotient is the Johnson graph of that family. Such a Johnson graph can fail to be Hamilton-connected, and we determine exactly when: the failures are one explicit family of examples, the Y-families, and each of them fails between a single pair of its members. A shifted family with a greatest member never fails, and those families are exactly the shifted matroids, where the conclusion already follows from the theorem of Naddef and Pulleyblank on the graphs of 0/1-polytopes. The obstruction lives entirely outside the matroid case, which is why it has not been met before.

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.