Documentation

Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers

Route63 same-tower target K/R closers #

Route62's active target hook still exposes the two broad same-tower atoms

Route48 already isolates the sharper manuscript packet: one coherent projection Y -> B.C with kernel K, together with the representative action law for the same projection. This sidecar gives that sharper packet Route63 names and exports the same downstream shape used by Route60's decoration-kernel provider.

Coherent Route63 packet #

source
structure Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.CentralCoverTargetRoute63SameTowerData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
Type

Route63 coherent same-tower data.

This packages the literal lower projection Y -> C = Y/K, the induced identification Y/K ~= B.C, and the ambient action law for that same selected projection. Its route-ready construction is supplied by Route48's single coherent projection/action residual.

Instances For
    source
    def Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.sameTowerData_of_route48 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : TargetKmodRRoute48BridgeProofs.CentralCoverTargetRoute48ProjectionActionData B D) :
    CentralCoverTargetRoute63SameTowerData B D

    Route63 same-tower data extracted from the sharper Route48 coherent packet.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.centralCover_targetRoute63SameTowerData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (CentralCoverTargetRoute63SameTowerData B D)

      Route63 replacement for the two broad Route62 same-tower atoms, reduced to Route48's one coherent projection/action packet.

      Same-tower and projection/action surfaces #

      source
      theorem Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.centralCover_targetLowerProjectionData_from_route63 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D)

      Route63 lower-projection provider.

      source
      theorem Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.centralCover_targetCanonicalLowerQuotientEquivData_from_route63 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
      Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D)

      Route63 provider for the actual same-tower lower-quotient equivalence.

      source
      theorem Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.centralCover_targetKmodRAmbientActionData_from_route63 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute63SameTowerData B D) :
      Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D H.lowerProjectionData)

      Route63 provider for the actual same-tower ambient action, tied to the Route63-selected lower projection.

      source
      def Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.projectedConjugationActionData_of_route63 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute63SameTowerData B D) :
      TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D H.lowerProjectionData

      The projected action packet obtained from Route63 same-tower data.

      Equations
      • ⋯ = ⋯
      Instances For
        source
        structure Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.CentralCoverTargetRoute63ProjectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
        Type

        Route63 projection/action packet, mirroring the useful Route60 downstream shape while depending on the single coherent Route48 residual.

        Instances For
          source
          def Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.projectionActionData_of_route63 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute63SameTowerData B D) :
          CentralCoverTargetRoute63ProjectionActionData B D

          Repackage Route63 same-tower data as a projection/action packet.

          Equations
          Instances For
            source
            theorem Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.centralCover_targetRoute63ProjectionActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
            Nonempty (CentralCoverTargetRoute63ProjectionActionData B D)

            Route63 route-ready projection/action provider.

            Downstream providers #

            source
            def Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.quotientActionData_of_route63 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute63ProjectionActionData B D) :
            TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

            Route63 quotient-action provider.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Q2Presentation.Induction.TargetKmodRRoute63SameTowerClosers.centralCover_targetKmodRQuotientActionData_from_route63 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
              Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

              Route63 replacement for the target K/R quotient-action hook.

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

              Route63 decoration-kernel provider, drop-in compatible with the Route60 integration-side target hook.

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

              Convenience Route63 framed-quotient provider for downstream integration.