Route58 target K/R projection/action refinement

Route57 leaves one coherent target-side Section 8 residual:

• TargetKmodRRoute57BridgeProofs.centralCover_targetRoute57ProjectionActionData.

This sidecar keeps the active integration untouched and refines that residual into smaller packets matching the manuscript tower

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

The split is deliberately not routed back through the older Route39/Route41/ Route26 selected-representative leaves, nor through the same-tower lower-level residual names. It records:

• the lower target map Y -> C and its surjectivity;
• the kernel identification ker(Y -> C) = K;
• the projected C-action law on the concrete quotient K/R.

These three packets reassemble theorem-level into Route57's coherent projection/action data and into the Route57-compatible decoration providers.

Route58 residual split

structure Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58LowerTargetMapData {p : FramedPair} (B : MinimalBlock p) : Type

Route58 lower target map packet.

Manuscript anchor: §7, eq:targettower, where the lower target in the central-cover recursion is C = Y/K. This packet provides the concrete map Y -> B.C and surjectivity, but does not include the kernel or action law.

• lowerTargetMap : p.fst.Y →* B.C
• lowerTargetMap_surj : Function.Surjective ⇑self.lowerTargetMap

structure Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58LowerTargetKernelData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute58LowerTargetMapData B) : Prop

Route58 kernel packet for the lower target map.

This is the exactness part of Y -> C = Y/K in eq:targettower, tied dependently to the selected lower target map.

• lowerTargetMap_ker : D.Ksub = P.lowerTargetMap.ker

structure Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.CentralCoverTargetRoute58ProjectedKmodRActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute58LowerTargetMapData B) : Prop

Route58 projected action packet for the selected lower target map.

This is the §8 action compatibility used by exact-image lower maps: after the selected identification K/R ~= M, the C-action on M is actual ambient right conjugation on the quotient K/R.

• projected_action_realizes_conjugation (y : p.fst.Y) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (P.lowerTargetMap y)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

axiom Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.centralCover_targetRoute58LowerTargetMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute58LowerTargetMapData B)

Route58 residual: construct the lower target map Y -> C and prove that it is onto.

axiom Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.centralCover_targetRoute58LowerTargetKernelData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute58LowerTargetMapData B) : Nonempty (CentralCoverTargetRoute58LowerTargetKernelData B D P)

Route58 residual: identify the kernel of the selected lower target map with the subgroup K from the concrete target tower.

axiom Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.centralCover_targetRoute58ProjectedKmodRActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute58LowerTargetMapData B) : Nonempty (CentralCoverTargetRoute58ProjectedKmodRActionData B D P)

Route58 residual: prove that the selected lower target action on M = K/R is induced by ambient conjugation on the concrete quotient K/R.

Reassembly into Route57 and transport-final surfaces

def Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.lowerProjectionData_of_route58 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute58LowerTargetMapData B) (K : CentralCoverTargetRoute58LowerTargetKernelData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Route58 map and kernel packets in the transport-final projection surface.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.projectedConjugationActionData_of_route58 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute58LowerTargetMapData B) (K : CentralCoverTargetRoute58LowerTargetKernelData B D P) (A : CentralCoverTargetRoute58ProjectedKmodRActionData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route58 B D P K)

Route58 projected action in the transport-final action surface.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.route57ProjectionActionData_of_route58 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute58LowerTargetMapData B) (K : CentralCoverTargetRoute58LowerTargetKernelData B D P) (A : CentralCoverTargetRoute58ProjectedKmodRActionData B D P) : TargetKmodRRoute57BridgeProofs.CentralCoverTargetRoute57ProjectionActionData B D

Reassemble Route57's coherent projection/action packet from the Route58 map, kernel, and action packets.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.centralCover_targetRoute57ProjectionActionData_from_route58 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute57BridgeProofs.CentralCoverTargetRoute57ProjectionActionData B D)

Route58 replacement for the Route57 coherent residual.

Route57-compatible providers without the Route57 axiom

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

Direct Route58 quotient-action provider through the selected lower target map and projected action law.

theorem Q2Presentation.Induction.TargetKmodRRoute58ProjectionActionProofs.centralCover_targetRoute54CanonicalSelectedActionData_from_route58 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData B D)

Route54 selected-action packet recovered from the Route58 split via the Route57 adapter, without calling the Route57 axiom.

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

Route58 decoration-kernel provider, with the same shape as the active Route57 hook but a strictly smaller axiom closure.

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

Convenience Route58 framed-quotient provider for downstream integration.