Route10 target projection/action proof sidecar

This file is a route10-owned sidecar for the four projection/action packets introduced by TargetKmodRProjectionSemanticClosers:

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

The direct route-ready provider below avoids those four names. It uses the canonical same-tower lower projection and representative action, while closing same-coset independence from the realized K/R ~= M bridge rather than from a separate commutator packet.

Canonical same-tower packets with inner conjugation closed

theorem Q2Presentation.Induction.TargetKmodRProjectionRoute10Proofs.centralCover_targetCanonicalLowerActionEquivData_from_projectionRoute10Proofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D)

The canonical lower action equivalence Y/K ~= B.C.

theorem Q2Presentation.Induction.TargetKmodRProjectionRoute10Proofs.centralCover_targetKmodRSameCosetConjugationData_from_projectionRoute10Proofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerLowerClosers.CentralCoverTargetKmodRSameCosetConjugationData B D)

Same-coset conjugation on K/R, with inner K-conjugation closed from the realized K/R ~= M bridge.

theorem Q2Presentation.Induction.TargetKmodRProjectionRoute10Proofs.centralCover_targetKmodRCanonicalActionData_from_projectionRoute10Proofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (TargetKmodRSameTowerLowerClosers.CentralCoverTargetKmodRCanonicalActionData B D E)

Canonical action transport with the inner-conjugation residual closed from K/R ~= M.

Route-ready provider avoiding the four projection residual names

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

Lower projection through the canonical same-tower quotient.

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

Projected conjugation action for the canonical lower projection, with same-class independence closed from K/R ~= M.

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

Route10 quotient-action provider that does not use the four projection semantic residual names.

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

Decoration-kernel provider through the route10 quotient-action provider.

This is the target-side provider that can replace the current route10 target branch without depending on the four projection/action residual names.

Exact replacements for the four route10 residual names

theorem Q2Presentation.Induction.TargetKmodRProjectionRoute10Proofs.centralCover_targetLowerQuotientMapData_from_projectionRoute10Proofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D)

Replacement for centralCover_targetLowerQuotientMapData, using the route10 decoration-kernel provider above to construct the explicit lower child Y/K.

theorem Q2Presentation.Induction.TargetKmodRProjectionRoute10Proofs.centralCover_targetLowerActionEquivData_from_projectionRoute10Proofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerActionEquivData B D Q)

Replacement for centralCover_targetLowerActionEquivData, induced from the canonical quotient equivalence Y/K ~= B.C.

theorem Q2Presentation.Induction.TargetKmodRProjectionRoute10Proofs.centralCover_targetKmodRRepresentativeActionData_from_projectionRoute10Proofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D P)

Replacement for centralCover_targetKmodRRepresentativeActionData.

For an externally supplied projection P, the only remaining compatibility field is the narrow assertion that P agrees with the canonical lower quotient projection.

theorem Q2Presentation.Induction.TargetKmodRProjectionRoute10Proofs.centralCover_targetKmodRConjugationClassIndependenceData_from_projectionRoute10Proofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRConjugationClassIndependenceData B D P)

Replacement for centralCover_targetKmodRConjugationClassIndependenceData, using the closed same-coset conjugation law.