ExampleConstruction: Literature-sourcedVerification: 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.

The $A_{5}$ permutation relation already needs a denominator

Example

Let $G = A_{5}$ , and let $C_{1}$ , $C_{2}$ , $C_{3}$ , and $C_{5}$ be cyclic subgroups of orders $1$ , $2$ , $3$ , and $5$ , respectively. Then

${Ind}_{C_{5}}^{A_{5}} 1_{C_{5}} + {Ind}_{C_{3}}^{A_{5}} 1_{C_{3}} + {Ind}_{C_{2}}^{A_{5}} 1_{C_{2}} - {Ind}_{C_{1}}^{A_{5}} 1_{C_{1}} = 2 \cdot 1_{A_{5}} .$

Dividing by $2$ shows that the trivial character of $A_{5}$ is not, in general, an integral combination of cyclic permutation characters.

Facts & Assumptions

Given: The alternating group $A_{5}$ .

[F1]

The Artin permutation relation expresses a positive multiple of $1_{G}$ as an integral combination of permutation characters induced from cyclic subgroups (A positive integer multiple of the trivial character is an integral combination of cyclic permutation characters).

[F2]

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

[A1]

The conjugacy classes of $A_{5}$ have representatives $1$ , $τ = (12) (34)$ , $σ = (123)$ , $ρ = (12345)$ , and $ρ^{2} = (13524)$ of sizes $1$ , $15$ , $20$ , $12$ , and $12$ .

Verification

technique · direct

1.1

By [A1], the numbers of cyclic subgroups of orders $2$ , $3$ , and $5$ are $15$ , $20 / 2 = 10$ , and $(12 + 12) / 4 = 6$ , because each subgroup of order $2$ , $3$ , or $5$ has $1$ , $2$ , or $4$ generators. Hence their normalizers have orders $60 / 15 = 4$ , $60 / 10 = 6$ , and $60 / 6 = 10$ .

A1givenalgebra

2.1

Put $U_{n} : = {Ind}_{C_{n}}^{A_{5}} 1_{C_{n}}$ . Frobenius' formula [F2] gives $U_{1} (1) = 60$ , $U_{2} (1) = 30$ , $U_{3} (1) = 20$ , and $U_{5} (1) = 12$ . If $g \in {τ, σ, ρ, ρ^{2}}$ , then $U_{n} (g) = 0$ unless $g$ has order $n$ . For an element whose order is $n$ , the same formula counts $∣ N_{A_{5}} (C_{n}) ∣ / ∣ C_{n} ∣ = 2$ fixed cosets, so $U_{2} (τ) = 2$ , $U_{3} (σ) = 2$ , and $U_{5} (ρ) = U_{5} (ρ^{2}) = 2$ , while all other nonidentity values among these four characters are $0$ .

F2step 1.1algebra

3.1

Therefore the character $U_{5} + U_{3} + U_{2} - U_{1}$ has value $12 + 20 + 30 - 60 = 2$ at the identity, and also value $2$ on each of the four nontrivial conjugacy classes from step 2.1. So it is the constant class function $2 = 2 \cdot 1_{A_{5}}$ . This is the concrete $A_{5}$ instance promised by [F1].

F1step 2.1algebra

4.1

If $1_{A_{5}}$ were an integral linear combination of cyclic permutation characters, then evaluating that combination on $τ$ would give $1$ as an integer combination of the values from step 2.1. But every cyclic permutation character of $A_{5}$ takes value either $0$ or $2$ on $τ$ , so any such integral combination would be even. This contradiction shows that the denominator $2$ is genuinely unavoidable.

step 2.1step 3.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

Tammo tom Dieck, Representation Theory, Problem 1 after Section 4.5 (standard reference, not scraped)
Kay Yang, Rational Valued Characters, Theorem 12 (standard reference, not scraped)

The A5A5​ permutation relation already needs a denominator