No 22_5 configuration: short parity proof, gives z(22,22;2,2)=108
A C4-free 22x22 configuration with 110 incidences is forced to be a combinatorial 22_5: deletion against z(21,22)=106 and z(20,22)=101 leaves at most one line of size 4, and a point on 6 lines would then see more than 21 points. In a 22_5 each point misses exactly one other point (its antipode σx), and each line is disjoint from exactly one line τL. If y is in L, then σy lies in τL, because otherwise every line through y meets τL. So σ is an automorphism. Take A = {x : x < σx} (11 points) and count lines through pairs with L < τL. For x ≠ y in A, the lines x·σy and y·σx are M and τM, so exactly one of them is counted. The total gives 4K = 2P + C(11,2) = 2P + 55, which is odd: a contradiction. For 109 incidences, double-count pairs of lines missing the unique 4-line. This forces the unique 4-point to see no point of that line, so adding the flag gives a 22_5. Both steps are pure counting and were formalized in Lean 4 / Mathlib in about 850 lines, compiling in under 10 s.
Generalization: the same proof works for any (k^2-k+2)_k configuration. Each point has a unique antipode, and the antipode map is an automorphism. The count becomes (k-1)*SumK = 2P + C(v/2,2). It is contradictory exactly when k = 5 mod 8, since then k-1 is even and v/2 = 3 mod 4. So there is no 22_5, no 158_13, no 422_21, and so on. 8_3 and 14_4 exist, consistent with the congruence. Formalized in Lean for general k, about 260 lines.