A transcribed presentation of the first 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 on the standard generators a and b as a TauCeti.GroupPresentation, together with the source, generator convention, transcription notes, and expected counts.

The presentation displayed by the ATLAS is

⟨a, b | a² = b³ = (ab)⁷
       = (ab(abab⁻¹)³)⁵
       = (ab(abab⁻¹)⁶abab(ab⁻¹)²)² = 1⟩.

The structured expressions below preserve those products and powers. The previously proved Relator.toWord_toFreeGroup theorem is the audit boundary between these expressions and the signed words used by PresentedGroup.

As an independent transcription check, GAP 4.15.1 was used in two directions. The five relators evaluate to the identity on the ATLAS package's independent 266-point standard generators for J₁; conversely, Todd--Coxeter enumeration of the abstract presentation gives order 175560, and GAP constructs an isomorphism from its permutation image to the ATLAS group. This computation is provenance for the transcription, not a Lean theorem. 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 J1G1-P1.M whose SHA-256 digest is d59534c449adee5461053f262627c77b3ffce57e2b25741dcdfecf9c030c9ae4. Its constructor G<x,y> fixes the generator order, and the assignments a := x; b := y immediately after it confirm that these are the standard generators called a,b in this row.

The five constructor entries, in source order, are

x²,
y³,
(xy)⁷,
(xy (xyxy⁻¹)³)⁵,
(xy (xyxy⁻¹)⁶ xyxy (xy⁻¹)²)².

They agree in every letter, inverse, exponent, and source-order position with j1Presentation_transcribed: repeatedWord is xyxy⁻¹, fifthPowerBase is the fourth source base, and squareBase is the fifth. No constructor entry is commented out or marked redundant. 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 j1a, j1b, and j1c generate a subgroup of Equiv.Perm (Fin 266) with proved order 175560 and proved simplicity. Write those three permutations as x, y, and z. The following words in them give images of the ATLAS presentation generators (products are written in display order):

a = (z⁻¹ z⁻¹ x⁻¹ y x⁻¹ x⁻¹ z z y z⁻¹ x z⁻¹ y z⁻¹ y⁻¹ y⁻¹
     x⁻¹ x⁻¹ z⁻¹ x z y⁻¹)⁵
b = (z⁻¹ y⁻¹ y⁻¹ z⁻¹ x⁻¹ y x z z z y⁻¹ z x⁻¹ y⁻¹ x z x x x
     z⁻¹ y z⁻¹ x z⁻¹ z⁻¹ x⁻¹)².

Direct permutation calculation gives orders 2, 3, and 7 for a, b, and ab, and all five 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 latter therefore has order 175560 and is the pinned subgroup.

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 8ce03dd9c719b08567f80eb6289a08146479a83653c57c6213226aead66c8b0e. 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 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.j1Presentation: the ATLAS finite presentation of J₁.
• TauCeti.Sporadic.j1Presentation_transcribed and the equations for the remaining fields: the characterization of the sealed row.
• TauCeti.Sporadic.j1Presentation_map_length_relators, TauCeti.Sporadic.j1Presentation_totalLength and TauCeti.Sporadic.j1Presentation_relatorsCyclicallyReduced: the three checks on the compiled words.

References

• R. A. Wilson, R. A. Parker, and J. N. Bray, ATLAS of Finite Group Representations, version 3, J₁, section "Presentation", https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/J1/.
• KitaKen1, FiniteSimpleGroups, J1 construction at commit 7f09e33a9ceef6b59ce03e34cd4f0558c763e325, https://github.com/KitaKen1/finite-simple-groups-lean.

def TauCeti.Sporadic.j1Presentation : GroupPresentation

The ATLAS version 3 finite presentation of the first Janko group J₁ on its standard generators a and b.

The ATLAS supplies a full presentation of the abstract group, rather than the semi-presentation used elsewhere in the database to recognize standard generators in an already constructed group. 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, and J. N. Bray, ATLAS of Finite Group Representations, version 3.

Source locator: J_1 page, Presentation section, https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/J1/

Generator convention: The ATLAS standard generators a and b, in that order, so index 0 is a and index 1 is b. Products are read left to right and negative exponents denote inverses.

Transcription notes: The five displayed words are stored as five relators equal to the identity. GAP 4.15.1 checks them on the independent ATLAS 266-point generators; enumeration of this abstract presentation gives order 175560 and an isomorphism to the ATLAS group.

@[simp]

theorem TauCeti.Sporadic.j1Presentation_generatorCount : j1Presentation.generatorCount = 2

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.

@[simp]

theorem TauCeti.Sporadic.j1Presentation_expectedRelatorCount : j1Presentation.expectedRelatorCount = 5

The relator count J₁'s source states; see TauCeti.Sporadic.j1Presentation_generatorCount.

@[simp]

theorem TauCeti.Sporadic.j1Presentation_transcribed : j1Presentation.transcribed = [(Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩).pow 2, (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩).pow 3, ((Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩)).pow 7, (((Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩)).mul (((((Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩)).mul (Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩)).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩).inv).pow 3)).pow 5, ((((((((Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩)).mul (((((Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩)).mul (Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩)).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩).inv).pow 6)).mul (Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩)).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩)).mul (Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩)).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩)).mul (((Relator.gen ⟨0, j1Presentation_transcribed._proof_1⟩).mul (Relator.gen ⟨1, j1Presentation_transcribed._proof_2⟩).inv).pow 2)).pow 2]

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.j1Presentation_generatorCount.

theorem TauCeti.Sporadic.j1Presentation_matchesMetadata : j1Presentation.matchesMetadata

The relator count recorded for J₁ agrees with the transcribed data.

theorem TauCeti.Sporadic.j1Presentation_map_length_relators : List.map List.length j1Presentation.relators = [2, 3, 14, 70, 68]

The lengths of the five compiled relator words for J₁, 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.j1Presentation_totalLength.

theorem TauCeti.Sporadic.j1Presentation_totalLength : j1Presentation.totalLength = 157

The compiled relator words for J₁ have 157 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.

theorem TauCeti.Sporadic.j1Presentation_relatorsCyclicallyReduced : j1Presentation.relatorsCyclicallyReduced

Every compiled relator word for J₁ is cyclically reduced. This is what makes the letter count of TauCeti.Sporadic.j1Presentation_totalLength comparable with a published presentation length, which is measured after free and cyclic reduction of each relator.