Documentation

Q2Presentation.Induction.TargetKmodRRoute106Closers

Route106 target `K/R` literal quotient-action lowering #

Route103 left two target-side non-local packets:

TargetKmodRRoute103Closers.centralCover_targetRoute103LowerActionEquivData;
TargetKmodRRoute103Closers.centralCover_targetRoute103LiteralQuotientActionData.

This sidecar avoids both Route103 axiom names in the downstream decoration-kernel provider. The literal lower quotient is still Route34's theorem-level child Y/K. The lower-action equivalence is exposed as Route28's lower-action packet for that child, and the all-representatives literal quotient action is recovered theorem-level from Route28's selected-representative action packet plus the already closed inner-conjugation bridge on K/R.

Axiom frontier effect for the target branch:

replaces the Route103 lower-action axiom by TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28LowerActionEquivData instantiated at Route34's literal quotient map;
replaces the Route103 all-representatives action axiom by TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28RepresentativeActionData for the induced lower projection and its theorem-level choice section.

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute106Closers.route106LowerQuotientMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerQuotientMapData B D

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

Equations

Q2Presentation.Induction.TargetKmodRRoute106Closers.route106LowerQuotientMapData B D = Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 B D

Instances For

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute106Closers.CentralCoverTargetRoute106LowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Route106 lower-action packet: the literal Route34 quotient child Y/K is identified with the abstract action group B.C.

Equations

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

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.centralCover_targetRoute106LowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetRoute106LowerActionEquivData B D)

Route106 lower-action provider, exposing the Route28 manuscript-shaped lower-action packet instead of the Route103 wrapper axiom.

def Q2Presentation.Induction.TargetKmodRRoute106Closers.canonicalLowerQuotientEquivData_of_route106LowerAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute106LowerActionEquivData B D) :

TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

Convert the Route106 lower-action equivalence to the same-tower actual surface consumed by Route102's downstream reassembly.

Equations

Q2Presentation.Induction.TargetKmodRRoute106Closers.canonicalLowerQuotientEquivData_of_route106LowerAction B D E = { canonicalLowerQuotientEquiv := E.lowerActionEquiv }

Instances For

def Q2Presentation.Induction.TargetKmodRRoute106Closers.lowerProjectionData_of_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute106LowerActionEquivData B D) :

TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The concrete lower projection induced by the Route34 quotient map and the Route106 lower-action equivalence.

Equations

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

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.lowerProjectionData_of_route106_route102LiteralRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute106LowerActionEquivData B D) (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) :

(lowerProjectionData_of_route106 B D E).lowerProjection (TargetKmodRRoute102SemanticClosers.route102LiteralRepresentative B D q) = E.lowerActionEquiv q

Route102's theorem-level literal representative has the Route106 lower projection expected from its literal class in Y/K.

def Q2Presentation.Induction.TargetKmodRRoute106Closers.route102LiteralRepresentativeActionData_of_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute106LowerActionEquivData B D) (Aproj : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route106 B D E)) :

TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData B D (canonicalLowerQuotientEquivData_of_route106LowerAction B D E)

Route106 turns Route28 selected-representative action data into Route102's literal representative-action packet. The selected-representative law is first promoted to the all-representatives projected conjugation law using the closed inner-conjugation bridge, then evaluated on Route102's literal representative.

Equations

⋯ = ⋯

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.centralCover_targetRoute102LiteralRepresentativeActionData_from_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute106LowerActionEquivData B D) :

Nonempty (TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData B D (canonicalLowerQuotientEquivData_of_route106LowerAction B D E))

Route106 replacement for Route102's literal representative-action residual, with frontier lowered to Route28's selected-representative action packet.

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.centralCover_targetCanonicalLowerQuotientEquivData_from_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D)

Route106 replacement for the old same-tower lower-quotient residual.

def Q2Presentation.Induction.TargetKmodRRoute106Closers.lowerProjectionData_of_route106Route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute106LowerActionEquivData B D) :

TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Route106 selected lower projection for the downstream transport-final surface.

Equations

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

Instances For

def Q2Presentation.Induction.TargetKmodRRoute106Closers.projectedConjugationActionData_of_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute106LowerActionEquivData B D) (A : TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData B D (canonicalLowerQuotientEquivData_of_route106LowerAction B D E)) :

TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route106Route102 B D E)

Route106 projected-conjugation packet, via Route102's theorem-level representative/class-independence conversion and the Route28 selected-action lowering above.

Equations

⋯ = ⋯

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.centralCover_targetKmodRProjectedConjugationActionData_from_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty ((P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) ×' TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Route106 projected-conjugation provider.

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.centralCover_targetKmodRQuotientActionData_from_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

Route106 quotient-action packet through the literal Y/K action lowering.

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.centralCover_targetKmodRActionCompatibilityData_from_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetDecorationCanonicalInvarianceProofs.CentralCoverTargetKmodRActionCompatibilityData B D)

Route106 action-compatibility packet.

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.centralCover_targetDecorationCanonicalInvarianceData_from_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetDecorationActualDescentProofs.CentralCoverTargetDecorationCanonicalInvarianceData B D)

Route106 canonical-invariance provider.

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.centralCover_targetDecorationKernelData_from_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetDecorationKernelData B D)

Route106 decoration-kernel provider, drop-in compatible with the Route103 call-site but with the two Route103 target residual names removed.

theorem Q2Presentation.Induction.TargetKmodRRoute106Closers.centralCover_targetCanonicalFramedQuotientData_from_route106 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

Convenience Route106 framed-quotient provider for downstream integrations.