Route48 target K/R coherent projection/action bridge

Route46's active target hook still depends on two broad actual same-tower leaves:

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData.

This Route48 sidecar does not route the older Route47 literal quotient sidecar. Instead it exposes one coherent same-tower target packet:

• a concrete lower projection Y -> B.C with kernel exactly K;
• the B.C-action on M = K/R, checked on the theorem-level representatives chosen from that same projection.

The quotient equivalence Y/K ~= B.C is then first-isomorphism-theorem bookkeeping, and the upgrade from selected representatives to all ambient representatives uses the already closed inner-conjugation theorem for K/R.

Coherent Route48 residual

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

Route48 coherent same-tower projection/action packet.

The representative in the action field is not extra data: it is the theorem-level representative selected from lowerProjection_surj. This keeps the lower projection and action law tied to the same Y/K tower.

• lowerProjection : p.fst.Y →* B.C
• lowerProjection_surj : Function.Surjective ⇑self.lowerProjection
• lowerProjection_ker : D.Ksub = self.lowerProjection.ker
• representative_action_realizes_conjugation (c : B.C) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM c) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (Classical.choose ⋯) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

axiom Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.centralCover_targetRoute48ProjectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute48ProjectionActionData B D)

Route48 target residual: one coherent same-tower packet replacing the Route46 pair of broad actual leaves.

Theorem-level adapters

def Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.lowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute48ProjectionActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The transport-final lower projection extracted from Route48 data.

Equations

• Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.lowerProjectionData B D A = { lowerProjection := A.lowerProjection, lowerProjection_surj := ⋯, lowerProjection_ker := ⋯ }

def Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.quotientRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute48ProjectionActionData B D) (c : B.C) : p.fst.Y

Route48's theorem-level representative for a lower class.

Equations

• Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.quotientRepresentative B D A c = Classical.choose ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.quotientRepresentative_spec {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute48ProjectionActionData B D) (c : B.C) : A.lowerProjection (quotientRepresentative B D A c) = c

The Route48 representative maps to its lower class.

def Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.representativeActionBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute48ProjectionActionData B D) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (lowerProjectionData B D A)

Convert Route48 data to the representative-action bridge packet.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.canonicalLowerQuotientEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute48ProjectionActionData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

Route48 lower quotient equivalence Y/K ~= B.C, induced by the concrete projection and its kernel statement.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.projectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute48ProjectionActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData B D A)

Route48 projected conjugation action, upgrading selected representatives to all representatives by closed inner conjugation on K/R.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.ambientActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute48ProjectionActionData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D (lowerProjectionData B D A)

Route48 ambient action packet for the lower projection supplied by the same Route48 data.

Equations

• ⋯ = ⋯

Route-ready providers

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

Route48 replacement for the canonical lower-quotient leaf, reduced to the single coherent Route48 packet.

theorem Q2Presentation.Induction.TargetKmodRRoute48BridgeProofs.centralCover_targetKmodRAmbientActionData_from_route48 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute48ProjectionActionData B D) : Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D (lowerProjectionData B D A))

Route48 ambient-action packet for the Route48 lower projection.

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

Route48 quotient-action provider. Its target closure has one custom same-tower residual: centralCover_targetRoute48ProjectionActionData.

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

Route48 decoration-kernel provider, drop-in compatible with the Route46 integration-side target hook.

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

Convenience Route48 framed-quotient provider for downstream integration.