Same-tower lower K/R closers

This sidecar targets the four current Section 8 lower target K/R packets:

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

The direct quotient-map construction is theorem-level once the decoration kills K, because the canonical lower child is literally Y/K. The action side is reduced to same-tower provenance: the abstract lower group B.C is the canonical quotient Y/K, B.actM is the transported conjugation action through that quotient, and conjugation on K/R only depends on the lower quotient coset.

Canonical same-tower residuals

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

Same-tower lower quotient identification: the abstract action group B.C is the canonical quotient Y/K.

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

structure Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.CentralCoverTargetKmodRCanonicalActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetCanonicalLowerActionEquivData B D) : Prop

Same-tower action transport: with the canonical Y/K ~= B.C identification, the abstract action B.actM is conjugation on K/R.

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

structure Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.CentralCoverTargetLowerProjectionCanonicalCompatibilityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (E : CentralCoverTargetCanonicalLowerActionEquivData B D) : Prop

Compatibility of an arbitrary concrete projection with the canonical same-tower quotient equivalence. This is only needed when closing the existing packet that quantifies over an externally supplied projection P.

• lowerProjection_eq_canonical (y : p.fst.Y) : P.lowerProjection y = E.canonicalLowerActionEquiv (TargetKmodRActionProofs.lowerQuotientClass B D y)

structure Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.CentralCoverTargetKmodRSameCosetConjugationData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Prop

Same-coset conjugation on the literal quotient K/R. This strips the class-independence packet down to the group-theoretic statement that right conjugation by representatives in the same Y/K coset agrees on K/R.

• quotientConjugate_eq_of_rightCoset (y z : p.fst.Y) : y * z⁻¹ ∈ D.Ksub → ∀ (q : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)), TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y q = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D z q

Theorem-level quotient and projection bookkeeping

def Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.lowerQuotientMapData_of_decorationKernel {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D

Construct the current lower quotient-map packet from the explicit framed quotient target Y/K.

Equations

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

def Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.lowerActionEquivData_of_canonicalEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D) (E : CentralCoverTargetCanonicalLowerActionEquivData B D) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerActionEquivData B D Q

The lower action equivalence for any lower child with kernel K, induced through the canonical quotient Y/K.

Equations

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

def Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.lowerProjectionData_of_canonicalEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetCanonicalLowerActionEquivData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The canonical lower projection Y -> B.C induced by Y -> Y/K and the same-tower quotient equivalence.

Equations

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

def Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.lowerProjectionCanonicalCompatibilityData_of_canonicalEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetCanonicalLowerActionEquivData B D) : CentralCoverTargetLowerProjectionCanonicalCompatibilityData B D (lowerProjectionData_of_canonicalEquiv B D E) E

The canonical projection is definitionally compatible with its same-tower quotient equivalence.

Equations

• ⋯ = ⋯

Reassembly of the existing action packets

def Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.representativeActionData_of_canonicalAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (E : CentralCoverTargetCanonicalLowerActionEquivData B D) (C : CentralCoverTargetLowerProjectionCanonicalCompatibilityData B D P E) (A : CentralCoverTargetKmodRCanonicalActionData B D E) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D P

Representative-level action compatibility from canonical action transport plus compatibility of the selected projection with the canonical quotient.

Equations

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

def Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.conjugationClassIndependenceData_of_sameCoset {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (I : CentralCoverTargetKmodRSameCosetConjugationData B D) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRConjugationClassIndependenceData B D P

Current class-independence packet from the same-coset conjugation datum.

Equations

• ⋯ = ⋯

Route-ready residual names

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

Identify the abstract lower action group with the canonical quotient Y/K, reduced to the canonical projection packet.

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

The canonical Y/K action on K/R is the abstract action B.actM, reduced to a canonical projection, representative action, projection/equivalence compatibility, and inner K-conjugation triviality.

axiom Q2Presentation.Induction.TargetKmodRSameTowerLowerClosers.centralCover_targetLowerProjectionCanonicalCompatibilityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (E : CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (CentralCoverTargetLowerProjectionCanonicalCompatibilityData B D P E)

Narrow residual: an externally selected projection agrees with the canonical lower quotient map.

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

Same-coset representatives act identically on K/R, reduced to inner K-conjugation triviality on K/R.

Replacement theorems for the four current packets

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

Replacement for centralCover_targetLowerQuotientMapData, using the explicit framed quotient child Y/K.

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

Replacement for centralCover_targetLowerActionEquivData, reduced to the canonical same-tower quotient equivalence Y/K ~= B.C.

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

Replacement for centralCover_targetKmodRRepresentativeActionData, reduced to canonical action transport plus compatibility of the selected projection with the canonical lower quotient.

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

Replacement for centralCover_targetKmodRConjugationClassIndependenceData, reduced to same-coset conjugation on the literal quotient K/R.

Direct same-tower quotient-action route

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

Lower projection from the canonical Y/K ~= B.C equivalence, avoiding the two current lower quotient-map/action-equivalence packet axioms.

theorem Q2Presentation.Induction.centralCover_targetKmodRProjectedConjugationActionData_from_sameTowerLowerClosers {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, avoiding the two current representative/class-independence packet axioms.

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

Quotient-action packet through the canonical same-tower lower projection and canonical conjugation action.