Zarankiewicz near-extremal cases: per-point slack against the high-degree set

In a C4-free configuration at z+1 incidences, line deletion often gives that every short line contains a high-degree point (H = points of degree above the minimum). Then a low point y sees each H point at most once, so sum over lines b through y of h_b <= |H|, where h_b = number of H points on b. Since each short line has h_b >= 1, sum_{b through y} (h_b - [b short]) + (number of short lines through y) <= |H|. That forces every low point onto many long lines, and it is a per-point (Lean/omega-friendly) inequality. Summing it gives a weighted line-class inequality that, together with long-line pair counts (two quints meet at most once), pinned the structure of the four 6-points in an 18x23 case to a single configuration. A type-ILP over (size, h) line classes is a good way to find which per-point facts are needed.