Route44 target K/R bridge cleanup

Route43 leaves two target-side non-local packets:

• a literal lower quotient identification Y/K ~= B.C;
• a selected representative section of Y/K whose representatives realize the B.C-action on K/R.

This sidecar reduces both packets against the literal quotient/tower APIs. Route34 already constructs the lower quotient map Y -> Y/K theorem-level, so Route44 leaves only the identification of that literal lower child with the abstract action group B.C. Likewise, the representative section is chosen theorem-level from the induced projection; Route44 leaves only the action law for that fixed section.

Manuscript anchors:

• §7, eq:targettower: Y -> B = Y/R -> C = Y/K and M = K/R;
• §8 target quotient semantics: exact-image lower maps use the literal lower quotient and selected representatives, with same-coset independence supplied by the closed inner-conjugation theorem for K/R.

Route44 literal lower child and theorem-level section

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

Route44 lower action data.

The lower child is Route34's literal quotient target with carrier Y/K; the only remaining content is identifying that carrier with the abstract action group B.C stored in MinimalBlock.

• literalLowerActionEquiv : (TargetKmodRRoute34BridgeProofs.route34LowerChild B D).fst.Y ≃* B.C

def Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.route28LowerActionEquivData_of_route44 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerActionEquivData B D (TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 B D)

Route44 lower action data in Route28's lower-action surface.

Equations

• Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.route28LowerActionEquivData_of_route44 B D E = { lowerActionEquiv := E.literalLowerActionEquiv }

def Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.route44LowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The projection Y -> B.C induced by the literal quotient map Y -> Y/K and the Route44 lower action equivalence.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.route44RepresentativeSectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeSectionData B D (route44LowerProjectionData B D E)

The selected representative section is theorem-level from surjectivity of the Route44 lower projection.

Equations

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

structure Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.CentralCoverTargetRoute44RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) : Prop

Route44 representative action data.

This is smaller than Route43's selected-representative packet: the section is not part of the data; it is the theorem-level section above. The residual is only the manuscript action statement for those selected representatives.

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

def Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.route28RepresentativeActionData_of_route44 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) (A : CentralCoverTargetRoute44RepresentativeActionData B D E) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeActionData B D (route44LowerProjectionData B D E) (route44RepresentativeSectionData B D E)

Route44 representative action data in Route28's selected-section surface.

Equations

• ⋯ = ⋯

Route43 packets recovered theorem-level

def Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.route43LowerQuotientIdentificationData_of_route44 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) : TargetKmodRRoute43BridgeProofs.CentralCoverTargetRoute43LowerQuotientIdentificationData B D

Route44 lower action data gives Route43's literal quotient identification.

Equations

• Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.route43LowerQuotientIdentificationData_of_route44 B D E = { lowerActionEquiv := E.literalLowerActionEquiv }

def Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.route43SelectedRepresentativeActionData_of_route44 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) (A : CentralCoverTargetRoute44RepresentativeActionData B D E) : TargetKmodRRoute43BridgeProofs.CentralCoverTargetRoute43SelectedRepresentativeActionData B D (route43LowerQuotientIdentificationData_of_route44 B D E)

Route44 action data gives Route43's selected-representative packet for the Route43 lower quotient identification induced by the same Route44 data.

Equations

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

Route44 residual declarations

axiom Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.centralCover_targetRoute44LiteralLowerActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute44LiteralLowerActionData B D)

Route44 lower residual: identify Route34's literal lower child Y/K with the abstract action group B.C.

axiom Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.centralCover_targetRoute44RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) : Nonempty (CentralCoverTargetRoute44RepresentativeActionData B D E)

Route44 action residual: for the theorem-level selected section of the literal lower projection, the representatives realize the B.C-action on K/R.

Route43 leaf replacements

theorem Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.centralCover_targetRoute43LowerQuotientIdentificationData_from_route44 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute43BridgeProofs.CentralCoverTargetRoute43LowerQuotientIdentificationData B D)

Route44 replacement for the Route43 lower quotient leaf.

theorem Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.centralCover_targetRoute43SelectedRepresentativeActionData_from_route44 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) : Nonempty (TargetKmodRRoute43BridgeProofs.CentralCoverTargetRoute43SelectedRepresentativeActionData B D (route43LowerQuotientIdentificationData_of_route44 B D E))

Route44 replacement for the Route43 selected representative action leaf, for the Route43 quotient identification induced by the same Route44 lower data.

Direct Route44 provider

def Q2Presentation.Induction.TargetKmodRRoute44BridgeProofs.projectedConjugationActionData_of_route44 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute44LiteralLowerActionData B D) (A : CentralCoverTargetRoute44RepresentativeActionData B D E) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (route44LowerProjectionData B D E)

Projected conjugation action from Route44 selected representatives and the closed same-coset/inner-conjugation theorem on K/R.

Equations

• ⋯ = ⋯

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

Route44 quotient-action provider.

Its target closure no longer mentions either Route43 residual name. The remaining target-side content is the Route44 lower action identification and the Route44 fixed-section action law.

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

Route44 decoration-kernel provider, drop-in compatible with Route43's target provider call shape.

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

Convenience Route44 framed-quotient provider for downstream integration.