Route60 target projection/action closers

Route58 split the target Section 8 surface into three packets: the lower target map Y -> C, its kernel, and the projected K/R action law. This sidecar lowers that split to the manuscript same-tower packets:

• B.C is identified with the literal quotient Y/K;
• the lower projection is induced by Y -> Y/K;
• the B.C action on M = K/R is ambient quotient conjugation.

The exported provider reassembles the Route58/Route57 downstream surfaces without using the three Route58 residual axioms.

Route60 coherent projection/action packet

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

Route60 coherent lower projection/action data.

This is the Route58 map, kernel, and action information bundled at the transport-final projection surface so all dependent fields refer to the same selected projection.

• lowerProjectionData : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D
• projectedActionData : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D self.lowerProjectionData

theorem Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.centralCover_targetRoute60ProjectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute60ProjectionActionData B D)

Route60 lower projection/action data from the literal same-tower quotient and ambient action packets.

Route58 surface conversions

def Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.route58LowerTargetMapData_of_route60 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute60ProjectionActionData B D) : TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58LowerTargetMapData B

The Route58 lower target map obtained from a Route60 coherent packet.

Equations

• Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.route58LowerTargetMapData_of_route60 B D H = { lowerTargetMap := H.lowerProjectionData.lowerProjection, lowerTargetMap_surj := ⋯ }

def Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.route58LowerTargetKernelData_of_route60 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute60ProjectionActionData B D) : TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58LowerTargetKernelData B D (route58LowerTargetMapData_of_route60 B D H)

The Route58 kernel packet for the Route60-selected lower target map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.route58ProjectedKmodRActionData_of_route60 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute60ProjectionActionData B D) : TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58ProjectedKmodRActionData B D (route58LowerTargetMapData_of_route60 B D H)

The Route58 projected action packet for the Route60-selected lower target map.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.centralCover_targetRoute58LowerTargetMapData_from_route60 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58LowerTargetMapData B)

Route60 replacement for the Route58 lower-target-map residual.

theorem Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.centralCover_targetRoute58LowerTargetKernelData_from_route60 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute60ProjectionActionData B D) : Nonempty (TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58LowerTargetKernelData B D (route58LowerTargetMapData_of_route60 B D H))

Route60 replacement for the Route58 kernel packet on the Route60-selected lower target map.

theorem Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.centralCover_targetRoute58ProjectedKmodRActionData_from_route60 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute60ProjectionActionData B D) : Nonempty (TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58ProjectedKmodRActionData B D (route58LowerTargetMapData_of_route60 B D H))

Route60 replacement for the Route58 projected action packet on the Route60-selected lower target map.

Route57 and downstream providers

def Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.route57ProjectionActionData_of_route60 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute60ProjectionActionData B D) : TargetKmodRRoute57BridgeProofs.CentralCoverTargetRoute57ProjectionActionData B D

Route60 coherent data reassembled into Route57's projection/action packet.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.centralCover_targetRoute57ProjectionActionData_from_route60 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute57BridgeProofs.CentralCoverTargetRoute57ProjectionActionData B D)

Route60 replacement for the Route57 coherent residual.

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

Route60 quotient-action provider through the coherent lower projection and projected action law.

theorem Q2Presentation.Induction.TargetKmodRRoute60ProjectionActionClosers.centralCover_targetRoute54CanonicalSelectedActionData_from_route60 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData B D)

Route60 Route54 selected-action provider, via the Route57 adapter.

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

Route60 decoration-kernel provider. This has the same downstream shape as the active Route58 provider but its axiom closure uses only the same-tower quotient and ambient-action residuals.

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

Convenience Route60 framed-quotient provider for downstream integration.