ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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 square-symmetry group has class equation $8=2+2+2+2$

Example

Let $D\le S_4$ be generated by the square rotation $r=(1\,2\,3\,4)$ and the reflection $s=(1\,3)$ . Its conjugacy classes are

$\{e\},\quad\{r^2\},\quad\{r,r^3\},\quad\{s,r^2s\},\quad\{rs,r^3s\}.$

Thus $Z(D)=\{e,r^2\}$ and the class equation is $8=2+2+2+2$ .

Facts & Assumptions

Given: The permutations $r=(1\,2\,3\,4)$ and $s=(1\,3)$ in $S_4$ .

[L1]

The class equation sums central singleton classes and noncentral conjugacy-class sizes (The class equation $|G|=|Z(G)|+\sum_i [G:C_G(x_i)]$ for a finite group).

[L2]

Conjugacy-class cardinality is a centralizer index ( $G/C_G(x)\to\operatorname{Cl}_G(x)$ is a bijection, so $|\operatorname{Cl}_G(x)|=[G:C_G(x)]$ whenever these cardinalities are finite).

[L3]

The symmetric group is the group of all permutations under composition (The symmetric group $\operatorname{Sym}(X)$ : the bijections of a set $X$ under composition, $\operatorname{Sym}(X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements).

[L4]

The subgroup axioms are those of Subgroup.

[L5]

Integer powers and their laws are given by Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ and Exponent laws in a group: $g^{m+n} = g^{m}g^{n}$ and $(g^{m})^{n} = g^{mn}$ for all $m, n \in \mathbb{Z}$ , and $(gh)^{n} = g^{n}h^{n}$ when $g$ and $h$ commute.

[L6]

Element order is the least positive exponent giving the identity (The order $|G|$ of a finite group and the order $\operatorname{ord}(g)$ of an element, with $\operatorname{ord}(g) = \infty$ when no positive power of $g$ is the identity).

Verification

technique · direct

1.1

Pointwise calculation gives $r^4=e$ , $s^2=e$ , and $sr=r^{-1}s$ .

L3L5L6algebra

2.1

The relations reduce every word in $r,s$ to one of $e,r,r^2,r^3,s,rs,r^2s,r^3s$ and show this set is closed under products and inverses. These eight permutations are distinct, so [L3] and [L4] make them a subgroup $D$ of order $8$ ; also $sr\ne rs$ , so $D$ is nonabelian.

step 1.1L3L4L5L6algebra

3.1

Using $sr=r^{-1}s$ , conjugation by $r$ and $s$ gives the five displayed conjugacy classes: $e$ and $r^2$ are central, $r$ is conjugate to $r^3$ , and the reflections split into the two displayed pairs.

step 1.1step 2.1L2algebra

4.1

Their sizes give $8=1+1+2+2+2=2+2+2+2$ , and [L1] identifies the two singleton classes with the center $\{e,r^2\}$ .

step 3.1L1L2algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 98 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

T. W. Judson, Abstract Algebra: Theory and Applications, 14.2 (standard reference, not scraped)

The square-symmetry group has class equation 8=2+2+2+28=2+2+2+28=2+2+2+2