feat: add six finite-group-theory benchmark problems

[kim-em]

This PR adds six benchmark statements at the boundary of finite group theory and representation theory: Brauer's theorem on cyclotomic character values, an existential M₂₃ tensor-square problem in the same style as the existing exceptional-Lie tensor-square problems, and four CFSG-adjacent results — Frobenius's kernel-is-normal theorem, Glauberman's Z*, Schreier's conjecture, and the order-restriction part of the classification of 5-transitive permutation groups.

Each statement was checked adversarially before commit. Notable choices:

• Brauer (brauer_character_in_cyclotomic): asserts ∃ φ : ℚ(ζ_exp G) →+* ℂ, ∀ g, tr(ρ g) ∈ φ.range. The docstring is explicit that this is the character-value form, which is strictly weaker than the full splitting-field statement (every irrep has a ℚ(ζₙ)-form). The latter would need scalar-extension scaffolding mathlib doesn't expose cleanly.
• M₂₃ (m23_irrep_tensor_square_decomp): existential for a finite group of order 10 200 960 with a 22-dim irrep whose tensor square has 4 isotypic components. Both MonoidAlgebra ℂ G actions (on V and on V ⊗ V) are explicit binders with IsScalarTower, and the V ⊗ V action is pinned by the diagonal-action equation g • (v ⊗ w) = (g • v) ⊗ (g • w) for g : G. The statement does not pin M₂₃ uniquely, but constructing any witness is essentially equivalent to constructing M₂₃.
• Frobenius (frobenius_kernel_isNormal): explicit 2 ≤ |X| to make the Frobenius-action package fully nondegenerate.
• Glauberman (glauberman_zStar): uses the global isolated-involution form (no distinct conjugate of t commutes with t); the conclusion form ∀ g, g·t·g⁻¹·t⁻¹ ∈ N is exactly "t central in G/N".
• Schreier (schreier_conjecture): a local innNormal instance proves Inn(S) ⊴ Aut(S) (one-line simp after ext) so the quotient MulAut S ⧸ MulAut.conj.range typechecks.
• 5-transitive (five_transitive_card_classification): 5 ≤ |X| defeats vacuity (otherwise C₃ on Fin 3 qualifies); the n!/2 branch is gated by 7 ≤ n since Aₙ is only 5-transitive for n ≥ 7. Title is "Possible orders of …" rather than "Classification of …" since only orders are formalized.

🤖 Prepared with Claude Code