Route27 target K/R bridge sidecar

Route26 leaves two target-side facts in the closure:

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRRoute26BridgeProofs.centralCover_targetRoute26RepresentativeSectionActionData.

This sidecar does not fall back to either name. It replaces them by the manuscript-shaped projection/action provenance for the tower

Y -> B.C = Y/K, with M = K/R:

• a concrete projection Y -> B.C whose kernel is the selected subgroup K;
• compatibility of the abstract action B.actM with ambient conjugation through that projection.

The first-isomorphism-theorem quotient equivalence, the route26 selected-section action packet for the induced section, and the downstream decoration-kernel provider are all rebuilt theorem-level from these two route27 packets.

Route27 projection/action packets

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

Route27 lower projection packet.

This is the concrete manuscript assertion that the lower action group is reached from the top target by the quotient projection 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.TargetKmodRRoute27BridgeProofs.CentralCoverTargetRoute27ProjectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute27LowerProjectionData B D) : Prop

Route27 action packet for the concrete lower projection.

It states that the abstract B.C-action on M, transported through K/R ~= M, is ambient right conjugation on the literal quotient K/R.

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

Theorem-level adapters

def Q2Presentation.Induction.TargetKmodRRoute27BridgeProofs.lowerProjectionData_of_route27LowerProjection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute27LowerProjectionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

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

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute27BridgeProofs.canonicalLowerProjectionData_of_route27LowerProjection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute27LowerProjectionData B D) : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D

Convert the route27 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.TargetKmodRRoute27BridgeProofs.canonicalLowerQuotientEquivData_of_route27LowerProjection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute27LowerProjectionData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

The route27 projection induces the actual same-tower quotient equivalence Y/K ~= B.C.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute27BridgeProofs.projectedConjugationActionData_of_route27ProjectionAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute27LowerProjectionData B D) (A : CentralCoverTargetRoute27ProjectionActionData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route27LowerProjection B D P)

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

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute27BridgeProofs.route26RepresentativeSectionActionData_of_route27ProjectionAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute27LowerProjectionData B D) (A : CentralCoverTargetRoute27ProjectionActionData B D P) (S : TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D (canonicalLowerProjectionData_of_route27LowerProjection B D P)) : TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26RepresentativeSectionActionData B D (canonicalLowerProjectionData_of_route27LowerProjection B D P) S

Convert route27 action data to route26's selected-section action packet for the route27-induced canonical projection.

Equations

• ⋯ = ⋯

Route27 residual names

axiom Q2Presentation.Induction.TargetKmodRRoute27BridgeProofs.centralCover_targetRoute27LowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute27LowerProjectionData B D)

Route27 residual 1: the concrete lower quotient projection Y -> B.C has kernel K.

axiom Q2Presentation.Induction.TargetKmodRRoute27BridgeProofs.centralCover_targetRoute27ProjectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute27LowerProjectionData B D) : Nonempty (CentralCoverTargetRoute27ProjectionActionData B D P)

Route27 residual 2: the abstract action B.actM is the conjugation action on K/R through the route27 lower projection.

Route26-compatible closures

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

Route27 replacement for TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData.

theorem Q2Presentation.Induction.TargetKmodRRoute27BridgeProofs.centralCover_targetRoute26RepresentativeSectionActionData_from_route27 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute27LowerProjectionData B D) (S : TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D (canonicalLowerProjectionData_of_route27LowerProjection B D P)) : Nonempty (TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26RepresentativeSectionActionData B D (canonicalLowerProjectionData_of_route27LowerProjection B D P) S)

Route27 replacement for route26's selected-section action residual, for the canonical projection induced by a route27 lower-projection packet.

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

Route27 quotient-action provider.

Its axiom closure contains the two route27 projection/action packets, not either of the two route26 target residual names.

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

Route26-compatible decoration-kernel provider downstream of route27.

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

Convenience route27 framed-quotient provider for downstream integration.