Route36 target K/R bridge sidecar

Route35's decoration-kernel provider still depends on the two actual same-tower target packets:

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData.

This sidecar keeps the same downstream conclusion as route35 but routes through TargetKmodRSameTowerBridgeClosers. The residual target frontier is therefore the stricter bridge surface:

• a concrete projection Y -> B.C with kernel K;
• one representative of each lower class whose action realizes conjugation on K/R.

The promotion from one representative to all ambient representatives uses the already closed inner-conjugation theorem for K/R.

Route36 quotient-action bridge

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

Route36 quotient-action provider.

Compared with route35, this avoids both actual same-tower residual names and uses the stricter bridge-closer residuals instead.

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

Route36 decoration-kernel provider, with the same downstream shape as TargetKmodRRoute35BridgeProofs.centralCover_targetDecorationKernelData_from_route35.

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

Convenience route36 framed-quotient provider for downstream integration.