Route24 target K/R close-out sidecar

Route23's target decoration provider still closes through the broad actual same-tower packets

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData.

This owned route24 sidecar keeps routed/root files untouched and avoids both names in its exported provider. It uses the existing transport-final target packets instead:

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

Manuscript anchors:

• §7 eq:targettower gives Y -> B = Y/R -> C = Y/K and M = K/R;
• §8 def:Xgamma uses exact-image lower maps to the lower target C;
• §8 lem:covertransform pulls central covers back through the same lower quotient/decorated target;
• §8 lem:elementarystage and lem:obstructionseparation consume the induced C-action on M = K/R.

Route23-compatible leaf replacements

theorem Q2Presentation.Induction.TargetKmodRRoute24ActualProofs.centralCover_targetRoute22CanonicalLowerActionEquivData_from_route24 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D)

Route24 replacement for route23's route22 lower-action leaf.

This is the first-isomorphism-theorem quotient Y/K ~= B.C, induced by the transport-final lower projection Y -> B.C with kernel K.

theorem Q2Presentation.Induction.TargetKmodRRoute24ActualProofs.centralCover_targetRoute22CanonicalRepresentativeActionData_from_route24 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRCanonicalRepresentativeActionData B D (TargetKmodRRoute22ActualProofs.canonicalLowerProjectionData_of_route22LowerActionEquiv B D E))

Route24 replacement for route23's route22 canonical representative-action leaf.

The representative law is obtained by choosing representatives through the canonical route22 projection and restricting the projected conjugation action to those representatives.

theorem Q2Presentation.Induction.TargetKmodRRoute24ActualProofs.centralCover_targetRoute21LowerProjectionBridgeData_from_route24 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21LowerProjectionBridgeData B D)

Route21 lower projection bridge rebuilt from the route24 lower equivalence.

theorem Q2Presentation.Induction.TargetKmodRRoute24ActualProofs.centralCover_targetRoute21RepresentativeActionData_from_route24 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21RepresentativeActionData B D (TargetKmodRRoute22ActualProofs.route21LowerProjectionBridgeData_of_route22LowerActionEquiv B D E))

Route21 representative action rebuilt from the route24 canonical representative action.

Direct route24 provider

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

Direct target K/R quotient-action provider through the transport-final projection/action packets.

This is the route24 replacement for route23's target provider; it avoids the two TargetKmodRSameTowerActualClosers packet names in the current route23 closure.

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

Decoration-kernel provider downstream of the route24 target bridge.