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

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.1 implements the revisions from a separate AI referee review of the manuscript and supplementary materials; see REVISION_NOTES.txt. This is not external human journal peer review. The mathematical certificate data and main result remain unchanged.