Route28 target K/R bridge sidecar

Route27 leaves two broad target-side packets:

• TargetKmodRRoute27BridgeProofs.centralCover_targetRoute27LowerProjectionData;
• TargetKmodRRoute27BridgeProofs.centralCover_targetRoute27ProjectionActionData.

This sidecar replaces those names by finer manuscript-shaped packets. The lower projection is split into the concrete quotient map Y -> C = Y/K and the identification of that lower child with the abstract action group B.C. The action law is required only for one selected representative of each lower class; the all-representatives route27 action is then recovered theorem-level from the already closed inner-conjugation triviality on K/R.

Route28 lower quotient packets

structure Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerQuotientMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type 1

Route28 lower quotient-map packet.

Manuscript anchor: §7, eq:targettower (current manuscript pp. 40--42), where the lower target is C = Y/K; §8, def:Xgamma, uses this lower target for exact-image lower maps.

• lowerChild : FramedPair
• topToLower : p.fst.Y →* self.lowerChild.fst.Y
• topToLower_surj : Function.Surjective ⇑self.topToLower
• topToLower_ker : self.topToLower.ker = D.Ksub

structure Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetRoute28LowerQuotientMapData B D) : Type

Route28 lower action-group identification.

Manuscript anchor: §7, eq:targettower (current manuscript pp. 40--42): the abstract C acting on M = K/R is the concrete lower quotient target Y/K.

• lowerActionEquiv : Q.lowerChild.fst.Y ≃* B.C

def Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.lowerQuotientMapData_of_route28 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetRoute28LowerQuotientMapData B D) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D

Convert the route28 quotient-map packet to the existing semantic lower-map surface.

Equations

• Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.lowerQuotientMapData_of_route28 B D Q = { lowerChild := Q.lowerChild, topToLower := Q.topToLower, topToLower_surj := ⋯, topToLower_ker := ⋯ }

def Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.lowerActionEquivData_of_route28 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetRoute28LowerQuotientMapData B D) (E : CentralCoverTargetRoute28LowerActionEquivData B D Q) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerActionEquivData B D (lowerQuotientMapData_of_route28 B D Q)

Convert the route28 lower action equivalence to the existing semantic surface.

Equations

• Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.lowerActionEquivData_of_route28 B D Q E = { lowerActionEquiv := E.lowerActionEquiv }

def Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.lowerProjectionData_of_route28LowerPackets {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetRoute28LowerQuotientMapData B D) (E : CentralCoverTargetRoute28LowerActionEquivData B D Q) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Build the concrete lower projection Y -> B.C from the route28 lower quotient map and lower-action equivalence.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.route27LowerProjectionData_of_route28LowerPackets {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetRoute28LowerQuotientMapData B D) (E : CentralCoverTargetRoute28LowerActionEquivData B D Q) : TargetKmodRRoute27BridgeProofs.CentralCoverTargetRoute27LowerProjectionData B D

Adapter from route28 lower packets to route27's broad lower-projection surface.

Equations

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

Route28 selected-representative action packets

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

A theorem-level selected section of any concrete lower projection.

• quotientRepresentative : B.C → p.fst.Y
• lowerProjection_quotientRepresentative (c : B.C) : P.lowerProjection (self.quotientRepresentative c) = c

def Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.representativeSectionData_of_lowerProjection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : CentralCoverTargetRoute28RepresentativeSectionData B D P

The selected section exists by choice from lower-projection surjectivity.

Equations

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

structure Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : CentralCoverTargetRoute28RepresentativeSectionData B D P) : Prop

Route28 selected-representative action packet.

Manuscript anchor: §7, eq:targettower (current manuscript pp. 40--42), with M = K/R acted on by C = Y/K; §8, lem:covertransform and the elementary lifting stage use this concrete transported C-action.

• representative_action_realizes_conjugation (c : B.C) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM c) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (S.quotientRepresentative c) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

def Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.representativeActionData_of_route28 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : CentralCoverTargetRoute28RepresentativeSectionData B D P) (A : CentralCoverTargetRoute28RepresentativeActionData B D P S) : TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D P

Convert the route28 selected-representative action packet to the existing representative-action surface.

Equations

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

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

Inner-conjugation triviality gives class-independence for any lower projection whose kernel is K.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.projectedConjugationActionData_of_route28RepresentativeAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : CentralCoverTargetRoute28RepresentativeSectionData B D P) (A : CentralCoverTargetRoute28RepresentativeActionData B D P S) (I : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRInnerConjugationData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P

Assemble route27's all-representatives action law from route28's selected representative action law and theorem-level inner-conjugation triviality.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.route27ProjectionActionData_of_route28RepresentativeAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetRoute28LowerQuotientMapData B D) (E : CentralCoverTargetRoute28LowerActionEquivData B D Q) (S : CentralCoverTargetRoute28RepresentativeSectionData B D (lowerProjectionData_of_route28LowerPackets B D Q E)) (A : CentralCoverTargetRoute28RepresentativeActionData B D (lowerProjectionData_of_route28LowerPackets B D Q E) S) (I : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRInnerConjugationData B D) : TargetKmodRRoute27BridgeProofs.CentralCoverTargetRoute27ProjectionActionData B D (route27LowerProjectionData_of_route28LowerPackets B D Q E)

Adapter from route28 selected-representative action data to route27's broad projection-action surface.

Equations

• ⋯ = ⋯

Route28 residual names

axiom Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28LowerQuotientMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute28LowerQuotientMapData B D)

Route28 residual 1a: construct the concrete lower quotient map Y -> C = Y/K.

Manuscript anchor: §7, eq:targettower (current manuscript pp. 40--42); §8, def:Xgamma, exact-image lower maps.

axiom Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28LowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetRoute28LowerQuotientMapData B D) : Nonempty (CentralCoverTargetRoute28LowerActionEquivData B D Q)

Route28 residual 1b: identify the concrete lower child with the abstract action group B.C.

Manuscript anchor: §7, eq:targettower (current manuscript pp. 40--42): C = Y/K acts on M = K/R.

axiom Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.centralCover_targetRoute28RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : CentralCoverTargetRoute28RepresentativeSectionData B D P) : Nonempty (CentralCoverTargetRoute28RepresentativeActionData B D P S)

Route28 residual 2: the selected representatives of lower classes realize the abstract B.C-action on K/R.

Manuscript anchor: §7, eq:targettower (current manuscript pp. 40--42); §8, lem:covertransform / elementary lifting through the transported C-action.

Route27-compatible closures

theorem Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.centralCover_targetRoute27LowerProjectionData_from_route28 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute27BridgeProofs.CentralCoverTargetRoute27LowerProjectionData B D)

Route28 replacement for route27's lower-projection residual.

theorem Q2Presentation.Induction.TargetKmodRRoute28BridgeProofs.centralCover_targetRoute27ProjectionActionData_from_route28 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetRoute28LowerQuotientMapData B D) (E : CentralCoverTargetRoute28LowerActionEquivData B D Q) : Nonempty (TargetKmodRRoute27BridgeProofs.CentralCoverTargetRoute27ProjectionActionData B D (route27LowerProjectionData_of_route28LowerPackets B D Q E))

Route28 replacement for route27's projection-action residual, stated for route28 lower packets and their induced route27 projection packet.

Route28 provider

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

Route28 quotient-action provider.

Its axiom closure avoids both route27 residual names and replaces them by the three narrower route28 packets above.

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

Route28 replacement provider with the same downstream conclusion as route27.

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

Convenience route28 framed-quotient provider for downstream integration.