Route35 target K/R bridge sidecar

Route34 closes the concrete lower quotient map Y -> Y/K, but its target decoration-kernel provider still depends on the two remaining route28 target packets:

• centralCover_targetRoute28LowerActionEquivData;
• centralCover_targetRoute28RepresentativeActionData.

This sidecar keeps route34's literal lower child and replaces those two route28 residual names by the already separated same-tower semantics:

• the lower action equivalence is the canonical same-tower equivalence Y/K ~= B.C;
• selected representatives realize the action because the all-ambient same-tower action law holds for every representative.

The exported provider has the same usable downstream shape as route34 while its target axiom closure contains no route28 lower-action or representative-action residuals.

Route34 lower child with route35 action semantics

def Q2Presentation.Induction.TargetKmodRRoute35BridgeProofs.lowerActionEquivData_of_route35 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerActionEquivData B D (TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 B D)

Route35 lower-action equivalence for route34's literal lower child.

Route34's lower child has carrier definitionally Y/K; the remaining content is the same-tower identification of that quotient with the abstract action group B.C.

Equations

• Q2Presentation.Induction.TargetKmodRRoute35BridgeProofs.lowerActionEquivData_of_route35 B D E = { lowerActionEquiv := id E.canonicalLowerQuotientEquiv }

theorem Q2Presentation.Induction.TargetKmodRRoute35BridgeProofs.centralCover_targetRoute35LowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerActionEquivData B D (TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 B D))

Route35 replacement for the route28 lower-action-equivalence residual, for the route34 literal quotient map.

Route28 representative action from same-tower ambient action

def Q2Presentation.Induction.TargetKmodRRoute35BridgeProofs.representativeActionData_of_route35 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeSectionData B D P) (A : TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D P) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeActionData B D P S

Route35 representative-action data from the stronger all-ambient action law.

If every ambient representative realizes the transported B.C-action on K/R, then the selected representatives used by route28 do so immediately.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute35BridgeProofs.centralCover_targetRoute35RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeSectionData B D P) : Nonempty (TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeActionData B D P S)

Route35 replacement for route28's selected-representative action residual.

Route34-compatible provider with route35 residual closure

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

Route35 lower-projection provider.

Compared with route34, this keeps the theorem-level lower quotient map and replaces the route28 lower-action residual by the same-tower quotient equivalence residual.

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

Route35 projected-action provider.

The selected representative law is derived from the same-tower all-ambient action packet; inner-conjugation independence remains theorem-level from the realized K/R ~= M bridge.

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

Route35 quotient-action provider.

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

Route35 decoration-kernel provider, route34-compatible downstream.

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

Convenience route35 framed-quotient provider for downstream integration.