Route67 target K/R projection/action closers

Route66's target hook routes through Route63, whose only remaining target atom is Route48's coherent representative-action packet:

• TargetKmodRRoute48BridgeProofs.centralCover_targetRoute48ProjectionActionData.

This sidecar lowers that atom to the manuscript projection/action split already isolated in Route58:

• the concrete lower map Y -> C;
• the kernel identification ker(Y -> C) = K;
• the projected action law on K/R for that same lower map.

The split data is packaged dependently before reassembling the Route48, Route63, quotient-action, and decoration-kernel provider surfaces.

Route67 split packet

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

Route67 dependent split of the target projection/action packet.

The kernel and projected-action fields are tied to the same selected lower map, so the downstream projection/action packet cannot be assembled from mismatched target data.

• lowerMapData : TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58LowerTargetMapData B
• lowerKernelData : TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58LowerTargetKernelData B D self.lowerMapData
• projectedActionData : TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58ProjectedKmodRActionData B D self.lowerMapData

theorem Q2Presentation.Induction.TargetKmodRRoute67ProjectionActionClosers.centralCover_targetRoute67ProjectionActionSplitData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute67ProjectionActionSplitData B D)

Route67 split provider. This is a lowering of the Route48 atom to the Route58 manuscript map/kernel/action packets.

Transport-final projection/action surfaces

def Q2Presentation.Induction.TargetKmodRRoute67ProjectionActionClosers.lowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute67ProjectionActionSplitData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Transport-final lower projection extracted from the Route67 split.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute67ProjectionActionClosers.projectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute67ProjectionActionSplitData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData B D H)

Transport-final projected conjugation action extracted from Route67.

Equations

• ⋯ = ⋯

Route48 and Route63-compatible adapters

def Q2Presentation.Induction.TargetKmodRRoute67ProjectionActionClosers.route48ProjectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute67ProjectionActionSplitData B D) : TargetKmodRRoute48BridgeProofs.CentralCoverTargetRoute48ProjectionActionData B D

Reassemble Route48's representative-action packet from the Route67 split by choosing representatives from the selected lower map.

Equations

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

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

Route67 replacement for the Route48 residual.

def Q2Presentation.Induction.TargetKmodRRoute67ProjectionActionClosers.route63SameTowerData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute67ProjectionActionSplitData B D) : TargetKmodRRoute63SameTowerClosers.CentralCoverTargetRoute63SameTowerData B D

Route63 same-tower packet reassembled from Route67 data.

Equations

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

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

Route67 replacement for Route63's same-tower provider.

def Q2Presentation.Induction.TargetKmodRRoute67ProjectionActionClosers.route63ProjectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute67ProjectionActionSplitData B D) : TargetKmodRRoute63SameTowerClosers.CentralCoverTargetRoute63ProjectionActionData B D

Route63 projection/action packet reassembled directly from Route67 data.

Equations

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

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

Route67 replacement for Route63's projection/action provider.

Downstream providers

def Q2Presentation.Induction.TargetKmodRRoute67ProjectionActionClosers.quotientActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute67ProjectionActionSplitData B D) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Route67 quotient-action data through the split lower projection and action law.

Equations

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

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

Route67 quotient-action provider with Route48 removed from the axiom closure.

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

Route67 decoration-kernel provider, matching the Route66 target call-site shape while replacing the Route48 atom by the Route58 split.

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

Convenience Route67 framed-quotient provider for downstream integration.