Chen-Raspaud 猜想 k=4 情形的独立计算机辅助证明
An independent computer-assisted proof of the Chen-Raspaud conjecture for k=4
浏览论文内容
中文总结 AI 辅助
本文用计算机辅助方法独立证明了 Chen-Raspaud 猜想在 k=4 时成立，即满足 odd-girth≥9 且 mad<9/4 的图可同态到 Kneser 图 K(9,4)，通过最小反例、局部类型分析和精确验证实现。
中文摘要 AI 辅助
我们给出了 Chen-Raspaud 猜想 k=4 情形的独立计算机辅助证明。我们证明了每个满足 odd-girth(G) ≥ 9 且 mad(G) < 9/4 的图 G 都同态到 Kneser 图 K(9,4)。该证明结合了最小反例论证与根星替换、K(9,4) 中的精确有限计算以及最终的计数论证。在移除所有可约局部类型后，唯一的正局部类型是 (3,3,4)。其单位盈余通过其 4-线程转移到具有足够负容量的相对类型。证明中使用的计算机辅助陈述由精确的 C++ 位集验证器认证，并且一个独立的 Python 实现提供了交叉检查；完整的源代码和原始证书随稿件一同提供。
英文摘要
We give an independent computer-assisted proof of the k=4 case of the Chen-Raspaud conjecture. We prove that every graph G with odd-girth(G) >= 9 and mad(G) < 9/4 admits a homomorphism to the Kneser graph K(9,4). The proof combines a minimal-counterexample argument with a rooted star replacement, exact finite computations in K(9,4), and a final charging argument. After all reducible local types are removed, the unique positive local type is (3,3,4). Its unit excess is transferred through its 4-thread to a relative with sufficient negative capacity. The computer-assisted statements used in the proof are certified by exact C++ bitset verifiers, and a separate Python implementation provides an independent cross-check; the complete source code and raw certificates accompany the manuscript.
发表机构
- Faculty of Mathematics, Informatics and Mechanics（数学、信息学和机械学院）
- University of Warsaw（华沙大学）
机构由 AI 辅助整理，请以论文原文为准。
