The finite SL2(F5) central-square certificate
Abstract
Finite SL2 over F5 has only the two square roots of identity, with the explicit transport matrices.
Work over the five-element field ZMod(5) and write M(a,b,c,d) for the two-by-two matrix with those four entries. The first clause enumerates all determinant-one matrices and checks the square-root alternatives I and -I. The remaining clauses check the explicit matrices used in the low and high return words.
This is a finite certificate for the central-involution obstruction in the SL2(F5) example. It does not formalize the general face-transport theorem, the projective quotient PSL2(F5), or the geometric realization of the resulting twelve-degree and nine-degree edges.
Theorem 1.1 (Finite central-square and return-word certificate).
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/SL2F5CentralSquareCertificate.sl2f5_central_square_certificate (✓ std3). ∎
Source. Repository-derived.
Commentary.
The universal clause is a bounded kernel computation over all four entries in ZMod(5). The explicit determinant, inverse, matrix, and power identities are checked in the same computation.