Route40 target K/R bridge sidecar

Route39 lowered the target branch to two literal same-tower packets:

• TargetKmodRRoute39BridgeProofs.centralCover_targetRoute39LowerQuotientIdentificationData;
• TargetKmodRRoute39BridgeProofs.centralCover_targetRoute39LiteralRepresentativeActionData.

This sidecar keeps the Route39 lower quotient identification, but lowers the fixed-literal representative action packet one more step. Instead of asking that Lean's theorem-level Classical.choose representative of each class in Y/K realizes the action, Route40 asks for some selected section of the literal quotient whose representatives realize the C-action on M = K/R.

The passage from that selected section to Route39's fixed literal representatives is theorem-level: two representatives of the same Y/K class differ by an element of K, and inner conjugation by K on K/R is already closed by centralCover_targetKmodRInnerConjugationData_from_KmodR_bridge.

Manuscript anchors:

• §7, eq:targettower (pp. 40--42): Y -> B = Y/R -> C = Y/K and M = K/R;
• §8, exact-image lower maps and central-cover transforms (pp. 42--49): choose lower-target representatives, while same-coset independence makes the choice immaterial.

Route40 selected-section packet

structure Q2Presentation.Induction.TargetKmodRRoute40BridgeProofs.CentralCoverTargetRoute40SelectedRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D) : Type

Route40 selected-representative action data.

This is strictly weaker than Route39's fixed-literal representative action packet: it supplies a section of the literal quotient Y/K together with the action law for that section. The fixed literal representatives used by Route39 are recovered below using the theorem-level same-coset action independence on K/R.

• 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))

axiom Q2Presentation.Induction.TargetKmodRRoute40BridgeProofs.centralCover_targetRoute40SelectedRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D) : Nonempty (CentralCoverTargetRoute40SelectedRepresentativeActionData B D E)

Route40 residual: choose a literal Y/K representative section whose action on K/R realizes the abstract lower action.

Manuscript shape: §7 C = Y/K acts on M = K/R by ambient conjugation; §8 chooses representatives only to evaluate the finite central-cover stages. Unlike Route39, this packet does not name Lean's fixed literal representatives.

Route39 fixed-literal action recovered theorem-level

def Q2Presentation.Induction.TargetKmodRRoute40BridgeProofs.literalRepresentativeActionData_of_route40Selected {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D) (A : CentralCoverTargetRoute40SelectedRepresentativeActionData B D E) : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LiteralRepresentativeActionData B D E

A selected section action law implies Route39's fixed-literal representative action law.

The only extra input is the already closed fact that changing representatives inside one Y/K class acts trivially on K/R.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute40BridgeProofs.centralCover_targetRoute39LiteralRepresentativeActionData_from_route40 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D) : Nonempty (TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LiteralRepresentativeActionData B D E)

Route40 replacement for Route39's fixed-literal representative residual.

Route40 provider

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

Route40 quotient-action provider.

Its axiom closure keeps the Route39 lower quotient identification residual, but replaces TargetKmodRRoute39BridgeProofs.centralCover_targetRoute39LiteralRepresentativeActionData by the selected-section Route40 residual above.

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

Route40 decoration-kernel provider, drop-in compatible with Route39's target provider and with the integration-side call shape.

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

Convenience Route40 framed-quotient provider for downstream integration.