§8 frame-enrichment, block layer

The constructibility half of the Prop. 8.9 assembly frame-enrichment layer: at the B = Y/R stage of the §8 recursion the scalar covers p_λ carry square-form data on M_B = π_B(K) with polar radical containing T_B = π_B((K∩S)·R) — a per-λ Lemma 8.6 datum (RadicalCoverData). The abstract per-λ fields live on the recursion frame (GQ2.SectionEight.RecursionFrame.Enrichment, in SectionEight.lean); this file proves the block-level facts the concrete frame construction will discharge them with:

• blockT_map_le_blockM_map — T_B ≤ M_B ((K∩S)·R ≤ K, via lemma_7_1_head);
• mForm_of_qbar — from the Prop 7.4 package (λ, q̄, hspec) (a Y-invariant additive λ on R with descended square values λ(k²) = q̄(k mod S)), the M_B-level form q_M(π_B k) := λ(k²) is well defined and has the (b)/(c) radical clauses of RadicalCoverData. The whole derivation rides on R ≤ K ∩ S (lemma_7_1_head): the π_B-fibres over M_B lie inside single S-cosets of K, so every value reads off q̄ through hspec. (The cover clause hq is definitional for the concrete pushout cover Y/ker λ ↠ Y/R and is not part of this lemma.)

All std-3; no axioms.

theorem GQ2.SectionEight.blockT_map_le_blockM_map {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) {YB : Type} [Group YB] (piB : Y →* YB) : Subgroup.map piB (B.K ⊓ B.S ⊔ B.frattiniK) ≤ Subgroup.map piB B.K

Under any projection of the block, the T-layer image lands in the M-layer image: (K ∩ S) ⊔ R ≤ K because R = Φ(K) ≤ K ∩ S (lemma_7_1_head).

theorem GQ2.SectionEight.mForm_of_qbar {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) {YB : Type} [Group YB] (piB : Y →* YB) (hker : piB.ker = B.frattiniK) (lam : ↥B.frattiniK → ZMod 2) (hlam_hom : ∀ (r r' : ↥B.frattiniK), lam (r * r') = lam r + lam r') (hsq : ∀ k ∈ B.K, k * k ∈ B.frattiniK) (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (hspec : ∀ (k : Y) (hk : k ∈ B.K), lam ⟨k * k, ⋯⟩ = qbar ↑⟨k, ⋯⟩) : ∃ (qM : ↥(Subgroup.map piB B.K) → ZMod 2), (∀ (k : Y) (hk : k ∈ B.K), qM ⟨piB k, ⋯⟩ = lam ⟨k * k, ⋯⟩) ∧ (∀ (t : YB) (ht : t ∈ Subgroup.map piB (B.K ⊓ B.S ⊔ B.frattiniK)) (m : YB) (hm : m ∈ Subgroup.map piB B.K), polarMul qM (fun (a b : ↥(Subgroup.map piB B.K)) => ⟨↑a * ↑b, ⋯⟩) ⟨t, ⋯⟩ ⟨m, hm⟩ = 0) ∧ ∀ (t : YB) (ht : t ∈ Subgroup.map piB (B.K ⊓ B.S ⊔ B.frattiniK)), qM ⟨t, ⋯⟩ = 0

The M_B-level square form from the Prop 7.4 descent (the Prop. 8.9 assembly): given the 7.4 package for a Y-invariant additive λ on R — the descended q̄ on V = P/S with λ(k²) = q̄(k mod S) — the assignment q_M(π_B k) := λ(k²) is well defined on M_B = π_B(K) and satisfies the value, polar-radical, and T-vanishing clauses of the per-λ RadicalCoverData. Route: ker π_B = R ≤ S (lemma_7_1_head), so π_B-fibres lie in single S-cosets and every clause reduces to an S-coset computation in q̄.

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

• Lemma 8.6 = ⟦lem-radicaledge⟧
• Prop 7.4 = ⟦prop-simpleheaddet⟧