Route144 same-tower target closers

This sidecar attacks the Route143 Section 8 target frontier. Route143 routes through four transport-final packets:

• centralCover_targetLowerQuotientMapData;
• centralCover_targetLowerActionEquivData;
• centralCover_targetKmodRRepresentativeActionData;
• centralCover_targetKmodRConjugationClassIndependenceData.

The replacement below uses the more literal same-tower data already isolated in TargetKmodRSameTowerActualClosers: the abstract lower action group is the canonical quotient Y/K, and the abstract B.C-action on K/R is ambient conjugation for every representative. This avoids the selected lower-child, representative-section, and class-independence packets in the integrated route.

theorem Q2Presentation.Induction.TargetKmodRRoute144SameTowerClosers.centralCover_targetLowerProjectionData_from_route144SameTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D)

Route144 lower projection: build the concrete map Y -> B.C directly from same-tower identification of B.C with the canonical quotient Y/K.

Axiom delta: this uses TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData instead of the two Route143 lower quotient/action packets.

theorem Q2Presentation.Induction.TargetKmodRRoute144SameTowerClosers.centralCover_targetKmodRProjectedConjugationActionData_from_route144SameTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty ((P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) ×' TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Route144 projected conjugation action: use the all-ambient-representatives action law for the canonical lower projection.

Axiom delta: this uses TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData instead of the Route143 representative-action and class-independence packets.

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

Quotient-action packet through the Route144 same-tower target route.

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

Drop-in target decoration-kernel provider for Route144.

Compared with Route143, this removes all four target transport-final axioms from the integrated path and replaces them by two same-tower actual atoms: centralCover_targetCanonicalLowerQuotientEquivData and centralCover_targetKmodRAmbientActionData.