Documentation

LeanPool.NandakumarRamanaRao.NRR.PrimePolyhedron.FoxNeuwirth.StableExactRelativeCollarConstructionAffinePullback

Exact relative stable collar from the affine-pullback Route B perturbation #

This module packages the concrete Route B assignment on the Step 4 affine-pullback collar into the exact relative-collar interface consumed by finite affine Stokes.

The construction uses the focused Route B API rather than repeating the perturbation selection:

source
def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.certificateTolerance :
ℝ

A fixed positive tolerance used to select one exact-collar perturbation. The exact certificate records no quantitative upper bound, so the value 1 is sufficient.

Equations
Instances For
    source
    theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.certificateTolerance_pos :
    0 < certificateTolerance

    Positivity of the canonical certificate tolerance.

    source
    noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.selectedRouteBResult {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
    ExplicitAffineRelativeCollar.RouteB.SmallGenericPerturbationResult hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment certificateTolerance (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).margin

    The canonical Route B result used by the exact collar certificate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.perturbedAssignment {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
      ExplicitAffineRelativeCollar.Parameters.Assignment hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells

      The full assignment selected by Route B on the concrete affine-pullback collar.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.perturbedAssignment_eq_assignmentOfMovableParameters {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
        perturbedAssignment hp F₀ F₁ H A₀ A₁ = ExplicitAffineRelativeCollar.RouteB.assignmentOfMovableParameters hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment (selectedRouteBResult hp F₀ F₁ H A₀ A₁).move

        The selected assignment is the assignment reconstructed from the selected Route B move.

        source
        theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.perturbedAssignment_horizontalVertexFixed {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
        ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar (perturbedAssignment hp F₀ F₁ H A₀ A₁)

        Movable replacement preserves both supplied endpoint assignments exactly.

        source
        theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.perturbedAssignment_positiveRayGeneralPosition {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) (q : (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells.Cell) :
        AffinePositiveRayBoundary.VertexMap.PositiveRayGeneralPosition hp (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (perturbedAssignment hp F₀ F₁ H A₀ A₁) q)

        Route B supplies positive-ray general position for every cell of the selected collar.

        source
        noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.exactRelativeStableCollarGeneralPositionDataAffinePullback {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
        StableCollarRelativeSubdivisionExact.ExactRelativeStableCollarGeneralPositionData hp H A₀ A₁

        The concrete Route B perturbation, packaged with exact endpoints and cellwise positive-ray general position.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.exactRelativeStableCollarDataAffinePullback {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
          StableCollarRelativeSubdivisionExact.ExactRelativeStableCollarData hp H A₀ A₁

          Exact local-Stokes collar data obtained from the positive-ray-general-position package.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.exactRelativeStableCollarData_affinePullback_horizontalVertexFixed {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
            ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ (exactRelativeStableCollarDataAffinePullback hp F₀ F₁ H A₀ A₁).collar (exactRelativeStableCollarDataAffinePullback hp F₀ F₁ H A₀ A₁).assignment

            The exact certificate retains the endpoint assignments literally.

            source
            theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.exactRelativeStableCollarData_affinePullback_localPositiveRayStokes {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
            ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.LocalPositiveRayStokes hp (exactRelativeStableCollarDataAffinePullback hp F₀ F₁ H A₀ A₁).collar.toFoxNeuwirthRelativeAffineCollar (exactRelativeStableCollarDataAffinePullback hp F₀ F₁ H A₀ A₁).assignment

            The exact certificate supplies the local positive-ray Stokes identity on every cell.

            source
            theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.exactRelativeStableCollarData_affinePullback_zeroCount_eq {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
            A₀.zeroCount = A₁.zeroCount

            The exact certificate identifies the two stable endpoint counts.

            source
            theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.exactRelativeStableCollarConstruction_affinePullback :
            StableCollarRelativeSubdivisionExact.ExactRelativeStableCollarConstructionTheorem

            The exact relative stable-collar construction proposition is inhabited by the concrete affine-pullback collar followed by the unconditional Route B perturbation.

            source
            theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableExactRelativeCollarConstructionAffinePullback.stableHomotopyInvariance_affinePullback :
            RefinedAffineMap.StableHomotopyInvarianceTheorem

            Immediate stable-homotopy invariance consequence of the exact collar construction.