Route43 target K/R bridge sidecar

Route42 leaves two target-side packets:

• a projection Y -> B.C with kernel K;
• the all-ambient projected conjugation action law for that projection.

This sidecar refines those packets to the literal same-tower data from the manuscript:

• an identification of the lower action group with the quotient Y/K;
• a selected section of Y/K whose representatives realize the action on K/R.

The projection, its kernel, and the extension from selected representatives to all ambient representatives are then theorem-level. The last step uses the already closed fact that inner conjugation by elements of K is trivial on K/R.

Manuscript anchors:

• §7, eq:targettower (pp. 40--42): Y -> B = Y/R -> C = Y/K and M = K/R;
• §8 (pp. 42--49): exact-image lower maps and central-cover transforms use selected lower-target representatives, with same-coset independence on K/R.

Route43 literal quotient packets

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

Route43 lower quotient identification.

This is the manuscript assertion that the abstract lower action group B.C is the literal quotient Y/K. The actual projection Y -> B.C is induced theorem-level from the quotient map Y -> Y/K.

• lowerActionEquiv : p.fst.Y ⧸ D.Ksub ≃* B.C

structure Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.CentralCoverTargetRoute43SelectedRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute43LowerQuotientIdentificationData B D) : Type

Route43 selected-representative action data.

Compared with Route42's all-ambient projected action packet, this only asks for one section of the literal quotient Y/K. Same-coset independence on K/R extends it to every ambient representative below.

• sectionRepresentative : p.fst.Y ⧸ D.Ksub → p.fst.Y
• sectionRepresentative_spec (q : p.fst.Y ⧸ D.Ksub) : (QuotientGroup.mk' D.Ksub) (self.sectionRepresentative q) = q
• selected_representative_action_realizes_conjugation (q : p.fst.Y ⧸ D.Ksub) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (E.lowerActionEquiv q)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (self.sectionRepresentative q) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

Reassembly of Route42 packets

def Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.route42LowerProjectionData_of_route43 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute43LowerQuotientIdentificationData B D) : TargetKmodRRoute42BridgeProofs.CentralCoverTargetRoute42LowerProjectionData B D

Route43's literal quotient identification induces Route42's concrete lower projection packet by the first isomorphism theorem.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.route39LowerQuotientIdentificationData_of_route43 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute43LowerQuotientIdentificationData B D) : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D

Convert Route43 lower quotient data to Route39's lower quotient surface.

Equations

• Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.route39LowerQuotientIdentificationData_of_route43 B D E = { lowerActionEquiv := E.lowerActionEquiv }

def Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.route40SelectedRepresentativeActionData_of_route43 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute43LowerQuotientIdentificationData B D) (A : CentralCoverTargetRoute43SelectedRepresentativeActionData B D E) : TargetKmodRRoute40BridgeProofs.CentralCoverTargetRoute40SelectedRepresentativeActionData B D (route39LowerQuotientIdentificationData_of_route43 B D E)

Convert Route43 selected representatives to Route40's selected-section surface over the same literal quotient.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.route42ProjectedConjugationActionData_of_route43 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute43LowerQuotientIdentificationData B D) (A : CentralCoverTargetRoute43SelectedRepresentativeActionData B D E) : TargetKmodRRoute42BridgeProofs.CentralCoverTargetRoute42ProjectedConjugationActionData B D (route42LowerProjectionData_of_route43 B D E)

Route43 selected representatives give Route42's all-ambient projected conjugation action for the Route43-induced projection.

Equations

• ⋯ = ⋯

Route43 residual declarations

axiom Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.centralCover_targetRoute43LowerQuotientIdentificationData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute43LowerQuotientIdentificationData B D)

Route43 lower residual: identify the lower target with the literal quotient Y/K.

axiom Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.centralCover_targetRoute43SelectedRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute43LowerQuotientIdentificationData B D) : Nonempty (CentralCoverTargetRoute43SelectedRepresentativeActionData B D E)

Route43 action residual: choose a literal Y/K section whose representatives realize the abstract B.C action on K/R.

Route42 leaf replacements

theorem Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.centralCover_targetRoute42LowerProjectionData_from_route43 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute42BridgeProofs.CentralCoverTargetRoute42LowerProjectionData B D)

Route43 replacement for the Route42 lower projection leaf.

theorem Q2Presentation.Induction.TargetKmodRRoute43BridgeProofs.centralCover_targetRoute42ProjectedConjugationActionData_from_route43 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute43LowerQuotientIdentificationData B D) : Nonempty (TargetKmodRRoute42BridgeProofs.CentralCoverTargetRoute42ProjectedConjugationActionData B D (route42LowerProjectionData_of_route43 B D E))

Route43 replacement for Route42's projected action leaf, for the projection induced by the same Route43 lower quotient identification.

Route43 provider

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

Route43 quotient-action provider.

Its closure avoids the two Route42 residual names. The remaining target-side content is the literal lower quotient identification and selected-section action law above.

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

Route43 decoration-kernel provider, drop-in compatible with Route42's target provider call shape.

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

Convenience Route43 framed-quotient provider for downstream integration.