Documentation

Q2Presentation.Induction.TargetKmodRRoute56BridgeProofs

Route56 target K/R literal-tower bridge for the Route54 hook #

The current Route54 target provider exposes two same-tower bridge residuals:

This sidecar does not edit the integrated route. It gives a theorem-level Route54-compatible provider whose remaining target facts are Route39's literal manuscript tower packets:

Thus the projection to B.C, the kernel statement, and the chosen representatives consumed by Route54 are rebuilt theorem-level from the literal quotient map Y -> Y/K.

Route39 literal packets in the current bridge surface #

source
def Q2Presentation.Induction.TargetKmodRRoute56BridgeProofs.lowerProjectionBridgeData_of_route39 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D) :
TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D

Route39's literal quotient identification induces the current same-tower lower projection bridge Y -> B.C with kernel K.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Q2Presentation.Induction.TargetKmodRRoute56BridgeProofs.representativeActionBridgeData_of_route39 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LowerQuotientIdentificationData B D) (A : TargetKmodRRoute39BridgeProofs.CentralCoverTargetRoute39LiteralRepresentativeActionData B D E) :
    TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D (lowerProjectionBridgeData_of_route39 B D E))

    Route39's theorem-level literal representatives give the current representative-action bridge for the projection induced by the same Route39 lower quotient identification.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Q2Presentation.Induction.TargetKmodRRoute56BridgeProofs.centralCover_targetSameTowerBridgePairData_from_route56 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty ((Pbridge : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D) ×' TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D Pbridge))

      Coherent replacement pair for the two current same-tower bridge residuals.

      This is the route-facing reduction: the current projection bridge and representative-action bridge are supplied together from the Route39 literal Y/K quotient/action packets, so the action packet is tied to the same projection.

      Route54-compatible providers #

      source
      theorem Q2Presentation.Induction.TargetKmodRRoute56BridgeProofs.centralCover_targetRoute54CanonicalSelectedActionData_from_route56 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (TargetKmodRRoute54BridgeProofs.CentralCoverTargetRoute54CanonicalSelectedActionData B D)

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

      Its axiom closure avoids the two TargetKmodRSameTowerBridgeClosers residual names and exposes only the narrower Route39 literal quotient/action packets.

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

      Route56 quotient-action provider for the current target K/R branch.

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

      Route56 decoration-kernel provider, with the same return type as the current Route54 target hook.

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

      Convenience Route56 framed-quotient provider for downstream integration.