Route126 target K/R closer

Route126's public target provider currently routes through TargetKmodRRoute53BridgeProofs.centralCover_targetDecorationKernelData_from_route53, whose only target-side non-local leaf is the broad Route45 literal selected-action packet.

This sidecar preserves the same downstream consumer shape, CentralCoverTargetDecorationKernelData B D, but routes through the literal Route106 lowering. The Route45 selected-section packet is replaced by the two smaller Route28 manuscript atoms tied to the literal quotient C = Y/K and the action on M = K/R:

• TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28LowerActionEquivData;
• TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28RepresentativeActionData.

Manuscript anchors: §7 eq:targettower, where C = Y/K and M = K/R, and §8 exact-image lower maps/central-cover transforms, where the transported C-action on K/R is the target-side input.

Route126 target provider

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

Route126 target quotient-action provider.

This has the same quotient-action consumer shape as the current Route126 target path, but avoids TargetKmodRRoute45BridgeProofs.centralCover_targetRoute45LiteralSelectedActionData by using Route106's literal quotient/action lowering.

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

Route126 target decoration-kernel provider.

This is the requested route-ready drop-in replacement for TargetKmodRRoute53BridgeProofs.centralCover_targetDecorationKernelData_from_route53.

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

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