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 M23G1-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, s₂ = ab² and s₋₁ = ab⁻¹ for the three syllables that occur, the nine
transcribed relators are
a², b⁴, s₁²³, s₂⁶, [a,b]⁶, (s₁s₋₁s₂)⁴,
s₁³ s₋₁ s₂ (s₁s₋₁)² s₁³ s₋₁³,
(s₁s₂s₂)⁶,
(s₁s₂)³ (s₂s₋₁)² s₁ s₂ s₁ s₋₁ s₂.
The eighth of these, (abab²ab²)⁶, is annotated "Is redundant, but very useful." in the source, and
the source's header records the two resulting counts as "NoRels: 8 [or 9]" with lengths 190 and 238.
Unlike the redundant words of the neighbouring ATLAS files — M24G1-P1, transcribed in
TauCeti.GroupTheory.SpecificGroups.CFSG.Sporadic.Mathieu.TwentyFour.Presentation, comments its
redundant word out of the Magma Group<x, y | ...> constructor — this word stands inside the
relator list as written, so it is transcribed and the recorded relator count is nine. The source's
demonstration of correctness covers the list both with and without it.
The source's commutator convention is [r,s] = r⁻¹s⁻¹rs, opposite to Mathlib's
commutatorElement, so the 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: the relations force the presented group to be perfect and hence
generated by conjugates of a, a coset enumeration returns the index 3795 of a subgroup that
visibly centralizes a, which is the index of the involution centralizer 2⁴:L₃(2) in M₂₃, and
M₂₃ has trivial Schur multiplier. GAP 4.15.1 independently checks the transcription in both
directions. The nine words compiled by Relator.toWord from the expressions below vanish on five
independent standard generating pairs of the natural 23-point representation of M₂₃, so the
presented group surjects onto M₂₃; and enumerating the compiled relators over the cyclic subgroup
generated by the image of ab returns the index 443520, which with s₁²³ bounding that subgroup
by 23 pins the order of the presented group at 10200960 = |M₂₃|. 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 M23 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 M23G1-P1.M whose SHA-256
digest is 3a4a7b8b116ac25b147b94ce0a6c6a73a730420e9865792d60587bd99cdc0e32. 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.
Reading the constructor from top to bottom gives the five short relators
x², y⁴, (xy)²³, (xy²)⁶, [x,y]⁶,
followed by these four words:
(xy xy⁻¹ xy²)⁴,
(xy)³ xy⁻¹ xy² (xy xy⁻¹)² (xy)³ (xy⁻¹)³,
(xy xy² xy²)⁶,
(xy xy²)³ (xy² xy⁻¹)² xy xy² xy xy⁻¹ xy².
They agree in exponent, inverse placement, and source order with the nine entries of
m23Presentation_transcribed, after substituting s₁ = ab, s₂ = ab², and s₋₁ = ab⁻¹ and
using the source convention [x,y] = x⁻¹y⁻¹xy. The source places the eighth word inside the
constructor and labels it redundant but useful; it therefore belongs in this row. Its header's
8 [or 9] relators and lengths 190 [or 238] are exactly the results of deleting or retaining
that 48-letter entry in m23Presentation_map_length_relators. This checks every source relator and
the only optional-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 m23a, m23b, and m23c generate a
subgroup of Equiv.Perm (Fin 23) with proved order 10200960 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 5)(2 7)(3 20)(6 14)(8 9)(11 17)(16 19)(18 21)
b = (0 15 6 7)(1 21 14 3)(4 12 5 11)(9 13 18 22)(10 20)(17 19).
Direct permutation calculation gives orders 2, 4, and 23 for a, b, and ab, and order
8 for the standard-pair word abababab²abab²ab². All nine compiled relators in this module
evaluate to the identity. Schreier--Sims calculation then verifies that a and b belong to the
subgroup generated by m23a, m23b, and m23c, while each of those three named generators
belongs to ⟨a,b⟩; equivalently, ⟨a,b⟩ has the same order 10200960 and is that subgroup.
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
1ee47ccfd4fa651541d3b0826fc4ef407705bd727921e885c0f4ae9bd442f8e4. 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.
Four decidable checks accompany those equations. The relator lengths and two aggregate totals record
the compiled data one word at a time and in aggregate, and cyclic reducedness makes the letter
counts comparable with the source's published lengths. The nine-word total is 238 and deleting the
useful redundant eighth relator leaves 190, exactly the two figures in the source header for the
two versions of the presentation.
Main definitions and results #
TauCeti.Sporadic.m23Presentation: the ATLAS finite presentation ofM₂₃.TauCeti.Sporadic.m23Presentation_transcribedand the equations for the remaining fields: the characterization of the sealed row.TauCeti.Sporadic.m23Presentation_map_length_relators,TauCeti.Sporadic.m23Presentation_totalLength,TauCeti.Sporadic.m23Presentation_sum_map_length_eraseIdx_relatorsandTauCeti.Sporadic.m23Presentation_relatorsCyclicallyReduced: the four checks on the compiled words. The two totals are the figures on the source's header lineLength: 190 [or 238]., whose bracketed alternative is the presence of the redundant eighth relator.
References #
- R. A. Wilson, R. A. Parker, J. N. Bray et al., ATLAS of Finite Group Representations,
version 3, presentation
M23G1-P1, https://brauer.maths.qmul.ac.uk/Atlas/v3/pres/M23G1-P1, with the relator list and the demonstration of correctness in the Magma source file https://brauer.maths.qmul.ac.uk/Atlas/spor/M23/mag/M23G1-P1.M. - KitaKen1, FiniteSimpleGroups,
M23construction at commit7f09e33a9ceef6b59ce03e34cd4f0558c763e325, https://github.com/KitaKen1/finite-simple-groups-lean.
The ATLAS version 3 finite presentation M23G1-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: M23G1-P1, https://brauer.maths.qmul.ac.uk/Atlas/v3/pres/M23G1-P1, with the relator list and the demonstration of correctness in the Magma source file https://brauer.maths.qmul.ac.uk/Atlas/spor/M23/mag/M23G1-P1.M
Generator convention: The ATLAS standard generators a and b of M23, that is, a of order 2 and b of order 4 with ab of order 23 and abababab^2abab^2ab^2 of order 8, 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 nine words of the source's Magma relator list are stored as nine relators
equal to the identity. The eighth, (ab*ab^2*ab^2)^6, carries the source's annotation 'Is
redundant, but very useful.' but stands inside the relator list as written rather than being
commented out of it, so it is transcribed; the source's header records the two counts as 'NoRels:
8 [or 9]', of total length 190 and 238, and demonstrates correctness for the list both with and
without that word. GAP 4.15.1 checks that the nine compiled words vanish on five independent
standard generating pairs of the natural 23-point representation of M23, and that enumerating the
compiled relators over the cyclic subgroup generated by the image of ab returns the index 443520,
hence the order 23 * 443520 = 10200960 of M23.
Instances For
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.
The relator count of the transcribed nine-word version of the M₂₃ presentation.
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.m23Presentation_generatorCount.
The relator count recorded for M₂₃ agrees with the transcribed data.
The lengths of the nine 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.
The compiled relator words for M₂₃ have the total length 238 published for the nine-word
version of the presentation.
Deleting the redundant eighth relator (ab·ab²·ab²)⁶ leaves 190 signed letters, which is
the length the source records for its eight-relator form.
With TauCeti.Sporadic.m23Presentation_totalLength this checks the transcription against both of
the figures on the source's header lines Length: 190 [or 238]. and NoRels: 8 [or 9]., whose
bracketed alternatives are exactly the presence of this relator.
Every compiled relator word for M₂₃ is cyclically reduced. This is what makes
TauCeti.Sporadic.m23Presentation_totalLength and
TauCeti.Sporadic.m23Presentation_sum_map_length_eraseIdx_relators comparable with the source's
published lengths, which are measured after free and cyclic reduction of each relator.