ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

The dihedral group of order eight is nilpotent of class two

Example

For $D_{8} = ⟨ r, s ∣ r^{4} = s^{2} = 1, s r s = r^{- 1} ⟩,$ the lower central series is $D_{8} > ⟨ r^{2} ⟩ > 1$ and the upper central series is $1 < ⟨ r^{2} ⟩ < D_{8}$ . Hence $D_{8}$ is nilpotent of class two.

Facts & Assumptions

Given: The displayed presentation of $D_{8}$ .

[F1]

$γ_{r + 1} (G) = [G, γ_{r} (G)]$ (Subgroup commutators and the lower central series).

[F2]

$Z_{1} (G) = Z (G)$ and $Z_{r + 1} (G) / Z_{r} (G) = Z (G / Z_{r} (G))$ (The upper central series).

[L1]

For $c = 2$ , the conditions $Z_{2} (G) = G$ and $γ_{3} (G) = 1$ are equivalent to the existence of a central series of length two, and the least terminating index is the nilpotency class (Nilpotence via central series, the upper central series, and the lower central series).

Verification

technique · direct

1.1

The relation $s r s = r^{- 1}$ gives $[s, r] = s r s^{- 1} r^{- 1} = r^{- 2} = r^{2}$ . Every commutator is generated by this one because $D_{8}$ is generated by $r, s$ , so $γ_{2} (D_{8}) = ⟨ r^{2} ⟩$ .

givenF1algebra

1.2

No element outside $⟨ r^{2} ⟩$ is central: $r, r^{3}$ do not commute with $s$ , and $s r^{k}$ does not commute with $r$ . Hence $Z (D_{8}) = ⟨ r^{2} ⟩$ .

givenalgebra

2.1

The element $r^{2}$ commutes with $r$ and $s$ , so $⟨ r^{2} ⟩ \leq Z (D_{8})$ and $γ_{3} (D_{8}) = [D_{8}, ⟨ r^{2} ⟩] = 1$ .

step 1.1F1algebra

2.2

The quotient $D_{8} / ⟨ r^{2} ⟩$ is abelian, so its center is the whole quotient and [F2] gives $Z_{2} (D_{8}) = D_{8}$ .

step 1.2F2algebra

3.1

Steps 1.1 to 2.2 give both asserted central series, and [L1] gives nilpotency class exactly two.

step 1.1step 2.1step 1.2step 2.2L1∎

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: 25 results over 9 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)