发表机构
Department of Mathematics Statistics University of Wisconsin–La Crosse（威斯康星大学拉克罗斯分校数学与统计系）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明度序列实现图是最大哈密顿的，通过归纳切割和移位族分类，解决了 Mütze 和 Barrus 的开放问题，并在 Lean 4 中形式化验证。
AI 中文摘要
我们证明了每个图度序列的实现图都是最大哈密顿的：当它是多于一个顶点的二分图时，它是哈密顿可 laceable 的，否则它是哈密顿连通的。这回答了 Mütze 的组合格雷码综述中的问题 P59，以及 Barrus 记录的开放哈密顿性问题，并以两者所允许的最强形式给出。论证是对地面顶点数量的归纳，在单个地面顶点处将实现图切割成纤维以及它们所在的商图。该证明在 Lean 4 中形式化，并由其内核检查，仅引用了文献中的七个结果，没有其他假设。其引擎是一个分类。地面顶点的可实现邻域构成一个移位族——即在用较小元素替换元素下封闭的族——而商图是该族的 Johnson 图。这样的 Johnson 图可能不是哈密顿连通的，我们精确确定了何时如此：失败情况是一个显式示例族，即 Y-族，并且每个族仅在其成员之间的单对之间失败。具有最大成员的移位族从不失败，而这些族正是移位拟阵，此时结论已从 Naddef 和 Pulleyblank 关于 0/1 多胞形图的定理得出。障碍完全存在于拟阵情形之外，这就是为什么之前没有遇到它的原因。
英文摘要
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.
Comments81 pages, 9 figures. The proof is formalized in Lean 4 and machine-checked; the development and the programs behind the reported computations are at https://github.com/jbaggett/realization_graphs_lean
