Route122 target closers #

Route122 currently calls the Route46 target hook, whose closure exposes the two broad actual same-tower target leaves:

TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData.

This sidecar keeps the same consumer shape as the Route46 decoration-kernel provider but routes through Route52's coherent literal quotient/action packet. The remaining target residual is a single manuscript-shaped packet tying the literal quotient Y/K ~= B.C to the fixed representative action law on K/R.

source

theorem Q2Presentation.Induction.TargetKmodRRoute122Closers.centralCover_targetKmodRQuotientActionData_from_route122Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

Route122 closer quotient-action provider.

This has the same downstream quotient-action surface as Route46 but avoids the two broad actual same-tower leaves by using Route52's coherent literal Y/K action packet.

source

theorem Q2Presentation.Induction.TargetKmodRRoute122Closers.centralCover_targetDecorationKernelData_from_route122Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetDecorationKernelData B D)

Route122 closer decoration-kernel provider, drop-in compatible with TargetKmodRRoute46BridgeProofs.centralCover_targetDecorationKernelData_from_route46.

source

theorem Q2Presentation.Induction.TargetKmodRRoute122Closers.centralCover_targetCanonicalFramedQuotientData_from_route122Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

Convenience framed-quotient provider downstream of the Route122 closer.