Route26 target K/R bridge sidecar

Route25's target decoration-kernel provider routes through the two bridge packets in TargetKmodRSameTowerBridgeClosers:

• centralCover_targetLowerProjectionBridgeData;
• centralCover_targetKmodRRepresentativeActionBridgeData.

This sidecar keeps the same downstream provider shape as route25, but avoids both route25 bridge residual names. The lower bridge is rebuilt from the literal same-tower quotient Y/K ~= B.C. The representative bridge is split into a theorem-level selected section of the canonical lower projection and a single narrower packet asserting that this selected section realizes the B.C-action on K/R.

Route26 selected-section packet

structure Q2Presentation.Induction.TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26CanonicalRepresentativeSectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) : Type

A selected section of the canonical lower projection Y -> B.C.

This packet is theorem-level from surjectivity of the canonical projection; the new route26 semantic content is separated into CentralCoverTargetRoute26RepresentativeSectionActionData below.

• quotientRepresentative : B.C → p.fst.Y
• canonicalLowerProjection_quotientRepresentative (c : B.C) : P.canonicalLowerProjection (self.quotientRepresentative c) = c

structure Q2Presentation.Induction.TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26RepresentativeSectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) (S : CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D P) : Prop

Route26 action packet for the selected canonical section.

Compared with route25's representative bridge, this no longer includes the existence of representatives and it is only stated for the canonical lower projection coming from the same-tower quotient.

• representative_section_action_realizes_conjugation (c : B.C) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM c) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (S.quotientRepresentative c) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

theorem Q2Presentation.Induction.TargetKmodRRoute26BridgeProofs.centralCover_targetRoute26CanonicalRepresentativeSectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) : Nonempty (CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D P)

The selected section exists by choice from the canonical lower projection's surjectivity.

axiom Q2Presentation.Induction.TargetKmodRRoute26BridgeProofs.centralCover_targetRoute26RepresentativeSectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) (S : CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D P) : Nonempty (CentralCoverTargetRoute26RepresentativeSectionActionData B D P S)

Route26 residual: the selected canonical representatives realize the abstract action on the literal quotient K/R.

This replaces route25's broader centralCover_targetKmodRRepresentativeActionBridgeData residual by a strictly smaller manuscript-shaped packet: the representative section itself is already constructed, and the lower projection is fixed to the canonical same-tower projection.

Conversions to existing target interfaces

def Q2Presentation.Induction.TargetKmodRRoute26BridgeProofs.lowerProjectionBridgeData_of_canonicalProjection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D

Rebuild the route25 lower bridge from the canonical lower projection.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute26BridgeProofs.canonicalRepresentativeActionData_of_route26Section {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) (S : CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D P) (A : CentralCoverTargetRoute26RepresentativeSectionActionData B D P S) : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRCanonicalRepresentativeActionData B D P

Convert the route26 selected-section action packet to the canonical representative-action packet used by the same-tower semantic closer.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute26BridgeProofs.representativeActionBridgeData_of_route26Section {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) (S : CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D P) (A : CentralCoverTargetRoute26RepresentativeSectionActionData B D P S) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerSemanticClosers.lowerProjectionData_of_canonicalProjection B D P)

Convert the route26 selected-section action packet to route25's representative bridge, specialized to the canonical lower projection.

Equations

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

Route25 bridge residual replacements

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

Route26 replacement for route25's lower-projection bridge residual.

The remaining lower-side axiom is the existing literal same-tower quotient identification Y/K ~= B.C, exposed by centralCover_targetCanonicalLowerProjectionData.

theorem Q2Presentation.Induction.TargetKmodRRoute26BridgeProofs.centralCover_targetKmodRRepresentativeActionBridgeData_from_route26 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) : Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerSemanticClosers.lowerProjectionData_of_canonicalProjection B D P))

Route26 replacement for route25's representative-action bridge residual, for the canonical lower projection.

Route25-compatible provider

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

Route26 quotient-action provider.

Its axiom closure removes both route25 bridge residual names and replaces them with the literal lower quotient packet plus the selected-section route26 action packet.

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

Route25-compatible decoration-kernel provider downstream of the route26 target bridge.

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

Convenience route26 framed-quotient provider for downstream integration.