Route172 target K/R same-tower closers

Route169's target decoration-kernel provider has a compact closure, but it still exposes the two broad actual same-tower packets:

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData.

This sidecar gives a drop-in provider with the same return type as TargetKmodRRoute169Closers.centralCover_targetDecorationKernelData_from_route152Closers_route169. It routes through the Route122/Route52 coherent literal same-tower packet: one selected identification Y/K ~= B.C together with the corresponding literal representative action on K/R.

Manuscript anchors:

• Section 7 fixes the same tower Y -> B = Y/R -> C = Y/K and M = K/R.
• Section 8 uses exact-image lower maps to that lower target C, and the target-side action on M is the action transported through this same literal quotient.

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

Route172 quotient-action provider through the coherent literal same-tower Route52 packet.

The closure removes both Route169 same-tower actual atoms and replaces them by TargetKmodRRoute52BridgeProofs.centralCover_targetRoute52CoherentLiteralActionData.

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

Route172 drop-in target decoration-kernel provider.

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

Name mirroring the current Route169 call-site role for one-line replacement.

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

Convenience framed-quotient provider downstream of the Route172 target closer.