Route101 target K/R projection/action semantic lowering

Route100's target provider uses Route99, whose axiom frontier is the two transport-final packets

• centralCover_targetLowerProjectionData;
• centralCover_targetKmodRProjectedConjugationActionData.

This sidecar is a drop-in Route101 provider which routes the decoration-kernel closure through TargetKmodRProjectionSemanticClosers. The target frontier is therefore lowered to the four smaller manuscript-shaped semantic packets:

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

No Route48 or Route99 coherent projection/action atom is used by the providers below.

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

Route101 lower-projection provider, assembled from the lower quotient map Y -> Y/K and the identification of the lower child with the abstract action group B.C.

theorem Q2Presentation.Induction.TargetKmodRRoute101ProjectionSemanticClosers.centralCover_targetKmodRProjectedConjugationActionData_from_route101 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Route101 projected-conjugation provider, assembled from representative-level action compatibility and class-independence of conjugation on K/R.

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

Route101 quotient-action packet through the semantic projection/action split.

theorem Q2Presentation.Induction.TargetKmodRRoute101ProjectionSemanticClosers.centralCover_targetKmodRActionCompatibilityData_from_route101 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationCanonicalInvarianceProofs.CentralCoverTargetKmodRActionCompatibilityData B D)

Route101 action-compatibility packet through the semantic projection/action split.

theorem Q2Presentation.Induction.TargetKmodRRoute101ProjectionSemanticClosers.centralCover_targetDecorationCanonicalInvarianceData_from_route101 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationActualDescentProofs.CentralCoverTargetDecorationCanonicalInvarianceData B D)

Route101 canonical-invariance provider through the semantic projection/action split.

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

Route101 decoration-kernel provider, drop-in compatible with the Route100 integration call-site, but with the target frontier lowered below the two transport-final Route100 packets.

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

Convenience Route101 framed-quotient provider for downstream integrations.