Integrated Route217: Route217 Section 7 plus actual candidate coherent closer

This route starts from Route212, then swaps in the Route212 Section 7 Frattini provider and the Route212 determinant/pushout provider.

• candidate side: Route211 current-semantic scalar/Frattini lowering, replacing the broad Route210 candidate obstruction/Frattini packets by the lower scalar-obstruction evaluator and affine-fibre coordinate packets;
• target side: Route212 literal quotient/action lowering, replacing TargetKmodRSameTowerBridgeClosers.centralCover_targetLowerProjectionBridgeData and TargetKmodRSameTowerBridgeClosers.centralCover_targetKmodRRepresentativeActionBridgeData by the lower Route146 quotient identification and literal representative-action atoms.

It lowers the current Section 7 kernel provider and determinant provider while keeping the Route146 target side and the actual candidate coherent side.

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

Route217 realization with Route217 Section 7 lowerings and the actual candidate coherent closer.

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

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated217KernelCompact (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)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_currentIntegrated217KernelCompact (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)

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

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated217KernelCompact (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)))