Route141 Section 8 closers

This sidecar attacks only the four Section 8 atoms exposed by Route141:

• centralCover_candidateMiddleRLiftObstructionMapData_residual;
• centralCover_candidateFrattiniAffineFiberPartition_residual;
• centralCover_targetLowerProjectionData;
• centralCover_targetKmodRProjectedConjugationActionData.

The integrated route below keeps the Route141 Section 7 kernel and pushout/determinant providers unchanged, but swaps the Section 8 construction to the lower semantic packets already isolated in the candidate and target sidecars.

Candidate Section 8 replacements

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

The selected middle R-obstruction map follows from the smaller obstruction-map packet on the canonical middle exact-image index.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_from_route141Section8Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty (CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F)

The selected Frattini affine-fibre exact-image partition follows from the smaller Frattini cardinality packet for the same selected obstruction datum.

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

Route141 candidate exact-image residual data with the two Route141 candidate atoms replaced by their smaller packet proofs.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_route141Section8Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Drop-in candidate lift-partition provider for the integrated route, using the supplied quotient-frame map from the target construction.

Target Section 8 replacements

theorem Q2Presentation.Induction.centralCover_targetLowerProjectionData_from_route141Section8Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D)

The concrete lower projection Y -> B.C follows from the smaller lower-quotient-map and lower-action-equivalence packets.

theorem Q2Presentation.Induction.centralCover_targetKmodRProjectedConjugationActionData_from_route141Section8Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

The projected K/R conjugation action follows from representative-level conjugation and class-independence of the literal quotient action.

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

Target decoration-kernel provider with the Route141 target atoms replaced by the semantic projection/action split.

Integrated Route142-style Section 8 lowered route

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

Route142-style cover realization: Route141 Section 7 providers, with Section 8 candidate and target atoms swapped for their lower semantic closers.

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

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

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