AI 中文总结
研究(0,1)矩阵交换图G(R,S)的哈密顿性，通过结构归纳等方法证明其是最大哈密顿图，二分图时哈密顿可迹，非二分图时哈密顿连通，完整论证经机器验证，为布鲁阿尔迪猜想提供更强结论。
AI 中文摘要
对于整数向量R、S，令A(R,S)表示具有行和向量R与列和向量S的(0,1)矩阵类。其交换图G(R,S)以A(R,S)为顶点集，两个矩阵若通过单个2×2交换不同则相邻。布鲁阿尔迪猜想对每个R、S，G(R,S)是哈密顿图。我们证明更强的结论：G(R,S)是最大哈密顿图，二分图时是哈密顿可迹的，非二分图时是哈密顿连通的。证明通过对类中矩阵数量进行结构归纳，利用交换图结构理论。删除非活动行和拆分不变位置可将任何类表示为笛卡尔积，归结为素因子。二分图类是完全转置图的乘积，利用相关定理证明其是配对2-不相交路径可覆盖的从而是哈密顿可迹的。非二分图类分为三种情况处理，完整论证已在Lean 4证明助手里从第一原理及七个文献引用结果进行机器验证。
英文摘要
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.
Comments45 pages, 4 figures. Ancillary public trust surface and reproducibility guide. Companion Lean 4 formalization, with continuous integration re-running the kernel check, at https://github.com/jbaggett/brualdi-interchange-lean (tag arxiv-v3)
