Route103 target K/R literal quotient-action lowering

Route102 leaves two target residuals:

• the literal quotient identification Y/K ~= B.C, packaged as the same-tower lower quotient equivalence; and
• the action law for the canonical representatives of literal Y/K classes.

This sidecar keeps the Route102 downstream API but lowers those two names to packets stated directly on the manuscript tower

Y -> B = Y/R -> C = Y/K, M = K/R.

The lower-side residual is now the Route28/Route34 lower-action equivalence for the already theorem-level lower child C = Y/K. The action residual is stated as well-defined quotient action: every representative of a literal class acts on K/R by the transported B.C action. Route102's chosen-representative packet is recovered theorem-level by applying this action law to its chosen quotient representative.

@[reducible, inline]

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

Route103 lower action equivalence for the literal Route34 lower child C = Y/K.

Equations

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

axiom Q2Presentation.Induction.TargetKmodRRoute103Closers.centralCover_targetRoute103LowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute103LowerActionEquivData B D)

Route103 lower residual: identify the theorem-level literal quotient child Y/K with the block's abstract lower action group B.C.

structure Q2Presentation.Induction.TargetKmodRRoute103Closers.CentralCoverTargetRoute103LiteralQuotientActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute103LowerActionEquivData B D) : Prop

Route103 quotient-action packet on the literal lower quotient.

This states the manuscript action of C = Y/K on M = K/R: any ambient representative of a lower quotient class induces the transported B.C action on the literal quotient K/R.

• literal_quotient_action_realizes_conjugation (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) (y : p.fst.Y) : (TargetKmodRRoute102SemanticClosers.lowerQuotientMapData_of_route102 B D).topToLower y = q → ∀ (m : B.M), D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (E.lowerActionEquiv q)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

axiom Q2Presentation.Induction.TargetKmodRRoute103Closers.centralCover_targetRoute103LiteralQuotientActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute103LowerActionEquivData B D) : Nonempty (CentralCoverTargetRoute103LiteralQuotientActionData B D E)

Route103 action residual: the literal quotient action of C = Y/K on M = K/R is induced by ambient conjugation on representatives.

Reassembly of the Route102 residual surfaces

def Q2Presentation.Induction.TargetKmodRRoute103Closers.canonicalLowerQuotientEquivData_of_route103LowerAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute103LowerActionEquivData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

Route103's literal Route34 lower-action equivalence gives the Route102 same-tower quotient equivalence Y/K ~= B.C.

Equations

• Q2Presentation.Induction.TargetKmodRRoute103Closers.canonicalLowerQuotientEquivData_of_route103LowerAction B D E = { canonicalLowerQuotientEquiv := E.lowerActionEquiv }

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

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

def Q2Presentation.Induction.TargetKmodRRoute103Closers.route102LiteralRepresentativeActionData_of_route103 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute103LowerActionEquivData B D) (A : CentralCoverTargetRoute103LiteralQuotientActionData B D E) : TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData B D (canonicalLowerQuotientEquivData_of_route103LowerAction B D E)

Route103's quotient-action packet implies Route102's chosen literal representative-action packet for the quotient equivalence selected above.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute103Closers.centralCover_targetRoute102LiteralRepresentativeActionData_from_route103 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute103LowerActionEquivData B D) : Nonempty (TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData B D (canonicalLowerQuotientEquivData_of_route103LowerAction B D E))

Route103 replacement for the old Route102 chosen-representative residual, for the Route103-selected quotient equivalence.

Route103 provider surfaces

def Q2Presentation.Induction.TargetKmodRRoute103Closers.lowerProjectionData_of_route103 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute103LowerActionEquivData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Route103 selected lower projection.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute103Closers.projectedConjugationActionData_of_route103 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute103LowerActionEquivData B D) (A : CentralCoverTargetRoute103LiteralQuotientActionData B D E) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route103 B D E)

Route103 projected-conjugation packet, via Route102's theorem-level representative/class-independence conversion.

Equations

• ⋯ = ⋯

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

Route103 projected-conjugation provider.

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

Route103 quotient-action packet through the literal Y/K action packets.

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

Route103 action-compatibility packet.

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

Route103 canonical-invariance provider.

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

Route103 decoration-kernel provider, with the same final output shape as TargetKmodRRoute102SemanticClosers.centralCover_targetDecorationKernelData_from_route102 but with the two Route102 target residual names lowered to Route103 literal quotient-action packets.

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

Convenience Route103 framed-quotient provider for downstream integrations.