Alphabeta Math
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 maximal elementary abelian subgroups of the two extraspecial groups of order 21+2n have orders 2n+1 and 2n

Statement

The maximal elementary abelian subgroups of the two extraspecial groups of order 21+2n have orders 2n+1 and 2n.

Facts & Assumptions

Given: The hypotheses of the Statement.

[L1]

For an extraspecial 2-group P of order 21+2n with Z(P)=z, the square map is the function q determined by x2=zq(xˉ), with values in F2 (The square map of an extraspecial 2-group relative to a chosen generator of its centre).

[L2]

The square map is well defined on the central quotient and satisfies q(xˉyˉ)=q(xˉ)+q(yˉ)+b(xˉ,yˉ) (The square map is well defined on the central quotient and satisfies q(xˉyˉ)=q(xˉ)+q(yˉ)+b(xˉ,yˉ)).

[L3]

For a subgroup Aˉ of P/Z(P) one has AˉAˉ=P/Z(P) (A subgroup of the central quotient and its orthogonal complement have orders multiplying to the order of the quotient).

[L4]

For each n1 there are exactly two extraspecial groups of order 21+2n up to isomorphism, with 22n+2n and 22n2n solutions of x2=1 (For each n1 there are exactly two extraspecial groups of order 21+2n).

[L5]

If P1 and P2 are extraspecial 2-groups with ti solutions of x2=1, then P1P2 has (t1t2+(P1t1)(P2t2))/2 such solutions (A product formula for the number of square roots of the identity in a central product of extraspecial 2-groups).

[L6]

Every maximal abelian subgroup of an extraspecial p-group of order p1+2n has order p1+n (In an extraspecial p-group of order p1+2n every maximal abelian subgroup has order p1+n).

[L7]

An extraspecial p-group has order p1+2n for some n1 (An extraspecial p-group has order p1+2n for some n1).

[L8]

The commutator pairing is independent of the coset representatives, is Fp-bilinear on P/Z(P), and is alternating (The commutator pairing is well defined on the central quotient, is bilinear over Fp, and is alternating).

[L9]

The commutator pairing of an extraspecial p-group has trivial radical (The commutator pairing of an extraspecial p-group has trivial radical).

[L10]

For an extraspecial p-group P with Z(P)=z, the commutator pairing is the map bz(xˉ,yˉ)Z/p determined by [x,y]=zbz(xˉ,yˉ) (The commutator pairing of an extraspecial p-group relative to a chosen generator of its centre).

[L11]

An elementary abelian p-group is a finite abelian p-group in which every nonidentity element has order p; the trivial group is permitted (,, ). (Elementary abelian p-groups).

[L12]

The set S is independent when sSsas=e with finite support forces every as=0. A basis of an elementary abelian p-group is an independent spanning subset for its canonical Fp-linear structure. (Fp-spanning sets, independence, and bases in an elementary abelian p-group).

[L13]

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

[L15]

S;:=;{H;:;HG and SH}. (The subgroup S generated by a subset, the cyclic subgroup g, and cyclic groups).

[L16]

Z(G):={zG:zg=gz for every gG}. (The center Z(G) of a group).

[L17]

An extraspecial 2-group of order 21+2n is of plus type when it has 22n+2n solutions of x2=1 and of minus type when it has 22n2n such solutions; for odd p, plus and minus mean exponent p and p2 respectively (Plus and minus type of an extraspecial p-group).

[L18]

A central product of extraspecial p-groups identified along their centres is extraspecial (A central product of extraspecial p-groups identified along their centres is extraspecial).

[L19]

Every extraspecial p-group is an internal central product of nonabelian subgroups of order p3 pairwise intersecting in its centre (Every extraspecial p-group is an internal central product of nonabelian subgroups of order p3).

Proof

technique · direct
1.1

A maximal elementary abelian subgroup E contains Z(P), so EˉP/Z(P) has order 2k with E=2k+1, and q vanishes on Eˉ.

L1L2L7L11L14L16
1.2

On a coset Eˉvˉ with vˉEˉ the map uˉb(uˉ,vˉ) is a nonzero F2-linear functional on Eˉ, so its kernel has index two and exactly 2k1 of the coset's classes have q=0.

L1L2L8L10L12L13
2.1

Maximality of E says no vˉEˉ orthogonal to Eˉ has q(vˉ)=0: the polar identity would make q vanish on Eˉvˉ, whose preimage is a strictly larger elementary abelian subgroup.

L2L10L11L15step 1.1
2.2

On the coset Eˉ itself q vanishes identically, contributing 2k classes.

L1step 1.1
3.1

On a coset Eˉvˉ with vˉEˉEˉ the correction term vanishes, so q is constantly q(vˉ)=1 by step 2.1 and the coset contributes no class.

L1L2step 2.1
4.1

With Eˉ=22nk there are 22n2k cosets inside the complement and 22nk22n2k outside, so the classes with q=0 number 2k+(22nk22n2k)2k1=22n1+2k22nk1, and the elements with x2=1 number twice that.

L1L2L3L7L9L14step 2.2step 3.1step 1.2algebra
5.1

The classification counts those elements as 22n+2n in the plus case and 22n2n in the minus case, so 2k22nk1=±2n1.

L4L5step 4.1algebra
6.1

The left side is strictly increasing in k, so k=n in the plus case and k=n1 in the minus case are the only solutions; both are attained, giving E=2n+1 and E=2n for EVERY maximal elementary abelian subgroup.

L11L13L17L18L19step 2.1step 5.1algebra
7.1

Independently, E is abelian, so the maximal-abelian bound gives E2n+1 and hence kn without the monotonicity argument; this is the free half of the plus case.

L6step 1.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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