Route42 target K/R bridge sidecar

Route41's target provider removes the Route39/Route40 bridge names, but its axiom closure still contains two target-side leaves:

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRRoute26BridgeProofs.centralCover_targetRoute26RepresentativeSectionActionData.

This sidecar replaces those two leaves by the direct manuscript quotient-action surface:

• a concrete projection Y -> B.C whose kernel is the selected subgroup K;
• the projected action law saying that the B.C-action on M = K/R is literal right conjugation on K/R.

The first-isomorphism-theorem quotient equivalence and the Route26 selected section action packet are both recovered theorem-level from these Route42 packets. The exported provider has the same downstream target shape as TargetKmodRRoute41BridgeProofs.centralCover_targetDecorationKernelData_from_route41.

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 the transported C-action on K/R.

Route42 projection/action packets

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

Route42 lower projection packet.

This is the concrete manuscript assertion that the abstract lower action group B.C is reached from the top finite target by the quotient map with kernel K.

• lowerProjection : p.fst.Y →* B.C
• lowerProjection_surj : Function.Surjective ⇑self.lowerProjection
• lowerProjection_ker : D.Ksub = self.lowerProjection.ker

structure Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.CentralCoverTargetRoute42ProjectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute42LowerProjectionData B D) : Prop

Route42 projected action packet.

It states directly that the transported B.C action on M agrees with ambient right conjugation on the literal quotient K/R.

• action_realizes_projected_conjugation (y : p.fst.Y) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (P.lowerProjection y)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

Adapters to existing target interfaces

def Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.lowerProjectionData_of_route42 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute42LowerProjectionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Convert the Route42 lower projection to the transport-final projection packet.

Equations

• Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.lowerProjectionData_of_route42 B D P = { lowerProjection := P.lowerProjection, lowerProjection_surj := ⋯, lowerProjection_ker := ⋯ }

def Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.canonicalLowerProjectionData_of_route42 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute42LowerProjectionData B D) : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D

Convert the Route42 lower projection to the canonical same-tower projection packet used by Route26.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.canonicalLowerQuotientEquivData_of_route42 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute42LowerProjectionData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

The Route42 lower projection induces the same-tower quotient equivalence Y/K ~= B.C by the first isomorphism theorem.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.projectedConjugationActionData_of_route42 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute42LowerProjectionData B D) (A : CentralCoverTargetRoute42ProjectedConjugationActionData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route42 B D P)

Convert Route42 projected action data to the transport-final projected conjugation packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.route26RepresentativeSectionActionData_of_route42 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute42LowerProjectionData B D) (A : CentralCoverTargetRoute42ProjectedConjugationActionData B D P) (S : TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D (canonicalLowerProjectionData_of_route42 B D P)) : TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26RepresentativeSectionActionData B D (canonicalLowerProjectionData_of_route42 B D P) S

Convert Route42 projected action data to Route26's selected-section action packet for the Route42-induced canonical projection.

Equations

• ⋯ = ⋯

Route42 residual declarations

axiom Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.centralCover_targetRoute42LowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute42LowerProjectionData B D)

Route42 lower residual: construct the concrete projection Y -> B.C with kernel K.

axiom Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.centralCover_targetRoute42ProjectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute42LowerProjectionData B D) : Nonempty (CentralCoverTargetRoute42ProjectedConjugationActionData B D P)

Route42 action residual: the projected C = Y/K action on K/R is ambient right conjugation.

Route41 leaf replacements

theorem Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.centralCover_targetCanonicalLowerQuotientEquivData_from_route42 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D)

Route42 replacement for TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData.

theorem Q2Presentation.Induction.TargetKmodRRoute42BridgeProofs.centralCover_targetRoute26RepresentativeSectionActionData_from_route42 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute42LowerProjectionData B D) (S : TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D (canonicalLowerProjectionData_of_route42 B D P)) : Nonempty (TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26RepresentativeSectionActionData B D (canonicalLowerProjectionData_of_route42 B D P) S)

Route42 replacement for Route26's selected-section action residual, for the canonical projection induced by a Route42 lower-projection packet.

Route42 provider

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

Route42 quotient-action provider.

Its axiom closure uses the two Route42 projection/action packets, not either of the two target leaves remaining in Route41.

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

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

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

Convenience Route42 framed-quotient provider for downstream integration.