A transcribed presentation of the Higman--Sims group #
This file carries the HS 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 Higman--Sims 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
thirteen transcribed relators are
a², b⁵, s₁¹¹, s₂¹⁰, [a,b]⁵, [a,bab]³, [a,b²]⁶,
s₁s₁s₂s₋₁s₋₂s₋₁s₂s₁s₁s₋₂⁴,
s₁(s₂s₋₂²)²s₂s₁s₂(s₋₁s₂)²,
s₁s₁s₂²s₁s₋₁²s₁s₂²s₁s₁s₋₂s₋₁s₋₂,
(s₁s₁s₂s₋₁s₋₂s₁s₁s₋₁)²,
(s₁s₁s₂)²s₁s₁s₋₁s₁s₁s₂³s₁s₁s₋₁,
s₁(s₁s₂)³s₁s₁s₂s₋₁s₁s₋₂s₁s₋₁s₂.
The last three 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 run 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 subgroup listed in the source visibly centralizes a and a
coset enumeration returns the index 5775 of the involution centralizer of HS; and the double
cover 2·HS is excluded because ab² lifts to elements of order 20 there, while (ab²)¹⁰ = 1 is
a relator. GAP 4.15.1 independently checks that the thirteen words compiled by Relator.toWord
from the expressions below vanish on five independent standard generating pairs of the 100-point
primitive representation of HS, that is, pairs generating the group with a an involution whose
centralizer has order 7680, b of order 5 with centralizer of order 500, and ab of order
11. 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 HSG1-P1.M whose SHA-256
digest is 6f1863b22ce2bf3a4c7dfb4b84200dc614d4b40a5f8f6bd164832ae998d3b25b. Its constructor
G<x,y> fixes the generator order corresponding to the standard generators a,b in this row.
Writing its words in this module's syllables gives the seven short entries
a², b⁵, s₁¹¹, s₂¹⁰, [a,b]⁵, [a,bab]³, [a,b²]⁶,
followed, in source order, by
s₁s₁s₂s₋₁s₋₂s₋₁s₂s₁s₁s₋₂⁴,
s₁(s₂s₋₂²)²s₂s₁s₂(s₋₁s₂)²,
s₁s₁s₂²s₁s₋₁²s₁s₂²s₁s₁s₋₂s₋₁s₋₂,
(s₁s₁s₂s₋₁s₋₂s₁s₁s₋₁)²,
(s₁s₁s₂)²s₁s₁s₋₁s₁s₁s₂³s₁s₁s₋₁,
s₁(s₁s₂)³s₁s₁s₂s₋₁s₁s₋₂s₁s₋₁s₂.
These are exactly the thirteen entries of hsPresentation_transcribed, including every inverse,
power, commutator, and source-order position. The Magma file marks the last three as R1, R2,
and R3, says they are redundant but useful, and keeps them inside the constructor; the Lean row
therefore correctly retains them. The rendered presentation page omits those three and swaps the
display order of [a,bab]³ and [a,b²]⁶, while 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 hsa, hsb, and hsc
generate a subgroup of Equiv.Perm (Fin 100) with proved order 44352000 and proved simplicity.
Write those permutations as x, y, and z. The following words in them give images of the
ATLAS presentation generators:
a = (z x x y x z⁻¹ x⁻¹ z⁻¹ z⁻¹ y⁻¹ x y x z⁻¹ y⁻¹ y⁻¹ y⁻¹ x⁻¹ z y⁻¹ x⁻¹ y⁻¹)⁴
b = (y⁻¹ x⁻¹ x⁻¹ z⁻¹ y⁻¹ z⁻¹ z⁻¹ x z y⁻¹ x y y z z y x x)⁴.
Direct calculation gives orders 2, 5, 11, and 10 for a, b, ab, and ab².
Moreover, the centralizers of a and b in the pinned subgroup have orders 7680 and 500, so
the pair has the source's exact ATLAS classes rather than only the required element orders. All
thirteen compiled relators in this module evaluate to the identity. Schreier--Sims membership
checks put a,b in the subgroup generated by x,y,z and put each of x,y,z back in ⟨a,b⟩;
the pair therefore generates the pinned group of order 44352000.
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
6820d1571023e66bfff5a2fac256bd6d6ccb7e38bffd5f86b56db6ee1e17f6f2. 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 HS 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.hsPresentation: John Bray's ATLAS finite presentation ofHS.TauCeti.Sporadic.hsPresentation_transcribedand the equations for the remaining fields: the characterization of the sealed row.TauCeti.Sporadic.hsPresentation_map_length_relators,TauCeti.Sporadic.hsPresentation_totalLengthandTauCeti.Sporadic.hsPresentation_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
HSG1-P1, contributed by John Bray, https://brauer.maths.qmul.ac.uk/Atlas/v3/pres/HSG1-P1, with the relators and the demonstration of correctness in the Magma source file https://brauer.maths.qmul.ac.uk/Atlas/spor/HS/mag/HSG1-P1.M. - J. N. Bray, presentation page for the Higman--Sims group,
https://webspace.maths.qmul.ac.uk/j.n.bray/web/Pres/HS.html, which records
Length ??and so publishes no letter count for this presentation. - KitaKen1, FiniteSimpleGroups,
HSconstruction at commit7f09e33a9ceef6b59ce03e34cd4f0558c763e325, https://github.com/KitaKen1/finite-simple-groups-lean.
John Bray's ATLAS version 3 finite presentation of the Higman--Sims group HS 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: HSG1-P1, https://brauer.maths.qmul.ac.uk/Atlas/v3/pres/HSG1-P1, with the relator list and the demonstration of correctness in the Magma source file https://brauer.maths.qmul.ac.uk/Atlas/spor/HS/mag/HSG1-P1.M
Generator convention: The ATLAS standard generators a and b of HS, that is, a in class 2A and b in class 5A with ab of order 11, 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 thirteen words of the source's relator list are stored as thirteen
relators equal to the identity. The last three, marked R1, R2 and R3 there, are redundant, and are
transcribed because the source runs its coset enumerations with them. The source demonstrates
correctness by enumerating the 5775 cosets of a subgroup that visibly centralizes a, using
(a*b^2)^10 = 1 to exclude the double cover 2.HS. GAP 4.15.1 checks that the thirteen compiled
words vanish on five independent standard generating pairs of the 100-point primitive
representation of HS, taking a with centralizer of order 7680, b of order 5 with centralizer of
order 500, and ab of order 11.
Instances For
The number of generators in the presentation of HS. The row's body is sealed, so this is
what lets a
consumer see that it is a two-generator presentation.
The relator count HS's source states; see
TauCeti.Sporadic.hsPresentation_generatorCount.
The relator expressions transcribed for HS, 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.hsPresentation_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 HS agrees with the transcribed data.
The lengths of the thirteen compiled relator words for HS, 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.hsPresentation_totalLength.
The compiled relator words for HS have 359 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 HS is cyclically reduced. This is what makes the letter count
of TauCeti.Sporadic.hsPresentation_totalLength comparable with a published presentation length,
which is measured after free and cyclic reduction of each relator.