Final target K/R quotient-action closers

This sidecar further decomposes the current final-closure residual centralCover_targetKmodRQuotientActionData.

Manuscript anchors:

• §7, eq:targettower: B = Y/R, C = Y/K, and M = K/R;
• §8, lem:decorationblock: the abstract C-action on M must be the right-conjugation action on the concrete quotient K/R.

The current concrete target packet already carries R <= K <= L_Y and K/R ~= M. What it does not yet expose is:

• that the abstract lower action group B.C is the concrete quotient Y/K;
• that B.actM, transported across K/R ~= M, is right conjugation by representatives in Y.

Those are recorded below as two smaller residuals and then reassembled into the existing quotient-action packet consumed by TargetKmodRActionProofs.

The two final semantic packets

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

The abstract lower group B.C is the actual quotient Y/K.

This is the lower-group part of §7 eq:targettower, separated from the action transport law below so quotient-target bookkeeping and module-action bookkeeping can be closed independently.

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

structure Q2Presentation.Induction.TargetKmodRQuotientActionFinalClosers.CentralCoverTargetKmodRActionTransportData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (L : CentralCoverTargetLowerQuotientEquivData B D) : Prop

The abstract action B.actM is right conjugation on the concrete quotient K/R, after transporting through the selected Y/K ~= B.C and K/R ~= M identifications.

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

Reassembly to the current packet

def Q2Presentation.Induction.TargetKmodRQuotientActionFinalClosers.quotientActionData_of_lowerEquivTransport {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (L : CentralCoverTargetLowerQuotientEquivData B D) (A : CentralCoverTargetKmodRActionTransportData B D L) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Assemble the existing quotient-action packet from the lower quotient identification and the transported conjugation action law.

Equations

• Q2Presentation.Induction.TargetKmodRQuotientActionFinalClosers.quotientActionData_of_lowerEquivTransport B D L A = { lowerQuotientEquiv := L.lowerQuotientEquiv, action_realizes_conjugation := ⋯ }

Residual names for final integration

axiom Q2Presentation.Induction.centralCover_targetLowerQuotientEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRQuotientActionFinalClosers.CentralCoverTargetLowerQuotientEquivData B D)

Smaller residual: identify the lower action group with the concrete quotient Y/K.

axiom Q2Presentation.Induction.centralCover_targetKmodRActionTransportData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (L : TargetKmodRQuotientActionFinalClosers.CentralCoverTargetLowerQuotientEquivData B D) : Nonempty (TargetKmodRQuotientActionFinalClosers.CentralCoverTargetKmodRActionTransportData B D L)

Smaller residual: prove the K/R action transport law for the selected Y/K ~= B.C quotient identification.

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

Replacement for centralCover_targetKmodRQuotientActionData, assembled from the two smaller final packets.

Route-ready consequences mirroring TargetKmodRActionProofs

theorem Q2Presentation.Induction.centralCover_targetKmodRActionCompatibilityData_from_finalClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationCanonicalInvarianceProofs.CentralCoverTargetKmodRActionCompatibilityData B D)

The older action-compatibility packet follows from the final quotient-action closers without using centralCover_targetKmodRQuotientActionData.

theorem Q2Presentation.Induction.centralCover_targetDecorationCanonicalInvarianceData_from_finalClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationActualDescentProofs.CentralCoverTargetDecorationCanonicalInvarianceData B D)

Canonical target-decoration invariance through the final quotient-action closers.

theorem Q2Presentation.Induction.centralCover_targetDecorationActualDescentData_from_finalClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationBlockMapActualProofs.CentralCoverTargetDecorationActualDescentData B D)

Actual target-decoration descent through the final quotient-action closers.

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

Decoration-kernel closure through the final quotient-action closers.

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

Canonical framed quotient closure through the final quotient-action closers.