Non-B-groups of order 3⁵ and exponent 9
Abstract
A finite group H is a B-group if every primitive permutation group containing a regular subgroup isomorphic to H is 2-transitive; equivalently, H fails to be a B-group exactly when it occurs as a regular subgroup of a uniprimitive group. Herbig has classified the B-groups of order p⁴ and names the order-p⁵ classification as the next step, observing that for p=3 and p=5 the answer is a finite computation over the primitive-groups and small-groups libraries; the outcome of that computation is not reported there. We carry out part of the case p=3 and certify the outcome inside a proof assistant. From an explicit list of 18 permutations of a 243-point set we prove that the group Γ they generate is uniprimitive — primitive by a statement quantified over all invariant partitions, not 2-transitive by an exhibited invariant set of 3888 ordered pairs — and that Γ contains three pairwise non-isomorphic regular subgroups of order 243: one elementary abelian, and two of exponent 9. Hence at least two groups of order 3⁵ of exponent 9 are not B-groups. Externally, GAP identifies Γ as the affine primitive group 3⁵:(2⁴:A₅) of order 233280 and the two subgroups as SmallGroup(243,51) and SmallGroup(243,63), both nonabelian with centres of order 9 and 27. Since these have order p^q with q>p and exponent p², they show that the hypothesis q<p in Herbig's Theorem B cannot be relaxed to q>p, and they answer an instance at p=3 of his closing question on regular subgroups of AGL(5,p). The primitivity, the failure of 2-transitivity and the three regular subgroups with their invariants are machine-checked in Lean 4; the few steps checked outside the proof assistant are named where they are used. We do not claim the resulting list of non-B-groups of order 243 is complete, and we say precisely which part of the search did not run.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
78709c095617f214dd8b8a8d68f033ca6e9dc9955143a83063d5b7b57b1dbc9f
Claim ledger
Stated results
BG1measurement2026-08-29
The degree-243 witness group is primitive: every gens-invariant partition of 0,...,242 relating point 0 to a second point is the universal partition, derived from a forced-merge closure with no trusted algorithm
BG2routine2026-08-29
The degree-243 witness group is not 2-transitive: a gens-invariant set of 3888 ordered pairs contains (0,1) and omits (0,2)
BG3known2026-08-29
C₃⁵ is a regular subgroup of a uniprimitive group of degree 243 – hence not a B-group – kernel-certified from an explicit permutation representation
BG4candidate2026-08-29
SmallGroup(243,51) and SmallGroup(243,63), both non-abelian of exponent 9, are regular subgroups of the uniprimitive group PrimitiveGroup(243,19) of order 233280 – hence not B-groups; kernel-certified, with order statistics, exponent and centre order checked in Lean
BG5routine2026-08-29
Negative control: the 18 listed permutations all have size 243 and map 0,...,242 into itself – the non-vacuity hypothesis the closure lemma consumes
BG6candidate2026-08-29
Two further non-B-groups of order 243, SmallGroup(243,38) and SmallGroup(243,6), found as regular subgroups of PrimitiveGroup(243,29) of order 3849120 – GAP output, not yet kernel-bound
This ledger entry is reported in prose and is not bound to a Lean theorem.BG7candidate2026-08-30
Fifteen further isomorphism types of order 243 are regular subgroups of uniprimitive groups of degree 243, hence not B-groups: SmallGroup(243,k) for k in 3, 6, 9, 13, 37, 38, 40, 52, 53, 56, 57, 58, 59, 62, 66, each kernel-certified inside one of three witness groups (3⁵:M₁1 twice, 3⁵:O(5,3) once) together with that group's primitivity and failure of 2-transitivity
BG8candidate2026-08-30
The p = 3 case of the source's named next step, computed: exactly 18 of the 67 groups of order 243 are not B-groups – SmallGroup(243,k) for k in 3, 6, 9, 13, 37, 38, 40, 51, 52, 53, 56, 57, 58, 59, 62, 63, 66, 67 – so 49 of the 67 are B-groups; seventeen of the eighteen are non-abelian and none has exponent above 9
This ledger entry is reported in prose and is not bound to a Lean theorem.BG9measurement2026-08-30
The three witness groups of degree 243 are primitive: for each, every invariant partition of 0,...,242 relating the base point to a second point is the universal partition, quantified over all partitions and derived from a forced-merge closure with no trusted algorithm
BG10routine2026-08-30
None of the three witness groups is 2-transitive: invariant sets of 53460, 26730 and 17496 of the 58806 ordered pairs of distinct points, each containing (0,1) and omitting an explicit pair
BG11routine2026-08-30
Non-vacuity of the witness data: the 8, 28 and 48 listed permutations have size 243 and map 0,...,242 into itself, and every step of each spanning structure uses a generator from the declared block, so the 243 rebuilt elements are words in the subgroup's own generators alone
BG12known2026-08-30
Every group of order 128 is a B-group: all 7 primitive groups of degree 128 are 2-transitive, so no uniprimitive group of that degree exists; in particular C₂⁷, the first Mersenne rank the source leaves unstated
This ledger entry is reported in prose and is not bound to a Lean theorem.BG13routine2026-08-30
Negative controls for the degree-243 witnesses: the primitivity checker rejects the regular subgroup's own generators (an explicit 81-block system for the seed 0 1), the generator list is certified NOT semiregular, and the spanning-structure block check is certified to fail on the wrong block
BG14known2026-08-30
Positive control on the source's own theorem: the same pipeline at degree 81 returns exactly the ten types SmallGroup(81,k) for k in 2,3,4,7,8,9,11,12,13,15 that Herbig's order-81 lemma predicts as the non-B-groups of order 81 – all ten found, nothing outside
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- A finite group H is a B-group (Burnside group) when every *primitive* permutation group containing a regular subgroup isomorphic to H is 2-transitive. Equivalently: H is not a B-group exactly when H occurs as a regular subgroup of some uniprimitive group — primitive but not 2-transitive. Burnside started the subject by asserting that cyclic groups of order pᵃ, a ≥ 2, are B-groups; groups of order p never are.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7