Route-ready replacements for actual same-tower target K/R packets

This sidecar targets the two current route8 target same-tower residuals:

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData.

The current API does not expose enough data in CentralCoverTargetSubgroupConcreteData to prove these packets outright for an arbitrary B,D: the packet gives R <= K and K/R ~= M, but it does not identify the abstract lower action group B.C with the literal quotient Y/K, nor does it state that B.actM is the conjugation action.

The replacements below therefore refine the two actual residuals through the already available projection-semantic split:

• lower quotient map Y -> Y/K plus lower-action equivalence to B.C;
• representative-level action plus class-independence of conjugation on K/R.

These are strictly smaller manuscript-shaped obligations than the two actual packets: the quotient construction and the action law are separated, and the all-ambient action law is rebuilt from representative compatibility plus same-class independence.

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

Replacement for the actual lower-quotient equivalence residual, assembled from the lower projection supplied by the projection-semantic split.

theorem Q2Presentation.Induction.TargetKmodRSameTowerActualProofs.centralCover_targetKmodRAmbientActionData_from_projectionSemanticClosers {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, assembled from the projected conjugation-action packet of the projection-semantic split.

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

Route-ready quotient-action provider using the two replacement theorems above instead of the two actual same-tower residual names.