§8 radical-edge def-layer

The Lemma 8.6 definition layer — CentralCover, polarMul, RadicalCoverData, NoDescent, MLifts, MLifts.Central — and the generic half-count engine two_mul_card_fiber, lifted out of GQ2/SectionEight.lean into this lower shared file.

Why. The §8 proof-layer files (GQ2/CentralObstruction.lean, …) need these definitions to state and prove their lemmas, but must not import SectionEight — otherwise splicing a proved lemma back into SectionEight (lemma_8_6_local := CentralObstruction…) is a circular import (the Prop. 5.16 proof prop_5_16 trap). Same pattern as GQ2/OrbitData.lean for §6 (docs/orchestration/orbit-data-refactor.md).

Moved verbatim from SectionEight (namespace preserved: GQ2.SectionEight). No axioms; Ax = ∅.

Central double covers (§8)

structure GQ2.SectionEight.CentralCover (Y : Type) [Group Y] [Finite Y] : Type 1

A central double cover of the finite group Y (§8): a surjection whose kernel is generated by a central element z ≠ 1 of square one.

• cover : Type

  The covering group.

• group : Group self.cover
• finite : Finite self.cover
• topo : TopologicalSpace self.cover
• disc : DiscreteTopology self.cover
• p : self.cover →* Y

  The covering surjection.

• surj : Function.Surjective ⇑self.p
• z : self.cover

  The central kernel generator.

• z_ne : self.z ≠ 1
• z_sq : self.z * self.z = 1
• central (x : self.cover) : self.z * x = x * self.z
• ker_eq : self.p.ker = Subgroup.zpowers self.z

theorem GQ2.SectionEight.CentralCover.sq_eq_one_of_mem_ker {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) {x : C.cover} (hx : x ∈ C.p.ker) : x * x = 1

Squares die in the kernel subgroup ⟨z⟩ (its elements have order ≤ 2).

theorem GQ2.SectionEight.CentralCover.z_pow_val_add {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (a b : ZMod 2) : C.z ^ (a + b).val = C.z ^ a.val * C.z ^ b.val

z-powers by 𝔽₂-exponents add (any central double cover: z² = 1).

The Lemma 8.6 datum (radical cover)

def GQ2.SectionEight.polarMul {M : Type u_1} (q : M → ZMod 2) (mul : M → M → M) (m m' : M) : ZMod 2

The multiplicative polar form of a 𝔽₂-valued square function on (a subgroup of) a group: B_q(m, m') = q(mm') + q(m) + q(m').

Equations

• GQ2.SectionEight.polarMul q mul m m' = q (mul m m') + q m + q m'

structure GQ2.SectionEight.RadicalCoverData (Bg : Type) [Group Bg] [Finite Bg] : Type 1

The Lemma 8.6 datum: a central double cover of Bg restricting to a quadratic form on the elementary abelian normal subgroup M, with polar radical containing T ≤ M and vanishing on T (paper §8, setting of Lemma 8.6; M = K/R, T = T₀ after §7).

• C : CentralCover Bg

  The central double cover p : B̃ ↠ B.

• M : Subgroup Bg

  The elementary abelian layer M (paper: M = K/R).

• hM : self.M.Normal
• T : Subgroup Bg

  The polar radical T (paper: T = T₀).

• hT : self.T.Normal
• hTM : self.T ≤ self.M
• helem (m : Bg) : m ∈ self.M → m * m = 1
• hcomm (m : Bg) : m ∈ self.M → ∀ m' ∈ self.M, m * m' = m' * m
• q : ↥self.M → ZMod 2

  The square form of the cover on M: x̃² = z^{q(x)} for any lift x̃ of x ∈ M.

• hq (x : self.C.cover) (hx : self.C.p x ∈ self.M) : x * x = self.C.z ^ (self.q ⟨self.C.p x, hx⟩).val
• hrad (t : Bg) (ht : t ∈ self.T) (m : Bg) (hm : m ∈ self.M) : polarMul self.q (fun (a b : ↥self.M) => ⟨↑a * ↑b, ⋯⟩) ⟨t, ⋯⟩ ⟨m, hm⟩ = 0

  T lies in the polar radical of q.

• hTzero (t : Bg) (ht : t ∈ self.T) : self.q ⟨t, ⋯⟩ = 0

  q vanishes on T.

instance GQ2.SectionEight.RadicalCoverData.instNormalM {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : D.M.Normal

The M-layer of a RadicalCoverData is normal (instance form, so that the quotient Bg ⧸ D.M carries its group structure in statement positions — the TameQuotientData Lean-detail pattern).

def GQ2.SectionEight.RadicalCoverData.NoDescent {Bg : Type} [Group Bg] [Finite Bg] (D : RadicalCoverData Bg) : Prop

"The radical edge is nonzero", operationally (Lemma 8.6, descent clause): the cover admits no descent to B/T, i.e. no normal complement to p⁻¹(T) missing z.

Equations

• D.NoDescent = ¬∃ (N : Subgroup D.C.cover), N.Normal ∧ Subgroup.map D.C.p N = D.T ∧ D.C.z ∉ N

Unrestricted M-lifts and the central relation (Lemma 8.6 count objects)

def GQ2.SectionEight.MLifts {Bg : Type} [Group Bg] [TopologicalSpace Bg] [Finite Bg] (D : RadicalCoverData Bg) {Γ' : Type} [Group Γ'] [TopologicalSpace Γ'] (ρ : Γ' →ₜ* Bg ⧸ D.M) : Type

The unrestricted M-lifts of a lower map ρ : Γ → B/M: continuous homomorphisms f : Γ → B over ρ.

Equations

• GQ2.SectionEight.MLifts D ρ = { f : Γ' →ₜ* Bg // ∀ (γ : Γ'), ↑(f γ) = ρ γ }

def GQ2.SectionEight.MLifts.Central {Bg : Type} [Group Bg] [TopologicalSpace Bg] [Finite Bg] (D : RadicalCoverData Bg) {Γ' : Type} [Group Γ'] [TopologicalSpace Γ'] {ρ : Γ' →ₜ* Bg ⧸ D.M} (f : MLifts D ρ) : Prop

An M-lift satisfies the central relation when it lifts through the cover.

Equations

• GQ2.SectionEight.MLifts.Central D f = ∃ (g : Γ' →ₜ* D.C.cover), ∀ (γ : Γ'), D.C.p (g γ) = ↑f γ

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 8.6 = ⟦lem-radicaledge⟧