Route29 target K/R bridge sidecar

Route28 refines the target bridge into three sidecar leaves:

• a framed lower quotient map Y -> C = Y/K;
• an identification of that lower child with the abstract action group B.C;
• selected-representative compatibility for the B.C-action on K/R.

This sidecar keeps the same downstream provider shape, but bypasses the route27 and route28 residual names. It routes through the selected canonical-section bridge from route26, whose residual frontier is:

• the literal same-tower quotient identification Y/K ~= B.C;
• the action law for the selected canonical section.

Inner conjugation on K/R is theorem-level from the realized K/R ~= M bridge, so this provider does not retain route28's class-independence or representative-generalization leaves.

Route29 same-tower provider

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

Route29 quotient-action provider.

The proof does not call route27 or route28 target residuals. Its remaining axioms are the route26 selected canonical-section action packet and the literal same-tower quotient identification.

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

Route29 replacement provider with the same downstream conclusion as route28.

This is the theorem intended for a later route integration attempt.

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

Convenience route29 framed-quotient provider for downstream integration.