A transcribed presentation of the McLaughlin group #
This file carries the McL row of the sporadic presentation data required by milestone S1 of
TauCetiRoadmap/CFSGStatement/README.md. It records John Bray's ATLAS version 3 presentation of
the McLaughlin group 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², s₋₁ = ab⁻¹ and s₋₂ = ab⁻² for the four syllables that occur, the
fifteen transcribed relators are
a², b⁵, [a,b]⁵, s₁¹¹, s₂¹², [a,b²]⁶, (s₁s₋₂)⁷,
[a, b⁻²s₁s₁s₂]²,
[a, b⁻²s₂s₋₁s₁s₂²s₁s₋₁],
[a, bs₂³]²,
[a, b²s₁s₂²]²,
s₁s₂s₋₂s₁s₋₁s₂(s₋₂s₁)²(s₂s₋₂s₂)²,
[a, b²s₂s₋₁s₂]²,
[a, b²s₁]⁴,
[a, b²s₂]⁴.
Three of these are redundant, and are flagged as such by the source; they are transcribed anyway because the coset enumerations that the source uses to justify the presentation are easier with them.
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, and it comes with a demonstration of
correctness: the relations a² = b⁵ = (ab)¹¹ = 1 force the presented group to be perfect and
generated by conjugates of a; the relations a² = [a,b]⁵ = [a,b²]⁶ = 1 force the subgroup listed
in the source to centralize a; a coset enumeration returns the index 22275 of the involution
centralizer of McL, leaving McL or its triple cover 3·McL; and the latter is excluded because
its standard generators have |AB| = 33, while (ab)¹¹ = 1 is a relator. GAP 4.15.1 independently
checks that the fifteen words compiled by Relator.toWord from the expressions below vanish on
five independent standard generating pairs of the 275-point primitive representation of McL,
that is, pairs generating the group whose centralizers have orders 40320 and 750 and which
meet the two ATLAS element-order conditions. Both computations are provenance for the
transcription, not Lean theorems: this file asserts no order, finiteness, simplicity, or
identification result.
Independent source-to-Lean read-through #
An independent read-through used the bytes of the ATLAS Magma source McLG1-P1.M whose SHA-256
digest is 84a601b1aecb12c3ab3b96a9f5009e94bec5fe6e1988f9f12cfde37512c59583. Its constructor
G<x,y> and later assignments a := x; b := y fix the generator order used by this row. In the
module's syllables, its fifteen constructor entries are
a², b⁵, [a,b]⁵, s₁¹¹, s₂¹², [a,b²]⁶, (s₁s₋₂)⁷,
[a,b⁻²s₁s₁s₂]²,
[a,b⁻²s₂s₋₁s₁s₂²s₁s₋₁],
[a,bs₂³]²,
[a,b²s₁s₂²]²,
s₁s₂s₋₂s₁s₋₁s₂(s₋₂s₁)²(s₂s₋₂s₂)²,
[a,b²s₂s₋₁s₂]²,
[a,b²s₁]⁴,
[a,b²s₂]⁴.
They agree entry for entry with mclPresentation_transcribed, including every inverse, power,
commutator, and source-order position. The Magma file labels entries eight, ten, and fifteen as
the redundant relators R0, R1, and R2 but retains them inside the constructor, so the Lean
row correctly retains all fifteen. The rendered presentation page omits those three and reorders
some of the short active relations; the row deliberately follows the raw Magma order. This
comparison was performed from the pinned source bytes 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 named permutations mcla through mcle
generate a subgroup of Equiv.Perm (Fin 275) with proved order 898128000 and proved simplicity.
Write those five permutations as x, y, z, w, and v. The following words in them give
images of the ATLAS presentation generators:
a = (w y x z⁻¹ y x z⁻¹ w v⁻¹ z y v⁻¹ w v⁻¹ y⁻¹ z⁻¹ x w⁻¹)⁶
b = (z z v⁻¹ y⁻¹ w⁻¹ y v⁻¹ x y w⁻¹ x z⁻¹ v w v⁻¹ v⁻¹ x v⁻¹ x⁻¹ z⁻¹ v⁻¹ y⁻¹)³.
Direct calculation gives orders 2, 5, 11, 12, and 7 for a, b, ab, ab², and
the source's standard-pair word ababababbababbabb. The centralizers of a and b in the pinned
subgroup have orders 40320 and 750, so this also checks the source's exact ATLAS classes. All
fifteen compiled relators in this module evaluate to the identity. Schreier--Sims membership checks
put a,b in the subgroup generated by x,y,z,w,v and all five named generators back in ⟨a,b⟩;
the pair therefore generates the pinned group of order 898128000.
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 a two-byte little-endian integer, has SHA-256
40408769e39c23b86c576421ba328889cd061d4ed14910271c2731b110e79c63. 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, since both are measured after free
and cyclic reduction of each relator. This row has no published length to check against: Bray's
presentation page for McL is one of the 1997 stubs that record Length ??, and neither the ATLAS
page nor its Magma source file gives a figure. The total below therefore states the transcribed
data for a reviewer to compare with the source, rather than checking it against a recorded number.
Main definitions and results #
TauCeti.Sporadic.mclPresentation: John Bray's ATLAS finite presentation ofMcL.TauCeti.Sporadic.mclPresentation_transcribedand the equations for the remaining fields: the characterization of the sealed row.TauCeti.Sporadic.mclPresentation_map_length_relators,TauCeti.Sporadic.mclPresentation_totalLengthandTauCeti.Sporadic.mclPresentation_relatorsCyclicallyReduced: the three checks on the compiled words.
References #
- R. A. Wilson, R. A. Parker, J. N. Bray et al., ATLAS of Finite Group Representations,
version 3, presentation
McLG1-P1, contributed by John Bray, https://brauer.maths.qmul.ac.uk/Atlas/v3/pres/McLG1-P1, with the relators and the demonstration of correctness in the Magma source file https://brauer.maths.qmul.ac.uk/Atlas/spor/McL/mag/McLG1-P1.M. - J. N. Bray, presentation page for the McLaughlin group,
https://webspace.maths.qmul.ac.uk/j.n.bray/web/Pres/McL.html, which records
Length ??and so publishes no letter count for this presentation. - KitaKen1, FiniteSimpleGroups,
McLconstruction at commit7f09e33a9ceef6b59ce03e34cd4f0558c763e325, https://github.com/KitaKen1/finite-simple-groups-lean.
John Bray's ATLAS version 3 finite presentation of the McLaughlin group McL 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; presentation contributed by John Bray.
Source locator: McLG1-P1, https://brauer.maths.qmul.ac.uk/Atlas/v3/pres/McLG1-P1, with the relator list and the demonstration of correctness in the Magma source file https://brauer.maths.qmul.ac.uk/Atlas/spor/McL/mag/McLG1-P1.M
Generator convention: The ATLAS standard generators a and b of McL, that is, a in class 2A and b in class 5A with ab of order 11 and ababababbababbabb of order 7, 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 fifteen words of the source's relator list are stored as fifteen relators equal to the identity. Three of them, marked R0, R1 and R2 there, are redundant, and are transcribed because the source's coset enumerations are easier with them. The source demonstrates correctness by enumerating the 22275 cosets of a subgroup that centralizes a, then excluding the triple cover 3.McL, whose standard generators have |AB| = 33 rather than 11. GAP 4.15.1 checks that the fifteen compiled words vanish on five independent standard generating pairs of the 275-point primitive representation of McL, taking a and b with centralizers of orders 40320 and 750 and imposing the two ATLAS element-order conditions.
Instances For
The number of generators in the presentation of McL. The row's body is sealed, so this is
what lets a
consumer see that it is a two-generator presentation.
The relator count McL's source states; see
TauCeti.Sporadic.mclPresentation_generatorCount.
The relator expressions transcribed for McL, with their generator indices written out and
the private syllable abbreviations of this file expanded.
The row's body is sealed, so this is the equation that 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, so a consumer never has to unfold the row. Index 0 is the
generator a and index 1 is b, and the bounds come from
TauCeti.Sporadic.mclPresentation_generatorCount. The comments name each relator in the syllables
s₁ = ab, s₂ = ab², s₋₁ = ab⁻¹ and s₋₂ = ab⁻² of the module docstring.
The relator count recorded for McL agrees with the transcribed data.
The lengths of the fifteen compiled relator words for McL, in the order of the source.
Reading the counts off one relator at a time is what lets a reviewer locate a discrepancy, rather
than only observe one in the total of TauCeti.Sporadic.mclPresentation_totalLength.
The compiled relator words for McL have 499 letters in total. The source records no
presentation length, so this figure states the transcribed data for a reviewer to compare with the
source, rather than checking it against a recorded number.
Every compiled relator word for McL is cyclically reduced. This is what makes the letter
count of TauCeti.Sporadic.mclPresentation_totalLength comparable with a published presentation
length, which is measured after free and cyclic reduction of each relator.