Stable collar comparison

This module isolates the exact finite theorem needed to compare two externally supplied StableRegularApproximations. A stable collar is a compatible prime-equivariant generic prism whose horizontal samples are fixed to the two supplied endpoint approximations. The global signed prism-facet cancellation already proved for RelativeResult then identifies their positive-ray counts.

The theorem proved here is the finite Stokes statement for such a collar. Existence of a stable collar for arbitrary endpoint triangulations is deliberately separated as StableCollarExistenceTheorem; constructing it requires a relative triangulation/perturbation which leaves both endpoint triangulations unchanged.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar {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) : Type

A finite generic prism collar whose two horizontal boundaries are prescribed stable approximations. The boundary-fixing field includes the necessary equality of endpoint levels with the horizontal triangulation level N + L.

• N : ℕ

  The spatial subdivision level of the stable collar.

• L : ℕ

  The final prism-refinement level of the stable collar.

• m : ℝ

  The positive norm margin retained by the stable prism perturbation.

• positive : 0 < self.m
• prism : EquivariantPrismGenericPerturbation.Result hp self.N self.L H self.m

  The generic prism perturbation with the prescribed endpoint approximations.

• boundaryFixed : BoundaryFixed hp self.N self.L A₀ A₁ self.prism.assignment

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar.toRelativeResult {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} (C : StableCollar hp H A₀ A₁) : RelativeResult hp C.N C.L H C.m

Regard a stable collar as a boundary-relative prism result.

Equations

• C.toRelativeResult = { prism := C.prism, lower := A₀, upper := A₁, boundaryFixed := ⋯ }

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar.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} (C : StableCollar hp H A₀ A₁) : A₀.zeroCount = A₁.zeroCount

Finite stable-collar Stokes theorem: the two prescribed transverse horizontal boundaries have the same positive-ray count.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarExistenceTheorem : Prop

Proposition asserting that every pair of stable endpoint approximations admits a finite boundary-fixed generic collar. This is the relative-triangulation existence statement used with the finite Stokes theorem.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarComparisonTheorem : Prop

The finite collar comparison theorem, packaged as a reusable proposition.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.stableCollarComparisonTheorem : StableCollarComparisonTheorem

The stable collar comparison proposition is proved by global signed prism cancellation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.stableHomotopyInvariance_of_collarExistence (HC : StableCollarExistenceTheorem) : RefinedAffineMap.StableHomotopyInvarianceTheorem

Existence of stable collars implies the stable homotopy-invariance theorem.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeResult.toStableCollar {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) {m : ℝ} (hm : 0 < m) (R : RelativeResult hp N L H m) : StableCollar hp H R.lower R.upper

Every canonical boundary-relative result constructed from a generic prism is itself a stable collar between its two induced stable endpoint approximations.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeResult.toStableCollar hp N L H hm R = { N := N, L := L, m := m, positive := hm, prism := R.prism, boundaryFixed := ⋯ }

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.exists_canonical_stable_collar {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), Nonempty (StableCollar hp H A₀ A₁)

The existing generic-prism construction produces at least one pair of stable approximations connected by a stable collar for every zero-free equivariant homotopy.