Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Refutation of the peak-group dichotomy

Abstract

The constructed finite peak group is neither solvable nor a Frobenius group.

Definition 1.1 (Complex character degrees).

Formalization. D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.degreeSet (✓ std3).

Citation. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

The set consists of the dimensions of simple finite-dimensional complex representations.

Definition 1.2 (Peak groups).

Formalization. D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.IsPeak (✓ std3).

Citation. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

A peak group has a character degree divisible by every character degree.

Definition 1.3 (Frobenius complements).

Formalization. D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.IsFrobeniusWithComplement (✓ std3).

Citation. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

A complement is a nontrivial proper subgroup with trivial intersection with each conjugate by an element outside it.

Definition 1.4 (The Fitting subgroup).

Formalization. D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.fitting (✓ std3).

Source. Repository-derived.

Acknowledgement. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

The Fitting subgroup is the supremum of the normal nilpotent subgroups.

Theorem 1.5 (Normality of the Fitting subgroup).

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.fitting_normal (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

A supremum of normal subgroups is normal.

Definition 1.6 (Excluded prime divisors).

Formalization. D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.HasAllowedOrder (✓ std3).

Citation. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

The order is divisible by none of two, three, and five.

Definition 1.7 (Structure of the quotient of a complement).

Formalization. D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.ComplementCondition (✓ std3).

Citation. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

The quotient by the Fitting subgroup contains a normal subgroup isomorphic to the product of SL(2, ZMod 5) and a group with cyclic Sylow subgroups and the specified prime exclusions. MulEquiv is the type of multiplicative equivalences.

Definition 1.8 (The Frobenius alternative).

Formalization. D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.AlternativeTwo (✓ std3).

Citation. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

The group has a Frobenius complement satisfying the quotient condition.

Definition 1.9 (Conjecture 31).

Formalization. D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.claim (✓ std3).

Citation. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

For every finite peak group, exactly one of solvability and the Frobenius alternative holds.

Theorem 1.10 (The conjecture is false).

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.result (✓ std3). ∎

Resolves. Problems/bahturin-centrone-pereira-2026-peak-group-refutation (refuted) by D5/S3/FiniteGroups/BahturinCentronePereiraPeakGroups.result.

Source. Repository-derived.

Acknowledgement. Bahturin, Yuri; Centrone, Lucio; Pereira, Kauê (2026). Quantum regularity of finite dimensional semisimple algebras. DOI: 10.48550/arXiv.2608.21936. URL: https://arxiv.org/abs/2608.21936v1.

Commentary.

The additive group of (ZMod 11) squared admits the displayed fixed-point-free SL(2, ZMod 5) action. Its semidirect product has a simple representation of dimension 120 and every simple degree divides 120. An abelian direct factor of order two preserves these degrees. The SL(2, ZMod 5) quotient prevents solvability, while the central element from the direct factor prevents every Frobenius complement.

References