Route30 target K/R bridge sidecar

Route29's target decoration-kernel provider closes through the route26 selected canonical-section action packet and the literal same-tower lower quotient equivalence. This sidecar keeps the same downstream decoration-kernel surface but bypasses both route29 residual names.

The lower side is routed through the concrete projection-semantic split:

• a framed lower quotient map Y -> C = Y/K;
• an equivalence from that concrete lower child to the abstract action group B.C.

The action side is routed through the all-ambient-representatives law on K/R; restricting that law to the chosen lower projection gives the projected conjugation action directly, so no selected-section residual is needed in the exported provider.

Route30 target bridge replacements

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

Route30 lower-projection provider.

This replaces the route29 dependence on the quotient equivalence Y/K ~= B.C by the more concrete projection-semantic packets for the lower target in the manuscript tower.

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

Route30 projected-action provider.

The selected-section action required by route26 is recovered theorem-level from the all-ambient action law: if every ambient representative realizes the transported B.C-action on K/R, then the projected conjugation action packet is immediate for any lower projection.

theorem Q2Presentation.Induction.TargetKmodRRoute30BridgeProofs.centralCover_targetKmodRQuotientActionData_from_route30 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

Route30 quotient-action provider.

Its axiom closure avoids both route29 target residual names:

• TargetKmodRRoute26BridgeProofs.centralCover_targetRoute26RepresentativeSectionActionData;
• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData.

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

Route30 decoration-kernel provider with the route29 target residual names removed from the axiom closure.

theorem Q2Presentation.Induction.TargetKmodRRoute30BridgeProofs.centralCover_targetCanonicalFramedQuotientData_from_route30 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

Convenience route30 framed-quotient provider for downstream integration.