Route39 target K/R bridge sidecar

Route38's target provider asks directly for:

• a concrete projection Y -> B.C with kernel K;
• the all-ambient projected conjugation action on K/R.

This sidecar keeps the same downstream provider shape but lowers those two Route38 names to the literal manuscript tower data:

• identify the abstract lower action group with the quotient Y/K;
• prove the action law for the theorem-level representative of each class in that quotient.

The projection Y -> B.C is then the quotient map followed by the identification, and the extension from representatives to all ambient elements uses the already closed theorem that inner conjugation by K is trivial on K/R.

Route39 manuscript-shaped packets

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

Route39 lower quotient identification.

Manuscript anchor: Section 7, eq:targettower, where the lower action target is the literal quotient C = Y/K. Since MinimalBlock.C is abstract in the current Lean interface, this is the remaining semantic identification.

• lowerActionEquiv : p.fst.Y ⧸ D.Ksub ≃* B.C

structure Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LiteralRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute39LowerQuotientIdentificationData B D) : Prop

Route39 representative action law over the literal quotient Y/K.

The representative itself is theorem-level, chosen from the quotient map. The residual content is only that representatives of the lower action classes realize B.actM by conjugation on the literal quotient K/R.

• literal_representative_action_realizes_conjugation (q : p.fst.Y ⧸ D.Ksub) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (E.lowerActionEquiv q)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (TargetKmodRRoute37BridgeProofs.literalQuotientRepresentative B D q) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

Reassembly of Route38-style projection and action data

def Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.lowerProjectionData_of_route39LowerQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute39LowerQuotientIdentificationData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The Route39 quotient identification induces the concrete lower projection Y -> B.C with kernel K.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.route38LowerProjectionData_of_route39LowerQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute39LowerQuotientIdentificationData B D) : TargetKmodRRoute38BridgeProofs.CentralCoverTargetRoute38LowerProjectionData B D

Route39 lower quotient data in the Route38 projection surface.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.representativeActionBridgeData_of_route39 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute39LowerQuotientIdentificationData B D) (A : CentralCoverTargetRoute39LiteralRepresentativeActionData B D E) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (lowerProjectionData_of_route39LowerQuotient B D E)

Convert the Route39 literal representative action law to the bridge surface that chooses one representative for each element of B.C.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.projectedConjugationActionData_of_route39 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute39LowerQuotientIdentificationData B D) (A : CentralCoverTargetRoute39LiteralRepresentativeActionData B D E) (I : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRInnerConjugationData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route39LowerQuotient B D E)

Route39 representative data plus closed inner-conjugation triviality gives the Route38 projected conjugation action law.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.route38ProjectedConjugationActionData_of_route39 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute39LowerQuotientIdentificationData B D) (A : CentralCoverTargetRoute39LiteralRepresentativeActionData B D E) (I : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRInnerConjugationData B D) : TargetKmodRRoute38BridgeProofs.CentralCoverTargetRoute38ProjectedConjugationActionData B D (route38LowerProjectionData_of_route39LowerQuotient B D E)

Route39 projected action data in the Route38 action surface.

Equations

• ⋯ = ⋯

Route39 residual declarations

axiom Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.centralCover_targetRoute39LowerQuotientIdentificationData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute39LowerQuotientIdentificationData B D)

Route39 lower residual: identify the abstract lower action group with the literal quotient Y/K from the manuscript tower.

axiom Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.centralCover_targetRoute39LiteralRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute39LowerQuotientIdentificationData B D) : Nonempty (CentralCoverTargetRoute39LiteralRepresentativeActionData B D E)

Route39 action residual: prove the action law for the theorem-level representative of each class in the literal quotient Y/K.

Route38-compatible closures

theorem Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.centralCover_targetRoute38LowerProjectionData_from_route39 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute38BridgeProofs.CentralCoverTargetRoute38LowerProjectionData B D)

Route38 lower projection reassembled from the Route39 lower quotient identification.

theorem Q2Presentation.Induction.TargetKmodRRoute39BridgeProofs.centralCover_targetRoute38ProjectedConjugationActionData_from_route39 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute39LowerQuotientIdentificationData B D) : Nonempty (TargetKmodRRoute38BridgeProofs.CentralCoverTargetRoute38ProjectedConjugationActionData B D (route38LowerProjectionData_of_route39LowerQuotient B D E))

Route38 projected action reassembled from Route39 representative action data for the lower projection induced by the same Route39 quotient identification.

Route39 provider

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

Route39 quotient-action provider.

Its closure avoids the two Route38 residual names. The remaining non-local target bridge facts are the lower quotient identification Y/K ~= B.C and the selected representative action law over that literal quotient.

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

Route39 decoration-kernel provider, drop-in compatible with the Route38 provider used by integration.

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

Convenience Route39 framed-quotient provider for downstream integration.