Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Sporadic.Mathieu.TwentyFour.Presentation

A transcribed presentation of the Mathieu group M₂₄ #

This file carries the M₂₄ row of the sporadic presentation data required by milestone S1 of TauCetiRoadmap/CFSGStatement/README.md. It records the ATLAS version 3 presentation M24G1-P1 of the Mathieu group M₂₄ on its standard generators a and b as a TauCeti.GroupPresentation, together with the source, the generator convention, transcription notes, and the expected counts.

Writing s₁ = ab and s₋₁ = ab⁻¹ for the two syllables that occur, the seven transcribed relators are

a², b³, s₁²³, [a,b]¹², [a,bab]⁵, (s₁s₁s₋₁)³(s₁s₋₁s₋₁)³, (s₁(s₁s₋₁)³)⁴.

The Magma source file carries an eighth word [a, b⁻¹abab]⁵, but comments it out of the Group<x, y | ...> constructor with the note "redundant, but quite useful.", so it lies outside the relator list and is not transcribed; the recorded relator count is therefore seven, and the presentation page displays the same seven words. Contrast the redundant word of M23G1-P1, transcribed in TauCeti.GroupTheory.SpecificGroups.CFSG.Sporadic.Mathieu.TwentyThree, which stands inside its relator list as written and is counted.

The source's commutator convention is [r,s] = r⁻¹s⁻¹rs, opposite to Mathlib's commutatorElement, so each commutator is stored as Relator.commInvInv r s as TauCeti.Relator prescribes. The proved TauCeti.Relator.toWord_toFreeGroup is the audit boundary between these expressions and the signed words that PresentedGroup consumes.

The source is a presentation rather than a semi-presentation — the ATLAS lists a separate semi-presentation for M₂₄, which is not what is transcribed here — and it comes with a demonstration of correctness: a² = b³ = (ab)²³ = 1 force the presented group to be perfect and hence generated by conjugates of a, the remaining relations force the source's subgroup H to centralize a, a coset enumeration returns the index 31878 of that subgroup, which is the index of the involution centralizer 2¹⁺⁶:L₃(2) of a class 2B involution in M₂₄, and M₂₄ has trivial Schur multiplier. GAP 4.15.1 independently checks the transcription in both directions. The seven words compiled by Relator.toWord from the expressions below vanish on five independent standard generating pairs of the natural 24-point representation of M₂₄, so the presented group surjects onto M₂₄; enumerating the compiled relators over the image of the source's subgroup H returns the index 31878 that the source predicts; and enumerating them over the cyclic subgroup generated by the image of ab returns the index 10644480, which with s₁²³ bounding that subgroup by 23 pins the order of the presented group at 244823040 = |M₂₄|. The two classes must be pinned by centralizer order, 7680 for a and 1080 for b, and not by element orders alone: pairs with a of order 2, b of order 3, ab of order 23 and ababab²abab²ab² of order 4 also occur with a in class 2A and b in class 3B, and on those the last three relators do not vanish. Both computations are provenance for the transcription, not Lean theorems: this file asserts no order, finiteness, simplicity, or identification result. The cross-check against the M24 of the FiniteSimpleGroups development, which TauCetiRoadmap/CFSGStatement/README.md asks for on the names that development covers, is still recorded below.

Independent source-to-Lean read-through #

An independent read-through used the bytes of the ATLAS Magma source M24G1-P1.M whose SHA-256 digest is 3bf09bbeddfa76f9fedd79ba8264cbd2b4d1d22947412b305cddba3a50798114. Its constructor G<x,y> fixes the generator order, and the later assignments a := x; b := y confirm that the source's x,y are the presentation generators called a,b here.

The seven active constructor entries, in source order, are

x², y³, (xy)²³, [x,y]¹², [x,yxy]⁵,
(xy xy xy⁻¹)³ (xy xy⁻¹ xy⁻¹)³,
(xy (xy xy⁻¹)³)⁴.

They agree in exponent, inverse placement, and source order with the seven entries of m24Presentation_transcribed, after substituting s₁ = ab and s₋₁ = ab⁻¹ and using the source convention [x,y] = x⁻¹y⁻¹xy. Between the sixth and seventh active entries, the Magma file has a commented line [x,y⁻¹xyxy]⁵ labelled redundant but useful. Because the comment delimiters keep it outside Group<x,y | ...>, omitting it from the seven-relator row is exact, and the ATLAS presentation page independently displays those same seven active words. This checks every source relator and the only commented-word boundary independently of the original transcription and closes this row's S1 source-to-Lean read-through.

Independent comparison with FiniteSimpleGroups #

The comparison used finite-simple-groups-lean at commit 7f09e33a9ceef6b59ce03e34cd4f0558c763e325, whose m24a, m24b, m24c, and m24d generate a subgroup of Equiv.Perm (Fin 24) with proved order 244823040 and proved simplicity. A deterministic search inside that subgroup found the following ATLAS standard pair, in the pinned development's zero-based point numbering:

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

The first permutation is fixed-point-free and has centralizer order 7680 in the pinned group; the second fixes six points and has centralizer order 1080. Thus they have the source's classes 2B and 3A, not merely the required element orders. Direct calculation gives order 23 for ab and order 4 for ababab²abab²ab², and all seven compiled relators in this module evaluate to the identity. Schreier--Sims calculation verifies both that a,b belong to the subgroup generated by the four named FiniteSimpleGroups permutations and that every named generator belongs to ⟨a,b⟩; the two generated groups have the common order 244823040.

The check used Python 3.14.6 and SymPy 1.14.0. Concatenating the forward image tables for a and then b, with each image stored as one byte, has SHA-256 c70cde4a6f85093e9226c6d884942312ef316f50eaddada2f13105735329add0. This is the independent comparison artifact required by S1; no external code or permutation data is imported into Tau Ceti.

The row is a sealed definition, so it publishes an equation for each of its fields: the transcribed relator expressions with their generator indices written out, and the provenance a manifest row exists to record. Together with TauCeti.GroupPresentation.relators_def and TauCeti.GroupPresentation.mem_relatorSet_iff the first of those determines the compiled words and the relations defining the presented group, so a consumer reasons about the row without unfolding it.

Three decidable checks accompany those equations. The relator lengths and their total record the compiled data one word at a time and in aggregate, and cyclic reducedness is what makes such a letter count comparable with a published presentation length. This row records no published length, so the total here states the transcription for a reviewer to compare with the source rather than checking it against a recorded number.

Main definitions and results #

References #

source
def TauCeti.Sporadic.m24Presentation :
GroupPresentation

The ATLAS version 3 finite presentation M24G1-P1 of the Mathieu group M₂₄ on its standard generators a and b.

The ATLAS lists this as a full presentation of the abstract group, separately from the semi-presentation used to recognize standard generators inside a group already constructed. No structural property of the presented group is asserted here: this definition records only the cited generators and relations.

Generator order (starting at index zero): a, b.

Source: R. A. Wilson, R. A. Parker, J. N. Bray et al., ATLAS of Finite Group Representations, version 3.

Source locator: M24G1-P1, https://brauer.maths.qmul.ac.uk/Atlas/v3/pres/M24G1-P1, with the relator list and the demonstration of correctness in the Magma source file https://brauer.maths.qmul.ac.uk/Atlas/spor/M24/mag/M24G1-P1.M

Generator convention: The ATLAS standard generators a and b of M24, that is, a in class 2B and b in class 3A with ab of order 23 and ababab^2abab^2ab^2 of order 4, in that order, so index 0 is a and index 1 is b. Products are read left to right, negative exponents denote inverses, and [r,s] denotes r^-1 s^-1 r s.

Transcription notes: The seven words of the source's relator list are stored as seven relators equal to the identity. The Magma file's eighth word [a, b^-1*a*b*a*b]^5 is commented out of the Group<x, y | ...> constructor with the note 'redundant, but quite useful.', so it lies outside the relator list and is not transcribed. GAP 4.15.1 checks that the seven compiled words vanish on five independent standard generating pairs of the natural 24-point representation of M24, taking a with centralizer of order 7680 and b with centralizer of order 1080; that enumerating the compiled relators over the image of the source's subgroup H returns the index 31878 that the source's demonstration of correctness predicts; and that enumerating them over the cyclic subgroup generated by the image of ab returns the index 10644480, hence the order 23 * 10644480 = 244823040 of M24.

Instances For
    source
    @[simp]
    theorem TauCeti.Sporadic.m24Presentation_generatorCount :
    m24Presentation.generatorCount = 2

    The number of generators in the presentation of M₂₄. The row's body is sealed, so this is what lets a consumer see that it is a two-generator presentation.

    source
    @[simp]
    theorem TauCeti.Sporadic.m24Presentation_expectedRelatorCount :
    m24Presentation.expectedRelatorCount = 7

    The relator count of the seven-word M₂₄ presentation.

    source
    @[simp]
    theorem TauCeti.Sporadic.m24Presentation_transcribed :
    m24Presentation.transcribed = [(Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).pow 2, (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩).pow 3, ((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩)).pow 23, ((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).inv.comm (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩).inv).pow 12, ((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).inv.comm (((Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩).mul (Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩)).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩)).inv).pow 5, (((((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩)).mul ((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩))).mul ((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩).inv)).pow 3).mul (((((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩)).mul ((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩).inv)).mul ((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩).inv)).pow 3), (((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩)).mul ((((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩)).mul ((Relator.gen ⟨0, m24Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, m24Presentation_transcribed._proof_2⟩).inv)).pow 3)).pow 4]

    The relator expressions transcribed for M₂₄, with their generator indices written out and the private syllable abbreviations expanded.

    The row's body is sealed, so this equation characterizes it: with TauCeti.GroupPresentation.relators_def it determines the compiled words, and with TauCeti.GroupPresentation.mem_relatorSet_iff it determines the relations defining TauCeti.GroupPresentation.Group. Index 0 is a and index 1 is b, with bounds supplied by TauCeti.Sporadic.m24Presentation_generatorCount.

    source
    theorem TauCeti.Sporadic.m24Presentation_matchesMetadata :
    m24Presentation.matchesMetadata

    The relator count recorded for M₂₄ agrees with the transcribed data.

    source
    theorem TauCeti.Sporadic.m24Presentation_map_length_relators :
    List.map List.length m24Presentation.relators = [2, 3, 46, 48, 40, 36, 56]

    The lengths of the seven compiled relator words for M₂₄, in the order of the Magma source. Reading the counts one word at a time makes any transcription discrepancy local.

    source
    theorem TauCeti.Sporadic.m24Presentation_totalLength :
    m24Presentation.totalLength = 231

    The compiled relator words for M₂₄ have 231 letters in total. The source records no published length, so this states the transcribed aggregate for an audit rather than checking it against a source figure.

    source
    theorem TauCeti.Sporadic.m24Presentation_relatorsCyclicallyReduced :
    m24Presentation.relatorsCyclicallyReduced

    Every compiled relator word for M₂₄ is cyclically reduced. This is what makes TauCeti.Sporadic.m24Presentation_totalLength comparable with a published presentation length.