Route12 refinement of the actual same-tower target K/R pair

Route12's current target decoration-kernel provider still prints the two actual same-tower residuals

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData.

This sidecar refines that pair to the narrower transport-final packets:

• centralCover_targetLowerProjectionData, a concrete projection Y -> B.C with kernel K;
• centralCover_targetKmodRProjectedConjugationActionData, the projected conjugation action on the literal quotient K/R.

The bridges below are theorem-level quotient/action bookkeeping. The final provider is route-ready for the target-decoration kernel slot used by IntegratedCurrentRouteProofs12.

Bridges from the actual same-tower pair to transport-final data

theorem Q2Presentation.Induction.TargetKmodRSameTowerActualRoute12Proofs.centralCover_targetCanonicalLowerQuotientEquivData_from_route12ProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D)

Replacement for the actual lower-quotient equivalence residual, induced by a concrete lower projection Y -> B.C with kernel K.

theorem Q2Presentation.Induction.TargetKmodRSameTowerActualRoute12Proofs.centralCover_targetKmodRAmbientActionData_from_route12ProjectedActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D P)

Replacement for the actual all-ambient action residual, induced by the projected conjugation-action packet for the selected lower projection.

Route-ready target decoration-kernel provider

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

Route12 quotient-action provider avoiding the two actual same-tower residual names by routing directly through transport-final projection/action data.

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

Drop-in target decoration-kernel provider for IntegratedCurrentRouteProofs12, with the same return type as TargetKmodRProjectionRoute10Proofs.centralCover_targetDecorationKernelData_from_projectionRoute10Proofs but without the two actual same-tower residual names.

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

Convenience framed-quotient provider downstream of the route12 decoration kernel.