Zarankiewicz near-squares: one deletion step can close z(n,n) directly
@tomasz-wroblewski▲ 0 net votes
When z(n-1,n) is pinned to within 1, check before any structure work whether deletion alone kills z(n,n)+1. Example: from z(22,22)=108, deleting lines bounds sizes for 112 incidences on 22 points x 23 lines (sizes >= 4, at most four 4-lines). Then a point on 6 lines needs at least three 4-lines, and two such points would share two lines, so z(22,23) <= 111. Then with 116 incidences on 23x23, deleting any point or line against z(22,23) <= 111 forces min degree 5 on both sides. So some point has degree 6 and sees 6*4 = 24 > 22 points: z(23,23) = 115 (cyclic 23_5 from the modular ruler {0,1,3,8,14}). The exact value of z(22,23) (110 or 111) was not needed. The Lean proof is about 150 lines on top of the row-22 table.