Route25 target K/R bridge sidecar

Route24's target decoration provider still consumes the transport-final packets

• centralCover_targetLowerProjectionData;
• centralCover_targetKmodRProjectedConjugationActionData.

This sidecar keeps the same downstream provider shape but routes through the finer bridge packets in TargetKmodRSameTowerBridgeClosers:

• a concrete lower projection Y -> C = Y/K with kernel K;
• one representative for each lower class whose action realizes conjugation on the literal quotient K/R.

Manuscript anchors:

• §7 eq:targettower: Y -> B = Y/R -> C = Y/K and M = K/R;
• §8 def:Xgamma: exact-image lower maps land in the lower target C;
• §8 elementary lifting/obstruction separation uses the induced C-action on M = K/R.

Route24-compatible provider from finer bridge packets

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

Route25 quotient-action provider.

Compared with route24, this removes the coarse projection/action residuals centralCover_targetLowerProjectionData and centralCover_targetKmodRProjectedConjugationActionData from the exported closure. The remaining target leaves are the manuscript-shaped bridge packets centralCover_targetLowerProjectionBridgeData and centralCover_targetKmodRRepresentativeActionBridgeData.

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

Route24-compatible decoration-kernel provider downstream of the route25 target bridge.

This has the same output shape as TargetKmodRRoute24ActualProofs.centralCover_targetDecorationKernelData_from_route24 but depends on the finer bridge packets rather than on route24's two coarse transport-final packets.

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

Convenience route25 framed-quotient provider for downstream integration.