Route45 target K/R literal lower-action bridge

Route44 leaves two target-side packets:

• a literal lower action equivalence from Route34's child Y/K to B.C;
• the action law for Route44's theorem-level selected representatives.

This sidecar replaces those two names by one coherent literal-tower packet. It supplies the Y/K ~= B.C identification together with a selected section of the literal lower child whose representatives realize the B.C action on K/R. Route44's fixed theorem-level representative section is recovered by same-coset independence, using the already closed inner-conjugation theorem for K/R.

Manuscript anchors:

• §7, eq:targettower: Y -> B = Y/R -> C = Y/K and M = K/R;
• §8 exact-image lower maps and central-cover transforms: representative choices in the lower quotient are immaterial because changing representatives inside a Y/K coset acts trivially on K/R.

Route45 coherent literal lower-action packet

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

Route45 literal selected-action data.

The lower child is exactly Route34's framed child with carrier Y/K. The packet keeps the quotient identification and the selected-section action law together, so the action law cannot be paired with an unrelated lower equivalence.

• lowerActionEquiv : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y ≃* B.C
• sectionRepresentative : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y → p.fst.Y
• sectionRepresentative_spec (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) : (TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 B D).topToLower (self.sectionRepresentative q) = q
• selected_representative_action_realizes_conjugation (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (self.lowerActionEquiv q)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (self.sectionRepresentative q) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

def Q2Presentation.Induction.TargetKmodRRoute45BridgeProofs.route44LiteralLowerActionData_of_route45 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A45 : CentralCoverTargetRoute45LiteralSelectedActionData B D) : TargetKmodRRoute44BridgeProofs.CentralCoverTargetRoute44LiteralLowerActionData B D

Route45 data gives Route44's literal lower-action packet.

Equations

• Q2Presentation.Induction.TargetKmodRRoute45BridgeProofs.route44LiteralLowerActionData_of_route45 B D A45 = { literalLowerActionEquiv := A45.lowerActionEquiv }

def Q2Presentation.Induction.TargetKmodRRoute45BridgeProofs.route45LowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A45 : CentralCoverTargetRoute45LiteralSelectedActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The Route44 lower projection induced by Route45 data.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute45BridgeProofs.route45RepresentativeSectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A45 : CentralCoverTargetRoute45LiteralSelectedActionData B D) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeSectionData B D (route45LowerProjectionData B D A45)

The Route44 theorem-level representative section induced by Route45 data.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute45BridgeProofs.route44RepresentativeActionData_of_route45 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A45 : CentralCoverTargetRoute45LiteralSelectedActionData B D) : TargetKmodRRoute44BridgeProofs.CentralCoverTargetRoute44RepresentativeActionData B D (route44LiteralLowerActionData_of_route45 B D A45)

Route45 selected representatives imply Route44's theorem-level representative action law.

The proof compares the Route45 selected representative of the literal class A45.lowerActionEquiv.symm c with Route44's theorem-level representative of c. Both map to the same class in Y/K; the closed K/R inner-conjugation bridge then makes their quotient-conjugation actions equal.

Equations

• ⋯ = ⋯

Route44 packet replacements

axiom Q2Presentation.Induction.TargetKmodRRoute45BridgeProofs.centralCover_targetRoute45LiteralSelectedActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute45LiteralSelectedActionData B D)

Route45 residual: coherent literal Y/K selected-action semantics.

This single packet replaces both Route44 target leaves: it identifies the literal lower child with B.C and states the action law for a selected literal section. Route44's fixed theorem-level section is recovered above.

theorem Q2Presentation.Induction.TargetKmodRRoute45BridgeProofs.centralCover_targetRoute44LiteralLowerActionData_from_route45 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute44BridgeProofs.CentralCoverTargetRoute44LiteralLowerActionData B D)

Route45 replacement for Route44's lower-action leaf.

theorem Q2Presentation.Induction.TargetKmodRRoute45BridgeProofs.centralCover_targetRoute44RepresentativeActionData_from_route45 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A45 : CentralCoverTargetRoute45LiteralSelectedActionData B D) : Nonempty (TargetKmodRRoute44BridgeProofs.CentralCoverTargetRoute44RepresentativeActionData B D (route44LiteralLowerActionData_of_route45 B D A45))

Route45 replacement for Route44's theorem-level representative-action leaf, for the Route44 lower-action packet induced by the same Route45 data.

Direct Route45 provider

def Q2Presentation.Induction.TargetKmodRRoute45BridgeProofs.projectedConjugationActionData_of_route45 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A45 : CentralCoverTargetRoute45LiteralSelectedActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (route45LowerProjectionData B D A45)

Projected conjugation action from Route45 selected representatives and the closed same-coset/inner-conjugation theorem on K/R.

Equations

• ⋯ = ⋯

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

Route45 quotient-action provider. Its target closure avoids both Route44 residual names and exposes only the coherent Route45 literal selected-action packet.

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

Route45 decoration-kernel provider, drop-in compatible with Route44's integration-side target hook.

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

Convenience Route45 framed-quotient provider for downstream integration.