The exact pair-cover number of two-intersecting five-uniform families

We prove that every finite family of five-element sets whose distinct members intersect in at least two elements can be covered by at most six two-element sets, each required to be wholly contained in the member it covers. The known eleven-block cyclic example makes the bound sharp. Thus g₁(5,2)=6, closing the 6–7 gap recorded by Parker. The proof reduces a hypothetical counterexample, through a canonical seven-pair cover and its private witnesses, to finitely many local configurations. Explicit pair covers exclude every configuration, and core-trace arguments make the reduction independent of the size of the ambient set. The universal upper bound, the completeness of the structural reductions, and the sharp lower example have complete Lean 4 proofs. This independent preprint includes the manuscript, a detailed proof supplement with 41 source-located certificate entries, and the complete pinned Lean source project, mathematical certificates and reproduction programs. Saved Lean build and axiom evidence is included; no new Lean compilation was performed for this preprint release. Default Windows integer and source checks passed; the reproduction commands and scope are documented in README.txt. The companion six-uniform preprint proves a distinct ten-pair upper bound. The articles share definitions, elementary covering tools and a verification framework; the six-uniform main theorem does not assume the five-uniform exact-value result. OpenAI’s ChatGPT was used primarily for translation, assistance with the Lean 4 formalization, and revisions to the manuscript wording. The author is responsible for checking all mathematical and formal details and takes responsibility for the final manuscript and formalization. License scope: manuscript and original mathematical certificate data are CC BY 4.0; original Lean, Python and JavaScript code is Apache-2.0. Third-party materials retain their own licenses.