Route127 target K/R closers

Route127's public target branch still uses TargetKmodRRoute45BridgeProofs.centralCover_targetRoute45LiteralSelectedActionData. The Route126 sidecar shows that the same downstream decoration-kernel consumer can instead be routed through the two Route28 atoms for the literal quotient C = Y/K and the action on M = K/R.

This file keeps both viewpoints available:

• centralCover_targetRoute45LiteralSelectedActionData_from_route127_via_route28 reconstructs the public Route45 selected-action packet from the two Route28 atoms, with the quotient map supplied theorem-level by Route34.
• centralCover_targetRoute45LiteralSelectedActionData_from_route127 lowers the same Route45 packet further to Route102's stricter same-tower residuals: the canonical quotient equivalence Y/K ~= B.C and the literal representative action law.
• centralCover_targetDecorationKernelData_from_route127 is the requested drop-in provider for downstream consumers.

Manuscript anchors: §7 eq:targettower, with C = Y/K and M = K/R; §8 exact-image lower maps and central-cover transforms, where selected representatives of lower classes realize the transported C-action on K/R.

Route28 reconstruction of the Route45 public leaf

@[reducible, inline]

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

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

Equations

• Q2Presentation.Induction.TargetKmodRRoute127Closers.route127LowerQuotientMapData B D = Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 B D

@[reducible, inline]

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

Route127 lower-action equivalence for the Route34 literal quotient child.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute127Closers.lowerProjectionData_of_route127LowerAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute127LowerActionEquivData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Route127 lower projection induced by the Route28 lower packets.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute127Closers.representativeSectionData_of_route127LowerAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute127LowerActionEquivData B D) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeSectionData B D (lowerProjectionData_of_route127LowerAction B D E)

Route127 selected section for the Route28-induced lower projection.

Equations

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

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute127Closers.CentralCoverTargetRoute127RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute127LowerActionEquivData B D) : Prop

Route127 selected-representative action data for the Route28-induced projection.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute127Closers.route45LiteralSelectedActionData_of_route28 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute127LowerActionEquivData B D) (A : CentralCoverTargetRoute127RepresentativeActionData B D E) : TargetKmodRRoute45BridgeProofs.CentralCoverTargetRoute45LiteralSelectedActionData B D

Rebuild the public Route45 literal selected-action packet from Route28's literal lower-action equivalence and selected-representative action law.

Equations

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

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

Public Route45 selected-action packet reconstructed from the two Route28 atoms named in the Route126 target lowering. This theorem does not use the Route45 axiom.

Stricter Route102/same-tower lowering of the Route45 leaf

def Q2Presentation.Induction.TargetKmodRRoute127Closers.route45LiteralSelectedActionData_of_route102 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D) (A : TargetKmodRRoute102SemanticClosers.CentralCoverTargetRoute102LiteralRepresentativeActionData B D E) : TargetKmodRRoute45BridgeProofs.CentralCoverTargetRoute45LiteralSelectedActionData B D

Rebuild the public Route45 selected-action packet from Route102's stricter literal representative action law and the canonical quotient equivalence Y/K ~= B.C.

Equations

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

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

Public Route45 selected-action packet lowered below Route28 to the same-tower canonical quotient equivalence and Route102 literal representative action residual.

Drop-in target providers

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

Quotient-action data from the Route127-lowered Route45 packet.

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

Route127 target decoration-kernel provider.

This is a drop-in replacement for TargetKmodRRoute53BridgeProofs.centralCover_targetDecorationKernelData_from_route53. Its target closure does not contain the public Route45 leaf or either Route28 atom; the remaining target residuals are Route102/same-tower quotient/action compatibility facts.

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

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

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

Route126/Route28 comparison provider kept for audit: same downstream conclusion, with closure exactly at the two Route28 atoms.