Route37 target K/R bridge sidecar

Route36's target provider routes through the bridge closers, whose remaining frontier is:

• TargetKmodRSameTowerBridgeClosers.centralCover_targetLowerProjectionBridgeData;
• TargetKmodRSameTowerBridgeClosers.centralCover_targetKmodRRepresentativeActionBridgeData.

This sidecar does not assert those bridge packets as axioms. Instead it uses the literal manuscript lower quotient C = Y/K and asks only for:

• the identification of that literal quotient with the abstract action group B.C;
• the representative action law for the theorem-level representatives of classes in Y/K.

The projection Y -> B.C, its kernel, the representatives over B.C, and the same-coset extension to all ambient representatives are then reassembled theorem-level. This is a strict lowering, not a full closure: the current MinimalBlock interface still stores B.C abstractly, so the manuscript identification B.C = Y/K remains real semantic data.

Route37 literal lower quotient packets

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

Route37 lower quotient identification.

Manuscript anchor: Section 7, eq:targettower, where the lower target is the literal quotient C = Y/K. Lean's MinimalBlock.C is currently abstract, so this packet supplies only the missing identification Y/K ~= B.C; the quotient map Y -> Y/K itself is theorem-level.

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

def Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.literalQuotientRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (q : p.fst.Y ⧸ D.Ksub) : p.fst.Y

The theorem-level representative of a literal quotient class in Y/K.

Equations

• Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.literalQuotientRepresentative B D q = Classical.choose ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.literalQuotientRepresentative_spec {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (q : p.fst.Y ⧸ D.Ksub) : (QuotientGroup.mk' D.Ksub) (literalQuotientRepresentative B D q) = q

The chosen literal representative maps to its quotient class.

structure Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.CentralCoverTargetRoute37LiteralRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute37LowerActionEquivData B D) : Prop

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

The representatives are not part of the residual: they are the canonical choice supplied by QuotientGroup.mk'_surjective. The only semantic content left is that the B.C action, after the quotient identification, is the conjugation action 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 (literalQuotientRepresentative B D q) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

Route37 residual declarations

axiom Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.centralCover_targetRoute37LowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute37LowerActionEquivData B D)

Route37 lower residual: identify the literal lower quotient Y/K with the abstract action group B.C.

axiom Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.centralCover_targetRoute37LiteralRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute37LowerActionEquivData B D) : Nonempty (CentralCoverTargetRoute37LiteralRepresentativeActionData B D E)

Route37 action residual: prove the representative action law for the theorem-level representatives of literal Y/K classes.

Reassembly of the current bridge packets

def Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.lowerProjectionBridgeData_of_route37LowerActionEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute37LowerActionEquivData B D) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D

The literal quotient equivalence induces the current lower projection bridge Y -> B.C with kernel K.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.centralCover_targetLowerProjectionBridgeData_from_route37 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D)

The current lower bridge residual, lowered to the literal quotient identification Y/K ~= B.C.

def Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.representativeActionBridgeData_of_route37Literal {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute37LowerActionEquivData B D) (A : CentralCoverTargetRoute37LiteralRepresentativeActionData B D E) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D (lowerProjectionBridgeData_of_route37LowerActionEquiv B D E))

Turn the literal quotient action law into the current representative bridge for the projection induced by E.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute37BridgeProofs.centralCover_targetKmodRRepresentativeActionBridgeData_from_route37 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute37LowerActionEquivData B D) : Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D (lowerProjectionBridgeData_of_route37LowerActionEquiv B D E)))

The current representative bridge residual for the Route37 projection, lowered to the literal quotient representative action packet.

Route37 provider

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

Route37 quotient-action provider.

Its axiom closure avoids the two current TargetKmodRSameTowerBridgeClosers residual names and replaces them by the Route37 literal quotient/action packets.

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

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

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

Convenience route37 framed-quotient provider for downstream integration.