ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck 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 ${i d, (12) (34), (13) (24), (14) (23)}$ of $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 $Sym (X)$ (The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition, $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), b = (1 3) (2 4), c = (1 4) (2 3),$

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

$V$ is a subgroup of $Sym (X)$ (Subgroup) with four distinct elements, so $∣ V ∣ = 4$ (The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $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} = i d$ , $a b = b a = c$ , $a c = c a = b$ and $b c = c b = a$ ;
every element of $V$ other than $i d$ has order $2$ ;
$V$ is not cyclic (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , 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 $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 $N$ (von Neumann), Every natural number is a transitive set and is not a member of itself).

[L2]

$Sym (X)$ is a group under composition, with identity $i d$ ( $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 $g h^{- 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} = i d$ , $f^{1} = f$ , $f^{2} = f \circ f$ , and $ord (f)$ is the least $k \geq 1$ with $f^{k} = i d$ (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 $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity).

[L6]

If $ord (g) = m$ is finite then $∣ ⟨ g ⟩ ∣ = m$ (If $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 $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ); $⟨ g ⟩$ is the smallest subgroup containing $g$ (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , 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 ⪯ B$ , The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $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 $i d (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 = i d$ ; the same computation with the corresponding pairs gives $b \circ b = i d$ and $c \circ c = i d$ .

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}$ : ${i d}^{- 1} = i d$ 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 $i d$ with anything returns that element, each of $a, b, c$ composed with itself gives $i d$ 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, $i d$ 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 $i d$ by step 1.1, so $ord \neq 1$ , and its square is $i d$ by step 1.2; hence $2$ is the least $k \geq 1$ with the $k$ -th power equal to $i d$ . This is claim 3, $ord (i d) = 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 $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 $i d, 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 = ⟨ g ⟩$ for some $g \in V$ , then $g$ has finite order and $∣ ⟨ g ⟩ ∣ = ord (g)$ , so $ord (g) = ∣ V ∣ = 4$ ; but every element of $V$ has order $1$ or $2$ by step 2.4, and $4 \neq 1$ and $4 \neq 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 $⟨ g ⟩ = {g^{n} : n \in 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 $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 $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ), and $(Z / 4, +)$ is such a group (For $n \geq 1$ the congruence classes modulo $n$ form an abelian group $(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 · two levels

46 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

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)}{id,(12)(34),(13)(24),(14)(23)} of Sym⁡({1,2,3,4})Sym({1,2,3,4}): abelian of order 44, non-cyclic, every non-identity element of order 22

Example

Facts & Assumptions

Verification

Remarks

Depends on

Used by

Dependency tree · two levels

Sources

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