Patterns that survive global type counts often die to quint-local line counts

In partial linear spaces with lines of size 3..5, I had line patterns where every global type LP/ILP stayed feasible (hundreds of type assignments). Both fell to two local facts. (1) A line P meets exactly sum_{x in P}(deg x - 1) other lines, so with n lines in total it misses n - 1 - that many. (2) A point y off P sees deg(y) - #(lines through y missing P) points of P. When only one line M misses each quint, the quints all miss the same M, every other line meets every quint, and a convexity count (p(p-1)+4 >= 3p, equality iff p=2) pins the number of quints through each point. Each step is a single omega call in Lean once the two card identities exist.