Route52 target K/R coherent literal bridge

Route51's target path uses Route50, whose closure exposes the two Route37 literal target leaves:

• an equivalence between the literal quotient Y/K and the abstract action group B.C;
• the representative action law for that selected equivalence.

This sidecar narrows that pair to one coherent packet. Instead of asking for an arbitrary lower equivalence and then an action law for every such equivalence, Route52 asks for one literal lower equivalence together with the action law for the theorem-level representatives attached to that same equivalence. The quotient projection, kernel statement, representative bridge, Route38-style projected action packet, and Route50/Route48 provider surfaces are then reassembled theorem-level.

Route52 coherent residual

structure Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.CentralCoverTargetRoute52CoherentLiteralActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type

Route52 coherent literal quotient/action packet.

This is the strict narrowing of the two Route37 target leaves used by Route51: it supplies one literal identification Y/K ~= B.C and the representative action law for that same identification. Route37's second residual is stronger because it is stated for an externally supplied equivalence.

• lowerActionEquiv : p.fst.Y ⧸ D.Ksub ≃* B.C
• literal_representative_action_realizes_conjugation (q : p.fst.Y ⧸ D.Ksub) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (self.lowerActionEquiv q)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (TargetKmodRRoute37BridgeProofs.literalQuotientRepresentative B D q) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

axiom Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.centralCover_targetRoute52CoherentLiteralActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute52CoherentLiteralActionData B D)

Route52 target residual: coherent literal lower quotient and action data, replacing the Route37 independent lower/action pair for the Route52 provider.

Route37 and Route50 adapters

def Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.route37LowerActionEquivData_of_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute52CoherentLiteralActionData B D) : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LowerActionEquivData B D

Forget the Route52 action law and recover Route37's lower-equivalence surface.

Equations

• Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.route37LowerActionEquivData_of_route52 B D A = { lowerActionEquiv := A.lowerActionEquiv }

def Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.route37LiteralRepresentativeActionData_of_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute52CoherentLiteralActionData B D) : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LiteralRepresentativeActionData B D (route37LowerActionEquivData_of_route52 B D A)

Recover the Route37 literal representative action surface for the Route37 equivalence induced by the same Route52 coherent packet.

Equations

• ⋯ = ⋯

structure Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.CentralCoverTargetRoute37CoherentPairData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type

A Route37 lower equivalence together with the literal action law for that same equivalence.

This wrapper is intentionally Type-valued: the Route37 action surface itself is proof-valued, so a plain Sigma package is not the right surface here.

• lowerData : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LowerActionEquivData B D
• actionData : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LiteralRepresentativeActionData B D self.lowerData

theorem Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.centralCover_targetRoute37CoherentPair_from_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute37CoherentPairData B D)

Route52 supplies a coherent Route37 lower/action pair. This is the direct replacement shape for the two Route37 leaves when downstream code can consume a coherent pair instead of two independent providers.

theorem Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.centralCover_targetRoute37LowerActionEquivData_from_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LowerActionEquivData B D)

Route37 lower-equivalence surface recovered from Route52.

theorem Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.centralCover_targetRoute37LiteralRepresentativeActionData_from_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute52CoherentLiteralActionData B D) : Nonempty (TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LiteralRepresentativeActionData B D (route37LowerActionEquivData_of_route52 B D A))

Route37 literal action surface recovered from Route52 for the equivalence induced by the same Route52 packet.

def Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.lowerProjectionData_of_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute52CoherentLiteralActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The Route52 lower projection Y -> B.C, induced by the literal quotient map Y -> Y/K and the selected equivalence.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.representativeActionBridgeData_of_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute52CoherentLiteralActionData B D) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (lowerProjectionData_of_route52 B D A)

Route52 representative bridge over the Route52 lower projection.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.projectedConjugationActionData_of_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute52CoherentLiteralActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route52 B D A)

Route52 projected conjugation action, using the closed inner-conjugation theorem on K/R to pass from representatives to all ambient elements.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.route38LowerProjectionData_of_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute52CoherentLiteralActionData B D) : TargetKmodRRoute38BridgeProofs.CentralCoverTargetRoute38LowerProjectionData B D

Route38 lower projection surface recovered from Route52.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.route38ProjectedConjugationActionData_of_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute52CoherentLiteralActionData B D) : TargetKmodRRoute38BridgeProofs.CentralCoverTargetRoute38ProjectedConjugationActionData B D (route38LowerProjectionData_of_route52 B D A)

Route38 projected action surface recovered from Route52.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.route48ProjectionActionData_of_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute52CoherentLiteralActionData B D) : TargetKmodRRoute48BridgeProofs.CentralCoverTargetRoute48ProjectionActionData B D

Route48 coherent projection/action packet rebuilt through Route50's Route37 adapter, but with the Route37 data sourced from the single Route52 packet.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute52BridgeProofs.centralCover_targetRoute48ProjectionActionData_from_route52 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute48BridgeProofs.CentralCoverTargetRoute48ProjectionActionData B D)

Route48 residual surface recovered from Route52.

Route52 provider

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

Route52 quotient-action provider.

Its custom target closure is the single coherent Route52 packet, not the two Route37 residual names currently visible in Route51.

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

Route52 decoration-kernel provider, drop-in compatible with Route51's target call site after swapping the Route50 provider for this one.

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

Convenience Route52 framed-quotient provider for downstream integration.