PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 Heisenberg group of order $p^{3}$ is extraspecial, and for odd $p$ it has exponent $p$

Statement

Let $p$ be a prime and let $H_{p}$ be the Heisenberg group of order $p^{3}$ . Then

$Z (H_{p}) = [H_{p}, H_{p}] = {(0, 0, c) : c \in Z / p},$

a subgroup of order $p$ , and $H_{p}$ is extraspecial. For odd $p$ the exponent of $H_{p}$ is $p$ . At $p = 2$ the exponent is $4$ , since $(1, 1, 0)^{2} = (0, 0, 1)$ .

Facts & Assumptions

Given: A prime $p$ and the Heisenberg group $H_{p}$ .

[F1]

The Heisenberg group of order $p^{3}$ is the set $H_{p} = {(a, b, c) : a, b, c \in Z / p}$ with $(a, b, c) (a^{'}, b^{'}, c^{'}) : = (a + a^{'}, b + b^{'}, c + c^{'} + a b^{'})$ (The Heisenberg group of order $p^{3}$ over $Z / p$ ).

[F2]

$Z (G) : = {z \in G : z g = g z for every g \in G}$ (The center $Z (G)$ of a group).

[F3]

For $g, h \in G$ the commutator is $[g, h] : = g h g^{- 1} h^{- 1}$ , and $[G, G]$ is the subgroup generated by all commutators (Commutators $[g, h] = g h g^{- 1} h^{- 1}$ and the commutator subgroup $[G, G]$ ).

[F4]

For a finite group $G$ , $\exp (G) = \min {n \in N : n > 0 and g^{n} = e for every g \in G}$ (The exponent of a finite group).

[L1]

The Heisenberg multiplication is a group law with identity $(0, 0, 0)$ and inverse $(a, b, c)^{- 1} = (- a, - b, - c + a b)$ ; the group is not abelian, $∣ H_{p} ∣ = p^{3}$ , and $(1, 0, 0)^{a} = (a, 0, 0)$ , $(0, 1, 0)^{b} = (0, b, 0)$ , $(0, 0, 1)^{c} = (0, 0, c)$ (The Heisenberg multiplication is a group law, nonabelian, on a set of $p^{3}$ elements).

[L2]

For a finite $p$ -group $P$ the following are equivalent: $P$ is extraspecial; $P$ is nonabelian, $∣ Z (P) ∣ = p$ and $P / Z (P)$ is elementary abelian; $P$ is nonabelian and $Z (P) = P^{'} = Φ (P)$ has order $p$ (Three equivalent descriptions of an extraspecial $p$ -group).

[L3]

For $N ⊴ G$ , the quotient $G / N$ is abelian if and only if $[G, G] \subseteq N$ ( $G / N$ is abelian if and only if $[G, G] \subseteq N$ ).

[L4]

If the quotient group $G / Z (G)$ is cyclic, then $G$ is abelian (If $G / Z (G)$ is cyclic, then $G$ is abelian).

[L5]

For a finite group $G$ and $H \leq G$ , $∣ G ∣ = [G : H] ∣ H ∣$ (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

[L6]

An elementary abelian $p$ -group is a finite abelian $p$ -group in which every nonidentity element has order $p$ (Elementary abelian $p$ -groups).

[L7]

For an odd prime $p$ and a finite group $G$ with $[G, G] \leq Z (G)$ of exponent dividing $p$ , $(x y)^{p} = x^{p} y^{p}$ for all $x, y$ (For an odd prime $p$ , the $p$ -th power map is a homomorphism on a finite group whose derived subgroup is central of exponent dividing $p$ ).

[L8]

$⟨ S ⟩$ is the smallest subgroup of $G$ containing $S$ (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[L9]

A finite $p$ -group is a finite group whose order has the form $p^{n}$ (A finite $p$ -group has order $p^{n}$ for a prime $p$ and some $n \in N$ ).

Proof

technique · direct

1.1

A triple $(a, b, c)$ commutes with $(a^{'}, b^{'}, c^{'})$ exactly when $a b^{'} = a^{'} b$ . Taking $(a^{'}, b^{'}, c^{'}) = (0, 1, 0)$ gives $a = 0$ , and taking $(a^{'}, b^{'}, c^{'}) = (1, 0, 0)$ gives $b = 0$ ; conversely every $(0, 0, c)$ commutes with everything. So $Z (H_{p}) = {(0, 0, c)}$ , a subgroup of order $p$ .

F1F2L1

1.2

For $g = (a, b, c)$ and $h = (a^{'}, b^{'}, c^{'})$ one has $g h = (a + a^{'}, b + b^{'}, c + c^{'} + a b^{'})$ and $h g = (a + a^{'}, b + b^{'}, c + c^{'} + a^{'} b)$ , so $g h = h g \cdot (0, 0, a b^{'} - a^{'} b)$ and therefore $[g, h] = (g h) (h g)^{- 1} = (0, 0, a b^{'} - a^{'} b)$ .

F1F3L1

1.3

$H_{p}$ is a finite $p$ -group of order $p^{3}$ and is not abelian.

L1L9

2.1

Every commutator lies in ${(0, 0, t)}$ , and taking $a = b^{'} = 1$ with $a^{'} = b = 0$ gives the commutator $(0, 0, 1)$ , which generates that subgroup; hence $[H_{p}, H_{p}] = Z (H_{p})$ , of order $p$ .

F3L8step 1.1step 1.2

3.1

By Lagrange the quotient $H_{p} / Z (H_{p})$ has order $p^{2}$ ; it is abelian because $[H_{p}, H_{p}] \leq Z (H_{p})$ , and it is not cyclic, since a cyclic central quotient would make $H_{p}$ abelian. An abelian group of order $p^{2}$ that is not cyclic has no element of order $p^{2}$ , so every one of its nonidentity elements has order $p$ and it is elementary abelian.

L3L4L5L6step 2.1step 1.3

4.1

By the second description in the characterisation, $H_{p}$ is extraspecial.

L2step 1.1step 1.3step 3.1

5.1

For odd $p$ , the derived subgroup is central of order $p$ , so the $p$ -th power map is a homomorphism; the three generators $(1, 0, 0)$ , $(0, 1, 0)$ and $(0, 0, 1)$ have $p$ -th power the identity, so the $p$ -th power map is trivial on a generating set and hence on $H_{p}$ . Since $H_{p}$ is nontrivial, its exponent is $p$ .

F4L1L7L8step 2.1step 4.1

6.1

At $p = 2$ the exponent is not $2$ : $(1, 1, 0)^{2} = (1 + 1, 1 + 1, 0 + 0 + 1 \cdot 1) = (0, 0, 1)$ , which is not the identity, while $(0, 0, 1)^{2} = (0, 0, 0)$ , so $(1, 1, 0)$ has order $4$ and the exponent is $4$ .

F1F4L1L5step 1.3∎

Remarks

The group is extraspecial at every prime, $p = 2$ included; only the exponent depends on the parity of $p$ . The step that fails at $p = 2$ is the $p$ -th power homomorphism, whose hypothesis is that $p$ be odd, and the failure is visible in the element $(1, 1, 0)$ of order four.

Depends on

Used by

Dependency tree · two levels

59 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

M. van Beek, Topics in Finite p-Groups, Proposition 2.32(iii) (standard reference, not scraped)
D. A. Craven, The Theory of p-Groups, Definition 3.3 (standard reference, not scraped)

The Heisenberg group of order p3p3 is extraspecial, and for odd pp it has exponent pp