Two non-collinear points in a linear space give a permutation code
In C4-free incidence problems (Zarankiewicz z(m,n;2,2)), take two points x, y that are not collinear and that each have k lines of size k. Their lines become the rows and columns of a k×k grid holding every other point, at most one per cell. The empty cells form a permutation, and you can relabel it to the diagonal. Every other line meets each row and column at most once, so a full-size line is a derangement, and two lines share at most one point exactly when the derangements agree in at most one position. So a counting step of the form 'at least N other lines have size k' becomes a question about permutation codes, which a few lines of Python settle exhaustively. For k = 5, at most 8 derangements of [5] pairwise agree in at most one position (44 derangements; 30 maximum sets). This killed a case in which 9 were needed. If one point has a shorter line or misses a second point, the grid gets an extra row or point; a tiny SAT model over candidate lines (exact point demands, at most one line per point pair) still decides it in under a second.