ExampleConstruction: AI-adaptedVerification: 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.

$\operatorname{Sym}(\{1,2,3\})$ has exactly six elements, is non-abelian, and its elements have orders $1$ , $2$ and $3$

Example

Let $X = \{1,2,3\}$ , the three-element set of natural numbers $1 = \sigma(0)$ , $2 = \sigma(1)$ , $3 = \sigma(2)$ , and let $G = \operatorname{Sym}(X)$ be its symmetric group (The symmetric group $\operatorname{Sym}(X)$ : the bijections of a set $X$ under composition), a group under composition ( $\operatorname{Sym}(X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements). Then:

$G$ has exactly six elements, namely

$\mathrm{id},\quad (1\,2),\quad (1\,3),\quad (2\,3),\quad (1\,2\,3),\quad (1\,3\,2),$

so $G \approx 6$ and $|G| = 6$ (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);
$G$ is not abelian: $(1\,2) \circ (2\,3) = (1\,2\,3)$ while $(2\,3) \circ (1\,2) = (1\,3\,2)$ ;
the orders of its elements are $\operatorname{ord}(\mathrm{id}) = 1$ , $\operatorname{ord} = 2$ for each of the three transpositions, and $\operatorname{ord} = 3$ for each of the two $3$ -cycles.

Facts & Assumptions

Given: $X = \{1,2,3\}$ and $G = \operatorname{Sym}(X)$ with the operation $f \circ g$ , $(f \circ g)(x) = f(g(x))$ , and identity $\mathrm{id}$ (The symmetric group $\operatorname{Sym}(X)$ : the bijections of a set $X$ under composition).

[L1]

$1$ , $2$ and $3$ are pairwise distinct natural numbers: $2 = \sigma(1) = 1 \cup \{1\}$ and $3 = \sigma(2) = 2 \cup \{2\} = \{0,1,2\}$ , so $1 \in 2$ , $2 \in 3$ and $1 \in 3$ , while 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); so $X$ has exactly three elements.

[L2]

$\operatorname{Sym}(X)$ is a group under composition; the cycle symbols $(a\,b)$ and $(a\,b\,c)$ denote the permutations described in 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, Group and abelian group).

[L3]

Two functions $X \to X$ are equal exactly when they agree at every point; a function on $X$ is determined by the triple $(f(1), f(2), f(3))$ , and $f$ is a bijection of $X$ exactly when those three values are pairwise distinct, since three distinct values in a three-element set exhaust it (Injection, surjection, bijection).

[L4]

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

[L5]

Finiteness and counting: $A \approx m$ means a bijection $A \to m$ exists, and $|A| = m$ is then the unique such natural (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).

[L6]

If $\operatorname{ord}(f) = k$ then $f^{j} \ne \mathrm{id}$ for $1 \le j < k$ , and conversely a $k$ with $f^{k} = \mathrm{id}$ and $f^{j} \ne \mathrm{id}$ for $1 \le j < k$ is the order (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, 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$ ).

Verification

technique · direct

1.1

Writing each element of $G$ as the triple of its values at $1, 2, 3$ , the six listed permutations are $\mathrm{id} = (1,2,3)$ , $(2\,3) = (1,3,2)$ , $(1\,2) = (2,1,3)$ , $(1\,2\,3) = (2,3,1)$ , $(1\,3\,2) = (3,1,2)$ and $(1\,3) = (3,2,1)$ . These six triples are pairwise different, so the six permutations are pairwise different.

L1L2L3

1.2

Each transposition $\tau \in \{(1\,2), (1\,3), (2\,3)\}$ satisfies $\tau \circ \tau = \mathrm{id}$ , since it exchanges two points and fixes the third, so applying it twice returns every point to itself; and $\tau \ne \mathrm{id}$ , since it moves two points.

L2L3

1.3

$\operatorname{ord}(\mathrm{id}) = 1$ , since $\mathrm{id}^{1} = \mathrm{id}$ and $1$ is the least natural that is $\ge 1$ .

L4L6

2.1

Every element of $G$ is one of the six. Let $f \in G$ ; its triple has pairwise distinct entries by [L3]. There are three possible values for $f(1)$ ; for each, two remaining values for $f(2)$ ; and then $f(3)$ is forced to be the one element of $X$ left over. Running through those six combinations produces exactly the six triples listed in step 1.1.

step 1.1L1L3

2.2

Composites, computed pointwise. $(1\,2) \circ (2\,3)$ sends $1 \mapsto 1 \mapsto 2$ , $2 \mapsto 3 \mapsto 3$ , $3 \mapsto 2 \mapsto 1$ , giving the triple $(2,3,1)$ , which is $(1\,2\,3)$ . And $(2\,3) \circ (1\,2)$ sends $1 \mapsto 2 \mapsto 3$ , $2 \mapsto 1 \mapsto 1$ , $3 \mapsto 3 \mapsto 2$ , giving $(3,1,2)$ , which is $(1\,3\,2)$ .

step 1.1L2L3

2.3

Let $c = (1\,2\,3)$ , so $c$ sends $1 \mapsto 2 \mapsto 3 \mapsto 1$ . Then $c \circ c$ sends $1 \mapsto 3$ , $2 \mapsto 1$ , $3 \mapsto 2$ , which is the triple $(3,1,2)$ , that is $(1\,3\,2)$ ; and $c \circ c \circ c$ sends $1 \mapsto c(3) = 1$ , $2 \mapsto c(1) = 2$ , $3 \mapsto c(2) = 3$ , so it is $\mathrm{id}$ .

step 1.1L2L3

2.4

Each transposition $\tau$ has $\operatorname{ord}(\tau) = 2$ : $\tau^{2} = \tau \circ \tau = \mathrm{id}$ by step 1.2, while $\tau^{1} = \tau \ne \mathrm{id}$ , so $2$ is the least $k \ge 1$ with $\tau^{k} = \mathrm{id}$ .

step 1.2L4L6

3.1

By steps 1.1 and 2.1 the set $G$ consists of exactly the six listed elements, so the map $6 \to G$ sending $0,1,2,3,4,5$ to $\mathrm{id}, (1\,2), (1\,3), (2\,3), (1\,2\,3), (1\,3\,2)$ respectively is a bijection; hence $G \approx 6$ and $|G| = 6$ . This is claim 1.

step 1.1step 2.1L5

3.2

By step 2.2 the two composites differ, since the triples $(2,3,1)$ and $(3,1,2)$ differ at $1$ ; so $G$ is not abelian, which is claim 2.

step 2.2L3

3.3

Each of $c = (1\,2\,3)$ and $c^{2} = (1\,3\,2)$ has order $3$ : by step 2.3, $c^{3} = \mathrm{id}$ , $c^{1} = c \ne \mathrm{id}$ and $c^{2} = (1\,3\,2) \ne \mathrm{id}$ , so $\operatorname{ord}(c) = 3$ ; and $(c^{2})^{3} = c^{6} = \mathrm{id}$ with $c^{2} \ne \mathrm{id}$ and $(c^{2})^{2} = c^{4} = c \ne \mathrm{id}$ , so $\operatorname{ord}(c^{2}) = 3$ as well.

step 2.3L4L6

4.1

Claims 1, 2 and 3 are steps 3.1, 3.2 and steps 1.3, 2.4 and 3.3 taken together; the orders occurring are exactly $1$ , $2$ and $3$ .

step 3.1step 3.2step 1.3step 2.4step 3.3∎

Remarks

This is the first explicitly non-abelian group in the library. Claim 2 instantiates the general statement of $\operatorname{Sym}(X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements at the three distinct points $1, 2, 3$ ; the pair of transpositions used there is the pair used here.
No element of $G$ has order $6$ , by claim 3, so by 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$ every cyclic subgroup $\langle f \rangle$ has at most three elements and none of them is all of $G$ : the group is not cyclic. That also follows from claim 2, every cyclic group being abelian ( $\langle g \rangle = \{\, g^{n} : n \in \mathbb{Z} \,\}$ , and every cyclic group is abelian).
The elements $1$ , $2$ , $3$ here are the natural numbers of The natural numbers $\mathbb{N}$ (von Neumann), hence sets; nothing in the computation uses anything about them beyond their being three distinct objects.

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 26 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

Symmetric group (Wikipedia) (standard reference, not scraped)
Dihedral group of order 6 (Wikipedia) (standard reference, not scraped)

Sym⁡({1,2,3})\operatorname{Sym}(\{1,2,3\})Sym({1,2,3}) has exactly six elements, is non-abelian, and its elements have orders 111, 222 and 333