inference Complete proof in proof_small_r.md (Theorem A): any minimal empty-intersection subfamily of m edges has 2 <= m <= r+1, contains m distinct distinguished vertices, and spans at most m(r-m+2) vertices; max_m m(r-m+2) = 3r-3 exactly for r=3,4,5, so the witness family lies inside a window where the local condition supplies a common vertex — contradiction. Arithmetic core machine-checked (verify_616.py part A); span bound independently certified by an LP over the atom formulation (verify_atoms_lp.py) with optimum m(r-m+2) for all 3<=r<=12, 2<=m<=r+1, plus failure-power controls.