Documentation

Q2Presentation.Induction.TargetKmodRRoute211BridgeLoweringClosers

Route211 target bridge lowering #

This sidecar is a Route210-compatible target provider that does not use the two same-tower bridge residual axioms

Instead it routes the target K/R decoration-kernel packet through the already available Route146 literal same-tower quotient/action surface:

The projection Y → B.C, its kernel, the selected representatives, and the upgrade to quotient-action data are theorem-level reassembly from that literal quotient/action surface.

source
@[reducible, inline]
abbrev Q2Presentation.Induction.TargetKmodRRoute211BridgeLoweringClosers.CentralCoverTargetRoute211LoweredBridgeSurfaceData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
Type

Route211 lowered bridge surface: the literal lower quotient Y/K ≃ B.C and the literal representative-action law, tied to the same quotient identification.

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

    The Route211 lowered bridge surface is exactly the Route146 literal quotient/action surface already present in the project.

    source
    def Q2Presentation.Induction.TargetKmodRRoute211BridgeLoweringClosers.lowerProjectionBridgeData_of_route211LoweredSurface {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute211LoweredBridgeSurfaceData B D) :
    TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D

    Route210's lower-projection bridge packet, assembled without the Route210 bridge residual axiom from the literal lower quotient equivalence.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Q2Presentation.Induction.TargetKmodRRoute211BridgeLoweringClosers.representativeActionBridgeData_of_route211LoweredSurface {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute211LoweredBridgeSurfaceData B D) :
      TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D (lowerProjectionBridgeData_of_route211LoweredSurface B D H))

      Route210's representative-action bridge packet, assembled without the Route210 representative bridge residual axiom from the literal representative action law.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Q2Presentation.Induction.TargetKmodRRoute211BridgeLoweringClosers.quotientActionData_of_route211LoweredSurface {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute211LoweredBridgeSurfaceData B D) :
        TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

        Direct quotient-action data from the Route211 lowered bridge surface.

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

          Drop-in target quotient-action provider for Route211. Its target-side non-local leaves are the two Route146 literal quotient/action atoms, not the two Route210 same-tower bridge residuals.

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

          Drop-in target decoration-kernel provider for the Route210 target slot, strictly lowering the target bridge residuals to the Route146 literal quotient and literal representative-action atoms.

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

          Convenience framed-quotient provider downstream of the Route211 target lowering.