F-不规则图的一个构造
A construction of F-irregular graphs
- New York University（纽约大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文证明每个至少三个顶点的有限连通图 F 都存在有限连通 F-不规则宿主，并通过阈值图与关联构件构造出无穷多个两两不同构的宿主，同时给出 Lean 4 形式化。
AI中文摘要：
对于固定的图 F，宿主图 H 中顶点 v 的 F-度是 H 中同构于 F 且包含 v 的子图的数量，若 H 的 F-度两两不同，则称 H 为 F-不规则的。我们证明，每个至少有三个顶点的有限连通图 F 都存在一个有限连通的 F-不规则宿主。对于非完全图 F，证明从删除一条边的阈值图构建宿主；当最小度至少为 2 时，一个具有不同加权列和的小关联构件分离剩余的例外顶点。该构造还为每个非完全图 F 产生无穷多个两两不同构的有限连通 F-不规则宿主。完全图情形由 Chartrand、Holbert、Oellermann 和 Swart 的一个定理给出。本文描述了定理 1.1 的 Lean 4 形式化，以已发表的完全图定理作为其唯一的自定义公理。
英文摘要：
For a fixed graph F, the F-degree of a vertex v in a host graph H is the number of subgraphs of H isomorphic to F that contain v, and H is F-irregular if its F-degrees are pairwise distinct. We show that every finite connected graph F on at least three vertices admits a finite connected F-irregular host. For noncomplete F, the proof builds the host from a threshold graph with one deleted edge; when the minimum degree is at least two, a small incidence gadget with distinct weighted column sums separates the remaining exceptional vertices. The construction also yields infinitely many pairwise non-isomorphic finite connected F-irregular hosts for every noncomplete F. The complete-pattern case follows from a theorem of Chartrand, Holbert, Oellermann and Swart. A Lean 4 formalization of Theorem 1.1 is described, taking the published complete-pattern theorem as its sole custom axiom.
