Route20 actual same-tower target K/R provider

Route19's target experiment routed through the older bridge surface. This sidecar stays on the actual same-tower API used by the route18 integration, but splits the target obstruction along the manuscript tower

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

The concrete subgroup packet already contains R <= K, normality/Frattini data, and K/R ~= M. It does not contain the two missing compatibility facts:

• the abstract lower action group B.C is the literal quotient Y/K;
• the abstract action B.actM is the conjugation-induced action on K/R.

Route20 records exactly those two facts and rebuilds the current target hook from them. The second fact is tied to the selected quotient identification, so it is weaker than the older all-projections ambient-action residual.

Manuscript-shaped route20 packets

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

Route20 lower-tower identification: the abstract action group B.C is the literal lower quotient C = Y/K.

• lowerQuotientEquiv : p.fst.Y ⧸ D.Ksub ≃* B.C

structure Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.CentralCoverTargetRoute20ActMInducedConjugationData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute20LowerQuotientIdentificationData B D) : Prop

Route20 action compatibility: under the selected identification Y/K ~= B.C, the abstract action B.actM is induced by ambient conjugation on the literal quotient K/R.

• actM_induced_conjugation (y : p.fst.Y) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (E.lowerQuotientEquiv (TargetKmodRActionProofs.lowerQuotientClass B D y))) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

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

Route20 provenance keeps the quotient identification and its induced-action law together, preventing the route18 action law from being used with an unrelated lower projection.

• lowerQuotientIdentification : CentralCoverTargetRoute20LowerQuotientIdentificationData B D
• actMInducedConjugation : CentralCoverTargetRoute20ActMInducedConjugationData B D self.lowerQuotientIdentification

Theorem-level adapters back to the actual same-tower surface

def Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.canonicalLowerQuotientEquivData_of_route20LowerQuotientIdentification {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute20LowerQuotientIdentificationData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

Convert the route20 lower quotient identification to the current actual same-tower lower-quotient packet.

Equations

• Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.canonicalLowerQuotientEquivData_of_route20LowerQuotientIdentification B D E = { canonicalLowerQuotientEquiv := E.lowerQuotientEquiv }

def Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.lowerProjectionData_of_route20LowerQuotientIdentification {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute20LowerQuotientIdentificationData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The concrete lower projection induced by the route20 quotient identification.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.ambientActionData_of_route20ActMInducedConjugation {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute20LowerQuotientIdentificationData B D) (A : CentralCoverTargetRoute20ActMInducedConjugationData B D E) : TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D (lowerProjectionData_of_route20LowerQuotientIdentification B D E)

Convert route20 induced-action compatibility to the current actual ambient action packet for the lower projection induced by the same quotient identification.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.projectedConjugationActionData_of_route20ActMInducedConjugation {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute20LowerQuotientIdentificationData B D) (A : CentralCoverTargetRoute20ActMInducedConjugationData B D E) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route20LowerQuotientIdentification B D E)

Projected conjugation action from the route20 induced-action packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.quotientActionData_of_route20ActualProvenance {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P20 : CentralCoverTargetRoute20ActualProvenanceData B D) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Route20 quotient-action data from the selected same-tower quotient identification and induced-action compatibility.

Equations

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

Route20 residual names

axiom Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.centralCover_targetRoute20LowerQuotientIdentificationData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute20LowerQuotientIdentificationData B D)

Route20 residual 1: identify the abstract lower group B.C with the literal lower quotient Y/K.

axiom Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.centralCover_targetRoute20ActMInducedConjugationData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute20LowerQuotientIdentificationData B D) : Nonempty (CentralCoverTargetRoute20ActMInducedConjugationData B D E)

Route20 residual 2: with the route20 quotient identification fixed, prove that B.actM is the conjugation-induced action on K/R.

Route-ready hooks

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

Route20 replacement for the actual lower-quotient residual, reduced to the manuscript-shaped quotient identification packet.

theorem Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.centralCover_targetKmodRAmbientActionData_from_route20 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute20LowerQuotientIdentificationData B D) : Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D (lowerProjectionData_of_route20LowerQuotientIdentification B D E))

Route20 replacement for the actual ambient-action residual, for the lower projection induced by the same route20 quotient identification.

theorem Q2Presentation.Induction.TargetKmodRRoute20ActualProofs.centralCover_targetRoute20ActualProvenanceData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute20ActualProvenanceData B D)

Route20 provenance from the two manuscript-shaped packets.

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

Route20 quotient-action provider for the target K/R branch.

This is the direct future-integration hook: it avoids the two route18 actual residual names and uses only the selected quotient identification plus the matching induced-action compatibility.

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

Route20 decoration-kernel provider suitable for replacing the route18 target hook in a future integrated route.

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

Convenience framed-quotient provider downstream of the route20 decoration-kernel hook.