The concrete recursion frame of a §7 block (blockFrame implementation)

Constructs the SectionEight.RecursionFrame T Blk of the paper's §9 induction from a marked target T and a §7 minimal block Blk on T.LY. The B-stage is Y/R and the C-stage is Y/K (R = Φ(K) ≤ K); the head and θ-decoration descend through these quotients (R ≤ K ≤ L_Y = ker π_Y for the head; lemma_7_3 + hE2 — K ⊆ ker θ — for the decoration). The scalar-character index D_R is the subtype of Y-normal index-≤2 subgroups of R, and each nonzero λ gives the scalar central cover Y/λ ↠ Y/R with central generator the class of an r₀ ∈ R ∖ λ (centrality: R/λ is an order-2 normal subgroup of Y/λ, hence central).

This is the implementation half of GQ2.SectionNine.blockFrame (the §9 induction); SectionNine.blockFrame delegates to blockFrameImpl.

noncomputable def GQ2.blockFrameImpl {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) : SectionEight.RecursionFrame T Blk

The concrete recursion frame of a §7 block (the §9 induction).

Equations

• One or more equations did not get rendered due to their size.