Route102 target K/R semantic lowering

Route101 exposed four target-side projection/action residuals:

• centralCover_targetLowerQuotientMapData;
• centralCover_targetLowerActionEquivData;
• centralCover_targetKmodRRepresentativeActionData;
• centralCover_targetKmodRConjugationClassIndependenceData.

This sidecar removes the lower quotient-map residual by using Route34's literal Y/K lower child, removes the lower-action residual by using the literal same-tower equivalence Y/K ~= B.C, and closes class-independence from the already theorem-level inner-conjugation bridge on K/R.

The only target semantic residual added here is a smaller literal representative-action packet for the Route34 lower child: representatives are the canonical quotient representatives of elements of Y/K, not arbitrary data in the packet.

Literal lower quotient and lower action

def Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.lowerQuotientMapData_of_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D

Route102 lower quotient map: Route34's theorem-level lower child with carrier group literally Y/K, converted to the Route101 semantic surface.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.centralCover_targetLowerQuotientMapData_from_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D)

Route102 replacement for the lower quotient-map residual.

def Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.lowerActionEquivData_of_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerActionEquivData B D (lowerQuotientMapData_of_route102 B D)

The lower-action equivalence for Route102's literal Y/K child, obtained from the same-tower identification Y/K ~= B.C.

Equations

• Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.lowerActionEquivData_of_route102 B D E = { lowerActionEquiv := E.canonicalLowerQuotientEquiv }

theorem Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.centralCover_targetLowerActionEquivData_from_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty ((Q : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D) ×' TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerActionEquivData B D Q)

Route102 replacement for the lower-action residual, for the Route102 literal lower child.

def Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.lowerProjectionData_of_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The concrete lower projection Y -> B.C selected by Route102.

Equations

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

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

Route102 selected lower projection.

Literal representatives and the smaller action residual

def Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.route102LiteralRepresentative {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 lower quotient class.

Equations

• Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.route102LiteralRepresentative B D q = Classical.choose ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.route102LiteralRepresentative_spec {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) : (lowerQuotientMapData_of_route102 B D).topToLower (route102LiteralRepresentative B D q) = q

The Route102 literal representative maps to its lower quotient class.

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

Route102 projection evaluated on the theorem-level literal representative.

structure Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : Prop

Route102's smaller literal representative-action residual.

The lower class is an element of the literal quotient child Y/K, and the representative is the theorem-level quotient representative of that class.

• literal_representative_action_realizes_conjugation (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (E.canonicalLowerQuotientEquiv q)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (route102LiteralRepresentative B D q) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

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

Route102 target residual: the canonical representatives of literal lower quotient classes realize the transported B.C action on K/R.

def Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.representativeActionData_of_route102LiteralAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) (A : CentralCoverTargetRoute102LiteralRepresentativeActionData B D E) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D (lowerProjectionData_of_route102 B D E)

Convert Route102 literal representative-action data to the Route101 representative-action surface for the Route102 lower projection.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.centralCover_targetKmodRRepresentativeActionData_from_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty ((P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) ×' TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D P)

Route102 replacement for the representative-action residual, for the Route102 lower projection.

Class-independence closed from inner conjugation on K/R

def Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.conjugationClassIndependenceData_from_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRConjugationClassIndependenceData B D P

Class-independence for any lower projection with kernel K, theorem-level from the closed inner-conjugation bridge K/R ~= M.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.centralCover_targetKmodRConjugationClassIndependenceData_from_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRConjugationClassIndependenceData B D P)

Route102 closes the old class-independence residual for any selected lower projection.

Route102 provider surfaces

def Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.projectedConjugationActionData_of_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) (A : CentralCoverTargetRoute102LiteralRepresentativeActionData B D E) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route102 B D E)

Projected conjugation action for the Route102 lower projection.

Equations

• ⋯ = ⋯

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

Route102 projected-conjugation provider, returning the selected lower projection together with its action law.

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

Route102 quotient-action packet through the literal lower quotient and the Route102 literal representative-action residual.

theorem Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.centralCover_targetKmodRActionCompatibilityData_from_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationCanonicalInvarianceProofs.CentralCoverTargetKmodRActionCompatibilityData B D)

Route102 action-compatibility packet.

theorem Q2Presentation.Induction.TargetKmodRRoute102SemanticClosers.centralCover_targetDecorationCanonicalInvarianceData_from_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationActualDescentProofs.CentralCoverTargetDecorationCanonicalInvarianceData B D)

Route102 canonical-invariance provider.

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

Route102 decoration-kernel provider, drop-in compatible with the Route101 integration call-site but with the four Route101 target leaves lowered to two literal same-tower residuals.

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

Convenience Route102 framed-quotient provider for downstream integrations.