Alphabeta Math
CorollaryStatement: AI-adaptedProof: 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.

An extraspecial p-group of order p1+2n has generator rank 2n

Statement

Let P be an extraspecial p-group of order p1+2n. Then Φ(P)=Z(P) has order p, the Frattini quotient P/Φ(P) has order p2n, the generator rank is d(P)=2n, and every minimal generating set of P has exactly 2n elements.

Facts & Assumptions

Given: An extraspecial p-group P of order p1+2n.

[F1]

For a finite p-group P, the generator rank d(P) is the common size of a basis of P/Φ(P) (The generator rank d(P) of a finite p-group).

[F2]

A subset S of an elementary abelian p-group spans when every element is a product sSsas with coefficients in Fp, and is independent when such a product is the identity only for zero coefficients; a basis is an independent spanning subset (Fp-spanning sets, independence, and bases in an elementary abelian p-group).

[L1]

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).

[L2]

An extraspecial p-group has P=p1+2n with n1 and P/Z(P)=p2n (An extraspecial p-group has order p1+2n for some n1).

[L3]

Every finite elementary abelian p-group has a basis; every independent subset extends to a basis, every spanning subset contains a basis, and all bases have the same finite size (Finite elementary abelian p-groups have bases, basis extension, and a well-defined dimension).

[L4]

A subset X of a finite p-group P is a minimal generating set if and only if the quotient map restricts to a bijection from X onto a basis of P/Φ(P) (Burnside Basis Theorem).

[L5]

The rule aˉx=xa gives every elementary abelian p-group its canonical Fp-vector-space structure (An elementary abelian p-group has a canonical Fp-vector-space structure).

Proof

technique · direct
1.1

By the third description in the characterisation, Φ(P)=Z(P) has order p, so the Frattini quotient is the central quotient.

L1
1.2

The central quotient has order p2n and is elementary abelian.

L1L2
2.1

It therefore has a basis, and all of its bases have the same size, say k; independence and spanning make the map sending a coefficient family (a1,,ak) to the product of the corresponding powers a bijection from the pk coefficient families onto the group, so pk=p2n and k=2n.

F2L3L5step 1.1step 1.2
3.1

Hence d(P)=2n by the definition of the generator rank, and by the Burnside basis theorem a minimal generating set of P is carried bijectively onto a basis of P/Φ(P), so it has 2n elements.

F1L4step 2.1

Remarks

The two clauses say different things. The first is about the quotient and is a count of a basis; the second is about P itself and needs the Burnside basis theorem, because a generating set of P of size 2n could a priori collapse in the quotient. It is the restricted-bijection clause of that theorem which rules that out.

Depends on

Used by

Dependency tree · two levels

35 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