Route130 target K/R closers

Route130's public target branch routes through TargetKmodRRoute127Closers.centralCover_targetDecorationKernelData_from_route127, whose target frontier contains two Route102/same-tower packets:

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRRoute102SemanticClosers.centralCover_targetRoute102LiteralRepresentativeActionData.

This sidecar attacks those leaves without promoting any root file. The lower quotient equivalence is rebuilt from Route28's lower-action packet for Route34's literal quotient child Y/K. The Route102 literal representative action packet is rebuilt, for any supplied quotient equivalence, from Route28's selected-representative action packet plus the theorem-level inner-conjugation bridge on K/R.

Manuscript anchors: §7 eq:targettower, with C = Y/K and M = K/R; §8 exact-image lower maps and central-cover transforms, where representative choices inside a Y/K coset are immaterial on K/R.

Route34 literal lower quotient with Route28 action data

@[reducible, inline]

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

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

Equations

• Q2Presentation.Induction.TargetKmodRRoute130Closers.route130LowerQuotientMapData B D = Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 B D

@[reducible, inline]

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

Route130 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.TargetKmodRRoute130Closers.canonicalLowerQuotientEquivData_of_route130LowerAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute130LowerActionEquivData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

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

Equations

• Q2Presentation.Induction.TargetKmodRRoute130Closers.canonicalLowerQuotientEquivData_of_route130LowerAction B D E = { canonicalLowerQuotientEquiv := E.lowerActionEquiv }

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

Route130 replacement for the same-tower canonical lower quotient leaf.

Generic Route102 literal-representative action from Route28

def Q2Presentation.Induction.TargetKmodRRoute130Closers.route130LowerActionEquivData_of_canonicalEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) : CentralCoverTargetRoute130LowerActionEquivData B D

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

Equations

• Q2Presentation.Induction.TargetKmodRRoute130Closers.route130LowerActionEquivData_of_canonicalEquiv B D E = { lowerActionEquiv := E.canonicalLowerQuotientEquiv }

def Q2Presentation.Induction.TargetKmodRRoute130Closers.lowerProjectionData_of_route130CanonicalEquiv {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.TargetKmodRRoute130Closers.lowerProjectionData_of_route130CanonicalEquiv_route102LiteralRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) (q : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y) : (lowerProjectionData_of_route130CanonicalEquiv 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.

def Q2Presentation.Induction.TargetKmodRRoute130Closers.route102LiteralRepresentativeActionData_of_route130ProjectedAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) (Aproj : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route130CanonicalEquiv B D E)) : TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData B D E

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

Equations

• ⋯ = ⋯

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

Route130 replacement for the Route102 literal representative-action leaf.

This theorem is generic in the supplied same-tower quotient equivalence E; its closure uses Route28 selected-representative action and the closed inner-conjugation bridge, not the Route102 action axiom.

Drop-in target providers

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

Route45 selected-action packet reconstructed through the Route130-lowered Route102/same-tower packets.

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

Route130 target quotient-action provider.

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

Route130 target decoration-kernel provider.

This is drop-in compatible with TargetKmodRRoute127Closers.centralCover_targetDecorationKernelData_from_route127, but the Route130 target closure is lowered from the Route102/same-tower leaves to Route28 lower-action and selected-representative action packets.

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

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