Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Generalized decomposition numbers exist and are unique

Statement

Fix a splitting p-modular system (K,O,k) for a finite group G. For every χ∈Irr⁡K(G) and every p-element u∈G, there is a unique family

(dχ,φu)φ∈IBr⁡(CG(u))

such that, for every p-regular v∈CG(u),

χ(uv)=∑φ∈IBr⁡(CG(u))dχ,φuφ(v).

Writing H=CG(u) and Res⁡HGχ=∑ζnχ,ζζ, these unique coefficients are

dχ,φu=∑ζ∈Irr⁡K(H)nχ,ζλu,ζdζ,φ.

In particular, dχ,φ1=dχ,φ.

Facts & Assumptions

Given: The splitting system, χ, u, and H=CG(u) in the Statement.

[F1]

Generalized decomposition numbers defines the displayed finite sum, including the scalar λu,ζ.

[F2]

Maschke's theorem gives complete reducibility over the characteristic-0 field K (Maschke's theorem for finite groups over fields whose characteristic does not divide ∣G∣).

[F3]

Schur's lemma makes a central group element an endomorphism of every irreducible constituent (Schur's lemma for irreducible representations: a nonzero intertwiner is an isomorphism, and End⁡G(V) is a division ring); the scalar conclusion here is supplied by the splitting-field clause recorded in F1.

[F4]

On p-regular elements, an ordinary irreducible character is the sum of irreducible Brauer characters with its ordinary decomposition numbers (Decomposition numbers and the decomposition matrix).

[F5]

A Brauer-character value is an element of K obtained as a sum of Teichmüller lifts of prime-to-p roots of unity (Brauer character of a finite-dimensional kG-module).

[F6]

Under the standard complex realization of those prime-to-p roots, irreducible Brauer characters form a basis of the complex class functions on the p-regular elements (Irreducible Brauer characters form a basis of the p-regular class functions).

Proof

1.1F1F2F3

By F2, restriction to H gives the finite decomposition Res⁡HGχ=∑ζnχ,ζζ. Since u∈Z(H), its representing operator commutes with H; F3 and the splitting condition give ρζ(u)=λu,ζid⁡. Moreover ρζ(u)∣u∣=1, so λu,ζ∣u∣=1 without any algebraic-closedness assumption.

2.1F1F4step 1.1algebra

Let v∈H be p-regular. Because u and v commute, trace gives ζ(uv)=tr⁡(ρζ(u)ρζ(v))=λu,ζζ(v). By F4, ζ(v)=∑φdζ,φφ(v). Substitution into the restriction formula and reordering its finite sums yields χ(uv)=∑φ(∑ζnχ,ζλu,ζdζ,φ)φ(v). The coefficient in parentheses is exactly dχ,φu by F1.

3.1F5F6step 2.1algebra

Let v1,…,vr represent the p-regular conjugacy classes of H, and list the irreducible Brauer characters as φ1,…,φr; equality of the two cardinalities follows from [F6]. By [F5], the evaluation matrix M=(φj(vi))i,j∈Mr(K) has entries in the cyclotomic subfield generated by the Teichmüller lifts that occur. Applying the standard complex realization entrywise gives the Brauer-character table from [F6], whose determinant is nonzero by complex linear independence. Hence det⁡M≠0 already in that cyclotomic subfield, and therefore M is invertible over K. If another family in Kr gave the same values, subtraction would yield Ma=0; invertibility forces a=0. This proves uniqueness without applying a complex-linear independence assertion directly to K-coefficients.

4.1F1step 2.1algebra∎

If u=1, then H=G, the restriction has only the constituent χ with multiplicity one, and λ1,χ=1. The formula in F1 becomes dχ,φ1=dχ,φ. The case v=1 in step 2.1 is valid and gives the corresponding value at u. All decompositions and sums are finite, so no choice principle is used.

Depends on

Used by

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources