Route57 target K/R coherent projection/action bridge

Route56 exposes two target Section 8 Route39 leaves:

• identify the abstract lower action group with the literal quotient Y/K;
• prove the K/R action law for the theorem-level representatives of that literal quotient.

This sidecar leaves the routed files untouched and replaces that pair, for a new provider chain, by one coherent manuscript-shaped packet: a concrete lower projection Y -> B.C with kernel K, together with the projected conjugation action law for that same projection. The quotient equivalence Y/K ~= B.C, the Route39 literal representative law, and the Route56-compatible decoration provider are then reassembled theorem-level.

Route57 coherent residual

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

Route57 coherent concrete projection/action packet.

Manuscript anchor: Section 7, eq:targettower, with Y -> B = Y/R -> C = Y/K and M = K/R. The packet keeps the concrete lower projection and the induced action law tied together, so downstream code cannot pair an action witness with an unrelated lower quotient identification.

• lowerProjection : p.fst.Y →* B.C
• lowerProjection_surj : Function.Surjective ⇑self.lowerProjection
• lowerProjection_ker : D.Ksub = self.lowerProjection.ker
• action_realizes_projected_conjugation (y : p.fst.Y) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (self.lowerProjection y)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

axiom Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.centralCover_targetRoute57ProjectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute57ProjectionActionData B D)

Route57 target residual: one coherent concrete lower projection and projected-action packet, replacing the two Route39 leaves in the Route57 provider chain.

Transport-final adapters

def Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.lowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute57ProjectionActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Transport-final lower projection extracted from Route57 data.

Equations

• Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.lowerProjectionData B D A = { lowerProjection := A.lowerProjection, lowerProjection_surj := ⋯, lowerProjection_ker := ⋯ }

def Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.projectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute57ProjectionActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData B D A)

Route57 projected conjugation action in the transport-final surface.

Equations

• ⋯ = ⋯

Route39-compatible adapters

def Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.route39LowerQuotientIdentificationData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute57ProjectionActionData B D) : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D

Route57 induces Route39's lower quotient identification Y/K ~= B.C by the first isomorphism theorem applied to the concrete lower projection.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.route39LiteralRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute57ProjectionActionData B D) : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LiteralRepresentativeActionData B D (route39LowerQuotientIdentificationData B D A)

Route57 proves Route39's literal representative action law for the quotient identification induced by the same Route57 projection/action packet.

Equations

• ⋯ = ⋯

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

Route39 lower/action data tied to one Route57 coherent packet.

This is the replacement surface for downstream code that wants the Route39 structures explicitly but should not call the two Route39 axiom names.

• lowerData : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D
• actionData : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LiteralRepresentativeActionData B D self.lowerData

theorem Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.centralCover_targetRoute39CoherentPairData_from_route57 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute39CoherentPairData B D)

Route39 coherent lower/action pair reassembled from Route57.

theorem Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.centralCover_targetRoute39LowerQuotientIdentificationData_from_route57 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D)

Route39 lower quotient data reassembled from Route57.

theorem Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.centralCover_targetRoute39LiteralRepresentativeActionData_from_route57 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute57ProjectionActionData B D) : Nonempty (TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LiteralRepresentativeActionData B D (route39LowerQuotientIdentificationData B D A))

Route39 literal action data reassembled from the same Route57 packet.

The return type is intentionally tied to route39LowerQuotientIdentificationData for the supplied Route57 data; this avoids claiming the action law for an unrelated externally supplied equivalence.

Route54/Route56-compatible providers

def Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.route54CanonicalSelectedActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetRoute57ProjectionActionData B D) : TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData B D

Route57 data supplies Route54's canonical selected-action packet by choosing section representatives through the same Route57 projection.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute57BridgeProofs.centralCover_targetRoute54CanonicalSelectedActionData_from_route57 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData B D)

Route57 replacement for Route54's canonical selected-action packet.

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

Direct Route57 quotient-action provider through the transport-final projection/action constructor.

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

Route57 decoration-kernel provider, with the same return type as the Route56 target hook used by the active integration.

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

Convenience Route57 framed-quotient provider for downstream integration.