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.

✓ 4 results · all verified · 4 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 4 also cleared it.

Artin Induction and Rational Characters - Examples

1 · Prerequisites

2 · Summary

These examples keep the theorem visible at the exact concrete points the page needs. The cyclic case shows that Artin induction can collapse to the identity, the $A_{5}$ calculation exhibits a genuine denominator, the $S_{3}$ table makes the fixed-space detection map explicit, and the quaternion example protects the page from confusing rational-valued characters with characters realized over $Q$ .

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

Artin induction is tautological for a cyclic group

Example

Let $G = C_{n}$ be cyclic, and let $x \in R_{Q} (C_{n})$ . Then Artin induction can be realized with the single cyclic subgroup $C_{n}$ itself:

$x = {Ind}_{C_{n}}^{C_{n}} x .$

For the trivial character when $n = 1$ , this specializes to $1_{C_{1}} = {Ind}_{C_{1}}^{C_{1}} 1_{C_{1}}$ .

Facts & Assumptions

Given: A cyclic group $C_{n} = ⟨ g ⟩$ and an element $x \in R_{Q} (C_{n})$ .

[F1]

Every rational character is a rational linear combination of characters induced from cyclic subgroups (Artin induction for rational characters).

[F2]

The notation $⟨ g ⟩ = C_{n}$ means that $g$ generates the whole group (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

Verification

technique · direct

1.1

By [F2], the whole group $C_{n}$ is already a cyclic subgroup of itself. Induction from a subgroup to itself is the identity construction, so ${Ind}_{C_{n}}^{C_{n}} x = x$ . Thus the Artin expression can be taken to have one summand, namely the subgroup $C_{n}$ itself.

F2givenalgebra

2.1

This realizes the conclusion of [F1] in the most degenerate possible way: no proper cyclic subgroup is needed. If $n = 1$ and $x = 1_{C_{1}}$ , then step 1.1 gives the displayed trivial-character identity.

F1step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

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∎

ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

The cyclic fixed-space data recovers an $S_{3}$ rational character

Example

Let $1$ , $sgn$ , and $χ_{s t d}$ be the usual rational characters of $S_{3}$ . Their fixed-space dimensions on the cyclic subgroups $1$ , $C_{2}$ , and $A_{3}$ are

$\begin{array}{cccc} 1 & C_{2} & A_{3} \\ 1 & 1 & 1 & 1 \\ sgn & 1 & 0 & 1 \\ χ_{s t d} & 2 & 1 & 0 \end{array} .$

Hence a character $a \cdot 1 + b \cdot sgn + c \cdot χ_{s t d}$ is recovered uniquely from its cyclic fixed-space data.

Facts & Assumptions

Given: The group $S_{3}$ , its cyclic subgroups $1$ , $C_{2}$ , and $A_{3}$ , and a rational character $x = a \cdot 1 + b \cdot sgn + c \cdot χ_{s t d}$ .

[F1]

Cyclic fixed-space data determines a rational virtual character (Cyclic fixed-space dimensions detect rational virtual characters).

[F2]

For a representation $V$ , the fixed subspace $V^{H}$ is the subspace of vectors fixed by every element of $H$ (The fixed subspace $V^{G}$ of a representation).

[A1]

On $S_{3}$ , the one-dimensional sign representation acts trivially on $A_{3}$ and by $- 1$ on a transposition, while the two-dimensional standard representation is fixed pointwise by the identity, has a one-dimensional fixed line for a transposition, and has no nonzero fixed vector for a $3$ -cycle.

Verification

technique · direct

1.1

By [F2] and [A1], the trivial representation has fixed-space dimensions $(1, 1, 1)$ on $(1, C_{2}, A_{3})$ , the sign representation has $(1, 0, 1)$ , and the standard representation has $(2, 1, 0)$ . This is exactly the displayed table.

F2A1givenalgebra

2.1

Therefore the cyclic fixed-space data of $x = a \cdot 1 + b \cdot sgn + c \cdot χ_{s t d}$ is $(a + b + 2 c, a + c, a + b)$ . The coefficient matrix $(\begin{array}{ccc} 1 & 1 & 2 \\ 1 & 0 & 1 \\ 1 & 1 & 0 \end{array})$ has determinant $2 \neq 0$ , so these three numbers determine $a$ , $b$ , and $c$ uniquely.

step 1.1algebra

3.1

Thus the cyclic fixed-space data recovers the rational character $x$ , which is the concrete $S_{3}$ instance of [F1].

F1step 2.1algebra∎

CounterexampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A rational-valued irreducible character need not come from a $Q$ -representation

Statement refuted

Every rational-valued irreducible character of a finite group is afforded by a representation over $Q$ .

Let $Q_{8} = {\pm 1, \pm i, \pm j, \pm k}$ be the quaternion group (The quaternion group $Q_{8} = {\pm 1, \pm i, \pm j, \pm k}$ inside the nonzero quaternions). Consider the complex representation $ρ : Q_{8} \to {GL}_{2} (C)$ given by

$ρ (i) = (\begin{array}{cc} i & 0 \\ 0 & - i \end{array}), ρ (j) = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array}), ρ (k) = (\begin{array}{cc} 0 & i \\ i & 0 \end{array}) .$

Then $ρ (- 1) = - I_{2}$ , and its character $χ$ has values

$χ (1) = 2, χ (- 1) = - 2, χ (\pm i) = χ (\pm j) = χ (\pm k) = 0.$

So $χ$ is rational-valued. However, the cited Schur-index computation shows that $χ$ has Schur index $2$ over $Q$ , so no $Q$ -representation affords it.

Facts & Assumptions

Given: The quaternion group $Q_{8}$ and the matrices displayed above.

[F1]

The group $Q_{8}$ is the eight-element group ${\pm 1, \pm i, \pm j, \pm k}$ (The quaternion group $Q_{8} = {\pm 1, \pm i, \pm j, \pm k}$ inside the nonzero quaternions).

[F2]

In $Q_{8}$ , the element $- 1$ is the unique element of order $2$ , while $\pm i$ , $\pm j$ , and $\pm k$ all have order $4$ ( $Q_{8}$ is a subgroup of $H^{\times}$ with eight elements, and $- 1$ is its only element of order $2$ ).

Counterexample

technique · direct

1.1

The displayed matrices satisfy $ρ (i)^{2} = ρ (j)^{2} = ρ (k)^{2} = - I_{2}$ and $ρ (i) ρ (j) = ρ (k)$ , $ρ (j) ρ (i) = - ρ (k)$ . Hence they obey the same relations as the generators of $Q_{8}$ from [F1], so they define a two-dimensional complex representation of $Q_{8}$ . Their traces are $2, - 2, 0, 0, 0$ on the conjugacy classes $1$ , $- 1$ , ${\pm i}$ , ${\pm j}$ , and ${\pm k}$ , so the character is rational-valued.

F1F2givenalgebra

2.1

The Magma Schur-index example in the cited source computes that this irreducible character has Schur index $2$ over $Q$ . A character with Schur index greater than $1$ is not afforded by any $Q$ -representation. Therefore this rational-valued irreducible character is not defined over $Q$ , refuting the statement.

step 1.1algebra∎

Artin Induction and Rational Characters - Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Artin induction is tautological for a cyclic group

Example

Facts & Assumptions

Verification

The A5A5​ permutation relation already needs a denominator

Example

Facts & Assumptions

Verification

The cyclic fixed-space data recovers an S3S3​ rational character

Example

Facts & Assumptions

Verification

A rational-valued irreducible character need not come from a QQ-representation

Statement refuted

Facts & Assumptions

Counterexample

Sources

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

The cyclic fixed-space data recovers an $S_{3}$ rational character

A rational-valued irreducible character need not come from a $Q$ -representation