Actual same-tower closers for the target K/R action

This sidecar keeps the current target K/R surface tied to the literal manuscript tower

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

It does not construct that tower. Instead it records the strictly smaller pieces needed by TargetKmodRSameTowerSemanticClosers:

• an equivalence from the literal lower quotient Y/K to the abstract action group B.C;
• an all-representatives action law, avoiding a separate representative section;
• the group-theoretic condition [K,K] <= R, stated pointwise, from which inner conjugation by K is theorem-level trivial on K/R.

Lower quotient and projection

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

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

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

def Q2Presentation.Induction.TargetKmodRSameTowerActualClosers.lowerProjectionData_of_lowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetCanonicalLowerQuotientEquivData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Build the canonical lower projection Y -> B.C from Y/K ~= B.C.

Equations

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

Ambient action law

structure Q2Presentation.Induction.TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Prop

The abstract B.C action is literal conjugation on K/R for every ambient representative y : Y.

This is smaller than a representative-section packet: no choice of section is part of the data.

• ambient_action_realizes_conjugation (y : p.fst.Y) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (P.lowerProjection y)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

def Q2Presentation.Induction.TargetKmodRSameTowerActualClosers.projectedConjugationActionData_of_ambientAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : CentralCoverTargetKmodRAmbientActionData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P

Convert the all-representatives action law to the existing projected-action packet.

Equations

• ⋯ = ⋯

Inner conjugation from [K,K] <= R

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

Pointwise form of [K,K] <= R for the selected manuscript tower.

With the manuscript right-conjugation convention, this says k⁻¹ * x * k and x have the same image in K/R.

• conjugation_commutator_mem_R (k x : p.fst.Y) : k ∈ D.Ksub → x ∈ D.Ksub → k⁻¹ * x * k * x⁻¹ ∈ D.Rsub

theorem Q2Presentation.Induction.TargetKmodRSameTowerActualClosers.quotientConjugate_eq_self_of_commutatorInR {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (C : CentralCoverTargetKmodRCommutatorInRData B D) (k : p.fst.Y) (hk : k ∈ D.Ksub) (q : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)) : TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D k q = q

If [K,K] <= R, then right conjugation by an element of K is trivial on the literal quotient K/R.

Route-ready smaller residuals

axiom Q2Presentation.Induction.TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalLowerQuotientEquivData B D)

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

axiom Q2Presentation.Induction.TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (CentralCoverTargetKmodRAmbientActionData B D P)

Smaller residual: the all-ambient-representatives B.C action law on K/R, for a selected lower projection.

axiom Q2Presentation.Induction.TargetKmodRSameTowerActualClosers.centralCover_targetKmodRCommutatorInRData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetKmodRCommutatorInRData B D)

Smaller residual: pointwise commutators of K lie in R.