Documentation

Q2Presentation.Induction.TargetKmodRRoute17BridgeProofs

Route17 target K/R bridge proofs #

This sidecar keeps route16's target bridge surface but supplies theorem-level providers for the two same-tower bridge leaves:

The lower projection bridge is assembled from the projection-semantic lower quotient map and lower-action equivalence. The representative bridge is assembled directly from the representative-level action packet. Thus the route17 quotient-action theorem avoids the two route16 bridge residual names and reduces them to strictly narrower manuscript-shaped packets.

Bridge adapters #

source
def Q2Presentation.Induction.TargetKmodRRoute17BridgeProofs.lowerProjectionBridgeData_of_projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) :
TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D

Convert the projection-semantic lower projection packet to the route16 same-tower bridge shape.

Equations
Instances For
    source
    def Q2Presentation.Induction.TargetKmodRRoute17BridgeProofs.representativeActionBridgeData_of_projectionRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D P) :
    TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D P

    Convert the projection-semantic representative-action packet to the route16 same-tower bridge representative shape.

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

      Route17 providers for the two route16 bridge leaves #

      source
      theorem Q2Presentation.Induction.TargetKmodRRoute17BridgeProofs.centralCover_targetLowerProjectionBridgeData_from_route17 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D)

      Route17 provider for the lower-projection bridge leaf.

      Remaining assumptions are the projection-semantic lower quotient map centralCover_targetLowerQuotientMapData and lower-action equivalence centralCover_targetLowerActionEquivData, not the route16 bridge axiom.

      source
      theorem Q2Presentation.Induction.TargetKmodRRoute17BridgeProofs.centralCover_targetKmodRRepresentativeActionBridgeData_from_route17 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) :
      Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D P)

      Route17 provider for the representative-action bridge leaf.

      Remaining assumption is the representative-level action packet centralCover_targetKmodRRepresentativeActionData, not the route16 bridge axiom.

      Route-ready downstream assembly #

      source
      theorem Q2Presentation.Induction.TargetKmodRRoute17BridgeProofs.centralCover_targetKmodRQuotientActionData_from_route17 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

      Target quotient-action packet through the route17 bridge providers.

      This removes both route16 bridge residual names from the target K/R branch. The same-coset independence step is supplied by the theorem-level inner conjugation closure from K/R ~= M.

      source
      theorem Q2Presentation.Induction.TargetKmodRRoute17BridgeProofs.centralCover_targetDecorationKernelData_from_route17 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (CentralCoverTargetDecorationKernelData B D)

      Decoration-kernel provider through route17 target K/R quotient action.

      source
      theorem Q2Presentation.Induction.TargetKmodRRoute17BridgeProofs.centralCover_targetCanonicalFramedQuotientData_from_route17 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

      Convenience framed-quotient provider downstream of route17.