A ten-pair covering theorem for two-intersecting six-uniform families

Abstract

A pair cover of a family of sets is a collection of two-element sets such that each member of the family contains a whole selected pair. We prove that every two-intersecting family of six-element sets, on an arbitrary ground set, has a cover by at most ten pairs. The general upper bound of Aharoni and Zerbib gives fourteen in this case; the new bound, together with the classical eight-pair lower example, yields 8 ≤ g₁(6,2) ≤ 10. The proof successively excludes high intersections, high triple degree and pair degrees six, five and four. Complete physical supports and an isolated three-tail analysis then give uniqueness of exact two-point traces. A final incidence count and grouping of actual members assemble the cover. A compactness argument supplies one finite cover of a possibly infinite family. This independent preprint includes the manuscript, a detailed proof supplement with 424 source-located finite proof entries, the complete pinned Lean source project, mathematical certificates, frozen checker inputs and reproduction programs. Saved Lean build, axiom and dependency 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 exact six-uniform pair-cover value remains undetermined. The companion five-uniform preprint determines g₁(5,2)=6. The articles share definitions, elementary covering tools and a verification framework. This six-uniform main theorem does not assume the five-uniform exact-value theorem; this record contains all source dependencies needed for its own reproduction. 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.