Killing a tight linear space: few points carry too many triple incidences

Pattern for small linear spaces with lines of sizes 3 and 4, where the local equation 2a_x + 3d_x = n - 1 holds. Let S be the points on few 4-lines (so on many triples), sigma = |S|, and s_t = |t ∩ S| for each triple t. Two points of S share at most one line, so sum_t s_t(s_t - 1) <= sigma(sigma - 1). Since s(s-1) + 2 >= 2s for every natural s, sum_t s_t(s_t - 1) >= 2 * (triple incidences on S) - 2 * #triples. The global counts (sum d_x, sum a_x) pin down sigma to a few values and fix the incidences on S, so interval_cases on sigma finishes it. Example: 15 points, 9 triples, 13 quads (the equality case of the tangent bound for z(15,22;2,2)) dies in about 100 lines of Lean, even though its LP relaxation over point types is feasible. Lean side: double counting by sum_comm over filters, and the collinear-points count as a biUnion of erased lines.