LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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 square map is well defined on the central quotient and satisfies $q (\overset{ˉ}{x} \overset{ˉ}{y}) = q (\overset{ˉ}{x}) + q (\overset{ˉ}{y}) + b (\overset{ˉ}{x}, \overset{ˉ}{y})$

Statement

Let $P$ be an extraspecial $2$ -group with $Z (P) = ⟨ z ⟩$ and $V = P / Z (P)$ , and let $q = q_{z}$ be its square map and $b = b_{z}$ its commutator pairing. Then $q$ is well defined on $V$ and

$q (\overset{ˉ}{x} \overset{ˉ}{y}) = q (\overset{ˉ}{x}) + q (\overset{ˉ}{y}) + b (\overset{ˉ}{x}, \overset{ˉ}{y}) for all \overset{ˉ}{x}, \overset{ˉ}{y} \in V .$

Moreover $q (\overset{ˉ}{x}) = 0$ exactly when the elements of the coset $\overset{ˉ}{x}$ satisfy $x^{2} = 1$ ; a subgroup $U \leq V$ on which $q$ vanishes satisfies $U \leq U^{⊥}$ and has elementary abelian preimage in $P$ of order $2 ∣ U ∣$ ; and every maximal elementary abelian subgroup of $P$ contains $Z (P)$ .

Facts & Assumptions

Given: An extraspecial $2$ -group $P$ with $Z (P) = ⟨ z ⟩$ of order two, the quotient $V = P / Z (P)$ , the commutator pairing $b$ and the square map $q$ .

[F1]

The square map of $P$ relative to $z$ is $q_{z} : V \to F_{2}$ determined by $x^{2} = z^{q_{z} (\overset{ˉ}{x})}$ (The square map of an extraspecial $2$ -group relative to a chosen generator of its centre).

[F2]

The commutator pairing of $P$ relative to $z$ is $b_{z} : V \times V \to F_{p}$ determined by $[x, y] = z^{b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y})}$ (The commutator pairing of an extraspecial $p$ -group relative to a chosen generator of its centre).

[F3]

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

[F4]

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

[F5]

$ord (g)$ is the least $k \geq 1$ with $g^{k} = e$ (The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity).

[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]

If $[G, G] \leq Z (G)$ then $(x y)^{n} = [y, x]^{(\binom{n}{2})} x^{n} y^{n}$ for every $n \in N$ (In a group with central derived subgroup, $(x y)^{n} = [y, x]^{(\binom{n}{2})} x^{n} y^{n}$ ).

[L3]

An extraspecial $p$ -group is nilpotent of class exactly two, its derived subgroup satisfies $P^{'} = Z (P)$ and has order $p$ (An extraspecial $p$ -group is nilpotent of class exactly two and its derived subgroup has order $p$ ).

[L4]

The commutator pairing is well defined, $F_{p}$ -bilinear and alternating, with $b_{z} (\overset{ˉ}{y}, \overset{ˉ}{x}) = - b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y})$ (The commutator pairing is well defined on the central quotient, is bilinear over $F_{p}$ , and is alternating).

[L5]

The rule $\overset{ˉ}{a} \cdot x = x^{a}$ gives every elementary abelian $p$ -group its canonical $F_{p}$ -vector-space structure (An elementary abelian $p$ -group has a canonical $F_{p}$ -vector-space structure).

[L6]

The quotient group $G / N$ has the left cosets $g N$ as elements (The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ ).

Proof

technique · direct

1.1

Since $P / Z (P)$ is elementary abelian, $x^{2} \in Z (P) = {1, z}$ for every $x \in P$ , and $z^{2} = 1$ ; so $(x z)^{2} = x^{2} z^{2} = x^{2}$ and the value of $q$ depends only on the coset $\overset{ˉ}{x}$ , which makes $q$ well defined on $V$ .

F1F3L1L6

2.1

By definition $q (\overset{ˉ}{x}) = 0$ exactly when $x^{2} = 1$ , and since $q$ is well defined this holds for one element of the coset exactly when it holds for both.

F1F5step 1.1

2.2

The class-two power formula at exponent two gives $(x y)^{2} = [y, x]^{(\binom{2}{2})} x^{2} y^{2} = [y, x] x^{2} y^{2}$ , and $[y, x] = z^{b (\overset{ˉ}{y}, \overset{ˉ}{x})}$ . Over $F_{2}$ one has $- 1 = 1$ , so $b (\overset{ˉ}{y}, \overset{ˉ}{x}) = - b (\overset{ˉ}{x}, \overset{ˉ}{y}) = b (\overset{ˉ}{x}, \overset{ˉ}{y})$ ; hence $z^{q (\overset{ˉ}{x} \overset{ˉ}{y})} = z^{b (\overset{ˉ}{x}, \overset{ˉ}{y}) + q (\overset{ˉ}{x}) + q (\overset{ˉ}{y})}$ and the displayed identity holds.

F1F2L2L3L4L5step 1.1

3.1

Let $U \leq V$ satisfy $q (u) = 0$ for every $u \in U$ . Then for $u, u^{'} \in U$ the identity gives $0 = q (u u^{'}) = q (u) + q (u^{'}) + b (u, u^{'}) = b (u, u^{'})$ , so $U \leq U^{⊥}$ .

F2step 2.2

4.1

Let $E$ be the preimage of such a $U$ in $P$ . It contains $Z (P)$ , has order $2 ∣ U ∣$ , is abelian because $b$ vanishes on $U$ , and every one of its elements $x$ satisfies $x^{2} = 1$ by step 2.1 together with $z^{2} = 1$ ; so $E$ is elementary abelian of order $2 ∣ U ∣$ .

F3F4L6step 2.1step 3.1

5.1

If $E$ is elementary abelian and does not contain $Z (P)$ , then $E \cap Z (P)$ is trivial and $E Z (P)$ is an abelian subgroup all of whose elements square to the identity, properly containing $E$ ; so a maximal elementary abelian subgroup contains $Z (P)$ .

F3F4step 2.1step 4.1∎

Remarks

The identity is not additivity, and the correction term is where the two isomorphism types differ: on a subspace where $b$ vanishes the map $q$ is additive and its zero set is a subspace, and it is precisely the size of the largest such subspace that separates the two extraspecial groups of a given order.

Depends on

Used by

The maximal elementary abelian subgroups of the two extraspecial groups of order 2¹⁺²ⁿ have orders 2ⁿ⁺¹ and 2ⁿ Proposition

Cited to discharge well-definedness by The square map of an extraspecial 2-group relative to a chosen generator of its centre.

Dependency tree · two levels

44 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

D. Kaur and A. Kulshrestha, Characters of real special 2-groups, §2 opening and §2.1 (standard reference, not scraped)

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