Transcribed presentations of the Mathieu groups `M₁₁`, `M₁₂` and `M₂₂` #

This file carries three rows of the sporadic presentation manifest: cited finite presentations of the Mathieu groups M₁₁, M₁₂ and M₂₂, transcribed from published sources in which each presentation is proved to define the named group. Each row is a TauCeti.GroupPresentation recording the generator and relator counts and the relator expressions. Its docstring records the generator names, source and locator, generator convention, and transcription notes.

Four decidable checks accompany every row. The first is the relator count. The second spells the compiled words out letter by letter, so that a reviewer comparing the Lean data with the source never has to unfold the relator compiler. The third reads off from those letters the total number of them, against the length published by the source. The fourth is that every compiled word is cyclically reduced, which is what makes the letter count comparable with a published length: both sources measure length after free and cyclic reduction of each relator.

The rows themselves are sealed definitions, so each also carries the equation that characterizes it, spelling out its transcribed relator expressions with their generator indices. Together with TauCeti.GroupPresentation.relators_def and TauCeti.GroupPresentation.mem_relatorSet_iff, and with the interpretation equations of TauCeti.Relator.toFreeGroup, that equation determines the compiled words and the relations defining the presented group, so a consumer downstream of this file reasons about a row without unfolding it. Each row also publishes equations for its generator count and expected relator count. Its provenance is documented alongside the definition.

The manifest rows #

Name	Source	Locator	Generators	Relators	Length
`M₁₁`	Campbell--Havas--Ramsay--Robertson	Table 2 row `M11`, Section 5.8	2	2	19
`M₁₂`	Campbell--Havas--Ramsay--Robertson	Table 2 row `M12`, Section 5.17	2	3	29
`M₂₂`	Conder--Havas--Ramsay	Section 3.4, p. 40	2	3	30

Both sources prove their presentations by coset enumeration over the trivial subgroup, and both record the number of cosets that the enumeration used; those figures are part of the transcription notes of each row. Each row is also an efficient presentation in the sense of its source, meaning that its deficiency attains the lower bound coming from the Schur multiplier; that is the property the sources are about, and it plays no role here beyond explaining why they list these words.

Independent source-to-Lean read-through #

The three rows were independently checked against the source PDFs, rather than against the Lean definitions or the existing GAP re-enumeration. The downloaded bytes of Campbell--Havas--Ramsay-- Robertson's paper have SHA-256 ab91fcb806b1bc50508100f01893dcd84825146a80027c12796db325f8cf9966; the paper's Table 2 (p. 270) and Sections 5.8 and 5.17 (pp. 275 and 279) give the M₁₁ and M₁₂ rows. The downloaded bytes of Conder--Havas--Ramsay's paper have SHA-256 f0cf99d0c46a8c0546e036a62ecdd4407e043c8f9e2aeba744d9db5afe9301ed; its Section 3.4 (p. 40) gives the M₂₂ quotient presentation.

For M₁₁, the source row is

b A^3 b A b^3,  b a B A B A b a B a

The first word expands to the nine letters in the first entry of m11Presentation_relatorLetters, and the second to its ten-letter second entry. The source's generator order is a,b, and its convention A = a⁻¹, B = b⁻¹ agrees with the row. The table and Section 5.8 both identify the presentation as M₁₁; the table reports length 19, 10428 cosets, and order 7920, matching the row's letter total and transcription notes.

For M₁₂, the source row is

(B a)^3,  a^5 b^6,  a b^2 a B a^2 b a^2 b^2

The first word expands to six letters, the second to eleven, and the third to twelve, in exactly the order of m12Presentation_relatorLetters. The source again uses alphabetical generators and upper-case inverses. Table 2 reports length 29, 119334 cosets, and order 95040; Section 5.17 describes the same row and distinguishes it from the separate covering-group presentation.

For M₂₂, the source's Section 3.4 starts from a presentation of the cover and then adjoins the central relation b^11. The final displayed presentation is

 a^4 b A b A b,  a^2 b A B a b^2 A B,  b^11

These expand to the three entries of m22Presentation_relatorLetters, of lengths 9, 10, and 11. In particular, the third word is the relation that passes from the cover to M₂₂; it is not omitted as a redundant cover relation. The source uses the same a,b and upper-case-inverse conventions, and reports length 30, 2104858 cosets, and order 443520 for this presentation.

Thus every source relator, exponent, generator index, and source-order position agrees with the corresponding sealed row and its compiled-letter theorem. This paragraph is the independent source-to-Lean review artifact for these three rows; it is not a theorem about the order or simplicity of any presented group.

What is and is not claimed #

Nothing in this file asserts that the presented groups are nontrivial, finite, or simple, that they have any particular order, or that they are isomorphic to any other construction of a Mathieu group. Those are downstream statements which the CFSG roadmap deliberately does not ask for. What is proved here is exactly the transcription arithmetic: the counts, the total length, the compiled letters, and cyclic reducedness.

Cross-checks #

The correctness of a transcription is a review obligation, not something these theorems establish. Two external checks are recorded below as provenance for a reviewer. Neither is a Lean proof, and neither is claimed by any theorem in this file.

The first is an independent re-enumeration of the transcribed words outside Lean, with GAP 4.15.1. Transcribing the compiled letters back into GAP's free-group syntax gives the input

F := FreeGroup("a", "b");;  a := F.1;;  b := F.2;;
G11 := F / [ b*a^-3*b*a^-1*b^3, b*a*b^-1*a^-1*b^-1*a^-1*b*a*b^-1*a ];;
G12 := F / [ (b^-1*a)^3, a^5*b^6, a*b^2*a*b^-1*a^2*b*a^2*b^2 ];;
G22 := F / [ a^4*b*a^-1*b*a^-1*b, a^2*b*a^-1*b^-1*a*b^2*a^-1*b^-1, b^11 ];;
List([G11, G12, G22], Size);
List([G11, G12, G22], IsSimpleGroup);
List([[G11, 11], [G12, 12], [G22, 22]], p -> IsomorphismGroups(p[1], MathieuGroup(p[2])) <> fail);

on which Todd--Coxeter over the trivial subgroup returns the orders 7920, 95040 and 443520, each group is simple, and an isomorphism to MathieuGroup(11), MathieuGroup(12) and MathieuGroup(22) is found. That reproduces the published claim about the words as transcribed here, and a mistyped letter would be very unlikely to survive it.

The second is the comparison the CFSG roadmap asks a sporadic row to record. It used the Lean 4 permutation-group development FiniteSimpleGroups at commit 7f09e33a9ceef6b59ce03e34cd4f0558c763e325, which builds M₁₁, M₁₂, and M₂₂ as subgroups of Equiv.Perm (Fin n) with their orders and simplicity proved. Deterministic searches inside those three pinned subgroups found the following images of the presentation generators, in the development's zero-based point numbering:

M11:
  a = (0 2 3 10 6 1 9 8 4 7 5)
  b = (0 4 1 5 9 8 3 6 7 10 2)
M12:
  a = (0 1 2 7 4)(3 8 10 5 6)
  b = (0 8 5)(1 6)(2 10 7 9 11 4)
M22:
  a = (0 12 11 21 10)(1 14 20 13 19)(3 16 7 18 4)(5 17 15 6 8)
  b = (0 20 10 9 14 16 15 4 13 19 1)(2 5 6 8 18 17 11 21 3 12 7).

Direct permutation calculation makes all two, three, and three compiled relators respectively equal to the identity. Schreier--Sims membership checks put each displayed pair in the subgroup generated by the pinned development's named generators and put every named generator back in the corresponding displayed pair's subgroup. The pair-generated orders are therefore 7920, 95040, and 443520, agreeing with the pinned theorems card_M11, card_M12, and card_M22.

The calculation used Python 3.14.6 and SymPy 1.14.0. For each pair, concatenate the forward image table of a with that of b, storing every image as one byte. The resulting SHA-256 values are 5def66f046fc1d01ff2cf1878e33b9f50dc938f1b393434435df4abaa4fba119 for M₁₁, 4760dae2a1c9048a473456e770425ee3163bb5f411c77e04395cea2f18531768 for M₁₂, and 5e05402c13ed8ab52c3c5b5b322fcdfd76c758eea39c32dfa5da587818ff859d for M₂₂. This is the independent comparison artifact rather than a Lean theorem or imported external data; the GAP re-enumeration above remains a separate check.

Main definitions #

TauCeti.Sporadic.m11Presentation, TauCeti.Sporadic.m12Presentation and TauCeti.Sporadic.m22Presentation: the three transcribed rows.

References #

This is part of milestone S1 of TauCetiRoadmap/CFSGStatement/README.md, which asks for a complete relator word list, with an admissible source, for each of the twenty-six sporadic names. It populates the presentation data for three of those rows and records both their independent source read-throughs and the required comparisons against the FiniteSimpleGroups development. The two presentation sources are:

C. M. Campbell, G. Havas, C. Ramsay and E. F. Robertson, Nice efficient presentations for all small simple groups and their covers, LMS J. Comput. Math. 7 (2004), 266--283, https://doi.org/10.1112/S1461157000001121, https://staff.itee.uq.edu.au/havas/2004chrr.pdf;
M. D. E. Conder, G. Havas and C. Ramsay, Efficient presentations for the Mathieu simple group M₂₂ and its cover, in Finite Geometries, Groups, and Computation, Walter de Gruyter, Berlin, 2006, 33--41, https://www.math.auckland.ac.nz/~conder/preprints/m22presentations.pdf.

The Lean development named in the cross-check above is FiniteSimpleGroups; nothing from it is imported, copied, or adapted here.

The remaining two Mathieu names, M₂₃ and M₂₄, are transcribed in the sibling modules TauCeti.GroupTheory.SpecificGroups.CFSG.Sporadic.Mathieu.TwentyThree and TauCeti.GroupTheory.SpecificGroups.CFSG.Sporadic.Mathieu.TwentyFour.Presentation.

The alphabet of a two-generator presentation #

Both sources write relators as words in two generators a and b, with an upper-case letter denoting an inverse, so that A is a⁻¹. The four expressions below are those four letters, and ⬝ below is TauCeti.Relator.mul, so a transcribed relator reads left to right exactly as the source prints it.

Transcribed presentations of the Mathieu groups M₁₁, M₁₂ and M₂₂ #

The manifest rows #

Independent source-to-Lean read-through #

What is and is not claimed #

Cross-checks #

Main definitions #

References #

The alphabet of a two-generator presentation #

M₁₁ #

M₁₂ #

M₂₂ #

Transcribed presentations of the Mathieu groups `M₁₁`, `M₁₂` and `M₂₂` #

`M₁₁` #

`M₁₂` #

`M₂₂` #