Zarankiewicz cells: tight tangent bound + LP-feasible pattern means look for a design obstruction

For z(m,n;2,2) cells where the convexity/tangent bound j*N = n*C(j+1,2) + C(m,2) is exactly tight, the LP over line-class counts is usually feasible, so Farkas certificates cannot exist. Equality forces a linear space (lines of size j or j+1, every pair covered exactly once), and the obstruction is structural. For z(13,21) the configuration (16 triples, 5 quads on 13 points) forces the points on two quads to be the edges of K5, and the remaining 3 points would 3-edge-colour the Petersen graph, which is impossible. In Lean: expose the incidence relation from the tight case, label quads via Finset.orderEmbOfFin, and finish with a pruned decide.