ExampleConstruction: Literature-sourcedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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 Klein four-group as the subgroup $\{\mathrm{id}, (12)(34), (13)(24), (14)(23)\}$ of $\operatorname{Sym}(\{1,2,3,4\})$ : abelian of order $4$ , non-cyclic, every non-identity element of order $2$

Example

Let $X = \{1,2,3,4\}$ , four pairwise distinct natural numbers, and work in $\operatorname{Sym}(X)$ (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). Put

$a = (1\,2)(3\,4), \qquad b = (1\,3)(2\,4), \qquad c = (1\,4)(2\,3),$

each being the composite of the two disjoint transpositions shown, and set $V = \{\mathrm{id}, a, b, c\}$ . Then:

$V$ is a subgroup of $\operatorname{Sym}(X)$ (Subgroup) with four distinct elements, so $|V| = 4$ (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);
$V$ is abelian, with multiplication table generated by $a^{2} = b^{2} = c^{2} = \mathrm{id}$ , $ab = ba = c$ , $ac = ca = b$ and $bc = cb = a$ ;
every element of $V$ other than $\mathrm{id}$ has order $2$ ;
$V$ is not cyclic (The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$ , and cyclic groups).

$V$ is called the Klein four-group.

Facts & Assumptions

Given: $X = \{1,2,3,4\}$ and the permutations $a, b, c$ of $X$ acting as follows: $a$ sends $1 \mapsto 2$ , $2 \mapsto 1$ , $3 \mapsto 4$ , $4 \mapsto 3$ ; $b$ sends $1 \mapsto 3$ , $3 \mapsto 1$ , $2 \mapsto 4$ , $4 \mapsto 2$ ; $c$ sends $1 \mapsto 4$ , $4 \mapsto 1$ , $2 \mapsto 3$ , $3 \mapsto 2$ (The symmetric group $\operatorname{Sym}(X)$ : the bijections of a set $X$ under composition).

[L1]

$1$ , $2$ , $3$ , $4$ are pairwise distinct natural numbers, since each is a member of every later one and no natural number is a member of itself (The natural numbers $\mathbb{N}$ (von Neumann), Every natural number is a transitive set and is not a member of itself).

[L2]

$\operatorname{Sym}(X)$ is a group under composition, with identity $\mathrm{id}$ ( $\operatorname{Sym}(X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements, Group and abelian group).

[L3]

Two permutations agree exactly when they agree at every point of $X$ (Injection, surjection, bijection).

[L4]

One-step test: a nonempty subset $H$ of a group with $x y^{-1} \in H$ for all $x, y \in H$ is a subgroup (One-step subgroup test: a nonempty $H \subseteq G$ is a subgroup iff $gh^{-1} \in H$ for all $g, h \in H$ ; the identity and the inverses of $H$ are then those of $G$ , Subgroup).

[L5]

Powers and order: $f^{0} = \mathrm{id}$ , $f^{1} = f$ , $f^{2} = f \circ f$ , and $\operatorname{ord}(f)$ is the least $k \ge 1$ with $f^{k} = \mathrm{id}$ (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ , 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).

[L6]

If $\operatorname{ord}(g) = m$ is finite then $|\langle g \rangle| = m$ (If $\operatorname{ord}(g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n-1}$ are distinct, and $\langle g \rangle$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ); $\langle g \rangle$ is the smallest subgroup containing $g$ (The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$ , and cyclic groups); $|A| = m$ means $A \approx m$ , and that natural is unique (Finite, countably infinite, countable, uncountable, Equinumerous sets, $A \approx B$ and $A \preceq B$ , 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

The four elements are pairwise distinct: at the point $1$ they take the values $\mathrm{id}(1) = 1$ , $a(1) = 2$ , $b(1) = 3$ and $c(1) = 4$ , which are pairwise distinct.

L1L3given

1.2

Each of $a$ , $b$ , $c$ is its own inverse: $a \circ a$ sends $1 \mapsto 2 \mapsto 1$ , $2 \mapsto 1 \mapsto 2$ , $3 \mapsto 4 \mapsto 3$ and $4 \mapsto 3 \mapsto 4$ , so $a \circ a = \mathrm{id}$ ; the same computation with the corresponding pairs gives $b \circ b = \mathrm{id}$ and $c \circ c = \mathrm{id}$ .

L2L3given

1.3

$a \circ b = c$ : it sends $1 \mapsto b(1) = 3 \mapsto a(3) = 4$ , $2 \mapsto 4 \mapsto 3$ , $3 \mapsto 1 \mapsto 2$ , $4 \mapsto 2 \mapsto 1$ , and $c$ sends $1 \mapsto 4$ , $2 \mapsto 3$ , $3 \mapsto 2$ , $4 \mapsto 1$ . And $b \circ a = c$ : it sends $1 \mapsto a(1) = 2 \mapsto b(2) = 4$ , $2 \mapsto 1 \mapsto 3$ , $3 \mapsto 4 \mapsto 2$ , $4 \mapsto 3 \mapsto 1$ .

L3given

1.4

$a \circ c = b$ and $c \circ a = b$ : the first sends $1 \mapsto c(1) = 4 \mapsto a(4) = 3$ , $2 \mapsto 3 \mapsto 4$ , $3 \mapsto 2 \mapsto 1$ , $4 \mapsto 1 \mapsto 2$ ; the second sends $1 \mapsto a(1) = 2 \mapsto c(2) = 3$ , $2 \mapsto 1 \mapsto 4$ , $3 \mapsto 4 \mapsto 1$ , $4 \mapsto 3 \mapsto 2$ ; and $b$ sends $1 \mapsto 3$ , $2 \mapsto 4$ , $3 \mapsto 1$ , $4 \mapsto 2$ .

L3given

1.5

$b \circ c = a$ and $c \circ b = a$ : the first sends $1 \mapsto c(1) = 4 \mapsto b(4) = 2$ , $2 \mapsto 3 \mapsto 1$ , $3 \mapsto 2 \mapsto 4$ , $4 \mapsto 1 \mapsto 3$ ; the second sends $1 \mapsto b(1) = 3 \mapsto c(3) = 2$ , $2 \mapsto 4 \mapsto 1$ , $3 \mapsto 1 \mapsto 4$ , $4 \mapsto 2 \mapsto 3$ ; and $a$ sends $1 \mapsto 2$ , $2 \mapsto 1$ , $3 \mapsto 4$ , $4 \mapsto 3$ .

L3given

2.1

$V$ is nonempty and closed under $x \mapsto x^{-1}$ : $\mathrm{id}^{-1} = \mathrm{id}$ and each of $a, b, c$ is its own inverse by step 1.2.

step 1.2L2

2.2

$V$ is closed under composition: composing $\mathrm{id}$ with anything returns that element, each of $a, b, c$ composed with itself gives $\mathrm{id}$ by step 1.2, and the six mixed products are computed in steps 1.3, 1.4 and 1.5, each landing in $V$ .

step 1.2step 1.3step 1.4step 1.5L2

2.3

$V$ is abelian: the products computed in steps 1.3, 1.4 and 1.5 agree in either order, $\mathrm{id}$ commutes with everything, and each element commutes with itself. With step 1.2 this is the table of claim 2.

step 1.2step 1.3step 1.4step 1.5L2

2.4

Each of $a, b, c$ has order $2$ : it is not $\mathrm{id}$ by step 1.1, so $\operatorname{ord} \ne 1$ , and its square is $\mathrm{id}$ by step 1.2; hence $2$ is the least $k \ge 1$ with the $k$ -th power equal to $\mathrm{id}$ . This is claim 3, $\operatorname{ord}(\mathrm{id}) = 1$ being immediate.

step 1.1step 1.2L5

3.1

Hence for $x, y \in V$ one has $y^{-1} \in V$ and $x y^{-1} \in V$ , so $V$ is a subgroup of $\operatorname{Sym}(X)$ by the one-step test.

step 2.1step 2.2L4

4.1

$V$ has exactly four elements: the map $4 \to V$ sending $0, 1, 2, 3$ to $\mathrm{id}, a, b, c$ is a bijection by step 1.1, so $V \approx 4$ and $|V| = 4$ . This with step 3.1 is claim 1.

step 1.1step 3.1L6

5.1

$V$ is not cyclic: if $V = \langle g \rangle$ for some $g \in V$ , then $g$ has finite order and $|\langle g \rangle| = \operatorname{ord}(g)$ , so $\operatorname{ord}(g) = |V| = 4$ ; but every element of $V$ has order $1$ or $2$ by step 2.4, and $4 \ne 1$ and $4 \ne 2$ . This is claim 4.

step 4.1step 2.4L6∎

Remarks

An abelian group need not be cyclic. $V$ is the smallest witness of that, and it separates the two conditions that $\langle g \rangle = \{\, g^{n} : n \in \mathbb{Z} \,\}$ , and every cyclic group is abelian relates in one direction only: cyclic implies abelian, never the converse.
The four-group is realised here inside a symmetric group rather than as a product. The external direct product of two groups is introduced on a later page, so $V$ is exhibited as a set of four explicit permutations and checked by hand; nothing above uses any construction the library has not built.
Every non-identity element having order $2$ is exactly what rules out a generator: a cyclic group of order $4$ must contain an element of order $4$ (If $\operatorname{ord}(g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n-1}$ are distinct, and $\langle g \rangle$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ), and $(\mathbb{Z}/4, +)$ is such a group (For $n \ge 1$ the congruence classes modulo $n$ form an abelian group $(\mathbb{Z}/n, +)$ of order $n$ , generated by the class of $1$ ). So there are at least two groups of order $4$ that are not the same group. Classifying the groups of a given order needs machinery from a later page and is not attempted here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 78 results over 24 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

Klein four-group (Wikipedia) (standard reference, not scraped)
Symmetric group (Wikipedia) (standard reference, not scraped)

The Klein four-group as the subgroup {id,(12)(34),(13)(24),(14)(23)}\{\mathrm{id}, (12)(34), (13)(24), (14)(23)\}{id,(12)(34),(13)(24),(14)(23)} of Sym⁡({1,2,3,4})\operatorname{Sym}(\{1,2,3,4\})Sym({1,2,3,4}): abelian of order 444, non-cyclic, every non-identity element of order 222

Example

Facts & Assumptions

Verification

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Sources

The Klein four-group as the subgroup $\{\mathrm{id}, (12)(34), (13)(24), (14)(23)\}$ of $\operatorname{Sym}(\{1,2,3,4\})$ : abelian of order $4$ , non-cyclic, every non-identity element of order $2$