Route41 target K/R bridge sidecar

Route40 leaves two target-side Section 8 K/R bridge residuals in the active provider:

• TargetKmodRRoute39BridgeProofs.centralCover_targetRoute39LowerQuotientIdentificationData;
• TargetKmodRRoute40BridgeProofs.centralCover_targetRoute40SelectedRepresentativeActionData.

This sidecar removes those two residual names from the target decoration-kernel provider without changing downstream interfaces. The lower quotient identification is supplied from the canonical same-tower quotient packet Y/K ~= B.C. The selected representatives are then chosen theorem-level from the induced canonical lower projection, and the only action-side residual used is the narrower Route26 section-action packet.

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 use selected lower-target representatives, with same-coset independence supplied theorem-level by the realized K/R ~= M bridge.

Route41 lower quotient data

def Q2Presentation.Induction.TargetKmodRRoute41BridgeProofs.route39LowerQuotientIdentificationData_of_route41Actual {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D

Route41 converts the canonical same-tower quotient packet into the Route39 lower quotient identification surface.

This is only a surface conversion: both packets express the manuscript identification C = Y/K.

Equations

• Q2Presentation.Induction.TargetKmodRRoute41BridgeProofs.route39LowerQuotientIdentificationData_of_route41Actual B D E = { lowerActionEquiv := E.canonicalLowerQuotientEquiv }

def Q2Presentation.Induction.TargetKmodRRoute41BridgeProofs.route41CanonicalProjectionData_of_actual {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D

Route41's canonical lower projection induced by Y/K ~= B.C.

This is the projection Y -> Y/K -> B.C; its kernel is K by the first isomorphism theorem. It is the projection used by the Route26 selected-section packet below.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute41BridgeProofs.centralCover_targetRoute39LowerQuotientIdentificationData_from_route41 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D)

Route41 replacement for the Route39 lower quotient residual, routed through the canonical same-tower quotient packet.

Route41 selected representatives

def Q2Presentation.Induction.TargetKmodRRoute41BridgeProofs.route40SelectedRepresentativeActionData_of_route41Section {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) (S : TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26CanonicalRepresentativeSectionData B D (route41CanonicalProjectionData_of_actual B D E)) (A : TargetKmodRRoute26BridgeProofs.CentralCoverTargetRoute26RepresentativeSectionActionData B D (route41CanonicalProjectionData_of_actual B D E) S) : TargetKmodRRoute40BridgeProofs.CentralCoverTargetRoute40SelectedRepresentativeActionData B D (route39LowerQuotientIdentificationData_of_route41Actual B D E)

Route41 selected representatives for Route40.

The representative section itself is theorem-level from the canonical lower projection. The action law is supplied by Route26's narrower selected-section action packet, which no longer bundles the existence of representatives.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute41BridgeProofs.centralCover_targetRoute40SelectedRepresentativeActionData_from_route41 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : Nonempty (TargetKmodRRoute40BridgeProofs.CentralCoverTargetRoute40SelectedRepresentativeActionData B D (route39LowerQuotientIdentificationData_of_route41Actual B D E))

Route41 replacement for Route40's selected-representative residual, for the canonical Route41 lower quotient identification.

Route41 provider

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

Route41 quotient-action provider.

Its axiom closure removes both current Route40 target residual names. The remaining target-side content is the canonical same-tower quotient packet and Route26's selected-section action packet.

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

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

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

Convenience Route41 framed-quotient provider for downstream integration.