Alphabeta Math
LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
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.

A positive integer multiple of the trivial character is an integral combination of cyclic permutation characters

Statement

Let G be a finite group. Then there is an integral linear combination of characters induced from trivial characters of cyclic subgroups whose value is ∣G∣1G. Equivalently,

∣G∣1G=∑iai Ind⁡CiG1Ci

for cyclic subgroups Ci≤G and integers ai.

Facts & Assumptions

Given: A finite group G and an element g∈G.

[F1]

For every finite cyclic subgroup C≤G, the generator-indicator class function ηC on C is an integral linear combination of characters Ind⁡DC1D with D≤C cyclic (The generator-indicator class function of a cyclic group is obtained by Mobius inversion).

[F2]

Frobenius' formula computes induced character values (Frobenius' formula for the character of an induced representation).

[F3]

Induction is transitive along subgroup chains (Induction is transitive along subgroup chains).

Proof

technique · direct
1.1F1givenconstruct

For each cyclic subgroup C≤G, let ηC be the class function from [F1], and define f:=∑C≤GC cyclicInd⁡CGηC. The sum is finite because a finite group has only finitely many subgroups.

2.1F2step 1.1givenalgebra

By [F2], for each cyclic C≤G one has Ind⁡CGηC(g)=1∣C∣∑x∈Gx−1gx∈CηC(x−1gx). Fix x∈G. Among all cyclic subgroups C≤G, exactly one of them can make the summand indexed by x nonzero, namely C=⟨x−1gx⟩; for that subgroup, the value of ηC is ∣C∣. Therefore the double sum defining f(g) contributes exactly 1 for each x∈G, so f(g)=∣G∣.

3.1F1F3step 1.1step 2.1algebra∎

Step 2.1 holds for every g∈G, hence f=∣G∣1G as class functions. Expanding each ηC by [F1] and then using [F3] to replace Ind⁡CG(Ind⁡DC1D) by Ind⁡DG1D expresses f as an integral linear combination of characters Ind⁡DG1D with D cyclic. Thus ∣G∣1G has the required form.

Depends on

Used by

Dependency tree · two levels

10 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