trureturing — Discovering truth

slug: bahturin-centrone-pereira-2026-peak-group-refutation
bibkey: bahturincentronepereira2026peak
doi: 10.48550/arXiv.2608.21936
url: https://arxiv.org/abs/2608.21936v1
triage: theorem
motivation_gids:
  - D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.result

Problem

Bahturin, Centrone and Pereira, Quantum regularity of finite dimensional semisimple algebras, arXiv:2608.21936v1, Conjecture 31, asks whether every peak group satisfies exactly one of solvability and the stated Frobenius-complement alternative. The preregistration is #19254.

The settling declaration is D5.S3.FiniteGroups.BahturinCentronePereiraPeakGroups.BCP31.result. It proves the negation of the literal claim.

Statement echo

Motivation

The counterexample is the direct product $B\times C_2$, where $B$ is the source’s semidirect product of $(\mathbb{Z}/11\mathbb{Z}{)}^2$ by $\mathrm{SL}(2,5)$. The supporting declarations show that $B$ has peak degree $120$, that adjoining the abelian factor preserves the simple degree set, and that the resulting group is nonsolvable.

Gap

The source leaves Conjecture 31 open. The settlement addresses the conjecture through the concrete group specified in #19254. Literature completeness remains ASSUMED-UNVERIFIED; the source and the recorded literature screen do not establish an exhaustive search of later work.

Route

The module constructs the sparse $\mathrm{SL}(2,5)$ action on $(\mathbb{Z}/11\mathbb{Z}{)}^2$, verifies the finite action certificates, forms the semidirect product and its direct product with $C_2$, constructs a simple degree-$120$ representation, and proves that every simple degree divides $120$. The abelian-product theorem transfers peakness. The central-obstruction theorem shows that a nontrivial central element rules out every Frobenius complement, while the $\mathrm{SL}(2,5)$ quotient rules out solvability.

Falsifier

A finite group satisfying the literal claim would not falsify the result. A contradiction would require a counterexample to one of the kernel-checked declarations, especially the degree divisibility, degree-$120$ simplicity, or central obstruction statements.

Evidence

The compiled settling module has the public definitions degreeSet, IsPeak, IsFrobeniusWithComplement, fitting, HasAllowedOrder, ComplementCondition, AlternativeTwo, and claim, together with the public theorem result. The axiom closure of every public declaration is contained in $\{\mathrm{propext},Classical.choice,Quot.sound\}$.

The result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9). The other public theorems in the delivered modules have an unfinished escape audit recorded in #19389.

Proof shape

The classification expands every same-delivery helper, public or private, across all ten modules and stops at the protected frozen base or pinned Mathlib. A theorem is content when its own non-normalization step or a same-delivery content proposition remains on its proof path. The invariant-span proposition CliffordConstituents.TauCeti.Representation.iSup_conjSubrep_eq_top is the surviving witness for the common multiplicity and restriction isomorphism results. Their atom-existence projections do not retain universal conjugacy. The multiplicity comparison instead uses the conjugate-isomorphism classification and its invariant-span proof. The supporting modules use escape-witness; the settling module uses open-problem-resolution (#19254; Refuted).

The module keys below name their Lean namespaces. Numeric witness and consumer references point to the id column of this same table; private declarations use their fully qualified source names. Direct frozen dependencies are absent: the mathematical prerequisites here are pinned Mathlib or same-delivery declarations.

• A: D5.S3.FiniteGroups.BahturinCentronePereiraPeakGroups.
• B: D5.S3.FiniteGroups.CharacterDegreeDivisibility.
• C: D5.S3.FiniteGroups.CliffordConstituents.
• D: D5.S3.FiniteGroups.CliffordDecomposition.
• E: D5.S3.FiniteGroups.ComplexCharacterAbelianProducts.
• F: D5.S3.FiniteGroups.FiniteCharacterAlgebra.
• G: D5.S3.FiniteGroups.FrobeniusCentralObstruction.
• H: D5.S3.FiniteGroups.FrobeniusCharacterDegrees.
• I: D5.S3.FiniteGroups.InducedCharacterFormula.
• J: D5.S3.FiniteGroups.MackeyCharacterFormula.

Triage

What the settlement shows

• Mechanism — proved, kernel-checked. FrobeniusCentralObstruction.central_eq_one_of_frobenius proves that a Frobenius complement forces every central element to be the identity. The direct $C_2$ factor supplies a nontrivial central element; BCP31.refutation_of_peak applies this obstruction to the constructed group.
• Peakness — proved, kernel-checked. ComplexCharacterAbelianProducts.degreesProdAbelian preserves the simple degree set under a finite abelian direct product. BCP31.degree120_mem gives the degree-$120$ member, BCP31.B_degree_dvd gives divisibility of all simple degrees, and BCP31.B_peak proves peakness of $B$; BCP31.result transfers peakness to the constructed direct product.
• Nonsolvability — proved, kernel-checked. BCP31.SL2F5_not_solvable and BCP31.semidirect_C2_not_solvable use the $\mathrm{SL}(2,5)$ quotient to prove that the constructed group is not solvable.
• Nearest surviving statement — proved, kernel-checked. For any group $B$ and finite abelian group $A$, the delivered theorem ComplexCharacterAbelianProducts.degreesProdAbelian states equality of the simple degree sets of $B\times A$ and $B$.
• Source dependence — open. The cited source section ends with Conjecture 31. The literature reading does not establish which results elsewhere depend on it; this settlement makes no claim about those dependencies.
• Follow-up: trivial centre — open. Whether an analogue of Conjecture 31 holds for peak groups with trivial centre is outside result.
• Follow-up: direct indecomposability — open. Whether an analogue holds for directly indecomposable peak groups is outside result.
• Experiment — open. The supplied preregistration does not name an experiment repository, commit, script hash, or exit code. No experiment citation is asserted.

ASSUMED-UNVERIFIED

Literature completeness is ASSUMED-UNVERIFIED. The experiment citation requested by the lane is absent from the supplied issue material, so no experiment result is used as evidence. The two follow-up questions are recorded as open repository follow-ups rather than as separately verified published open problems.