A transcribed presentation of the third Conway group

This file carries the Co₃ row of the sporadic presentation data required by milestone S1 of TauCetiRoadmap/CFSGStatement/README.md. It records Đoković's Coxeter-type presentation of the third Conway group on seven involutions as a TauCeti.GroupPresentation, together with its exact source, generator convention, transcription notes, expected counts, and decidable checks on the transcription: the relator count, the per-relator and total letter counts of the compiled words, and their cyclic reducedness.

The twenty-four defining relators are

a², b², c², d², e², f², g²,
(ac)², (ad)², (ae)², (bd)², (ce)², (dg)², (eg)²,
(ab)³, (cd)³, (de)³,
f(ag)³, g(bf)³, (cfg)³, e(abc)³, e(acg)⁴, (bcfcf)³, e(abcf)⁷.

These expressions have source length 174: the sum of their freely reduced word lengths plus one separator for each relator. This reproduces presentation (13.1) and its stated length exactly. The paper obtains the presentation from a faithful permutation representation of Co₃ and verifies its defining data using Todd--Coxeter enumeration and recognition results, rather than presenting the displayed relations as a generator-recognition test inside a pre-existing group.

As an independent transcription check, GAP 4.15.1 enumerates 170775 cosets of the subgroup generated by a, b, c, e, f, and g, exactly the index reported in the paper. Its coset action has degree 170775, is simple of order 495766656000, and GAP constructs an isomorphism from that image to AtlasRep 2.1.9's independent 276-point permutation group for Co₃. This is transcription provenance rather than a Lean theorem: the file asserts no order, finiteness, simplicity, or identification result.

Independent source-to-Lean read-through

An independent read-through used Cambridge University Press's 26-page scan of the cited paper, whose PDF bytes have SHA-256 digest da209040c860db5c0f3bef11a55d5e434beeae3bf9acf18f488b5c8632b23606. On printed page 162, presentation (13.1) names its generators, in order, as a,b,c,d,e,f,g. Reading its defining relators from left to right gives the same four consecutive blocks as the list above: the seven generator squares; the seven pair squares from (ac)² through (eg)²; the three pair cubes; and the seven remaining mixed words, from f(ag)³ through e(abcf)⁷. This is exactly the order and grouping of the twenty-four entries in co3Presentation_transcribed. In particular, the adjacent leading factors in f(ag)³, g(bf)³, e(abc)³, e(acg)⁴, and e(abcf)⁷ lie outside their parenthesized powers in both the print and Lean. The paper then states Length = 174, agreeing with the checked 150 letters plus 24 separators. Its following Consequences line separately lists twelve words, from afaf through (bede)⁴; none is part of the defining-relator list or the Lean row. This checks every source relator, exponent, binding boundary, and the defining-relator/consequence boundary independently of the original transcription and closes this row's S1 source-to-Lean read-through without duplicating the audited list.

Independent comparison with FiniteSimpleGroups

The comparison used finite-simple-groups-lean at commit 7f09e33a9ceef6b59ce03e34cd4f0558c763e325, whose named permutations co3a through co3f generate a subgroup of Equiv.Perm (Fin 276) with proved order 495766656000 and proved simplicity. Its first five generators fix point 275 and restrict to the pinned McL generators; the sixth moves that point.

An independent ATLAS 276-point standard pair is given by the files Co3G1-p276B0.g1 and Co3G1-p276B0.g2. It has orders 3 and 4, with product of order 14, and the two files have respective SHA-256 digests 3681b302dfb31792d27d3d5c82b29ffb8576cd6f8fea063c5c5de97cc4fc7ed9 and ef3a53d716836ee0d773dc5591e42f16c9c4954c84902eddc15fc42e8a42fce8. In that group, the centralizer of an involution whose conjugacy class has length 170775 has order 2903040. GAP 4.15.1 maps presentation (12.4) for 2·S₆(2), augmented only by its seven separately published consequences, onto this centralizer. For the resulting images of a,b,c,e,f,g, their common centralizer under a,b,g has order 6 and contains exactly two involutions d satisfying (cd)³ = (de)³ = 1; both seven-tuples generate the ATLAS group. The comparison selected the lexicographically first forward image table for d.

To align point numberings, the ATLAS two-point stabilizer was computed. Its suborbits on a point-0 descendant have lengths 1, 112, and 162; the orbital of length 112 gives its McLaughlin graph. Canonically labeling that graph and the pinned construction's point-275 descendant with pynauty transports the selected seven involutions into the pinned numbering. Direct calculation makes all twenty-four compiled relators in this module the identity. Schreier--Sims membership checks put those seven involutions in the subgroup generated by co3a through co3f and put all six named generators back in the subgroup generated by the seven; both subgroups therefore have order 495766656000 and are equal.

The check used GAP 4.15.1, Python 3.14.6, pynauty 2.8.8.1, and SymPy 1.14.0. Concatenating the transported forward image tables for a through g, with each image stored as a two-byte little-endian integer, has SHA-256 ee4532949351e7b12adf4a156f7d7aeecb07c4c3ae134773f1cbf19da7da546c. 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, and here they check the transcription against a published figure. The twenty-four compiled words have 150 letters in total, so with one separator for each relator they have the length 174 that presentation (13.1) states. Đoković measures a relator by its freely reduced length, so what makes that comparison legitimate is that every compiled word is cyclically reduced and hence, by FreeGroup.IsCyclicallyReduced.isReduced, already freely reduced: its letter count is the reduced length the source counts. The individual lengths locate any discrepancy in the total.

These field equations and the checks beside them follow the shape that the TauCeti.GroupTheory.SpecificGroups.CFSG.Sporadic.Janko modules established for a manifest row.

Main definitions and results

• TauCeti.Sporadic.co3Presentation: Đoković's finite presentation of Co₃.
• TauCeti.Sporadic.co3Presentation_transcribed and the equations for the remaining fields: the characterization of the sealed row.
• TauCeti.Sporadic.co3Presentation_map_length_relators, TauCeti.Sporadic.co3Presentation_totalLength and TauCeti.Sporadic.co3Presentation_relatorsCyclicallyReduced: the three checks on the compiled words, the second of which gives their 150-letter total.
• TauCeti.Sporadic.co3Presentation_totalLength_add_length_transcribed: that total together with one separator for each relator, the length 174 that presentation (13.1) states.

References

• D. Ž. Đoković, Presentations of some finite simple groups, J. Austral. Math. Soc. Ser. A 45 (1988), 143--168, presentation (13.1), p. 162, https://doi.org/10.1017/S1446788700030068.
• R. A. Wilson, R. A. Parker, J. N. Bray et al., ATLAS of Finite Group Representations, the 276-point Co3 standard-generator files https://brauer.maths.qmul.ac.uk/Atlas/spor/Co3/gap/Co3G1-p276B0.g1 and https://brauer.maths.qmul.ac.uk/Atlas/spor/Co3/gap/Co3G1-p276B0.g2.
• KitaKen1, FiniteSimpleGroups, Co3 construction at commit 7f09e33a9ceef6b59ce03e34cd4f0558c763e325, https://github.com/KitaKen1/finite-simple-groups-lean.

def TauCeti.Sporadic.co3Presentation : GroupPresentation

Đoković's Coxeter-type finite presentation of the third Conway group Co₃ on seven involutions a, b, c, d, e, f, and g.

The cited source gives a presentation of the abstract group, not a semi-presentation used only to recognize generators inside a group already constructed. No structural property of the presented group is asserted here: this definition records only the cited generators and relators.

Generator order (starting at index zero): a, b, c, d, e, f, g.

Source: Dragomir Z. Djokovic, Presentations of some finite simple groups, Journal of the Australian Mathematical Society Series A 45 (1988), 143-168.

Source locator: presentation (13.1), p. 162, https://doi.org/10.1017/S1446788700030068

Generator convention: The seven involutory generators a, b, c, d, e, f, and g in presentation (13.1), in that order, so indices 0 through 6 carry those names. Products are read left to right, juxtaposition denotes multiplication, and powers bind before an adjacent factor: for example, f(ag)^3 is f multiplied by the third power of ag.

Transcription notes: Transcribe the twenty-four defining relators in presentation (13.1), excluding the twelve words listed separately as consequences. Their source length is 174. GAP 4.15.1 reproduces the reported index 170775 for the subgroup generated by a,b,c,e,f,g; the resulting simple coset-action image has order 495766656000 and GAP identifies it with AtlasRep 2.1.9's independent 276-point Co3 permutation group.

@[simp]

theorem TauCeti.Sporadic.co3Presentation_generatorCount : co3Presentation.generatorCount = 7

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

@[simp]

theorem TauCeti.Sporadic.co3Presentation_expectedRelatorCount : co3Presentation.expectedRelatorCount = 24

The relator count Co₃'s source states; see TauCeti.Sporadic.co3Presentation_generatorCount.

@[simp]

theorem TauCeti.Sporadic.co3Presentation_transcribed : co3Presentation.transcribed = [(Relator.gen ⟨0, co3Presentation_transcribed._proof_2⟩).pow 2, (Relator.gen ⟨1, co3Presentation_transcribed._proof_4⟩).pow 2, (Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩).pow 2, (Relator.gen ⟨3, co3Presentation_transcribed._proof_7⟩).pow 2, (Relator.gen ⟨4, co3Presentation_transcribed._proof_6⟩).pow 2, (Relator.gen ⟨5, co3Presentation_transcribed._proof_1⟩).pow 2, (Relator.gen ⟨6, co3Presentation_transcribed._proof_3⟩).pow 2, ((Relator.gen ⟨0, co3Presentation_transcribed._proof_2⟩).mul (Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩)).pow 2, ((Relator.gen ⟨0, co3Presentation_transcribed._proof_2⟩).mul (Relator.gen ⟨3, co3Presentation_transcribed._proof_7⟩)).pow 2, ((Relator.gen ⟨0, co3Presentation_transcribed._proof_2⟩).mul (Relator.gen ⟨4, co3Presentation_transcribed._proof_6⟩)).pow 2, ((Relator.gen ⟨1, co3Presentation_transcribed._proof_4⟩).mul (Relator.gen ⟨3, co3Presentation_transcribed._proof_7⟩)).pow 2, ((Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩).mul (Relator.gen ⟨4, co3Presentation_transcribed._proof_6⟩)).pow 2, ((Relator.gen ⟨3, co3Presentation_transcribed._proof_7⟩).mul (Relator.gen ⟨6, co3Presentation_transcribed._proof_3⟩)).pow 2, ((Relator.gen ⟨4, co3Presentation_transcribed._proof_6⟩).mul (Relator.gen ⟨6, co3Presentation_transcribed._proof_3⟩)).pow 2, ((Relator.gen ⟨0, co3Presentation_transcribed._proof_2⟩).mul (Relator.gen ⟨1, co3Presentation_transcribed._proof_4⟩)).pow 3, ((Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩).mul (Relator.gen ⟨3, co3Presentation_transcribed._proof_7⟩)).pow 3, ((Relator.gen ⟨3, co3Presentation_transcribed._proof_7⟩).mul (Relator.gen ⟨4, co3Presentation_transcribed._proof_6⟩)).pow 3, (Relator.gen ⟨5, co3Presentation_transcribed._proof_1⟩).mul (((Relator.gen ⟨0, co3Presentation_transcribed._proof_2⟩).mul (Relator.gen ⟨6, co3Presentation_transcribed._proof_3⟩)).pow 3), (Relator.gen ⟨6, co3Presentation_transcribed._proof_3⟩).mul (((Relator.gen ⟨1, co3Presentation_transcribed._proof_4⟩).mul (Relator.gen ⟨5, co3Presentation_transcribed._proof_1⟩)).pow 3), (((Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩).mul (Relator.gen ⟨5, co3Presentation_transcribed._proof_1⟩)).mul (Relator.gen ⟨6, co3Presentation_transcribed._proof_3⟩)).pow 3, (Relator.gen ⟨4, co3Presentation_transcribed._proof_6⟩).mul ((((Relator.gen ⟨0, co3Presentation_transcribed._proof_2⟩).mul (Relator.gen ⟨1, co3Presentation_transcribed._proof_4⟩)).mul (Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩)).pow 3), (Relator.gen ⟨4, co3Presentation_transcribed._proof_6⟩).mul ((((Relator.gen ⟨0, co3Presentation_transcribed._proof_2⟩).mul (Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩)).mul (Relator.gen ⟨6, co3Presentation_transcribed._proof_3⟩)).pow 4), (((((Relator.gen ⟨1, co3Presentation_transcribed._proof_4⟩).mul (Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩)).mul (Relator.gen ⟨5, co3Presentation_transcribed._proof_1⟩)).mul (Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩)).mul (Relator.gen ⟨5, co3Presentation_transcribed._proof_1⟩)).pow 3, (Relator.gen ⟨4, co3Presentation_transcribed._proof_6⟩).mul (((((Relator.gen ⟨0, co3Presentation_transcribed._proof_2⟩).mul (Relator.gen ⟨1, co3Presentation_transcribed._proof_4⟩)).mul (Relator.gen ⟨2, co3Presentation_transcribed._proof_5⟩)).mul (Relator.gen ⟨5, co3Presentation_transcribed._proof_1⟩)).pow 7)]

The relator expressions transcribed for Co₃, 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. Indices 0 through 6 are the involutions a through g of presentation (13.1), and the bounds come from TauCeti.Sporadic.co3Presentation_generatorCount.

theorem TauCeti.Sporadic.co3Presentation_matchesMetadata : co3Presentation.matchesMetadata

The relator count recorded for Co₃ agrees with the transcribed data.

theorem TauCeti.Sporadic.co3Presentation_map_length_relators : List.map List.length co3Presentation.relators = [2, 2, 2, 2, 2, 2, 2, 4, 4, 4, 4, 4, 4, 4, 6, 6, 6, 7, 7, 9, 10, 13, 15, 29]

The lengths of the twenty-four compiled relator words for Co₃, in the order of presentation (13.1).

Reading the counts off one relator at a time is what lets a reviewer locate a discrepancy against the source, rather than only observe one in the total of TauCeti.Sporadic.co3Presentation_totalLength.

theorem TauCeti.Sporadic.co3Presentation_totalLength : co3Presentation.totalLength = 150

The compiled relator words for Co₃ have 150 letters in total.

This is the check against the source's stated figure. Đoković measures the length of a presentation as the sum of the freely reduced lengths of its relators together with one separator for each of them, so the twenty-four relators here give 150 + 24 = 174, which is the length presentation (13.1) states.

theorem TauCeti.Sporadic.co3Presentation_totalLength_add_length_transcribed : co3Presentation.totalLength + co3Presentation.transcribed.length = 174

The source's stated length of presentation (13.1), recovered from the transcribed data: the letters of the compiled relator words together with one separator for each relator.

theorem TauCeti.Sporadic.co3Presentation_relatorsCyclicallyReduced : co3Presentation.relatorsCyclicallyReduced

Every compiled relator word for Co₃ is cyclically reduced, hence by FreeGroup.IsCyclicallyReduced.isReduced freely reduced. This is what makes the letter count of TauCeti.Sporadic.co3Presentation_totalLength comparable with the length stated by presentation (13.1), which measures each relator by its freely reduced length.