Route190 target literal Y/K quotient and K/R action lowering

This sidecar is a Route189-compatible target provider. It removes the two Route189 target atoms

• TargetKmodRRoute102SemanticClosers.centralCover_targetRoute102LiteralRepresentativeActionData;
• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData.

The replacement surface is the older and more literal Route28/Route34 manuscript layer:

• Route34 supplies the theorem-level lower child with carrier literally Y/K and the quotient map Y -> Y/K;
• Route28 supplies the identification of this literal lower child with the abstract action group B.C;
• Route28 supplies the selected-representative action law on M = K/R;
• inner conjugation by K on K/R is theorem-level from the already-realized K/R ≃ M bridge.

No new axiom is introduced in this file. The expected new target frontier is therefore exactly the two Route28 residuals

• TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28LowerActionEquivData;
• TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28RepresentativeActionData.

Literal lower quotient Y/K

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute190LiteralQuotientActionClosers.route190LowerQuotientMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerQuotientMapData B D

Route190 uses Route34's theorem-level literal lower quotient map Y -> Y/K.

Equations

• Q2Presentation.Induction.TargetKmodRRoute190LiteralQuotientActionClosers.route190LowerQuotientMapData B D = Q2Presentation.Induction.TargetKmodRRoute130Closers.route130LowerQuotientMapData B D

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute190LiteralQuotientActionClosers.CentralCoverTargetRoute190LowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type

Route190 lower-action packet for the literal quotient child Y/K.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute190LiteralQuotientActionClosers.canonicalLowerQuotientEquivData_of_route190LowerAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute190LowerActionEquivData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

Convert the Route28 lower-action data for Route34's literal quotient into Route102/same-tower's canonical quotient equivalence Y/K ≃ B.C.

Equations

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

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

Route190 replacement for the old same-tower canonical lower quotient leaf.

Route102 literal representatives from Route28 selected representatives

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute190LiteralQuotientActionClosers.route190LowerActionEquivData_of_canonicalEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : CentralCoverTargetRoute190LowerActionEquivData B D

A Route28 lower-action packet induced by an externally supplied same-tower quotient equivalence.

Equations

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

@[reducible, inline]

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

The concrete lower projection attached to an externally supplied Y/K ≃ B.C quotient equivalence.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute190LiteralQuotientActionClosers.lowerProjectionData_of_route190CanonicalEquiv_route102LiteralRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) : (lowerProjectionData_of_route190CanonicalEquiv B D E).lowerProjection (TargetKmodRRoute102SemanticClosers.route102LiteralRepresentative B D q) = E.canonicalLowerQuotientEquiv q

Route102's theorem-level literal representative has the lower projection expected from its literal quotient class.

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute190LiteralQuotientActionClosers.route102LiteralRepresentativeActionData_of_route190ProjectedAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) (Aproj : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route190CanonicalEquiv B D E)) : TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData B D E

A projected conjugation law for the Route190 projection gives Route102's literal-representative action law for the supplied quotient equivalence.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute190LiteralQuotientActionClosers.centralCover_targetRoute102LiteralRepresentativeActionData_from_route190 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : Nonempty (TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData B D E)

Route190 replacement for the old Route102 literal representative-action leaf. The closure uses Route28 selected-representative action plus the closed inner-conjugation theorem, not the Route102 action axiom.

Drop-in target providers

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

Route45 selected-action packet reconstructed through the Route190-lowered literal quotient/action surface.

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

Route190 target quotient-action provider.

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

Route190 target decoration-kernel provider.

This is the drop-in replacement used by the integrated Route190 file. Relative to Route189, its axiom closure should replace the two Route102/same-tower atoms by the two Route28 literal lower-action / representative-action atoms.

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

Convenience framed-quotient provider downstream of the Route190 target closer.