Theorem-level bridge packets for the target same-tower K/R route

This is the first route4 -> route5 step from the four-turn Pro plan. The route4 theorem currently depends on the two bridge residuals in TargetKmodRSameTowerBridgeClosers. This file supplies replacement theorem names for those bridge packets, built from the older literal lower-quotient and ambient-action same-tower packets.

The immediate route5 acceptance check is that the replacement quotient-action provider below does not depend on the two bridge residual names.

theorem Q2Presentation.Induction.TargetKmodRSameTowerBridgeProofs.centralCover_targetLowerProjectionBridgeData_proven {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D)

The bridge lower projection is induced by the literal quotient equivalence Y/K ~= B.C.

theorem Q2Presentation.Induction.TargetKmodRSameTowerBridgeProofs.centralCover_targetKmodRRepresentativeActionBridgeData_proven {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D P)

A bridge representative action follows by choosing representatives through the supplied lower projection and restricting the all-ambient action law to those representatives.

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

Route5 target quotient-action provider with the bridge residual names replaced by the theorem-level bridge proofs above.

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

Decoration-kernel provider through the theorem-level bridge proofs.

This is the target-side input needed by the integrated central-cover realization route. Compared with route4, this theorem avoids the two bridge residual names; its remaining target assumptions are the older literal same-tower actual quotient/action packets exposed by the P1 replacement.