Candidate/target Route133 Section 8 closers

This sidecar leaves the promoted route files untouched. It gives Route133-context provider hooks that avoid the two candidate exact-image residual axioms and the Route130 target bridge, replacing them by narrower Section 8 sidecar surfaces:

• candidate exact-image residuals -> Route113 current semantic split;
• target Route28 bridge surface -> Route21 concrete lower-projection / representative-action bridge.

Kernel and determinant/pushout providers are kept exactly as in the current Route133 all-Route130-lowered route.

Candidate Route133 residual replacements

theorem Q2Presentation.Induction.centralCover_candidateMiddleExactImageObstructionEvaluationData_from_candidateTargetRoute133Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T)

Route133 candidate middle exact-image obstruction evaluation, lowered to the Route113 current semantic split.

theorem Q2Presentation.Induction.centralCover_candidateTopExactImageAffineFiberEquivData_from_candidateTargetRoute133Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (E : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) : Nonempty (CentralCoverCandidateTopExactImageAffineFiberEquivData B T E)

Route133 candidate top affine-fibre equivalence, lowered to the Route113 current semantic split.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateTargetRoute133Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Route133 candidate lift partition provider using the Route113 current semantic exact-image split.

Target Route133 bridge replacement

theorem Q2Presentation.Induction.centralCover_targetDecorationKernelData_from_candidateTargetRoute133Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetDecorationKernelData B D)

Route133 target decoration-kernel provider through the concrete Route21 lower-projection / representative-action bridge.

Route-context integration

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCurrentIntegrated133_candidateTargetClosers {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))

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

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated133_candidateTargetClosers (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_currentIntegrated133_candidateTargetClosers (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_currentIntegrated133_candidateTargetClosers (p : FramedPair) : framedCountA p = framedCountQ p

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