Route54 target K/R canonical selected-action bridge

Route53 still exposes the Route45 target residual

• TargetKmodRRoute45BridgeProofs.centralCover_targetRoute45LiteralSelectedActionData.

This sidecar narrows that residual to one canonical selected-tower packet. The Route54 packet is tied directly to the manuscript tower Y -> C = Y/K and M = K/R: it supplies a concrete lower projection Y -> B.C with kernel K, selected representatives for that projection, and the action law for those same representatives. The literal Route45 Y/K-indexed selected-section packet is then recovered theorem-level from the projection-induced quotient equivalence.

Route54 canonical selected-action packet

structure Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type

Route54 canonical selected-action data.

This is narrower than Route45's literal selected-section packet in the sense used by the current route: the quotient identification is not an independent field over an auxiliary lower child. It is induced by the concrete lower projection whose kernel is the selected subgroup K, and the selected action law is stated for representatives of that same projection.

• canonicalLowerProjection : p.fst.Y →* B.C
• canonicalLowerProjection_surj : Function.Surjective ⇑self.canonicalLowerProjection
• canonicalLowerProjection_ker : D.Ksub = self.canonicalLowerProjection.ker
• sectionRepresentative : B.C → p.fst.Y
• sectionRepresentative_spec (c : B.C) : self.canonicalLowerProjection (self.sectionRepresentative c) = c
• selected_action_realizes_conjugation (c : B.C) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM c) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (self.sectionRepresentative c) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

def Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData.lowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute54CanonicalSelectedActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The transport-final lower projection selected by Route54 data.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData.lowerActionEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute54CanonicalSelectedActionData B D) : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y ≃* B.C

The Y/K ~= B.C equivalence induced by the Route54 lower projection.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData.representativeActionBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute54CanonicalSelectedActionData B D) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (lowerProjectionData B D A)

Route54 representative data in the same-tower bridge surface.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData.projectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute54CanonicalSelectedActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData B D A)

Route54 projected conjugation action.

The only theorem-level repair needed after the selected representatives is the already closed same-coset/inner-conjugation theorem on K/R.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData.quotientActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute54CanonicalSelectedActionData B D) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Direct quotient-action data selected by Route54.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData.route45LiteralSelectedActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute54CanonicalSelectedActionData B D) : TargetKmodRRoute45BridgeProofs.CentralCoverTargetRoute45LiteralSelectedActionData B D

Route45's literal selected-section packet, induced by the canonical Route54 projection/section/action data.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData.route52CoherentLiteralActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute54CanonicalSelectedActionData B D) : TargetKmodRRoute52BridgeProofs.CentralCoverTargetRoute52CoherentLiteralActionData B D

Route52's coherent literal packet induced from Route54 through the Route53 Route45-to-Route52 adapter.

Equations

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

Route54 residual and route-compatible providers

def Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.route54CanonicalSelectedActionData_of_bridgePackets {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Pbridge : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D) (Abridge : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D Pbridge)) : CentralCoverTargetRoute54CanonicalSelectedActionData B D

Build the Route54 canonical selected-action packet from the two smaller same-tower bridge packets: the concrete lower projection and the representative-level K/R action law for that projection.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.centralCover_targetRoute54CanonicalSelectedActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute54CanonicalSelectedActionData B D)

Route54 target packet, reduced to the two smaller same-tower bridge residuals.

This removes the broad Route54 axiom from the final closure. The remaining target-side non-local content is exactly:

• TargetKmodRSameTowerBridgeClosers.centralCover_targetLowerProjectionBridgeData;
• TargetKmodRSameTowerBridgeClosers.centralCover_targetKmodRRepresentativeActionBridgeData.

theorem Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.centralCover_targetRoute45LiteralSelectedActionData_from_route54 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute45BridgeProofs.CentralCoverTargetRoute45LiteralSelectedActionData B D)

Route54 replacement for Route45's selected-action residual.

theorem Q2Presentation.Induction.TargetKmodRRoute54BridgeProofs.centralCover_targetRoute52CoherentLiteralActionData_from_route54 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute52BridgeProofs.CentralCoverTargetRoute52CoherentLiteralActionData B D)

Route54 replacement for Route52's coherent literal action packet.

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

Route54 direct quotient-action provider.

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

Route54 decoration-kernel provider, drop-in compatible with Route53's target hook.

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

Convenience Route54 framed-quotient provider for downstream integration.