Refuting near-linear spaces: make every big line meet a small set exactly once
For small partial linear spaces (Zarankiewicz exceptions), the line-local count sum over lines M disjoint from L of (|M|-1) = (I-B) - (k-1) - k(m-k) + eps_L, where eps_L counts uncovered pairs leaving L, often pins down the unique line each big line misses. Example: on 18 points with one 2-line l, one triple T, 13 quads, 7 quints and one uncovered pair {u,v}, a quint avoiding u,v misses exactly l, and one through u or v misses exactly T. So every quint meets the set T ∪ {u,v} exactly once, and the sum of p_x over those 5 points is 7, where p_x is the number of quints through x. The other 13 points have p_x <= 2 from the point equation (or because their quints must contain u or v), so 35 = sum p <= 7 + 26, a contradiction. This kind of argument is much cheaper to formalize than a case split on how the big lines intersect.