发表机构
University of Cambridge; Lancaster University（剑桥大学; 兰卡斯特大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明每个 N≥9 的二部图表示数至多为 ⌈N/4⌉，结合 Crown 图已知表示数，证实 Crown 图在同阶二部图中使表示数最大化的猜想，并在 Lean 4 中形式化验证。
AI 中文摘要
图的表示数是最小的正整数 $k$，使得其顶点可以排列在一个单词中，每个顶点出现 $k$ 次，且当且仅当对应的顶点相邻时，两个不同的字母交替出现。我们证明了每个具有 $N\ge9$ 个顶点的二部图的表示数至多为 $\lceil N/4\rceil$。结合 Crown 图的已知表示数，这解决了关于 Crown 图在同阶二部图中使表示数最大化的猜想。证明通过将表示单词的选择简化为邻域的一个排序问题，发展了 Mozhui 和 Krishna 的构造。我们刻画了这种排序的障碍，并使用概率估计来排除所有足够大的平衡二部划分中的这些障碍。两个有限断言完成了论证，每个断言都通过一个已检查的布尔不可满足性证书建立。排序论证的一个改进直接处理剩余的奇数部分大小。主定理和 Crown 极值推论，包括有限证书论证，也已在 Lean 4 中形式化并验证。
英文摘要
The representation number of a graph is the least positive integer $k$ for which its vertices can be arranged in a word, each occurring $k$ times, so that two distinct letters alternate precisely when the corresponding vertices are adjacent. We prove that every bipartite graph on $N\ge9$ vertices has representation number at most $\lceil N/4\rceil$. Together with the known representation number of crown graphs, this settles the conjecture that crowns maximise the representation number among bipartite graphs of the same order. The proof develops a construction of Mozhui and Krishna by reducing the choice of a representing word to an ordering problem for neighbourhoods. We characterise the obstructions to this ordering and use probability estimates to exclude them for all sufficiently large balanced bipartitions. Two finite assertions complete the argument, each established by a checked Boolean unsatisfiability certificate. A refinement of the ordering argument treats the remaining odd part sizes directly. The main theorem and the crown-extremality corollary, including the finite certificate arguments, have also been formalised and verified in Lean 4.
