Route46 target K/R canonical ambient-action bridge

Route45 leaves one coherent target-side packet:

• a literal lower quotient equivalence from Route34's Y/K child to B.C;
• a selected section of that literal quotient;
• the selected-representative action law on K/R.

This Route46 sidecar removes that selected-section packet from the target provider closure. It constructs the section theorem-level from the quotient map Y -> Y/K, and obtains the action law by restricting the older all-ambient action packet to those representatives.

The remaining residuals are the sharper manuscript-shaped facts already exposed by TargetKmodRSameTowerActualClosers:

• the canonical same-tower quotient equivalence Y/K ~= B.C;
• the all-ambient assertion that the B.C-action on M = K/R is conjugation on the literal quotient K/R.

Route46 construction of the Route45 selected-action packet

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute46BridgeProofs.route46LowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The lower projection induced by a Route46 canonical quotient equivalence.

Equations

• Q2Presentation.Induction.TargetKmodRRoute46BridgeProofs.route46LowerProjectionData B D E = Q2Presentation.Induction.TargetKmodRSameTowerActualClosers.lowerProjectionData_of_lowerQuotientEquiv B D E

def Q2Presentation.Induction.TargetKmodRRoute46BridgeProofs.route46LiteralRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) : p.fst.Y

The theorem-level representative of a literal class in Route34's lower child Y/K.

Equations

• Q2Presentation.Induction.TargetKmodRRoute46BridgeProofs.route46LiteralRepresentative B D q = Classical.choose ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute46BridgeProofs.route46LiteralRepresentative_spec {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) : (TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 B D).topToLower (route46LiteralRepresentative B D q) = q

The Route46 representative maps to its literal class in Y/K.

def Q2Presentation.Induction.TargetKmodRRoute46BridgeProofs.route45LiteralSelectedActionData_of_route46 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) (A : TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D (route46LowerProjectionData B D E)) : TargetKmodRRoute45BridgeProofs.CentralCoverTargetRoute45LiteralSelectedActionData B D

Route46 builds the Route45 coherent literal selected-action packet from the canonical Y/K ~= B.C equivalence and the all-ambient conjugation-action law.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute46BridgeProofs.centralCover_targetRoute45LiteralSelectedActionData_from_route46 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute45BridgeProofs.CentralCoverTargetRoute45LiteralSelectedActionData B D)

Route46 replacement for the active Route45 selected-action leaf.

The closure no longer contains TargetKmodRRoute45BridgeProofs.centralCover_targetRoute45LiteralSelectedActionData.

Direct Route46 provider

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

Route46 quotient-action provider.

Unlike the Route45 provider, this is assembled directly from the canonical lower projection and all-ambient action law, so no selected-section or same-coset repair step is needed.

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

Route46 decoration-kernel provider, drop-in compatible with the Route45 integration-side target hook.

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

Convenience Route46 framed-quotient provider for downstream integration.