A transcribed presentation of the second Janko group

This file carries the J₂ row of the sporadic presentation manifest required by milestone S1 of TauCetiRoadmap/CFSGStatement/README.md. It records a published two-generator, three-relator presentation in TauCeti.GroupPresentation, including its exact source, generator convention, transcription notes, and expected counts.

The presentation is the n = 7, order 604800 entry in Section 3 of Stoytchev's paper. In the source's notation it is

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

The source writes the exponent in the last relation as ±3, thereby giving two presentations; this file chooses the displayed positive exponent. Equalities are transcribed as relators by multiplying the left-hand side by the inverse of the right-hand side. Thus the first two compiled words are a b a B A B and a b b a B B B B B, where capitals denote inverses.

Checks

The relator count is checked by j2Presentation_matchesMetadata. The stored expressions preserve the source's powers and display each relation in the same left-to-right order; Relator.toWord_toFreeGroup is the already-proved audit boundary from those expressions to the signed words used by PresentedGroup.

Three further decidable checks record the compiled words: their lengths one relator at a time, their total, and cyclic reducedness, which 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.

The row is a sealed definition, so it also 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.

As an independent transcription check, the exact three relators below were enumerated with GAP 4.15.1 over the trivial subgroup; the resulting finitely presented group has order 604800, agreeing with both the paper and GAP's Atlas group J2. This computation is provenance for the transcription, not a Lean theorem, and 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 arXiv v1 PDF whose SHA-256 digest is ecdc292ea95ec143251eef270c892bac9edeb4fbf4302f494cf71db75dbf79f6. In Section 3, under n = 7 (Hurwitz groups), the order-604800 entry labelled J₂ first presents

aba = bab,
ab²a = b⁵,
(ab⁻¹ab⁻³a³b⁻¹)^(±3) a⁷ = 1.

The source then gives a second efficient presentation with the long word moved into the right-hand side of the second equality; this row deliberately transcribes the first display. Its choice of the positive sign gives the third entry of j2Presentation_transcribed exactly. For the first equality, multiplying by (bab)⁻¹ gives the stored six-letter relator; for the second, multiplying by b⁻⁵ gives the stored nine-letter relator. Thus the source family, chosen display, sign, equation orientation, every exponent, and all three source-order positions agree with the sealed row. This comparison was performed from the pinned PDF 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 j2a, j2b, j2c, and j2d generate a subgroup of Equiv.Perm (Fin 100) with proved order 604800 and proved simplicity. Write those permutations as x, y, z, and w. The following words in them give images of Stoytchev's presentation generators (products are written in display order):

a = w z x⁻¹ z y⁻¹ w⁻¹ w⁻¹ x⁻¹ w x z⁻¹ x z⁻¹ x⁻¹ z y⁻¹ y⁻¹ x⁻¹ y z x x
b = w⁻¹ y x⁻¹ w y w z y w⁻¹ x z x⁻¹ y⁻¹ x y z⁻¹ w⁻¹ z⁻¹ y x y x⁻¹
    z⁻¹ z⁻¹ x⁻¹ x⁻¹ w z⁻¹.

Both displayed permutations have order 7, and direct calculation makes all three compiled relators in this module equal to the identity, including the row's chosen positive exponent in the last relation. Schreier--Sims membership checks put a,b in the subgroup generated by x,y,z,w and put all four named generators back in ⟨a,b⟩; this pair therefore generates the pinned group of order 604800.

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 one byte, has SHA-256 2208e51b4e8a911e8618a614f0c475cc88b08e3a858fa137e304d6e63c4c6f71. This is the independent comparison artifact required by S1; no external code or permutation data is imported into Tau Ceti.

Main definitions and results

• TauCeti.Sporadic.j2Presentation: Stoytchev's finite presentation of J₂.
• TauCeti.Sporadic.j2Presentation_transcribed and the equations for the remaining fields: the characterization of the sealed row.
• TauCeti.Sporadic.j2Presentation_map_length_relators, TauCeti.Sporadic.j2Presentation_totalLength and TauCeti.Sporadic.j2Presentation_relatorsCyclicallyReduced: the three checks on the compiled words.

References

• O. Stoytchev, A Class of Efficient Presentations of Finite Simple Groups, arXiv:2011.05660v1 (2020), Section 3, n = 7, order 604800 entry.
• KitaKen1, FiniteSimpleGroups, J2 construction at commit 7f09e33a9ceef6b59ce03e34cd4f0558c763e325, https://github.com/KitaKen1/finite-simple-groups-lean.

def TauCeti.Sporadic.j2Presentation : GroupPresentation

A finite presentation of the second Janko group J₂, transcribed from the order 604800 entry in Section 3 of Stoytchev's A Class of Efficient Presentations of Finite Simple Groups.

The source obtains this presentation by enumerating the finitely presented group and checking that the group of order 604800 is simple. No such structural property is asserted here: this definition records only the cited generators and relations.

Generator order (starting at index zero): a, b.

Source: O. Stoytchev, A Class of Efficient Presentations of Finite Simple Groups, arXiv:2011.05660v1 (2020).

Source locator: Section 3, n = 7, order 604800 entry (the presentation labelled J_2)

Generator convention: The generators a and b of the source, in that order, so index 0 is a and index 1 is b. Products are read left to right, negative exponents denote inverses, and each displayed equality is imposed as a relator equal to the identity.

Transcription notes: The relations aba = bab and ab^2 a = b^5 are transcribed as aba(bab)^-1 and ab^2 a b^-5. For the source's final relation (a b^-1 a b^-3 a^3 b^-1)^(±3) a^7 = 1, this row chooses the positive exponent +3. GAP 4.15.1 independently enumerates these exact three relators to order 604800.

@[simp]

theorem TauCeti.Sporadic.j2Presentation_generatorCount : j2Presentation.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.j2Presentation_expectedRelatorCount : j2Presentation.expectedRelatorCount = 3

The relator count J₂'s source states; see TauCeti.Sporadic.j2Presentation_generatorCount.

@[simp]

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

The relator expressions transcribed for J₂, with their generator indices written out and the private abbreviation 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.j2Presentation_generatorCount.

theorem TauCeti.Sporadic.j2Presentation_matchesMetadata : j2Presentation.matchesMetadata

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

theorem TauCeti.Sporadic.j2Presentation_map_length_relators : List.map List.length j2Presentation.relators = [6, 9, 37]

The lengths of the three 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.j2Presentation_totalLength.

theorem TauCeti.Sporadic.j2Presentation_totalLength : j2Presentation.totalLength = 52

The compiled relator words for J₂ have 52 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.j2Presentation_relatorsCyclicallyReduced : j2Presentation.relatorsCyclicallyReduced

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