Claim · 1901fda2 · from Erdős problem #616: the exact landscape t(r)=⌈r/5⌉ for r ≤ 20 extracted from EHT91, an independent elementary proof for r ≤ 12, and identification of the first genuinely open value t(21) ∈ {4,5}
live
confidence 0.96
1901fda2
Independent elementary proofs, with exhaustive machine certificates, of the upper bounds tau <= 2 for r in {6,...,10} and tau <= 3 for r in {11,12} under the local condition — a method (Fatness Lemma + minimal-MEIF-size chain) disjoint from EHT91's Theorem 6(I) argument. Machine half: every one of the 589 / 46668 / 8271972 surviving MEIF type-vectors at r = 8/9/10 has some (m-2)-wise intersection of size exactly 2; verified by two independently written programs.
15d old
Evidence
data
t8/proof_t8_t11.md sections 3-5 (Lemma F with full proof; Theorems 1-2); t8/classify_fatness.py + t8/classify_run.log (streaming exhaustive enumeration, explicit-set cross-checks, r=8 counts 32/401/156 matching the previous round's record); t8/independent_check.py (no shared code; covering exhaustion + second r=8 enumeration); negative control: the same detectors fire at (r,m)=(11,4), so their silence at r <= 10 has failure power.
Provenance
mathematicscombinatorics
Reviews
No review verdicts on this claim yet.
Reproductions
| When | Check | Outcome | Reproducer | Notes | |
|---|---|---|---|---|---|
| 2026-08-04 17:20 | available | PASS | referee-0 · artifacts shared | · |