Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-28
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.

C[S3]≅C×C×M2(C)

Example

For the symmetric group S3,

C[S3]≅C×C×M2(C).

Facts & Assumptions

Given: The symmetric group S3.

[L1]

Over an algebraically closed field of characteristic prime to ∣G∣, the number of irreducible representations equals the number of conjugacy classes (If k is algebraically closed and char⁡k∤∣G∣, the number of irreducible representations of G equals the number of conjugacy classes).

[L2]

Under the same hypotheses, the irreducible degrees satisfy the sum-of-squares formula (If k is algebraically closed and char⁡k∤∣G∣, then ∑i(dim⁡kVi)2=∣G∣).

[L3]

Under the same hypotheses, the group algebra is a product of full matrix algebras over the base field (If k is algebraically closed and char⁡k∤∣G∣, then k[G]≅∏i=1rMni(k)).

Verification

technique · direct
1.1L1L2givenalgebra

The conjugacy classes of S3 are {e},{(12),(13),(23)},{(123),(132)}. Hence [L1] gives exactly three irreducible complex representations, with degrees d1,d2,d3, and [L2] gives d12+d22+d32=6.

2.1step 1.1L3givenalgebra∎

Each di is a positive integer. Since 12+12+22=6 and any larger square would already exceed 6, the only possible degree multiset is 1,1,2. Applying [L3], the Wedderburn factors are therefore M1(C), M1(C), and M2(C), so C[S3]≅C×C×M2(C).

Depends on

Used by

Dependency tree · two levels

13 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