Route169 target K/R closers

Route168's target frontier still contains the four projection-semantic atoms from TargetKmodRProjectionSemanticClosers:

• centralCover_targetLowerQuotientMapData;
• centralCover_targetLowerActionEquivData;
• centralCover_targetKmodRRepresentativeActionData;
• centralCover_targetKmodRConjugationClassIndependenceData.

This sidecar exposes a Route169 drop-in replacement for TargetKmodRRoute167Closers.centralCover_targetDecorationKernelData_from_route152Closers_route167. It takes the older direct same-tower provider from TargetKmodRProjectionRoute10Proofs, whose axiom closure bypasses those four atoms and lowers the target side to the narrower manuscript tower facts:

• the literal lower quotient Y/K is the abstract action group B.C;
• the ambient B.C action on K/R is conjugation on representatives.

Same-coset independence is theorem-level from the realized K/R ~= M bridge, so it no longer appears as a residual atom in the final Route169 closure.

theorem Q2Presentation.Induction.TargetKmodRRoute169Closers.centralCover_targetLowerProjectionData_from_route169Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D)

Route169 lower projection through the canonical same-tower quotient.

This provider avoids the Route168 lower quotient-map and lower action-equivalence atoms.

theorem Q2Presentation.Induction.TargetKmodRRoute169Closers.centralCover_targetKmodRProjectedConjugationActionData_from_route169Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty ((P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) ×' TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Route169 projected conjugation action through canonical same-tower data.

This provider avoids the Route168 representative-action and class-independence atoms.

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

Route169 quotient-action provider with the four Route168 target atoms strictly removed from the closure.

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

Route169 drop-in target decoration-kernel provider.

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

Name mirroring the Route167 call site for a one-line replacement.

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

Convenience framed-quotient provider through Route169.