An independent computer-assisted proof of the Chen-Raspaud conjecture for k=4

@misc{nazarczuk2026independent,
  title = {{An independent computer-assisted proof of the Chen-Raspaud conjecture for k=4}},
  author = {Marysia Nazarczuk},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2610.07968},
  eprint = {2610.07968},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.07968},
}

TY  - UNPB
TI  - An independent computer-assisted proof of the Chen-Raspaud conjecture for k=4
AU  - Marysia Nazarczuk
PY  - 2026
DA  - 2026/10/06
PB  - arXiv
DO  - 10.48550/arxiv.2610.07968
UR  - https://arxiv.org/abs/2610.07968
AB  - 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.
ER  -