Integrated semantic route for the remaining Section 7/8 packets

This sidecar is the current final-route aggregator. It combines:

• the Section 7 semantic group-tower/determinant packets from MinimalBlockGroupTowerSemanticClosers;
• the candidate canonical concrete obstruction route from CandidateObstructionConcreteProofs, tied to the same canonical target quotient tower used below;
• the proper-image actual middle-restriction route from ProperImageRestrictionActualClosers.

The point is to avoid routing the final theorem through the three old proper-image residuals

• centralCover_elementaryProperImageMiddleKernelMarkedData,
• centralCover_elementaryProperImageMapsToLowerMarkedData,
• centralCover_elementaryProperImageRestrictedSurjData,

while preserving the manuscript semantics: the restricted maps are the actual restrictions of the target quotient map B -> C.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerIntegratedSemanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) : Nonempty (CoverRealization (G.toMinimalBlock h F A R))

Cover realization for a block built from a Section 7 semantic group tower, using the actual middle marked restriction for the elementary proper-image stage.

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_integratedSemanticClosers (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Nonterminal Fourier branch through the integrated semantic route.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_integratedSemanticClosers (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursive branch through the integrated semantic route.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_integratedSemanticClosers (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursion step through the integrated semantic route.

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_integratedSemanticClosers (p : FramedPair) : framedCountA p = framedCountQ p

Boundary-framed counts equal through the integrated semantic route.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_integratedSemanticClosers (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Equal finite surjection counts through the integrated semantic route.