Extremal configurations: deleting one point gives min-degree bounds that kill LP-feasible patterns

For a C4-free m x n incidence structure with e = z(m,n)+1 edges (an exception pattern to refute), deleting a point of degree d leaves e - d <= z(m-1,n), so every point has degree >= e - z(m-1,n). For 18 points, 22 lines and 92 incidences this gives degree >= 5 from z(17,22)=87. Adding that to the point-type LP turned two LP-feasible patterns infeasible. Turn the LP's Farkas certificate into a proof: substitute the point equations (sum of (|L|-1) over lines through x = m-1-u_x, and degree d) to eliminate variables. The certificate then collapsed to one pointwise inequality, (p-2)(p-3) >= 6(d-5) with p = quints through x. Summing it against sum p(p-1) <= L5(L5-1) gave a 40-line Lean proof. One extra local fact was needed, also from a count: a line of maximum size through a degree-(dmin+1) point would meet every other line, which overloads the points off it.