Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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, srs1=r1, the conjugacy classes are represented by 1, r2, r, s, sr (sizes 1, 1, 2, 2, 2), and the character table is

1r2rssrχ111111χ211111χ311111χ411111ψ22000

Both orthogonality relations hold.

Facts & Assumptions

Given: The dihedral group G=Dih(C4)=C4C2 with C4=r and C2=s.

[F1]

G has order 8, presentation r4=s2=1, srs1=r1, and every element has the unique form ri or ris ( Dih(Cn)=CnC2 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; srs1=r1 conjugates r to r3; rsr1=sr2 conjugates s to sr2; and r(sr)r1=sr3 conjugates sr to sr3. Hence the classes are {1}, {r2}, {r,r3}, {s,sr2}, {sr,sr3}.

[A2]

The commutator [r,s]=rsr1s1 equals r2, the quotient G/r2 has order 4 and is abelian, and every assignment rε, sδ with ε,δ{±1} extends to a homomorphism GC×.

Verification

technique · direct
1.1

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

A1given
1.2

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

A2F3given
2.1

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).

F2F3A2step 1.2given
3.1

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

F4step 2.1algebra
4.1

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 11+11+2ψ(r)=0, 1+111+2ψ(s)=0, and 111+1+2ψ(sr)=0, so ψ(r)=ψ(s)=ψ(sr)=0.

F6step 2.1step 3.1algebra
5.1

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.

F5step 2.1step 4.1algebra
6.1

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.

F6F1step 1.1step 4.1algebra

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