Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29
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 character table of Dih⁡(C4)

Example

For G=Dih⁡(C4)=⟨r,s:r4=s2=1, srs−1=r−1⟩, the conjugacy classes are represented by 1, r2, r, s, sr (sizes 1, 1, 2, 2, 2), and the character table is

1r2rssrχ111111χ211−11−1χ3111−1−1χ411−1−11ψ2−2000

Both orthogonality relations hold.

Facts & Assumptions

Given: The dihedral group G=Dih⁡(C4)=C4⋊C2 with C4=⟨r⟩ and C2=⟨s⟩.

[F1]

G has order 8, presentation r4=s2=1, srs−1=r−1, and every element has the unique form ri or ris ( Dih⁡(Cn)=Cn⋊C2 with inversion action has order 2n and the dihedral relations).

[F3]

Homomorphisms to abelian groups factor uniquely through the abelianization Gab=G/G′ (The derived subgroup is characteristic and the abelianization is universal).

[F4]

The squared degrees of the irreducible characters sum to ∣G∣ (The regular character gives a second proof of the sum-of-squares formula).

[F5]

Row orthogonality: irreducible characters are orthonormal (The first orthogonality relation for irreducible complex characters).

[F6]

Column orthogonality: distinct columns are orthogonal and a column has squared norm the centralizer size (The second orthogonality relation for irreducible complex characters).

[A1]

From [F1]'s relations: r2 is central; srs−1=r−1 conjugates r to r3; rsr−1=sr2 conjugates s to sr2; and r(sr)r−1=sr3 conjugates sr to sr3. Hence the classes are {1}, {r2}, {r,r3}, {s,sr2}, {sr,sr3}.

[A2]

The commutator [r,s]=rsr−1s−1 equals r2, the quotient G/⟨r2⟩ has order 4 and is abelian, and every assignment r↦ε, s↦δ with ε,δ∈{±1} extends to a homomorphism G→C×.

Verification

technique · direct
1.1A1given

By [A1] the classes are {1}, {r2}, {r,r3}, {s,sr2}, {sr,sr3}, of sizes 1, 1, 2, 2, 2.

1.2A2F3given

By [A2], r2∈G′, and the quotient G/⟨r2⟩ of order 4 is abelian; by [F3] the homomorphisms to abelian groups factor through it, so G′=⟨r2⟩.

2.1F2F3A2step 1.2given

By [F2] and [F3], the degree-one characters are the homomorphisms factoring through the abelianization of step 1.2, namely the four assignments of [A2]: χ(r)=ε, χ(s)=δ. Their values are the first four rows of the table (with χ(sr)=εδ and χ(r2)=1).

3.1F4step 2.1algebra

By [F4], the remaining irreducible degree d satisfies 1+1+1+1+d2=8, so d=2.

4.1F6step 2.1step 3.1algebra

By [F6], the column of r2 is orthogonal to the column of 1: 1+1+1+1+2ψ(r2)‾=0, so ψ(r2)=−2. The columns of r, s, and sr are orthogonal to the column of 1, giving 1−1+1−1+2ψ(r)‾=0, 1+1−1−1+2ψ(s)‾=0, and 1−1−1+1+2ψ(sr)‾=0, so ψ(r)=ψ(s)=ψ(sr)=0.

5.1F5step 2.1step 4.1algebra

The five rows form the displayed table. By [F5], ⟨ψ,ψ⟩=18(4+4)=1 and ψ is orthogonal to each degree-one row, so the table is complete; the degrees sum correctly.

6.1F6F1step 1.1step 4.1algebra∎

By [F6], the column squared norms are 8, 8, 4, 4, 4; the norm 8 of the first column is the group order ∣G∣=8 of [F1], equal to the centralizer size of the identity, and the remaining norms are the centralizer sizes. Distinct columns are orthogonal.

Depends on

Used by

Dependency tree · two levels

29 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