A transcribed presentation of the Harada--Norton group #
This file carries the HN row of the sporadic presentation data required by milestone S1 of
TauCetiRoadmap/CFSGStatement/README.md. It records the corrected five-generator presentation of
the Harada--Norton group given by Bray and Curtis as a TauCeti.GroupPresentation, together with
its source, generator convention, transcription notes, characteristic equations, and decidable
checks on the compiled and freely reduced relator words.
The nineteen relators are
a⁴, [a²,b], b⁷, (ab²)⁴, a⁻²(abab³)³, ((ab)³ab⁻³)²,
c²a², [a,c], [bab,c], (bab³c)³,
d², (ad)², [b,d], d^(cbcb⁻¹)(cd)³,
t⁵, t^a t², t^c t⁻², [t,b], (dt)³.
Here [r,s] = r⁻¹s⁻¹rs and r^s = s⁻¹rs, following the Magma source. Mathlib's
commutatorElement uses the opposite commutator convention, so a source commutator is represented
by Relator.commInvInv r s. Conjugates are expanded directly in the structured
expressions. The proved TauCeti.Relator.toWord_toFreeGroup theorem is the audit boundary between
these expressions and the signed words consumed by PresentedGroup.
Section 4 of Bray--Curtis constructs HN as a quotient of a progenitor by coset enumeration over
the visible subgroup 2·HS:2. Section 5 derives the five-generator presentation used here. The
authors' corrected Magma file HNpb.m gives the same nineteen relators exactly; in particular, it
uses (ad)², correcting the preprint's [a,d] at that position. The source describes c and d
as generators adjoined while successively presenting U₃(5):2 and HS:2, and t as the
order-five symmetric generator whose final relations produce HN.
For this audit, the source-to-Lean transcription was independently read against the first
presentation in the corrected machine-readable HNpb.m file. All nineteen expressions agree in
order, including the conjugation convention in the fourteenth relator. The fifth compiled word has
the freely cancelling boundary a⁻²a; the checks below therefore record the raw total of 153
letters alongside the freely reduced length of each relator, and prove that every reduced word is
cyclically reduced. This file asserts no order, finiteness, simplicity, or identification result.
Independent source-to-Lean read-through #
The independent read-through used the bytes of the corrected machine-readable source HNpb.m
whose SHA-256 digest is
69a39c69670aa28dd28f2b3c9ec8f44c35086174d97ba4fc073a16ad7ecec596. The first constructor is
G<a,b,c,d,t>, fixing exactly the generator names and order used by the Lean row. Reading that
constructor from top to bottom gives
a⁴, [a²,b], b⁷, (ab²)⁴, a⁻²(abab³)³, ((ab)³ab⁻³)²,
c²a², [a,c], [bab,c], (bab³c)³,
d², (ad)², [b,d], d^(cbcb⁻¹)(cd)³,
t⁵, t^a t², t^c t⁻², [t,b], (dt)³.
These are exactly the nineteen entries of hnPresentation_transcribed. In particular, the Lean
row preserves the corrected twelfth word (ad)²; expands the Magma conjugates using
r^s = s⁻¹rs, including the full conjugator cbcb⁻¹ in the fourteenth word; and uses the source
commutator [r,s] = r⁻¹s⁻¹rs. The same file contains a second nineteen-relator constructor whose
only changed entry is the fifth, replaced there by [a,b³]³; the row explicitly transcribes the
first presentation and therefore correctly retains a⁻²(abab³)³. There are no commented or
optional entries inside that first constructor. This checks every source relator, inverse,
exponent, conjugation boundary, and constructor boundary independently of the original
transcription and closes this row's S1 source-to-Lean read-through.
Main definitions and results #
TauCeti.Sporadic.hnPresentation: the Bray--Curtis finite presentation ofHN.TauCeti.Sporadic.hnPresentation_transcribedand the equations for the remaining fields: the characterization of the sealed row.TauCeti.Sporadic.hnPresentation_map_length_relatorsandTauCeti.Sporadic.hnPresentation_totalLength: the compiled-word length checks.TauCeti.Sporadic.hnPresentation_map_length_reduce_relatorsandTauCeti.Sporadic.isCyclicallyReduced_reduce_mem_hnPresentation_relators: the corresponding freely reduced checks.
References #
- J. N. Bray and R. T. Curtis, Monomial modular representations and symmetric generation of the Harada--Norton group, J. Algebra 268 (2003), no. 2, 723--743, Sections 4--5, https://doi.org/10.1016/S0021-8693(03)00298-9.
- The authors' corrected version and known-errors record, https://webspace.maths.qmul.ac.uk/j.n.bray/Papers/HN/HN.html, and the corrected machine-readable presentation, https://webspace.maths.qmul.ac.uk/j.n.bray/Papers/HN/HNpb.m.
- The presentation-row characterization and audit theorem scaffold is adapted from the Janko-row formalization in https://github.com/TauCetiProject/TauCeti/pull/5283.
The corrected Bray--Curtis finite presentation of the Harada--Norton group HN on five
generators.
The paper proves that this is a presentation of the abstract group, rather than a semi-presentation used only to recognize generators inside an existing group. 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, t.
Source: J. N. Bray and R. T. Curtis, Monomial modular representations and symmetric generation of the Harada--Norton group, J. Algebra 268 (2003), 723--743.
Source locator: Sections 4--5, especially p. 735; corrected Magma file HNpb.m at https://webspace.maths.qmul.ac.uk/j.n.bray/Papers/HN/HNpb.m
Generator convention: The generators a, b, c, d and t of Bray--Curtis HNpb.m, in that order, so indices 0 through 4 have those names. Products are read left to right, negative exponents denote inverses, [r,s] denotes r^-1 s^-1 r s, and r^s denotes s^-1 r s.
Transcription notes: The nineteen words in the first presentation of the corrected HNpb.m file are
stored as nineteen relators equal to the identity. They agree in order and spelling with the
five-generator presentation displayed in Section 5 of the corrected paper. The corrected source
uses (a*d)^2 as its twelfth relator; the authors' known-errors record notes that the preprint's
[a,d] at this position was wrong. An independent source-to-Lean read-through of the corrected
HNpb.m file confirms all nineteen stored expressions and their order.
Instances For
The number of generators in the presentation of HN. The row's body is sealed, so this
equation is what shows
a consumer that the transcription is on five generators, and it supplies the index bounds in
TauCeti.Sporadic.hnPresentation_transcribed.
The relator count stated by the HN source.
The relator expressions transcribed for HN, 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 auditing the transcription never has to unfold the
row. Indices 0 through 4 are the generators a, b, c, d and t, and their bounds come
from TauCeti.Sporadic.hnPresentation_generatorCount.
The relator count recorded for HN agrees with the transcribed data.
The lengths of the nineteen compiled relator words for HN, in source order.
The fifth source word contains the freely cancelling boundary a⁻²a; this theorem records the
compiled words before reduction, exactly as TauCeti.GroupPresentation.relators stores them.
The nineteen compiled HN relator words contain 153 letters before free reduction.
The compiled HN relator list is not freely, hence not cyclically, reduced: its fifth word
contains the cancelling boundary a⁻²a.
Free reduction makes every compiled HN relator word cyclically reduced.
The freely reduced lengths of the nineteen HN relators, in source order. Only the fifth
compiled word shortens, from 20 letters to 18, so the reduced words carry 151 of the 153
compiled letters.