A transcribed presentation of the third Janko group #
This file carries the J₃ row of the sporadic presentation data required by milestone S1 of
TauCetiRoadmap/CFSGStatement/README.md. It records the ATLAS version 3 presentation of the third
Janko group on its standard generators a and b as a TauCeti.GroupPresentation; the ATLAS page
records no individual contributor for this presentation. The data includes the source, the
generator convention, transcription notes, and the expected counts.
Writing s₁ = ab and s₋₁ = ab⁻¹ for the two syllables that occur, the eight transcribed relators
are
a², b³, [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₋₁)²)⁴.
They are stored in the order of the source's Magma file, which lists [a,b]⁹ before s₁¹⁹; the
presentation page displays the same eight words with those two interchanged. No word in this source
is marked redundant, in either of its two renderings.
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 structured expressions otherwise preserve the displayed products
and powers. 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 of the abstract group rather than a semi-presentation, and it comes
with a demonstration of correctness: its Magma file exhibits the cyclic subgroup K₁ = ⟨ab⟩ of
order 19 and prescribes the coset enumeration 19 * Index(G, K₁), which returns the order
50232960 of J₃, together with enumerations over the involution centralizer 2^{1+4}:A₅ and over
each maximal subgroup at the indices the ATLAS records for J₃.
As an independent transcription check, GAP 4.15.1 was run in both directions on the eight words
that Relator.toWord compiles from the expressions below, so that the check applies to the
compiled data rather than to a rereading of the source. Each compiled word evaluates to the
identity on the ATLAS 6156-point standard generators of J₃, which are representation data
unrelated to this presentation; those generators have a an involution with centralizer of order
1920, b of order 3 with centralizer of order 1080, and ab of order 19, as the ATLAS classes
2A and 3A require, and they generate a simple group of order 50232960. Conversely, Todd--Coxeter
enumeration of the compiled presentation over the subgroup generated by ab returns the index
2643840, and the relator (ab)¹⁹ bounds that subgroup by 19, so the presented group has order at
most 50232960 and hence exactly 50232960. Both computations are provenance for the
transcription, not Lean theorems: this file asserts no order, finiteness, simplicity, or
identification result. The roadmap's further cross-check against the FiniteSimpleGroups
permutation development is unavailable for J₃, which that development does not cover.
Independent source-to-Lean read-through #
An independent read-through used the bytes of the ATLAS Magma source J3G1-P1.M whose SHA-256
digest is db34e17432d777cb96784c78883ff956352f822ae1f9472f60fdff96a26f5082. Its constructor
G<x,y> and later assignments a := x; b := y fix the generator order used by the Lean row.
The source constructor lists, in order,
x², y³, [x,y]⁹, (xy)¹⁹, ((xy)⁶(xy⁻¹)⁵)²,
((xyxyxy⁻¹)² xy xy⁻¹ xy⁻¹ xy xy⁻¹)²,
xyxy (xyxy⁻¹)³ xyxy (xyxy⁻¹)⁴ xy⁻¹ (xyxy⁻¹)³,
((xy)³(xyxy⁻¹)²)⁴.
These are exactly the eight entries of j3Presentation_transcribed after substituting
s₁ = ab and s₋₁ = ab⁻¹ and expanding the source commutator as x⁻¹y⁻¹xy. In particular, the
Lean row follows the Magma order in placing [x,y]⁹ before (xy)¹⁹; the rendered ATLAS page has
the same words with those two positions swapped. No constructor entry is commented out or marked
redundant. This checks every source relator, inverse, exponent, and source-order position
independently of the original transcription and closes this row's S1 source-to-Lean read-through.
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 records no published length, so the total here states the transcription for a reviewer to compare with the source, rather than checking it against a recorded number.
Main definitions and results #
TauCeti.Sporadic.j3Presentation: the ATLAS finite presentation ofJ₃, for which the ATLAS records no individual contributor.TauCeti.Sporadic.j3Presentation_transcribedand the equations for the remaining fields: the characterization of the sealed row.TauCeti.Sporadic.j3Presentation_map_length_relators,TauCeti.Sporadic.j3Presentation_totalLengthandTauCeti.Sporadic.j3Presentation_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
J3G1-P1, with no individual contributor recorded, https://brauer.maths.qmul.ac.uk/Atlas/v3/pres/J3G1-P1, with the relator list and the demonstration of correctness in the Magma source file https://brauer.maths.qmul.ac.uk/Atlas/spor/J3/mag/J3G1-P1.M.
The ATLAS version 3 finite presentation of the third Janko group J₃ on its standard
generators a and b; the ATLAS records no individual contributor for this presentation.
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; individual presentation contributor not recorded.
Source locator: J3G1-P1, https://brauer.maths.qmul.ac.uk/Atlas/v3/pres/J3G1-P1, with the relator list and the demonstration of correctness in the Magma source file https://brauer.maths.qmul.ac.uk/Atlas/spor/J3/mag/J3G1-P1.M
Generator convention: The ATLAS standard generators a and b of J3, that is, a in class 2A and b in class 3A with ab of order 19, 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 eight words of the source's relator list are stored as eight relators
equal to the identity, in the order of the Magma file; the ATLAS page records no individual
contributor for this presentation. The presentation page displays the same eight words with
(x,y)^9 and (x*y)^19 interchanged. No word is marked redundant in either rendering. The source
demonstrates correctness by the coset enumeration 19*Index(G,K1) over the cyclic subgroup K1 =
<a*b> of order 19, returning the order 50232960 of J3. GAP 4.15.1 reproduces that enumeration
from the eight compiled words, obtaining the index 2643840, and checks that the same eight words
vanish on the ATLAS 6156-point standard generators of J3, which have a an involution with
centralizer of order 1920, b of order 3 with centralizer of order 1080, ab of order 19, and which
generate a simple group of order 50232960.
Instances For
The number of generators in the presentation of J₃. The row's body is sealed, so this is
what lets a
consumer see that it is a two-generator presentation.
The relator count J₃'s source states; see
TauCeti.Sporadic.j3Presentation_generatorCount.
The relator expressions transcribed for J₃, with their generator indices written out and the
private 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.j3Presentation_generatorCount. Every occurrence of a syllable ab or ab⁻¹ is
bracketed, since the stored expression is a tree and not a flat word.
The relator count recorded for J₃ agrees with the transcribed data.
The lengths of the eight compiled relator words for J₃, in the order of the Magma source
file.
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.j3Presentation_totalLength.
The compiled relator words for J₃ have 273 letters in total. The row records no published
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 J₃ is cyclically reduced. This is what makes the letter count
of TauCeti.Sporadic.j3Presentation_totalLength comparable with a published presentation length,
which is measured after free and cyclic reduction of each relator.