Same-tower semantic packets for the target K/R action

This sidecar narrows the route2 same-tower target packets to the concrete manuscript semantics:

• the lower action group is reached by one canonical projection Y -> B.C with kernel K;
• representatives for B.C realize the abstract action on M by conjugation on the literal quotient K/R;
• inner conjugation by elements of K is trivial on K/R.

The last item is the exact group-theoretic core behind "same Y/K coset representatives act identically on K/R".

Narrow semantic packets

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

The canonical lower projection Y -> B.C, with kernel the selected manuscript subgroup K.

This is the first-isomorphism-theorem form of the lower quotient assertion B.C = Y/K.

• canonicalLowerProjection : p.fst.Y →* B.C
• canonicalLowerProjection_surj : Function.Surjective ⇑self.canonicalLowerProjection
• canonicalLowerProjection_ker : D.Ksub = self.canonicalLowerProjection.ker

structure Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerEquivCompatibilityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetCanonicalLowerProjectionData B D) (E : p.fst.Y ⧸ D.Ksub ≃* B.C) : Prop

Compatibility between an externally supplied quotient equivalence Y/K ~= B.C and the canonical projection. This is needed only to reduce the legacy action packet that quantifies over an arbitrary selected equivalence.

• canonicalLowerEquiv_agrees_projection (y : p.fst.Y) : E (TargetKmodRActionProofs.lowerQuotientClass B D y) = P.canonicalLowerProjection y

structure Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRCanonicalRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetCanonicalLowerProjectionData B D) : Type

Representative-level action compatibility for the canonical lower projection. This asks only for one coherent representative per lower class.

• quotientRepresentative : B.C → p.fst.Y
• canonicalLowerProjection_quotientRepresentative (c : B.C) : P.canonicalLowerProjection (self.quotientRepresentative c) = c
• representative_action_realizes_conjugation (c : B.C) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM c) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (self.quotientRepresentative c) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

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

Inner conjugation by elements of K is trivial on the quotient K/R.

This is the precise semantic reduction of same-coset independence: changing a representative by an element of K changes the conjugating element by an inner K-conjugation, which is trivial modulo R = Phi(K).

• innerConjugation_trivial (k : p.fst.Y) : k ∈ D.Ksub → ∀ (q : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)), TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D k q = q

Theorem-level reassembly helpers

def Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.lowerProjectionData_of_canonicalProjection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetCanonicalLowerProjectionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Turn the canonical projection into the transport-final projection packet.

Equations

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

def Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.canonicalLowerActionEquiv_of_projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetCanonicalLowerProjectionData B D) : p.fst.Y ⧸ D.Ksub ≃* B.C

The canonical projection induces the quotient equivalence Y/K ~= B.C.

Equations

• Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.canonicalLowerActionEquiv_of_projection B D P = QuotientGroup.liftEquiv D.Ksub ⋯ ⋯

theorem Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.canonicalLowerActionEquiv_of_projection_apply {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetCanonicalLowerProjectionData B D) (y : p.fst.Y) : (canonicalLowerActionEquiv_of_projection B D P) (TargetKmodRActionProofs.lowerQuotientClass B D y) = P.canonicalLowerProjection y

The induced quotient equivalence sends the class of y to the canonical projection of y.

def Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.representativeActionData_of_canonicalRepresentativeAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetCanonicalLowerProjectionData B D) (A : CentralCoverTargetKmodRCanonicalRepresentativeActionData B D P) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D (lowerProjectionData_of_canonicalProjection B D P)

Convert canonical representative action data to the existing representative packet over the projection induced by P.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.quotientConjugate_eq_of_rightCoset {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (I : CentralCoverTargetKmodRInnerConjugationData B D) (y z : p.fst.Y) (h : 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

Inner-conjugation triviality implies the two-representative same-coset conjugation law.

def Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.conjugationClassIndependenceData_of_innerConjugation {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetCanonicalLowerProjectionData B D) (I : CentralCoverTargetKmodRInnerConjugationData B D) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRConjugationClassIndependenceData B D (lowerProjectionData_of_canonicalProjection B D P)

Inner-conjugation data gives the existing class-independence packet for the canonical projection induced by P.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.projectedConjugationActionData_of_semanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetCanonicalLowerProjectionData B D) (A : CentralCoverTargetKmodRCanonicalRepresentativeActionData B D P) (I : CentralCoverTargetKmodRInnerConjugationData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_canonicalProjection B D P)

Assemble the projected conjugation action from the three narrow semantic packets.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRSameTowerSemanticClosers.quotientActionData_of_semanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetCanonicalLowerProjectionData B D) (A : CentralCoverTargetKmodRCanonicalRepresentativeActionData B D P) (I : CentralCoverTargetKmodRInnerConjugationData B D) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Assemble the concrete quotient-action packet used downstream.

Equations

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

Route-ready narrow residual names

theorem Q2Presentation.Induction.centralCover_targetCanonicalLowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D)

Canonical lower projection Y -> B.C with kernel K, reduced to the literal same-tower quotient equivalence Y/K ~= B.C.

theorem Q2Presentation.Induction.centralCover_targetKmodRCanonicalRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) : Nonempty (TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRCanonicalRepresentativeActionData B D P)

Selected lower-class representatives realize the B.actM action by conjugation on K/R, reduced to the all-ambient-representatives action law.

axiom Q2Presentation.Induction.centralCover_targetCanonicalLowerEquivCompatibilityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D) (E : p.fst.Y ⧸ D.Ksub ≃* B.C) : Nonempty (TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerEquivCompatibilityData B D P E)

Narrow residual: an externally selected Y/K ~= B.C equivalence agrees with the canonical lower projection.

theorem Q2Presentation.Induction.centralCover_targetKmodRInnerConjugationData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRInnerConjugationData B D)

Inner conjugation by K is trivial on K/R, reduced to the pointwise commutator condition [K,K] <= R.

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

Quotient-action packet through the narrowed same-tower semantic closers.