Bridge closers for the same-tower target K/R packets

This sidecar replaces the two current actual same-tower target residuals by strictly lower manuscript-shaped data:

• a concrete lower projection Y -> B.C with kernel K;
• one representative of each lower class whose action realizes conjugation on the literal quotient K/R.

The all-ambient-representatives action law is then theorem-level: changing a representative inside the same Y/K coset is inner conjugation by an element of K, and that has already been closed from the realized bridge K/R ~= M.

Lower bridge packets

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

Manuscript-shaped lower projection data: the abstract lower action group B.C is reached by the concrete quotient map with kernel K.

• lowerProjection : p.fst.Y →* B.C
• lowerProjection_surj : Function.Surjective ⇑self.lowerProjection
• lowerProjection_ker : D.Ksub = self.lowerProjection.ker

def Q2Presentation.Induction.TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionBridgeData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Convert bridge projection data to the transport-final projection packet.

Equations

• Q2Presentation.Induction.TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D P = { lowerProjection := P.lowerProjection, lowerProjection_surj := ⋯, lowerProjection_ker := ⋯ }

def Q2Presentation.Induction.TargetKmodRSameTowerBridgeClosers.canonicalLowerQuotientEquivData_of_bridge {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionBridgeData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

The lower projection induces the actual same-tower quotient equivalence Y/K ~= B.C by the first isomorphism theorem.

Equations

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

Representative action bridge

structure Q2Presentation.Induction.TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Type

Single-representative action law. This is strictly weaker than the ambient law because it asks for one representative per lower class, not every ambient representative.

• quotientRepresentative : B.C → p.fst.Y
• lowerProjection_quotientRepresentative (c : B.C) : P.lowerProjection (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))

def Q2Presentation.Induction.TargetKmodRSameTowerBridgeClosers.projectedConjugationActionData_of_representativeBridge {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : CentralCoverTargetKmodRRepresentativeActionBridgeData B D P) (I : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRInnerConjugationData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P

A representative action law plus closed inner-conjugation triviality gives the projected all-representatives conjugation action.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRSameTowerBridgeClosers.ambientActionData_of_representativeBridge {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : CentralCoverTargetKmodRRepresentativeActionBridgeData B D P) (I : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRInnerConjugationData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D P

The same theorem-level conversion, stated in the actual ambient packet's surface form.

Equations

• ⋯ = ⋯

Route-ready residual names

axiom Q2Presentation.Induction.TargetKmodRSameTowerBridgeClosers.centralCover_targetLowerProjectionBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetLowerProjectionBridgeData B D)

Lower residual: construct the concrete projection Y -> B.C with kernel K.

axiom Q2Presentation.Induction.TargetKmodRSameTowerBridgeClosers.centralCover_targetKmodRRepresentativeActionBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (CentralCoverTargetKmodRRepresentativeActionBridgeData B D P)

Lower residual: choose one representative in each lower class and prove that representative's action on K/R realizes the abstract B.C action.

theorem Q2Presentation.Induction.TargetKmodRSameTowerBridgeClosers.centralCover_targetCanonicalLowerQuotientEquivData_from_bridgeClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D)

Replacement for the actual quotient-equivalence residual, reduced to the lower projection bridge.

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

Replacement for the actual all-ambient-representatives action law, reduced to the single-representative bridge and the already closed inner-conjugation theorem.

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

Direct quotient-action route avoiding both actual same-tower residuals.

The remaining non-local facts are the lower projection bridge and the single-representative action bridge.