Route38 target K/R bridge sidecar

Route37 lowered the target bridge to the literal quotient Y/K and the action of theorem-level representatives of classes in that quotient. This sidecar keeps the same downstream provider, but removes the two Route37 residual names from its closure.

The remaining Route38 packets are the manuscript-shaped quotient-action facts:

• a concrete projection Y -> B.C whose kernel is K, i.e. the abstract lower action group is reached from the literal lower target C = Y/K;
• the projected action law saying that the B.C-action on M = K/R is actual right conjugation on the literal quotient K/R.

This does not honestly close the lower quotient identification, because MinimalBlock.C is still an abstract field. Route38 records the needed provenance as a concrete projection, then derives the Route37 literal quotient equivalence by the first isomorphism theorem.

Route38 manuscript-shaped packets

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

Route38 lower projection packet.

Manuscript anchor: Section 7, eq:targettower, where the lower target is C = Y/K. Since MinimalBlock.C is an abstract field, this packet supplies the concrete projection to that abstract lower action group, 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.TargetKmodRRoute38BridgeProofs.lowerProjectionData_of_route38 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute38LowerProjectionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Convert Route38 lower projection data to the transport-final projection packet.

Equations

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

structure Q2Presentation.Induction.TargetKmodRRoute38BridgeProofs.CentralCoverTargetRoute38ProjectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute38LowerProjectionData B D) : Prop

Route38 projected action packet.

Manuscript anchor: Section 7, eq:targettower, and Section 8 target induction: the action of C = Y/K on M = K/R is induced by right conjugation in the ambient finite target.

• action_realizes_projected_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.TargetKmodRRoute38BridgeProofs.projectedConjugationActionData_of_route38 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute38LowerProjectionData B D) (A : CentralCoverTargetRoute38ProjectedConjugationActionData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route38 B D P)

Convert Route38 projected action data to the transport-final projected action packet.

Equations

• ⋯ = ⋯

Route37 residuals derived from Route38 packets

def Q2Presentation.Induction.TargetKmodRRoute38BridgeProofs.route37LowerActionEquivData_of_route38LowerProjection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute38LowerProjectionData B D) : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LowerActionEquivData B D

The Route38 concrete projection induces Route37's literal quotient identification Y/K ~= B.C.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute38BridgeProofs.route37LiteralRepresentativeActionData_of_route38ProjectedAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute38LowerProjectionData B D) (A : CentralCoverTargetRoute38ProjectedConjugationActionData B D P) : TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LiteralRepresentativeActionData B D (route37LowerActionEquivData_of_route38LowerProjection B D P)

Route38's projected action law gives Route37's representative action law for the quotient equivalence induced by the same Route38 projection.

Equations

• ⋯ = ⋯

Route38 residual declarations

axiom Q2Presentation.Induction.TargetKmodRRoute38BridgeProofs.centralCover_targetRoute38LowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute38LowerProjectionData B D)

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

axiom Q2Presentation.Induction.TargetKmodRRoute38BridgeProofs.centralCover_targetRoute38ProjectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute38LowerProjectionData B D) : Nonempty (CentralCoverTargetRoute38ProjectedConjugationActionData B D P)

Route38 action residual: prove the projected C = Y/K action law on K/R, with no selected representative section.

theorem Q2Presentation.Induction.TargetKmodRRoute38BridgeProofs.centralCover_targetRoute37LowerActionEquivData_from_route38 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LowerActionEquivData B D)

Route37 lower quotient residual, reassembled from Route38 projection data.

theorem Q2Presentation.Induction.TargetKmodRRoute38BridgeProofs.centralCover_targetRoute37LiteralRepresentativeActionData_from_route38 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute38LowerProjectionData B D) : Nonempty (TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LiteralRepresentativeActionData B D (route37LowerActionEquivData_of_route38LowerProjection B D P))

Route37 literal representative action residual, reassembled for the Route37 equivalence induced by a Route38 projection.

Route38 provider

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

Route38 quotient-action provider.

Its closure avoids the two Route37 residual names and uses the concrete projection plus projected conjugation action packets directly.

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

Route38 decoration-kernel provider, drop-in compatible with Route37's exported target provider.

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

Convenience route38 framed-quotient provider for downstream integration.