A transcribed presentation of the Suzuki sporadic group #
This file carries the Suz row of the sporadic presentation data required by milestone S1 of
TauCetiRoadmap/CFSGStatement/README.md. It records the presentation GPLTable.Suz.1 from
Rolf Lindenbergh's Group Presentations Library as a TauCeti.GroupPresentation, together with
the exact source, generator convention, transcription notes, expected counts, and decidable
checks on the transcription.
The presentation uses the Coxeter graph
a --5-- b --3-- c --8-- d --3-- e
b --3-- f --4-- g --3-- b
where every generator is an involution and every omitted edge has label 2. In particular, the
graph contributes seven square relations and one product-order relation for each of the twenty-one
unordered pairs of generators. The labels in the display are the source's path strings
a5b3c8d3e,b3f4g3b; the second string is the triangle on b, f, and g and is not joined to
c.
The source then appends the six relations
a = (cd)^4, a = (fg)^2, (abcf)^5, (bfg)^5,
((bcdcd)^5 e)^3, (abcg)^5.
The last relation occupies the source record's presdef[4] field. The library initialization
includes that field when its GPL_PCE option is true, and version 1.0 sets this option to true by
default, so it belongs to the default full presentation transcribed here. The equality decoder in
the same source compiles x = y as x⁻¹y; that convention determines the first two extra words.
There are therefore 7 + 21 + 6 = 34 relators, and the metadata theorem checks that count. A count
does not see a relator exchanged for another of the same shape, so the compiled words are also
spelled out one signed letter at a time, and the per-relator lengths, the total length 275 and
the cyclic-reduction check are stated against that spelling rather than against the sealed record.
Both lengths are derived transcription checks: the source publishes no presentation length to
compare them with. An independent read-through of the version 1.0 GPLTable.Suz.1 record and its
DeCoxList, MakeWordList, and InitializeGroupPresentationGPL decoders checked the generator
order, both Coxeter paths, all six appended relations, and the compiled signed letters below. As a
separate consistency check, GAP 4.15.1 enumerates 1782 cosets of the subgroup generated by a
through f, which the GPL record labels G2(4). These checks are transcription provenance rather
than Lean theorems: no order, finiteness, simplicity, or identification result is asserted here.
The independent comparison below identifies this permutation image with the FiniteSimpleGroups
construction of Suz; it too is a review artifact rather than a theorem in this module.
Independent source-to-compiled audit record #
This audit was performed from the GPL artifact independently of the original transcription. The
retrieved version 1.0 gpl.g bytes have SHA-256
8b90a7a65317a585b5b74d015083bd2fa3db8a969c117a220d00d7e8773103c8. The source record is
presdef := [ "a5b3c8d3e,b3f4g3b", ,
"a=(cd)^4,a=(fg)^2,(abcf)^5,(bfg)^5,((bcdcd)^5e)^3", "(abcg)^5" ]
and the decoder comparison with suzPresentation_relatorLetters is:
- entries 1--7 are the squares of
a,b,c,d,e,f,ginserted byAddTrivialRelations; - entries 8--14 are
(ab)^5,(bc)^3,(cd)^8,(de)^3,(bf)^3,(fg)^4,(gb)^3, the seven labeled edges of the two paths; - entries 15--28 are the exponent-two relations on the fourteen complementary pairs
ac,ad,ae,af,ag,bd,be,ce,cf,cg,df,dg,ef,eginserted byAddNonEdgeRelations; - entries 29--33 are the five comma-separated words in
presdef[3], withMakeWordListdecoding the two equalities asa⁻¹(cd)^4anda⁻¹(fg)^2; and - entry 34 is
(abcg)^5frompresdef[4], included byInitializeGroupPresentationGPLbecause version 1.0 setsGPL_PCE := true.
Expanding these powers gives exactly the signed lists in suzPresentation_relatorLetters; no
source letter, pair relation, or optional relation differs from that theorem. This itemized record
is the independent source-to-Lean review artifact; the theorem remains the kernel-checked target
against which it was read.
Independent comparison with FiniteSimpleGroups #
The independent comparison used finite-simple-groups-lean at commit
7f09e33a9ceef6b59ce03e34cd4f0558c763e325. From the GPL presentation above, SymPy's
Todd--Coxeter implementation enumerated the cosets of ⟨a,b,c,d,e,f⟩. It completed at
exactly 1782 cosets; the induced action satisfies all thirty-four source relators, and the point
stabilizer has suborbits of sizes 1, 416, and 1365. Developing the 416-point suborbit gives
a 416-regular orbital graph on those 1782 cosets.
That graph was compared with the 1782-vertex graph encoded by
FiniteSimpleGroups.Sporadic.Suz.SuzMask. A vertex-coloured canonical labelling, distinguishing
the base vertex and one neighbour, produced an isomorphism; every one of the 1782 * 416 directed
adjacencies was then checked under it. Transporting the seven GPL permutations across this
isomorphism produced seven even involutions preserving the encoded graph and still satisfying all
thirty-four relators. Finally, direct Schreier--Sims membership checks put all seven transported
permutations in the subgroup generated by SuzPerm.suza through SuzPerm.suzf, and put all six
of those generators in the subgroup generated by the transported permutations. Both generated
groups have order 448345497600, agreeing with FiniteSimpleGroups' theorem card_Suz.
The computation used Python 3.14.6, SymPy 1.14.0, and pynauty 2.8.8.1. For a compact check on the
transport step, concatenating the seven image tables in generator order, with every image encoded
as a two-byte little-endian integer, has SHA-256
30670ef2e7e902035636fa63568ef957a91fea59d4536f6d2c431dc9448b8cd7; the corresponding
concatenation of the six pinned FiniteSimpleGroups tables has SHA-256
75a378c50ccaad53155d65869595601436384ecd59eecc73fb02e22e59ef972b. This is the roadmap's
independent comparison artifact; no external code or generated permutation table is imported into
Tau Ceti.
Main definition #
TauCeti.Sporadic.suzPresentation: the GPL finite presentation of the Suzuki sporadic group.
Main results #
TauCeti.Sporadic.suzPresentation_transcribedandTauCeti.Sporadic.suzPresentation_relatorLetters: the thirty-four relator expressions, and the signed letters they compile to.TauCeti.Sporadic.suzPresentation_matchesMetadata,TauCeti.Sporadic.suzPresentation_map_length_relators,TauCeti.Sporadic.suzPresentation_totalLengthandTauCeti.Sporadic.suzPresentation_relatorsCyclicallyReduced: the decidable checks on the transcribed data, namely its relator count, its per-relator letter counts, their total, and cyclic reducedness of every compiled word.
References #
- R. Lindenbergh, Group Presentations Library, version 1.0, record
GPLTable.Suz.1, https://doris.tudelft.nl/~rlindenbergh/GPL/gpl.g. - C. E. Praeger and L. H. Soicher, Low Rank Representations and Graphs for Sporadic Groups, Cambridge University Press, 1997, Chapter 4, doi:10.1017/CBO9780511526039.005.
- KitaKen1, FiniteSimpleGroups, Suzuki construction at commit
7f09e33a9ceef6b59ce03e34cd4f0558c763e325, https://github.com/KitaKen1/finite-simple-groups-lean.
The Group Presentations Library finite presentation GPLTable.Suz.1 of the Suzuki sporadic
group on generators a, b, c, d, e, f, and g.
The source describes this as a full presentation of the abstract group and identifies its origin as Praeger--Soicher. 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, c, d, e, f, g.
Source: R. Lindenbergh, Group Presentations Library, version 1.0; presentation attributed there to C. E. Praeger and L. H. Soicher, Low Rank Representations and Graphs for Sporadic Groups, Cambridge University Press, 1997.
Source locator: GPLTable.Suz.1 in https://doris.tudelft.nl/~rlindenbergh/GPL/gpl.g; Praeger--Soicher, Chapter 4, doi:10.1017/CBO9780511526039.005
Generator convention: Generators have source order a,b,c,d,e,f,g, so indices 0 through 6 have
those names. A Coxeter path declares each node to be an involution, a labeled edge x-m-y declares
(x*y)^m = 1, and an omitted edge declares (x*y)^2 = 1. Products are read left to right. The
source decoder compiles x = y as x^-1*y.
Transcription notes: Expand the paths a5b3c8d3e and b3f4g3b to seven square relations, seven
labeled-edge relations, and fourteen omitted-edge relations. Append the five words in presdef[3],
compiling the two equalities by the source's MakeWordList decoder, and the one word in presdef[4].
The latter is present because InitializeGroupPresentationGPL includes presdef[4] when GPL_PCE is
true, as it is by default in version 1.0. The expected relator count and total length are derived
from this exact expansion. An independent read-through of GPLTable.Suz.1 and its DeCoxList,
MakeWordList, and InitializeGroupPresentationGPL decoders checked the generator order, both paths,
all six appended relations, and the compiled signed letters; the itemized comparison is recorded
in this module's independent audit section. GAP 4.15.1 enumerates 1782 cosets of the subgroup
generated by a through f, which the source labels G2(4). An independent comparison transports the
resulting 1782-point action to the graph in finite-simple-groups-lean at commit
7f09e33a9ceef6b59ce03e34cd4f0558c763e325 and checks mutual generator membership with that
construction of Suz; the comparison is recorded in this module's independent audit section.
Instances For
The number of generators in the presentation of Suz.
The relator count recorded for Suz.
The relator expressions transcribed for Suz, with all thirty-four words visible to consumers
of the sealed presentation definition.
The relator count recorded for Suz agrees with the transcribed data.
The compiled letters and the counts read off them #
The compiled relator words of Suz, spelled out letter by letter. A letter (i, true) is
the generator of index i and (i, false) is its inverse, so index 0 reads a and index 6
reads g.
This is the form in which the transcription is compared with the source one letter at a time, and
it is the check the relator count of TauCeti.Sporadic.suzPresentation_matchesMetadata cannot make:
a relator exchanged for another of the same shape, or an omitted-edge pair written twice while
another is dropped, leaves the count unchanged. Read off this list, the twenty-one pair relations
among the twenty-eight words decoded from the two Coxeter paths carry each unordered pair of the
seven generators exactly once: the seven pairs named by the paths with the exponents
5, 3, 8, 3, 3, 4, 3 in that order, and the remaining fourteen with exponent two.
The per-relator lengths and the total below are read off these letters. The cyclic-reduction check
instead recompiles the bounded words from TauCeti.Sporadic.suzPresentation_transcribed, since
forgetting the generator bounds forgets the type that predicate is stated on.
The lengths of the thirty-four compiled relator words of Suz, in the order of the
transcription: the seven involution relations, the twenty-one pair relations, and then the six
words appended after the Coxeter paths.
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.suzPresentation_totalLength.
The compiled relators of the Suz presentation contain 275 signed letters in total. This is
read off from the spelled-out letters rather than from the record. The source publishes no
presentation length, so the figure states the transcribed data for a reviewer to compare against
the source and is not matched to a published number.
Every compiled relator of the Suz presentation is cyclically reduced. This is what would make
the letter count of TauCeti.Sporadic.suzPresentation_totalLength comparable with a published
presentation length, which is measured after free and cyclic reduction of each relator. Every
compiled word here being already cyclically reduced, that length is the 275 of
TauCeti.Sporadic.suzPresentation_totalLength itself.