Route18 target projection-semantic sidecar

Route17 exposed three target K/R projection-semantic leaves:

• centralCover_targetLowerQuotientMapData;
• centralCover_targetLowerActionEquivData;
• centralCover_targetKmodRRepresentativeActionData.

This sidecar gives a route18 target hook whose primary path avoids those route17 leaves. It uses the more concrete same-tower provenance:

• the literal lower quotient Y/K is equivalent to the abstract action group B.C;
• the B.C action on M = K/R is realized by ambient conjugation on the literal quotient K/R.

After the route18 decoration-kernel theorem is available, the old lower-child quotient-map shape is recovered as theorem-level framed-quotient bookkeeping.

Concrete same-tower route18 provenance

structure Q2Presentation.Induction.TargetKmodRRoute18ProjectionProofs.CentralCoverTargetRoute18ProjectionProvenanceData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type

The route18 target projection provenance: the abstract action group B.C is the literal lower quotient Y/K, and the resulting action on M = K/R is ambient conjugation on the literal quotient K/R.

• lowerQuotientEquivData : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D
• ambientActionData : TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D (TargetKmodRSameTowerActualClosers.lowerProjectionData_of_lowerQuotientEquiv B D self.lowerQuotientEquivData)

def Q2Presentation.Induction.TargetKmodRRoute18ProjectionProofs.lowerProjectionData_of_route18ProjectionProvenance {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute18ProjectionProvenanceData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The concrete lower projection Y -> B.C carried by route18 provenance.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.TargetKmodRRoute18ProjectionProofs.projectedConjugationActionData_of_route18ProjectionProvenance {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute18ProjectionProvenanceData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route18ProjectionProvenance B D P)

The projected conjugation-action packet carried by route18 provenance.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute18ProjectionProofs.quotientActionData_of_route18ProjectionProvenance {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute18ProjectionProvenanceData B D) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Route18 quotient-action data from concrete same-tower provenance.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Induction.TargetKmodRRoute18ProjectionProofs.centralCover_targetRoute18ProjectionProvenanceData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute18ProjectionProvenanceData B D)

Route18 provenance assembled from the two concrete same-tower residuals.

Route-ready target hook

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

Route18 provider for the target K/R quotient-action packet.

The axiom closure contains the concrete same-tower quotient/action provenance, not the route17 projection-semantic leaves.

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

Decoration-kernel provider through route18 target K/R quotient action.

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

Convenience framed-quotient provider downstream of route18.

Route17 residual surfaces recovered from route18

theorem Q2Presentation.Induction.TargetKmodRRoute18ProjectionProofs.centralCover_targetLowerQuotientMapData_from_route18 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D)

Route18 recovery of the old lower quotient-map packet.

This theorem is deliberately downstream of centralCover_targetDecorationKernelData_from_route18: the framed lower child Y/K is a quotient target only after the decoration is known to kill K.

theorem Q2Presentation.Induction.TargetKmodRRoute18ProjectionProofs.centralCover_targetLowerActionEquivData_from_route18 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerActionEquivData B D Q)

Route18 recovery of the lower action equivalence for any selected lower-child quotient map.

def Q2Presentation.Induction.TargetKmodRRoute18ProjectionProofs.representativeActionData_of_ambientAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D P) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D P

Convert the all-ambient action law into the route17 representative-action packet for an arbitrary selected lower projection.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Induction.TargetKmodRRoute18ProjectionProofs.centralCover_targetKmodRRepresentativeActionData_from_route18 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D P)

Route18 recovery of the old representative-action packet from the narrower all-ambient conjugation action law.