Route23 actual bridge for the target K/R tower

Route22 left two target-side leaves:

• TargetKmodRRoute22ActualProofs.centralCover_targetRoute22CanonicalLowerActionEquivData;
• TargetKmodRRoute22ActualProofs.centralCover_targetRoute22CanonicalRepresentativeActionData.

This sidecar closes those leaves from the finer same-tower lower/semantic APIs. It does not change route22 or the integrated route; the supervisor can import this file and wire the theorem names below in place of the route22 residuals.

Route22 leaf replacements

theorem Q2Presentation.Induction.TargetKmodRRoute23ActualProofs.centralCover_targetRoute22CanonicalLowerActionEquivData_from_route23 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D)

Route23 closes route22's canonical lower-action equivalence leaf from the same-tower lower closer.

theorem Q2Presentation.Induction.TargetKmodRRoute23ActualProofs.centralCover_targetRoute22CanonicalRepresentativeActionData_from_route23 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRCanonicalRepresentativeActionData B D (TargetKmodRRoute22ActualProofs.canonicalLowerProjectionData_of_route22LowerActionEquiv B D E))

Route23 closes route22's canonical representative-action leaf for the projection induced by a supplied canonical lower-action equivalence.

Downstream route21 and decoration providers

theorem Q2Presentation.Induction.TargetKmodRRoute23ActualProofs.centralCover_targetRoute21LowerProjectionBridgeData_from_route23 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21LowerProjectionBridgeData B D)

Route21 lower projection bridge rebuilt from the route23 lower equivalence.

theorem Q2Presentation.Induction.TargetKmodRRoute23ActualProofs.centralCover_targetRoute21RepresentativeActionData_from_route23 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21RepresentativeActionData B D (TargetKmodRRoute22ActualProofs.route21LowerProjectionBridgeData_of_route22LowerActionEquiv B D E))

Route21 representative action rebuilt from the route23 canonical representative action.

theorem Q2Presentation.Induction.TargetKmodRRoute23ActualProofs.centralCover_targetRoute21ActualBridgeData_from_route23 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21ActualBridgeData B D)

Route21 bridge provenance with both route22 target leaves replaced by route23 theorem-level witnesses.

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

Direct target K/R quotient-action provider using the route23 witnesses.

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

Decoration-kernel provider downstream of the route23 target bridge.