ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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 $3 \times 3$ upper-unitriangular group over a prime field has generator rank two

Example

For a prime $p$ , let $H_{p}$ be the set of $3 \times 3$ upper-unitriangular matrices over the prime field $Z / p$ under matrix multiplication. Writing

$M (a, b, c) = (\begin{array}{ccc} 1 & a & c \\ 0 & 1 & b \\ 0 & 0 & 1 \end{array}) (a, b, c \in Z / p),$

the assignment $(a, b, c) \mapsto M (a, b, c)$ is a bijection from $(Z / p)^{3}$ onto $H_{p}$ that turns matrix multiplication into

$(a, b, c) (a^{'}, b^{'}, c^{'}) = (a + a^{'}, b + b^{'}, c + c^{'} + a b^{'}) .$

Working in these coordinates, $H_{p}$ is a group of order $p^{3}$ ,

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

and $d (H_{p}) = 2$ . This includes $p = 2$ , when $H_{p}$ does not have exponent $p$ .

Facts & Assumptions

Given: A prime $p$ , the $3 \times 3$ upper-unitriangular matrices over $Z / p$ , and the displayed coordinate parametrisation.

[L1]

For every finite $p$ -group $P$ , $Φ (P) = P^{'} P^{p}$ ( $Φ (P) = P^{'} P^{p}$ for a finite $p$ -group).

[F1]

The generator rank is the common size of a basis of the Frattini quotient (The generator rank $d (P)$ of a finite $p$ -group).

[L2]

The operations make $Z / p$ a field with $p$ elements, and the threefold Cartesian product has $p^{3}$ elements (For every prime $p$ , the two operations on $Z / p$ make it a field, For $n \geq 1$ , every class in $Z / n$ has one representative $r$ with $0 \leq r < n$ , so $∣ Z / n ∣ = n$ ; while $Z / 0$ is in bijection with $Z$ , The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

[F2]

A basis is an independent spanning subset for the canonical $F_{p}$ -linear structure ( $F_{p}$ -spanning sets, independence, and bases in an elementary abelian $p$ -group).

Verification

technique · direct

1.1

Multiplying $M (a, b, c) M (a^{'}, b^{'}, c^{'})$ entrywise gives the matrix with $(1, 2)$ entry $a + a^{'}$ , $(2, 3)$ entry $b + b^{'}$ and $(1, 3)$ entry $c + c^{'} + a b^{'}$ , so the parametrisation carries matrix multiplication to the displayed coordinate operation and is a bijection. Direct substitution shows associativity; the identity is $(0, 0, 0)$ and $(a, b, c)^{- 1} = (- a, - b, - c + a b)$ . By [L2] the set has order $p^{3}$ , so this is a finite $p$ -group.

givenL2algebra

2.1

A calculation with the inverse in step 1.1 gives $[(a, b, c), (a^{'}, b^{'}, c^{'})] = (0, 0, a b^{'} - a^{'} b)$ . Every commutator lies on the central $c$ -axis, and $(0, 0, t) = [(t, 0, 0), (0, 1, 0)]$ , so $H_{p}^{'} = {(0, 0, c)}$ .

step 1.1L2algebra

3.1

Induction gives $(a, b, c)^{m} = (m a, m b, m c + (\binom{m}{2}) a b)$ . For odd $p$ , every $p$ th power is the identity; for $p = 2$ , every square is $(0, 0, a b)$ and hence lies on the central axis. Since the derived subgroup already equals that axis, [L1] gives $Φ (H_{p}) = {(0, 0, c)}$ in both cases.

step 1.1step 2.1L1algebra

4.1

Modulo the central axis, the first two coordinate classes give unique coordinates and form a two-vector basis by [F2]. Therefore [F1] gives $d (H_{p}) = 2$ .

step 3.1F1F2algebra∎

Remarks

The prime field is a hypothesis, not a convenience. Over $F_{q}$ with $q = p^{e}$ the same coordinates and the same two computations give $H^{'} = {(0, 0, c) : c \in F_{q}}$ and $(a, b, c)^{p} = (0, 0, (\binom{p}{2}) a b)$ , so the Frattini subgroup is again that central axis and the Frattini quotient is $F_{q} \oplus F_{q}$ — a vector space of dimension $2 e$ over $F_{p}$ , not $2$ . For $q = 4$ the generator rank is therefore $4$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

K. Conrad, Generating Sets, Example 6.11 (standard reference, not scraped)
Y. Harpaz and O. Wittenberg, The Massey Vanishing Conjecture for Number Fields, §2 (standard reference, not scraped)

The 3×33×3 upper-unitriangular group over a prime field has generator rank two