The Proper Hat-Guessing Number of the Five-Cycle: A Computer-Assisted Argument

We give a computer-assisted proof that the proper hat-guessing number of the five-cycle is four. The upper bound concerns arbitrary deterministic local rules, with no symmetry assumption. A counting argument selects a color guessed on at most 25 strategy-table entries. A classification of two-vertex covers in a bipartite graph proves the necessary lower bound 17. These restrictions, followed by vertex and color relabeling, reduce the exclusion to 1413 count representatives and 8613 terminal Boolean formulas. We separate three obligations: coverage of every hypothetical strategy, preservation of that strategy by the actual encoding, and refutation of each terminal formula. The encoding check exhausts all 65,399 admissible inputs of the 14 counter-component types; the complete local replay checks 66,403,934 reverse-unit-propagation additions, including every final empty clause. We give examples of the reductions, explain the inference rule, and specify how the versioned code, input and proof records fit together. A local witness attaining 17 shows why the two-occurrence argument alone is insufficient. The verification uses separately implemented local programs within one AI-assisted workflow; it is not a proof-assistant formalization. This record contains the 23-page English preprint dated October 27, 2026. The manuscript has not undergone external peer review. Reproducibility materials, code and audit records: https://github.com/Lshiqi67/proper-hat-guessing-c5-reproducibility The CC BY 4.0 license applies to the manuscript deposited in this record. Materials in the linked repository are governed by their respective license notices.