Generalized Tuza's conjecture for pair-packing number four

For a finite three-uniform hypergraph, the pair-packing number is the maximum number of edges no two of which share a pair, and the pair-cover number is the minimum number of vertex pairs such that every edge contains a selected pair. We prove that pair-packing number four implies pair-cover number at most eight, and the bound is sharp. A reference packing with maximum union forces exterior edges to extend at most four fixed pairs. Selecting at most four exterior neighbors for each pair and then taking the induced hypergraph on the reference-packing core together with the union of selected neighbors gives a cover-preserving kernel on at most 24 vertices. Extra neighbors may be retained through another selected pair. Ten connected reference-packing types are excluded by independently executable RUP certificates, using the known theorem for pair-packing number at most three in the disconnected cases. The record contains the manuscript, LaTeX source, original frozen certificate archive, and complete verification and optional search programs. The finite certificate verification does not constitute a proof-assistant formalization of the handwritten reduction. 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.