Route34 target K/R bridge sidecar

Route33's target branch goes through route31, whose remaining non-local target frontier is the three route28 packets:

• centralCover_targetRoute28LowerQuotientMapData;
• centralCover_targetRoute28LowerActionEquivData;
• centralCover_targetRoute28RepresentativeActionData.

This sidecar closes the first of those at the current interface level. The lower quotient group is the literal quotient Y/K; for the FramedPair carrier we keep the original tame quotient and attach a trivial elementary decoration. The route28 packet only uses the carrier group and the quotient map, so no decoration-kernel circularity is introduced.

The exported provider has the same downstream shape as route31, but its axiom closure no longer contains TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28LowerQuotientMapData.

Theorem-level route34 lower quotient map

noncomputable def Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.route34TrivialPsi : PiGrp ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Multiplicative (ZMod 2)))

The trivial elementary marking used for the route34 auxiliary lower child.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.route34LowerTarget {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : BoundaryFramedTarget

Route34's auxiliary lower boundary-framed target with carrier group Y/K.

Only the carrier group and quotient map are consumed by the route28 lower-action adapter. The tame quotient is inherited from p, while the decoration is chosen trivial to avoid depending on the later decoration-kernel conclusion.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.route34LowerFrame {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : BoundaryFrame (route34LowerTarget B D)

Boundary frame for the route34 lower child.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.route34LowerChild {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : FramedPair

Route34 lower child, with carrier group definitionally Y/K.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerQuotientMapData B D

The route28 lower quotient-map packet is theorem-level at the current interface: use the literal quotient map Y -> Y/K.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.centralCover_targetRoute34LowerQuotientMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerQuotientMapData B D)

Route34 replacement for the first route28 residual.

Route31-compatible target provider

theorem Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.centralCover_targetLowerProjectionData_from_route34 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D)

Route34 lower-projection provider.

Compared with route31, this closes the route28 lower quotient-map packet and leaves only the lower action equivalence packet on the lower side.

theorem Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.centralCover_targetKmodRProjectedConjugationActionData_from_route34 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty ((P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) ×' TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Route34 projected-action provider.

The remaining target action residual is exactly route28's selected representative action law for the route34 lower projection; inner conjugation on K/R remains theorem-level from the realized K/R ≃ M bridge.

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

Route34 quotient-action provider.

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

Route34 decoration-kernel provider, route31-compatible downstream.

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

Convenience route34 framed-quotient provider for downstream integration.