A transcribed presentation of the O'Nan sporadic group #

This file carries the ONan row of the sporadic presentation data required by milestone S1 of TauCetiRoadmap/CFSGStatement/README.md. It records GPLTable.ON.1 from Roderik 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 starts with the Coxeter path

a --3-- b --3-- c --8-- d --3-- e --3-- f.

Thus the path declares x² = 1 for each of a through f, (xy)^m = 1 for each displayed edge x --m-- y, and (xy)² = 1 for every pair omitted from the path. These are power relations, so they force each of those orders to divide the exponent shown; that any exponent is attained is not recorded here and is not proved below. The source then adds a seventh generator g and the eight relations

g^4,  af = g^2,  af = (cd)^4,  c c^(dgdg),  d d^(cgcg),  (bcdg)^5,
g b g^c g^b g^c,  g e g^d g^e g^d.

Here the source uses x^y = y^-1 x y, and its decoder compiles an equality x = y to the relator x^-1 y. The Coxeter path contributes six square relations and fifteen pair relations, so the complete list has 21 + 8 = 29 relators.

The row's body is sealed, so the equations below publish its generator count, expected relator count, and relator expressions, and spell the compiled words out letter by letter. Its docstring records the sources, generator convention, and transcription notes. The metadata theorem checks the relator count, and two further decidable checks show that the compiled words contain 172 signed letters and are cyclically reduced. GPL records no relator total or presentation length, so the figures 29 and 172 compare the compiler's output with the hand expansion of the path and eight auxiliary words, rather than with published figures. As a separate transcription check, GAP 4.15.1 enumerates 122760 cosets of the subgroup generated by a through f, agreeing with the index of the L3(7):2 subgroup recorded by GPL. An independent read-through of the version 1.0 GPLTable.ON.1 record and its DeCoxList, MakeWordList, and InitializeGroupPresentationGPL decoders checked the generator order, Coxeter path, all eight appended relations, conjugation convention, and compiled signed letters below. These checks are provenance rather than Lean theorems: this file asserts no order, finiteness, simplicity, or identification result. The independent FiniteSimpleGroups development does not cover ONan, so no further comparison against it applies to this row.

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 := [ "a3b3c8d3e3f", "g",
  "g^4,af=g^2,af=(cd)^4,cc^(dgdg),dd^(cgcg),(bcdg)^5,
   gbg^cg^bg^c,geg^dg^eg^d", ]

and the decoder comparison with onanPresentation_relatorLetters is:

entries 1--6 are the squares of a,b,c,d,e,f inserted by AddTrivialRelations;
entries 7--11 are (ab)^3,(bc)^3,(cd)^8,(de)^3,(ef)^3, the five labeled edges;
entries 12--21 are the exponent-two relations on the ten complementary pairs ac,ad,ae,af,bd,be,bf,ce,cf,df inserted by AddNonEdgeRelations;
entry 22 is g^4;
entries 23--24 are the equality words (af)⁻¹g^2 and (af)⁻¹(cd)^4, using MakeWordList's left-inverse convention;
entries 25--26 are c c^(dgdg) and d d^(cgcg), with every conjugate expanded using the source convention x^y = y⁻¹xy; and
entries 27--29 are (bcdg)^5, g b g^c g^b g^c, and g e g^d g^e g^d.

Expanding the powers, inverses, and conjugates gives exactly the signed lists in onanPresentation_relatorLetters; no source letter or pair 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.

Main definition #

TauCeti.Sporadic.onanPresentation: the GPL finite presentation of the O'Nan sporadic group.

References #

R. Lindenbergh, Group Presentations Library, version 1.0, record GPLTable.ON.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.

source

def TauCeti.Sporadic.onanPresentation :

GroupPresentation

The Group Presentations Library finite presentation GPLTable.ON.1 of the O'Nan 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.ON.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. The Coxeter path declares x^2 = 1 for each of a through f, 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, x^y means y^-1*x*y, and the source decoder compiles x = y as x^-1*y.

Transcription notes: Expand the path a3b3c8d3e3f to six square relations, five labeled-edge relations, and ten omitted-edge relations. Append the eight words in presdef[3], compiling the two equalities and all conjugation expressions by the source's MakeWordList decoder. The expected relator count and total length are derived from this exact expansion. GAP 4.15.1 enumerates 122760 cosets of the subgroup generated by a through f, agreeing with the index of the L3(7):2 subgroup recorded by GPL. An independent read-through of GPLTable.ON.1 and its DeCoxList, MakeWordList, and InitializeGroupPresentationGPL decoders checked the generator order, Coxeter path, all eight appended relations, conjugation convention, and compiled signed letters; the itemized comparison is recorded in this module's independent audit section. The independent FiniteSimpleGroups development does not cover ONan, so no further comparison against it applies to this row.

Instances For

source

@[simp]

theorem TauCeti.Sporadic.onanPresentation_generatorCount :

onanPresentation.generatorCount = 7

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

source

@[simp]

theorem TauCeti.Sporadic.onanPresentation_expectedRelatorCount :

onanPresentation.expectedRelatorCount = 29

The relator count obtained by expanding the source's Coxeter path into six squares, five labeled edges, and ten omitted edges, then appending its eight auxiliary words.

source

theorem TauCeti.Sporadic.onanPresentation_transcribed :

The relator expressions transcribed for ONan, with their generator indices written out.

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 or its private helpers. Indices 0 through 6 are the generators a through g, and the bounds come from TauCeti.Sporadic.onanPresentation_generatorCount. The first twenty-one entries are the Coxeter relations and the last eight are the source's auxiliary words.

source

theorem TauCeti.Sporadic.onanPresentation_matchesMetadata :

onanPresentation.matchesMetadata

The relator count recorded for ONan agrees with the transcribed data.

source

theorem TauCeti.Sporadic.onanPresentation_relatorLetters :

The compiled relator words for ONan, spelled out. A letter (i, true) is the generator with 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 letter by letter. The length check below is read off from these letters; the cyclic-reduction check instead recompiles the bounded words from TauCeti.Sporadic.onanPresentation_transcribed.

source

theorem TauCeti.Sporadic.onanPresentation_totalLength :

onanPresentation.totalLength = 172

The compiled relators of the ONan presentation contain 172 signed letters in total. This is read off from the spelled-out letters rather than from the record.

source

theorem TauCeti.Sporadic.onanPresentation_relatorsCyclicallyReduced :

onanPresentation.relatorsCyclicallyReduced

Every compiled relator of the ONan presentation is cyclically reduced. This is what makes the letter count in TauCeti.Sporadic.onanPresentation_totalLength comparable with a presentation length, which is measured after free and cyclic reduction of each relator.

Only the compiler needs unfolding here: once the transcribed expressions are compiled away, the words are closed data and the kernel decides the predicate.

Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Sporadic.ONan

A transcribed presentation of the O'Nan sporadic group #

Independent source-to-compiled audit record #

Main definition #

References #