The vertex cover number of three-intersecting nine-partite hypergraphs

Abstract

We prove that every nine-partite nine-uniform hypergraph whose distinct edges intersect in at least three vertices has an ordinary vertex cover of size at most four. Combined with the known lower construction of Bishnoi, Das, Morris and Szabó, this gives Ryser(9,3)=4. The computer-assisted proof reduces a hypothetical counterexample to a minimal family of between three and seven edges with empty common intersection. The unique three-edge normal form is excluded by a verified reverse unit propagation certificate. The remaining cases give 51 finite candidate records: 50 have explicit covers and the last has a four-branch type-deletion certificate. The reduction preserves equality between unknown vertices and imposes no ambient vertex bound. The complete standard-library verification package checks the finite enumeration, witness interfaces, covering exclusions and proof traces. This is not a proof-assistant formalization. OpenAI Codex assisted with mathematical exploration, computational verification and manuscript preparation. The author is responsible for the final manuscript and accompanying materials. License scope: manuscript, documentation and original mathematical certificate data are CC BY 4.0; original code is Apache-2.0. Third-party materials retain their own attribution and licenses. Version 1.0.2 implements a new independent AI review-revision-cross-review cycle, with two reviews per manuscript. All adopted comments were resolved in the second review. See REVISION_NOTES.txt and review_history/ in the complete source archive. The main result and mathematical certificate data are unchanged. This is independent AI review, not external human journal peer review. Published version 1.0.1 remains available separately.