ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13

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.

A composition series and the derived series of $S_{3}$

Example

The chain $S_{3} ▹ A_{3} ▹ 1$ is a composition series with factors $C_{2}$ and $C_{3}$ . It is also the derived series: $S_{3}^{'} = A_{3}$ and $A_{3}^{'} = 1$ . Thus $S_{3}$ is solvable of derived length two, but it is not nilpotent.

Facts & Assumptions

Given: The symmetric group $S_{3}$ and its alternating subgroup $A_{3}$ .

[F1]

A composition series is a strict subnormal chain with simple factors (Composition series, composition factors, and composition length).

[F2]

Derived length is the least $n$ with $G^{(n)} = 1$ (The derived series, solvable groups, and derived length).

[F3]

A group is nilpotent when $Z_{c} (G) = G$ for some $c$ , equivalently when it has a central series from $1$ to $G$ (Nilpotent groups and nilpotency class, Nilpotence via central series, the upper central series, and the lower central series).

[L1]

$S_{3}^{'} = A_{3}$ ( $[S_{n}, S_{n}] = A_{n}$ for $n \geq 2$ , and $[A_{n}, A_{n}] = A_{n}$ for $n \geq 5$ ).

Verification

technique · direct

1.1

The normal subgroup $A_{3}$ has order three and quotient $S_{3} / A_{3}$ has order two; both factors are cyclic of prime order and simple, so $S_{3} ▹ A_{3} ▹ 1$ is a composition series by [F1].

givenF1algebra

1.2

By [L1], $S_{3}^{'} = A_{3}$ ; the cyclic group $A_{3}$ is abelian, so $A_{3}^{'} = 1$ . Thus the same chain is the derived series and [F2] gives derived length two.

L1F2algebra

1.3

The center of $S_{3}$ is trivial: a central element must commute with $(12)$ and $(123)$ , but direct multiplication shows that none of the five nonidentity permutations commutes with both.

algebra

2.1

If a nontrivial group has a central series, take its first nontrivial term $H_{j}$ . Then $H_{j - 1} = 1$ and centrality gives $H_{j} \leq Z (G)$ , so the center is nontrivial. By [F3], a nontrivial nilpotent group has such a series; step 1.3 therefore shows that $S_{3}$ is not nilpotent.

step 1.3F3∎

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: 48 results over 10 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

J. S. Milne, Group Theory, Chapter 6 (standard reference, not scraped)
K. Conrad, Subgroup Series I (standard reference, not scraped)
K. Igusa, Notes on Jordan-Hölder, section 5 (standard reference, not scraped)

A composition series and the derived series of S3S3​