A. the maps and the permutations
   [ok] U(z) = -I z = (z2, -z1)
   [ok] W(z) = IJ z + (1,0) = (2 z1 + z2 + 1, z1 + z2)
   [ok] image lists of T,U,W as printed: (1, 2, 0, 4, 5, 3, 7, 8, 6) (0, 6, 3, 1, 7, 4, 2, 8, 5) (1, 3, 8, 5, 7, 0, 6, 2, 4)
   [ok] cycle forms as printed: T=(012)(345)(678), U=(1623)(4785), W=(0135)(2847)
   [ok] I^2 = J^2 = -1, IJ = -JI
   [ok] [T,U][T,W] = 1 for maps and [p,q] = p q p^-1 q^-1
   [ok] [T,U] = t_(1,1), [T,W] = t_(2,2)
   [ok] relation also holds: left-to-right products and [p,q] = p^-1 q^-1 p q
   [ok] relation FAILS: maps with [p,q] = p^-1 q^-1 p q
   [ok] relation FAILS: left to right with [p,q] = p q p^-1 q^-1
   [ok] left to right with p q p^-1 q^-1 holds for the inverse permutations
   [ok] <x,uxu^-1,v,wvw^-1> (maps) = <x,u^-1xu,v,w^-1vw> (left to right) as sets, order 9
B. the group
   [ok] T,U,W generate a group of order 72
   [ok] it is M_9 = {z -> Az+t : A in <I,J>, t in F_3^2}
   [ok] the 9 translations form a normal subgroup
   [ok] point stabiliser: orders [1, 2, 4, 4, 4, 4, 4, 4], non-abelian (quaternion group)
   [ok] the action on the 9 points is sharply 2-transitive (sample)
   [ok] centre trivial; commutator subgroup of order 18 (so M_9 is not perfect)
   [ok] normaliser of M_9 in Sym(9) has order 432 (= |AGL(2,3)|)
   [ok] M_9 has 68 subgroups, 62 of them intransitive
   [ok] a subgroup is transitive iff it contains the translations
C. the central extension
   [ok] Q_8 = {+-1,+-I,+-J,+-IJ} is closed, 8 matrices
   [ok] all of determinant 1
   [ok] order 216; identity, inverses, associativity on all 216^3 triples
   [ok] (t,s,A) -> (z -> Az+t) is a homomorphism onto M_9
   [ok] its kernel is Z = {(0,s,1)}, of order 3, and central
   [ok] the centre of the extension is exactly Z
   [ok] the preimage of the translations is non-abelian of order 27 and exponent 3
   [ok] formulas for g (a,0,1) g^-1 and [(a,0,1),g] hold for all g and a
D. the obstruction of phi_0
   [ok] [x~,u~][v~,w~] = (0,2,1) for all 81 choices of lifts: [((0, 0), 2, ((1, 0), (0, 1)))] -- phi_0 does not lift
   [ok] kappa(phi_0) = 2 with the section (A|t) -> (t,0,A)
E. all homomorphisms pi_1(S_2) -> M_9
   [ok] number of homomorphisms: 1592136 (= |G| sum (|G|/chi(1))^2 = 1592136)
   [ok] epimorphisms: 1036800
   [ok] epimorphisms which do not lift: 622080 ; which lift: 414720
   [ok] epimorphisms which do not lift and have J intransitive: 0  (Theorem 1.1(c) for the standard generators)
   [ok] epimorphisms which lift and have J intransitive: 25920
   [ok] among them J cap V = 0: 19008 ; |J cap V| = 3: 6912  (the two cases of the main lemma)
   [ok] non-surjective homomorphisms with kappa != 0: 321840, of which 22032 have J intransitive (the generation hypothesis is needed)
   classes modulo Sym(9) of epimorphisms onto conjugates of M_9 which do not lift: 622080 / 432 = 1440
   [ok] this number is 1440
F. orbits of the substitutions M1..M5 (r2_moves.py) on the epimorphisms
   orbits on the 1036800 epimorphisms (no conjugation applied): ['size 311040 = 4320*72, kappa [1], J intransitive on 0', 'size 311040 = 4320*72, kappa [2], J intransitive on 0', 'size 414720 = 5760*72, kappa [0], J intransitive on 25920']
   [ok] three orbits, of 4320, 4320 and 5760 classes modulo M_9 (each orbit is closed under conjugation by M_9: sizes are multiples of 72)
   [ok] kappa is constant on each orbit and takes the values 0,1,2
   [ok] J is transitive on the whole of the two orbits with kappa != 0; the orbit with kappa = 0 contains failing tuples
   [ok] the orbit of phi_0 has 311040 tuples = 4320 classes modulo M_9
   [ok] conjugation by AGL(2,3) maps phi_0 into both orbits with kappa != 0: so the 622080 epimorphisms which do not lift form ONE orbit of 1440 classes modulo Sym(9)
   [ok] classes of the orbit of phi_0 modulo AGL(2,3): 1440
G. cut-and-glue model
   [ok] the nine octagons glue to a closed surface (every edge on two sides with opposite directions, every vertex link a circle)
   [ok] it is connected, with Euler characteristic -18: genus 10
   [ok] after cutting along the lifts of the two curves (chords s2-s4 and s6-s8) the 27 pieces form 1 component: the preimage of H_0 is connected
   [ok] components of the cut model = number of orbits of <x,uxu^-1,v,wvw^-1> on 46638 homomorphisms to M_9 (every 7th x 5th pair of each commutator class); distribution of the number of components: [(1, 43232), (2, 1411), (3, 1498), (5, 332), (9, 165)]
H. pairs of pants (Proposition 1.8(b)), Galois closure
   [ok] <phi_0(a1),phi_0(a2)> = <T> has 3 orbits: P(a1,a2) has disconnected preimage
   [ok] <TU^2, U TU^2 U^-1> has order 6 and 2 orbits: the pair of pants of handle type for (a1 b1^2, b1, a2, b2)
   [ok] on the 1440 classes: <x,v> intransitive for 190 classes, <x,uxu^-1> intransitive for 240 classes
   [ok] these numbers are 190 and 240 as stated
   [ok] J(phi_0) is the group of translations (order 9): in the regular cover with deck group M_9 the preimage of H_0 has 72/9 = 8 components
I. the exceptional tuples of r2_blk.c for n = 9
   [ok] 14 exceptional blocks; each representative generates a group of order 72 conjugate to M_9 and, after conjugation into M_9, is an epimorphism which does not lift (14 of 14)

r2_m9.py: 55 checks, 0 failed
