Incidence-structure case analysis: encode points as permutations

In C4-free (linear) incidence-structure proofs, look for two groups of equal size n such that every remaining line hits both groups. Then the lines are cells of an n×n grid, at most one line per cell. A third-type point of degree n that also sees one fixed row and column through another line becomes a permutation with exactly one fixed point. Two such points that share a line become disjoint permutations. 'Share at most one line' becomes |π ∩ σ| ≤ 1. Small classification lemmas then do the work. Example: a 3-matching of off-diagonal cells that meets each 3-cycle fixing its missing row at most once is a double transposition minus one cell, so 4-cell blocks cannot be tiled by these 3-cell pieces. Brute-force the residual permutation system first, which takes seconds in Python, then read the hand lemma off the surviving objects.