Necessary conditions for arbitrary stable-collar existence

The concrete StableCollar developed by the prism modules uses one standard refined prism PrismCell hp N L. Consequently both horizontal boundaries are represented on the same barycentric level N + L. Moreover the prism result carries the strong condition AvoidsCodimTwoDeviationZero; when restricted to a horizontal facet this excludes every deviation-zero point on the endpoint subdivision skeleton, independently of the sign of the common coordinate mean.

The public StableRegularApproximation interface is weaker in both respects:

• two supplied approximations may have different levels;
• PositiveRaySkeletonFree excludes only positive-ray intersections on the skeleton.

This file records the two necessary consequences of an existing concrete collar. They show that StableCollarExistenceTheorem, as currently stated for arbitrary stable approximations, cannot be constructed from the available hypotheses. A genuine arbitrary-endpoint theorem needs a relative prism complex with independent lower and upper triangulations, and a boundary version of the local affine theorem requiring only positive-ray skeleton transversality.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar.lower_level_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₀.level = C.N + C.L

Both endpoint triangulations of a concrete standard-prism collar necessarily have the common level N + L.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar.upper_level_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₁.level = C.N + C.L

Upper endpoint version of lower_level_eq.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar.endpoint_levels_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₀.level = A₁.level

A concrete standard-prism stable collar can only connect approximations living on the same barycentric level.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar.lower_value_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₁) (q : RefinedAffineMap.TopCell hp (C.N + C.L)) (w : StandardSimplex (p - 1)) : RefinedAffineMap.value hp (C.N + C.L) A₀.map q w = RefinedAffineMap.value hp (C.N + C.L) (endpointInterpolant hp C.N C.L EndpointSide.lower C.prism.assignment) q w

Equality of the lower endpoint affine interpolation with the lower horizontal interpolant of the collar assignment.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar.upper_value_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₁) (q : RefinedAffineMap.TopCell hp (C.N + C.L)) (w : StandardSimplex (p - 1)) : RefinedAffineMap.value hp (C.N + C.L) A₁.map q w = RefinedAffineMap.value hp (C.N + C.L) (endpointInterpolant hp C.N C.L EndpointSide.upper C.prism.assignment) q w

Upper endpoint analogue of lower_value_eq.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar.lower_deviationSkeletonFree_at_collarLevel {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₁) : DeviationSkeletonFree hp (C.N + C.L) A₀.map

The lower boundary of a concrete collar satisfies sign-independent deviation-skeleton transversality.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollar.upper_deviationSkeletonFree_at_collarLevel {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₁) : DeviationSkeletonFree hp (C.N + C.L) A₁.map

The upper boundary of a concrete collar satisfies sign-independent deviation-skeleton transversality.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.collarExistence_implies_endpoint_level_alignment (HC : StableCollarExistenceTheorem) {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₀.level = A₁.level

The currently stated arbitrary collar-existence theorem would force every supplied endpoint pair to have equal subdivision levels. This consequence is absent from its hypotheses and is the first structural obstruction to proving it with StableCollar.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.collarExistence_implies_lower_deviationSkeletonFree (HC : StableCollarExistenceTheorem) {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) : DeviationSkeletonFree hp A₀.level A₀.map

The currently stated arbitrary collar-existence theorem would also force every lower endpoint to satisfy the stronger sign-independent skeleton condition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.collarExistence_implies_upper_deviationSkeletonFree (HC : StableCollarExistenceTheorem) {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) : DeviationSkeletonFree hp A₁.level A₁.map

Upper endpoint version of collarExistence_implies_lower_deviationSkeletonFree.