(1) Q8 of order 8 in SL(2,3), fixed-point-free on V-{0}; M9 of order 72, sharply 2-transitive on 9 points: OK
(2) G~ = E x| Q8 of order 216, centre contains Z of order 3, G~/Z = M9: OK
(3) phi_0: relation holds, image = M9, kappa(phi_0) = z^2 != 1 (independent of the 81 choices of lifts): OK
(5) number of homomorphisms pi_1(S_2) -> M9: 1592136 = 72*(4*72^2+36^2+9^2): OK
(4) surjective homomorphisms by (kappa != 1, J transitive): {('kappa=1', 'J intransitive'): 25920, ('kappa=1', 'J transitive'): 388800, ('kappa!=1', 'J transitive'): 622080}
    every surjective homomorphism with kappa != 1 has J = <x,uxu^-1,v,wvw^-1> transitive: OK (622080 homomorphisms)
(6) among them: <x,v> intransitive for 82080, <x,uxu^-1> intransitive for 103680 (pairs of pants with disconnected preimage exist)
    surjectivity criterion (linear parts generate Q8, no common fixed point) agrees with closure on 4000 random homomorphisms: OK
(7) all 68 subgroups of M9 generated by at most 3 elements: transitive iff it contains V; an intransitive one is a 2-group fixing a point, or has order 3 or 6 with linear parts +-1: OK
ALL CHECKS PASSED
