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

The integral Heisenberg group is nilpotent of class two

Example

On $H = Z^{3}$ , define $(a, b, c) (a^{'}, b^{'}, c^{'}) = (a + a^{'}, b + b^{'}, c + c^{'} + a b^{'}) .$ This is the integral Heisenberg group. Its commutator subgroup is ${(0, 0, c) : c \in Z}$ , which is central and nontrivial, so $H$ is nilpotent of class two.

Facts & Assumptions

Given: The displayed operation on $H = Z^{3}$ .

[F1]

A group operation must be associative and have an identity and inverses (Group and abelian group).

[F2]

$γ_{2} (H) = [H, H]$ and $γ_{3} (H) = [H, γ_{2} (H)]$ (Subgroup commutators and the lower central series).

[L1]

For $c = 2$ , the condition $γ_{3} (H) = 1$ is 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 element $(0, 0, 0)$ is an identity and $(a, b, c)^{- 1} = (- a, - b, - c + a b)$ .

givenalgebra

2.1

Both $(x y) z$ and $x (y z)$ have first two coordinates equal to the coordinate sums and third coordinate $c + c^{'} + c^{''} + a b^{'} + a b^{''} + a^{'} b^{''}$ , so the operation is associative. Thus [F1] makes $H$ a group.

givenstep 1.1F1algebra

2.2

Direct use of step 1.1 gives $[(a, b, c), (a^{'}, b^{'}, c^{'})] = (0, 0, a b^{'} - a^{'} b) .$ Hence every commutator lies in $C : = {(0, 0, c) : c \in Z}$ .

step 1.1algebra

3.1

Every element of $C$ commutes with every element of $H$ , and $[(1, 0, 0), (0, c, 0)] = (0, 0, c)$ ; therefore $[H, H] = C \leq Z (H)$ .

step 2.2algebra

4.1

By [F2], $γ_{3} (H) = [H, C] = 1$ , while $(0, 0, 1) \in γ_{2} (H)$ is nonidentity. Thus [L1] gives nilpotency class exactly two.

step 3.1F2L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

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)