F-G1 — the citable axiom (generic m-data form, design §2.3) #
F-ram F-G1 — the ONE citable axiom of the wave (class (c): citable-as-is plus ONE named referee step).
Citation (primary). R. L. Griess, Jr., Automorphisms of extra
special groups and nonvanishing degree 2 cohomology, Pacific J. Math.
48 (1973) 403–422, Theorem 1, SPLIT half — verbatim, both types
ε = ±: for E extraspecial of order 2^{2n+1} the sequence
1 → Inn(E) → Aut(E) → O^ε(2n,2) → 1 is "nonsplit when n ≥ 3, split
when n = 1, 2" (quoted in full at audit/CITABILITY_AUDIT_20260708.md
§F l.462–471). D. L. Winter, The automorphism group of an
extraspecial p-group, Rocky Mountain J. Math. 2 (1972) 159–168,
supplies the identification Out(E) ≅ O^ε(2n,2) of the quotient. So
for dim V = 2n ≤ 4 a homomorphic section σ : O(q) → Aut(E_f)
exists; composing with any form-preserving act : G → O(q) lifts the
WHOLE acting group — the split half covers EVERY acting subgroup at
small heads (audit §F finding 3(iii) grades exactly this clause
EXACT-CITABLE, with the instruction "check dimV ≤ 4 instances
first").
The ONE named step (the coordinate dictionary).
lem:extraspecialconnecting (reference/q2_manuscript.tex
l.2102–2131) states — AS AN EQUIVALENCE, verbatim "Equivalently,
c⋅(v,z) = (cv, z + m_c(v)) defines an action by automorphisms of
E_f" — that centre-fixing lifts of the action through Aut(E_f) ARE
the families m_c : V → 𝔽₂ satisfying eq:mquadratic and
eq:mcoherent, i.e. exactly the conclusion below. For biadditive f
with diagonal q nonsingular, E_f = V × 𝔽₂ is extraspecial with
E_f/Z ≅ V, squaring map q, commutator = polar, so
Aut(E_f) → O(q) IS the Griess–Winter sequence. This
normalized-coordinates reading is textbook-standard (lifting a group
action to a central extension) and the manuscript states it as an
equivalence; a referee accepts it as one step (design §2.1: match
grade "EXACT after one named step"; restriction of the split section
along act is composition, not a step).
Guards (load-bearing). hd : finrank ≤ 4 is exactly n ≤ 2:
Griess Thm 1's NONSPLIT half makes the ambient extension genuinely
nonsplit for every n ≥ 3, and Griess Thm 0 manufactures nonlifting
2-local subgroup configurations there — Griess: "our methods do not
indicate how big these nonzero cohomology groups are"; NO positive
subgroup-restriction criterion exists in the literature (audit §F
findings 1–2, 4). Dropping or weakening hd is refutable in
principle. hns is load-bearing: E_f is extraspecial (centre
exactly 𝔽₂) only for nondegenerate polar. At odd finrank the
hypotheses are vacuous (no nonsingular form exists —
Quadratic.nonsingular_even_finrank); at V = 0 the instance is
outright provable (m := 0). Biadditivity of f is STRONGER than
Griess needs (any normalized factor set with square map q works), so
the axiom is WEAKER than the citation — the safe direction.
Refutation instrument (design §6.2): per-instance falsifiable — at
a concrete (V, q, f, G, act) with finrank ≤ 4 the conclusion is a
finite search over m : G → V → 𝔽₂ (|G|·2^{dim V} bits); a failed
exhaustive search at a nonsingular instance refutes the axiom AND the
citation. Statement verbatim design §2.3.
F-E1 at the block — the head dimension is even #
The head dimension is even (F-E1 at the block, design §2.2):
edgeHeadForm is nonsingular (edgeHeadForm_nonsingular, proven), so
Quadratic.nonsingular_even_finrank applies. With head nontriviality
(Section7SimpleHeadRadical.lean:122) the honest stratification is
dimV ∈ {2, 4, 6, …}; the F-G1 axiom's ≤ 4 gate therefore covers
exactly the strata dimV ∈ {2, 4} (n = 1, 2).
F-G2 — the low-dimension discharge (instantiate + inflate) #
BaseModelExists holds whenever dimV ≤ 4 (F-G2, design §2.4):
instantiate griess_baseModel_dim_le_four at the head
(V := towerM/towerT, q := edgeHeadForm, f := edgeBaseFactor,
G := HeadIm, act := actQ — the hypotheses are the PROVEN laws
edgeBaseFactor_add_left/right/_diagonal and actQ_form_inv), then
inflate the m-data along towerC ↠ HeadIm exactly as the banked
baseModelExists_of_oddHeadAction does (actQ_mk' is rfl, so the
three BaseModelData field proofs are ascribed-have bridges).
Mission-shaped alias of baseModelExists_of_lowDim (the F-G3-prep
"baseModelExists_of_dim_le_four-shaped exit" spelling).
F-G3-prep — the assembly glue for the coordinator's keep swap #
The keeps-file surgery (design §2.4) replaces the axiom q2_baseModel
by the byte-identical THEOREM
q2_baseModel … := q2_baseModel_of_residual (fun chief K lam hinv hne hd hodd => q2_baseModel_highdim_even chief K lam hinv hne hd hodd) …
against the strictly smaller residual keep
axiom q2_baseModel_highdim_even … (hne : lam ≠ 0)
(hd : 4 < dimV chief K)
(heven : ¬ Odd (Nat.card (HeadIm chief K))) :
BaseModelExists chief K lam hinv hne
whose gates certify genuinely ramified blocks (F-H5's contrapositive,
BaseModelHeadStructure.lean). The swap is the COORDINATOR's; nothing
here touches BlockRecursionKeeps.lean.
The three-way case split (F-G3-prep, per-block form): the
residual 4 < dimV ∧ ¬Odd |HeadIm| branch as a local hypothesis; the
odd branch exits through the banked baseModelExists_of_oddHeadAction,
the low-dimension branch through F-G2.
The ∀-glue for the mechanical keep swap (F-G3-prep): from the
residual (the future q2_baseModel_highdim_even keep, quantified over
all blocks), conclude BaseModelExists at every block — the exact
statement shape q2_baseModel needs, so the coordinator's swap is
:= q2_baseModel_of_residual (q2_baseModel_highdim_even) …-mechanical.