Route31 target K/R bridge sidecar

Route32 currently reaches the target decoration-kernel provider through the route30 split:

• centralCover_targetLowerQuotientMapData;
• centralCover_targetLowerActionEquivData;
• TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData.

This sidecar keeps the route32 downstream surface, but routes the target K/R quotient action through the already available route28 manuscript-shaped packets. The lower side is still split into the concrete lower quotient map and its action-group equivalence, while the action side is narrowed from the all-ambient action packet to a selected-representative action packet plus the closed inner-conjugation theorem.

It is intentionally not imported by the integrated route; the supervisor can wire the exported provider below in place of the route30 target provider.

Route31 target bridge replacements

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

Route31 lower-projection provider.

This avoids the current route32 residual names centralCover_targetLowerQuotientMapData and centralCover_targetLowerActionEquivData; its remaining lower-side assumptions are the narrower route28 quotient-map/equivalence packets.

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

Route31 projected-action provider.

This avoids the current route32 ambient-action residual by using the route28 selected-representative action packet and the theorem-level inner-conjugation closure on K/R.

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

Route31 quotient-action provider.

Its axiom closure contains none of the three current route32 target residual names. The remaining target branch is the route28 lower-map/equivalence plus selected-representative action frontier.

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

Route31 decoration-kernel provider with the current route32 target residual names removed from the axiom closure.

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

Convenience route31 framed-quotient provider for downstream integration.