Route99 target K/R projection/action lowering

Route98's target provider routes through Route63 and leaves one coherent Route48 projection/action atom:

• TargetKmodRRoute48BridgeProofs.centralCover_targetRoute48ProjectionActionData.

This sidecar lowers that single coherent atom to the two transport-final manuscript packets already isolated in TargetKmodRActionTransportFinalProofs:

• centralCover_targetLowerProjectionData, a concrete projection Y -> B.C whose kernel is the selected subgroup K;
• centralCover_targetKmodRProjectedConjugationActionData, the assertion that the projected B.C-action on M = K/R is quotient conjugation on the literal quotient K/R.

The Route48, Route63, quotient-action, decoration-kernel, and framed-quotient surfaces are then reassembled theorem-level from the same selected projection.

Route48 lowering to transport-final packets

def Q2Presentation.Induction.TargetKmodRRoute99ProjectionActionClosers.route48ProjectionActionData_of_transportFinal {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P) : TargetKmodRRoute48BridgeProofs.CentralCoverTargetRoute48ProjectionActionData B D

Reassemble Route48's coherent projection/action packet from the two transport-final packets.

The representative used by Route48 is Classical.choose from the selected projection's surjectivity proof. Since the transport-final action packet is an all-representatives statement, it applies directly to that theorem-level choice.

Equations

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

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

Route99 replacement for the Route48 residual.

Axiom frontier effect: this theorem replaces TargetKmodRRoute48BridgeProofs.centralCover_targetRoute48ProjectionActionData by the two transport-final packets centralCover_targetLowerProjectionData and centralCover_targetKmodRProjectedConjugationActionData.

Route63-compatible surfaces

def Q2Presentation.Induction.TargetKmodRRoute99ProjectionActionClosers.route63SameTowerData_of_transportFinal {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P) : TargetKmodRRoute63SameTowerClosers.CentralCoverTargetRoute63SameTowerData B D

Route63 same-tower packet reassembled from the Route99 transport-final split.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute99ProjectionActionClosers.centralCover_targetRoute63SameTowerData_from_route99 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute63SameTowerClosers.CentralCoverTargetRoute63SameTowerData B D)

Route99 replacement for Route63's same-tower provider, with Route48 removed from the target closure.

def Q2Presentation.Induction.TargetKmodRRoute99ProjectionActionClosers.route63ProjectionActionData_of_transportFinal {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P) : TargetKmodRRoute63SameTowerClosers.CentralCoverTargetRoute63ProjectionActionData B D

Route63 projection/action packet reassembled directly from the Route99 transport-final split.

Equations

• Q2Presentation.Induction.TargetKmodRRoute99ProjectionActionClosers.route63ProjectionActionData_of_transportFinal B D P A = { lowerProjectionData := P, projectedActionData := A }

theorem Q2Presentation.Induction.TargetKmodRRoute99ProjectionActionClosers.centralCover_targetRoute63ProjectionActionData_from_route99 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute63SameTowerClosers.CentralCoverTargetRoute63ProjectionActionData B D)

Route99 replacement for Route63's projection/action provider.

Downstream drop-in providers

def Q2Presentation.Induction.TargetKmodRRoute99ProjectionActionClosers.quotientActionData_of_route99 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Route99 quotient-action data through the selected transport-final lower projection and projected action law.

Equations

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

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

Route99 quotient-action provider with the Route48 atom replaced by the two transport-final manuscript packets.

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

Route99 decoration-kernel provider, drop-in compatible with the Route98 integration call-site but with the target frontier lowered from Route48 to the transport-final projection/action split.

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

Convenience Route99 framed-quotient provider for downstream integrations.