g(r) is the least number of cards in a pairwise intersecting family of r-symbol cards that no r − 1 symbols can cover. Two kinds of result are here.
Every card carries six symbols and every two cards share one. A transversal is a set of symbols meeting every card, and τ is the smallest size of one. The six symbols of any single card already meet every other card, so τ is at most 6 always, and τ = 6 says that no five symbols cover everything. The question is how few cards such a family can have.
Families of at most fifteen cards are excluded by two independent routes. Sixteen cards are excluded by a finite reduction to 463 canonical cores whose SAT instances are all unsatisfiable, each with a DRAT proof accepted by an independent checker. An explicit seventeen-card family on 27 symbols gives the matching upper bound.
The two bounds are not evidence of the same kind. The upper bound is a witness: seventeen sets, 136 pairs, 80,730 subsets, standard library only, nothing trusted but arithmetic. The lower bound is computer-assisted, and a checked certificate does not establish that the reduction reaches every counterexample or that the encoding means what the mathematics means. Both are named as open obligations in the text. No priority is claimed, and this is not offered as a settled answer: it needs human review.
Repository · DOI 10.5281/zenodo.22883809 · Independent re-verification log · The Cell System (the author's other work)
python code/verify_witness_17.py — the seventeen-card family
python code/verify_k7.py — the finite lemma, all 294,239,817 cases
python code/verify_p1_hand_steps.py — the numbers in the hand proofs of Paper 1
drat-trim data/cnf/core_007.cnf data/cnf/core_007.drat — one certificate
The first two need nothing but Python's standard library.
python -S code/verify_snd_intersection.py — the final minimisation of Paper 6, exact rational arithmetic, a few seconds