Route15 target K/R bridge provider #
This sidecar was recovered from the Default Pro target-K/R request and then
tested locally against the current project. It routes the target decoration
kernel through the smaller same-tower bridge API, rather than through the
transport-final residuals
centralCover_targetLowerProjectionData, andcentralCover_targetKmodRProjectedConjugationActionData.
The remaining leaves are the manuscript-shaped same-tower bridge fields from
TargetKmodRSameTowerBridgeClosers.
theorem
Q2Presentation.Induction.TargetKmodRRoute15BridgeProofs.centralCover_targetKmodRQuotientActionData_from_route15BridgeProofs
{p : FramedPair}
(B : MinimalBlock p)
(D : CentralCoverTargetSubgroupConcreteData B)
:
Target quotient-action packet through the same-tower bridge route.
theorem
Q2Presentation.Induction.TargetKmodRRoute15BridgeProofs.centralCover_targetDecorationKernelData_from_route15BridgeProofs
{p : FramedPair}
(B : MinimalBlock p)
(D : CentralCoverTargetSubgroupConcreteData B)
:
Target decoration-kernel provider assembled from the same-tower target quotient-action packet.
theorem
Q2Presentation.Induction.TargetKmodRRoute15BridgeProofs.centralCover_targetCanonicalFramedQuotientData_from_route15BridgeProofs
{p : FramedPair}
(B : MinimalBlock p)
(D : CentralCoverTargetSubgroupConcreteData B)
:
Convenience framed-quotient provider downstream of the route15 target bridge decoration-kernel provider.