Lemma 7.2 (Frattini–centralizer collapse) and Lemma 7.3 (decorations vanish)

Split off from GQ2.SectionSeven, building on GQ2.SectionSeven.Basic. This file provides:

• Lemma 7.2 (lemma_7_2): for a tame head, the Frattini–centralizer collapse;
• Lemma 7.3 (lemma_7_3): every homomorphism from Y to an elementary target that is trivial on the block's decorations vanishes.

See GQ2.SectionSeven for the umbrella module docstring.

Lemma 7.2 (Frattini–centralizer collapse) and Lemma 7.3 (decorations vanish)

theorem GQ2.SectionSeven.lemma_7_2 {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} {H : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] (π : Y →* H) : Function.Surjective ⇑π → π.ker = L → ∀ (cH : ↑Ttame.toProfinite.toTop →ₜ* H), Function.Surjective ⇑cH → ∀ (B : MinimalBlock L), (∀ r ∈ B.frattiniK, ∀ k ∈ B.K, r * k = k * r) ∧ (∀ r ∈ B.frattiniK, r * r = 1) ∧ ∀ k ∈ B.K, k ^ 4 = 1

Lemma 7.2: for a tame head (the target's head map factors through GQ2.Ttame), R = Φ(K) is central elementary abelian in K, and K⁴ = 1. [the §§6–7 statement; proof the §§6–7 proof layer (odd Hall lift + three-subgroup lemma + the G-equivariant fourth-power map).]

theorem GQ2.SectionSeven.lemma_7_3 {Y : Type} [Group Y] {L : Subgroup Y} (B : MinimalBlock L) {E : Type} [CommGroup E] (hE : ∀ (e : E), e ^ 2 = 1) (f : Y →* E) : B.K ≤ f.ker

Lemma 7.3 (decorations vanish on the block): every homomorphism from Y to an elementary abelian 2-group kills K (via Lemma 7.1's dual clause). The frame decorations θ_Y of GQ2.MarkedTarget are such homomorphisms. [the §§6–7 statement; proof the §§6–7 proof layer: a nonzero value f k₀ ≠ 1 yields — through the 𝔽₂-module structure on Additive E and a separating dual functional — a C₂-character of Y nontrivial on K and killing R, whose kernel meets K in a Y-normal index-2 subgroup above R, contradicting lemma_7_1_dual. Finiteness-free.]