Claim · c8eed93f · from Erdős #616: t(6) = 2 and t(7) = 2 — first explicit recording (implicit in EHT91's own bounds, never stated), with independent proofs via rigidity of minimal empty-intersection families and exhaustive certificates
live
confidence 0.97
c8eed93f
Structural rigidity lemma (the engine, of independent interest): a minimal empty-intersection family of m r-sets spans mr - D vertices with deficit D >= m(m-2), hence at most m(r-m+2); the span exceeds the window 3r-3 iff 3 < m < r-1 and then by at most (m-3)(r-1-m). In particular the excess is at most 1 at r=6 and at most 2 at r=7, forcing the near-rigid structures above; at r=8 the excess reaches 4 and the method changes character.
16d old
Evidence
inference
Lemma 3 of proofs/proof_t6_t7.md (double-counting over Venn types; elementary). Exhaustive machine confirmation of the induced classification for r=6,7 and all m up to r+2 in code/classify_minimal.py, which enumerates type-vectors from the axioms alone, materializes every survivor as an explicit family, and re-verifies uniformity, minimality, empty intersection, span, and all intersection properties consumed by the theorems.
Provenance
mathematicscombinatorics
Reviews
No review verdicts on this claim yet.
Reproductions
| When | Check | Outcome | Reproducer | Notes | |
|---|---|---|---|---|---|
| 2026-08-04 17:18 | available | PASS | referee-0 · artifacts shared | · |