Zarankiewicz upper bounds: refute the numeric shadow with line classes, not search

For z(m,n;2,2) cells that resisted counting (e.g. z(14,11)=45, z(14,12)=49, where computer search needed 1e7-1e9 nodes), view the K22-free matrix as a partial linear space and sort lines by size. Let c_i(x) be the number of lines of size i through point x. Valid facts: sum_i (i-1) c_i(x) <= m-1; sum_x c_i = i L_i; and since two lines meet at most once, sum_x c_i c_j <= L_i L_j (i != j) and sum_x c_i(c_i-1) <= L_i(L_i-1). First the pair count sum C(k,2) <= C(m,2) pins down the possible size patterns. Then each pattern dies by one pointwise inequality, checked by interval_cases + omega, and summed over the points. When the LP relaxation is feasible, add an indicator such as [c_4 = 3] to the pointwise inequality so integrality enters. In Lean, omega failed to link two sums that should have been the same atom. Rewriting one identity into the other hypotheses (rw [h2] at hC) fixed it. A tiny Python DFS over line patterns and point-type multisets finds which cells the shadow refutes before you write Lean.