[1] Lemma 3.1 (F1)-(F4)
PASS  lines L0..L7 as printed
PASS  (F1) three lines per point; P, Q on a common line iff Q-P != 4, then exactly one; lines meet in <= 1 point
PASS  (F2) every non-line triple contains two points of a common line
PASS  (F3) closure of L u {P} is everything, for all 40 non-incident (P, L)
PASS  (F4) no line contains three of 0, 1, 2, 5
PASS  MK has 48 collineations  [found 48]
[2] Proposition 3.2 over Z[c]/(c^2-c+1)
PASS  the 8 line determinants vanish modulo c^2 - c + 1
PASS  all 120 non-incidence determinants det(x_P, x_a, x_b) are units (norm 1)
PASS  matrix B(c) = (x_P . y_j) equals the matrix printed in (3)
PASS  zeros of B(c) exactly at the 24 incidences, units elsewhere
PASS  c (1 - c) = 1 in Z[c]/(c^2 - c + 1)
[3] Proposition 3.2(b),(c): search over P^2(F_p) for x3, x4, x6, x7
PASS  p = 2: 0 normalised exact realisations = c(p) = 0
PASS  p = 3: 1 normalised exact realisations = c(p) = 1
PASS  p = 5: 0 normalised exact realisations = c(p) = 0
PASS  p = 7: 2 normalised exact realisations = c(p) = 2
[4] Theorem 5.7: h recomputed by scripts/rank3_formula.py (exact arithmetic)
PASS  rank3_formula.py mk ran (exit code 0)  [6.6 s; ]
PASS  h equals the polynomial printed in Theorem 1.1
PASS  remainders of the division by |GL_3(q)| are 0
PASS  no graph is stuck (no exception) and 4139 point partitions are used
PASS  P_0 equals the polynomial printed in Section 5
PASS  fresh JSON output identical to the recorded outputs/mk_rank3_formula.json
[5] direct count N(2) by scripts/rref3.c
PASS  rref3.c compiled
PASS  rref3 2: N(2) = 14818566 over 97155 column spaces  [p 2 subspaces 97155 N 14818566]
[6] Table 1, leading terms, N(q) for q = 2, 4, 8, 9, rook congruence, recorded Z_3
PASS  Table 1, p = 3: c(p), N(p) and p^10 N(p) as printed
PASS  Table 1, p = 5: c(p), N(p) and p^10 N(p) as printed
PASS  Table 1, p = 7: c(p), N(p) and p^10 N(p) as printed
PASS  Table 1, p = 11: c(p), N(p) and p^10 N(p) as printed
PASS  Table 1, p = 13: c(p), N(p) and p^10 N(p) as printed
PASS  N(2) = h(2) = 14818566
PASS  N(4), N(8), N(9) as printed in Section 8
PASS  leading terms (1065 + (-3/p)) p^25 + (5033 - 15 (-3/p)) p^24
PASS  Remark 5.8(a): (q-1)^3 divides h exactly, h/(q-1)^3 at q = 1 is 4760 = rook placements  [rooks = 4760]
PASS  recorded zcount values Z_3(p), p = 2..13, equal A_3 + c(p) B_3
ALL CHECKS PASSED
