The small Davenport constant of the extraspecial groups of order p¹⁺²ᵐ

H_(p³) = UT₃(Fₚ) as a concrete computable group at every p, with its order, centre and commutator

The sources' definition transcribed, ordering quantifier included, with a decision bridge

Headline: d(H_(p³)) >= 3p-3 at every p, by argument, with no computation

d(H₈) = 4 exactly, both halves – and therefore 3p-3 is false at p = 2

Negative controls, the ordering convention chief among them

The constant exists for every finite group, and d(G) <= |G| - 1 by prefix-product pigeonhole

Volkmann's order-value growth theorem, read inside the group, with no odd-p hypothesis

Olson's D(𝔽ₚ²) = 2p−1, both halves, from Chevalley–Warning — mathlib has Cauchy–Davenport but not Olson

Volkmann's relative subsum theorem (his Thm 4.1) via Alon's Combinatorial Nullstellensatz, and the Σ₀ machinery

The block theorem's first half, the cyclic equality case, and representation rigidity (his Thm 5.1(i), Lemmas 4.3 and 4.4)

d(Hₚ³) = 3p−3 for every odd prime — Volkmann's theorem, formalized

Negative controls for the growth theorem and the line bound, and sharpness in both directions

d(G) ≥ d(N) + d(G/N): the concatenation lemma for the small Davenport constant, ordering quantifier included

Every group of order pⁿ has d(G) ≥ n(p−1) — the concatenation lemma iterated along a chief series

The Heisenberg group of order p²ᵐ⁺¹ as a computable group, with its order, centre and commutator

d(H_(p²ᵐ⁺¹)) ≥ (2m+1)(p−1) at every prime p and every m, and the bracket to p²ᵐ⁺¹ − 1

d(H_(2²ᵐ⁺¹)) ≥ 2m+2 at every m — the exponent-p shape n(p−1) fails at p = 2 for every m, not only at m = 1

Controls: hypothesis-by-hypothesis for the concatenation lemma, sharpness at m = 1 against the family's own theorems, transcription, too-small and too-large

d(G)+1 ≤ (d(N)+1)(d(G/N)+1) and the sharp reduction d(G) ≤ d_(d(N)+1)(G/N), ordering quantifier included

Olson's theorem at every rank: d(Cₚᵏ) = k(p−1), both halves, from Chevalley–Warning — mathlib has neither Olson nor any Davenport constant

d(H_(p¹⁺²ᵐ)) ≤ 2mp(p−1)+p−1 — the extraspecial bracket becomes polynomial at every prime and every m

d(H_(2¹⁺²ᵐ)) ≤ d₂(C₂²ᵐ) at p = 2, and d(H₈) = 4 re-proved with no search — the family's two native axioms retired from that value

Controls: the shape of the multiplicative bound, both hypotheses, tightness in both directions, Olson at rank 2, the new cells, and the comparison with the literature

d(⟨x⟩) = orderOf x − 1 for a cyclic subgroup of any finite group, and d(G) ≥ pᵏ − 1 + (n−k)(p−1) whenever a group of order pⁿ has a normal cyclic subgroup of order pᵏ

The extraspecial group p^(1+2(m+1)) of exponent p² as a concrete computable group, with the additive Cₚ ↪ Cₚ² cocycle

d(p^(1+2M)) ≥ (p−1)(2M+p) for the exponent-p² extraspecial group — (p−1)² more than its exponent-p sibling of the same order, at every prime and every M

d(p^(1+2M)) ≤ 2Mp(p−1) + p − 1 for the exponent-p² extraspecial group, and the polynomial bracket

Controls: the group is H₈ at p = 2, m = 0, the centre is exactly Cₚ, the cyclic hypothesis, sharpness, too-small, too-large, non-vacuity, and the same-order separation

d(p^(1+2M)) = (p−1)(2M+p) for the exponent-p² extraspecial group at every odd prime and every M, and hence Dimitrov's conjecture Dₒ(G) = L(G) for that class