Route50 target K/R projection-action bridge

Route48 leaves one coherent target packet:

• TargetKmodRRoute48BridgeProofs.centralCover_targetRoute48ProjectionActionData.

This sidecar removes that broad packet from the exported Route50 providers. The Route48 structure is rebuilt from the more literal Route37 packets:

• an equivalence between the manuscript lower quotient Y/K and the abstract action group B.C;
• the representative action law for theorem-level representatives of literal Y/K classes.

The lower projection Y -> B.C, its kernel, representatives, and same-coset transport on K/R are theorem-level from quotient algebra plus the closed inner-conjugation theorem.

Literal lower projection from Route37 data

def Q2Presentation.Induction.TargetKmodRRoute50BridgeProofs.lowerProjectionData_of_route37LowerAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LowerActionEquivData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Route50 lower projection Y -> B.C, induced by the literal quotient identification Y/K ~= B.C.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute50BridgeProofs.representativeActionBridgeData_of_route37Literal {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LowerActionEquivData B D) (A : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LiteralRepresentativeActionData B D E) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (lowerProjectionData_of_route37LowerAction B D E)

Route37 literal representative action data as the bridge packet over the Route50 lower projection.

Equations

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

Route48 packet rebuilt from Route37 leaves

def Q2Presentation.Induction.TargetKmodRRoute50BridgeProofs.route48ProjectionActionData_of_route37 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LowerActionEquivData B D) (A : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LiteralRepresentativeActionData B D E) : TargetKmodRRoute48BridgeProofs.CentralCoverTargetRoute48ProjectionActionData B D

Rebuild the Route48 coherent projection/action packet from the smaller literal Route37 quotient and representative-action packets.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute50BridgeProofs.centralCover_targetRoute48ProjectionActionData_from_route50 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute48BridgeProofs.CentralCoverTargetRoute48ProjectionActionData B D)

Route50 replacement for the Route48 residual. Its non-standard target closure is exactly the Route37 literal lower quotient/action pair.

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

Route50 quotient-action provider with the Route48 residual eliminated.

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

Route50 decoration-kernel provider, drop-in compatible with Route48's integration-side target hook but without the Route48 residual in its closure.

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

Convenience Route50 framed-quotient provider for downstream integration.