Stable homotopy-invariant positive-ray obstruction

The raw refined count is not invariant under arbitrary subdivision: a positive-ray intersection can move onto a triangulation face and disappear from the relative-interior count. This module is the stable obstruction API. It uses StableRegularApproximation, whose positive-ray intersections avoid the endpoint skeleton.

Existence of a stable approximation follows from the generic boundary-relative prism construction applied to the reflexive homotopy. The negative reference has an explicit stable level-zero approximation. The reference-specific input is packaged as PositiveReferenceStableTheorem: a stable approximation of the positive reference with the known nonzero orbit count. This obligation is strictly smaller than, and does not imply, the invalid raw homotopy-invariance proposition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.exists_stableRegularApproximation {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) : Nonempty (RefinedAffineMap.StableRegularApproximation hp F.map)

Every zero-free equivariant coordinate map has at least one stable regular approximation.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.chosenStableApproximation {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) : RefinedAffineMap.StableRegularApproximation hp F.map

A chosen stable approximation of a zero-free equivariant map.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.chosenStableApproximation hp F = Classical.choice ⋯

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.stableObstructionValue {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) : ZMod p

Stable positive-ray obstruction count of a zero-free equivariant coordinate map.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.stableObstructionValue hp F = (NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.chosenStableApproximation hp F).zeroCount

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.stableObstructionValue_eq {p : ℕ} (HPL : RefinedAffineMap.StableHomotopyInvarianceTheorem) (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) : stableObstructionValue hp F = A.zeroCount

The chosen stable count agrees with every stable approximation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.stableObstructionValue_homotopy {p : ℕ} (HPL : RefinedAffineMap.StableHomotopyInvarianceTheorem) (hp : Nat.Prime p) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) : stableObstructionValue hp F₀ = stableObstructionValue hp F₁

Stable obstruction values are invariant under zero-free equivariant homotopy.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.negativeReferenceStableApproximation {p : ℕ} (hp : Nat.Prime p) : RefinedAffineMap.StableRegularApproximation hp (negativeReferenceZeroFreeMap hp).map

The explicit negative level-zero approximation is stable because every sampled coordinate is strictly negative; consequently a positive coordinate mean is impossible.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.negativeReferenceStableApproximation_zeroCount {p : ℕ} (hp : Nat.Prime p) : (negativeReferenceStableApproximation hp).zeroCount = 0

structure NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.PositiveReferenceStableData {p : ℕ} (hp : Nat.Prime p) : Type

The stable positive reference endpoint together with its nonzero count.

• approximation : RefinedAffineMap.StableRegularApproximation hp (positiveReferenceZeroFreeMap hp).map

  The stable regular approximation of the positive reference map with nonzero count.

• zeroCount_ne_zero : self.approximation.zeroCount ≠ 0

def NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.PositiveReferenceStableTheorem : Prop

Uniform positive-reference stability theorem required by the stable obstruction route.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.positiveReferenceSkeletonFree {p : ℕ} (hp : Nat.Prime p) : RefinedAffineMap.PositiveRaySkeletonFree hp 0 (positiveReferenceZeroFreeMap hp).map

At level zero, every positive-ray intersection of the explicit positive reference lies in the relative interior of its maximal simplex. The coordinate-equality equations are exactly the zero equations for ReferenceAffineOrbitCount.referenceMap; the latter were shown above to force all barycentric coordinates to be positive.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.positiveReferenceStableApproximation {p : ℕ} (hp : Nat.Prime p) : RefinedAffineMap.StableRegularApproximation hp (positiveReferenceZeroFreeMap hp).map

The explicit positive level-zero approximation is stable.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.positiveReferenceStableApproximation_zeroCount {p : ℕ} (hp : Nat.Prime p) : (positiveReferenceStableApproximation hp).zeroCount = (PrimeOrbitCycle.orbitCycle hp).zeroCount (ReferenceAffineOrbitCount.referenceIndex hp)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.positiveReferenceStableData {p : ℕ} (hp : Nat.Prime p) : PositiveReferenceStableData hp

Concrete stable positive-reference endpoint data.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.positiveReferenceStableTheorem : PositiveReferenceStableTheorem

The positive-reference stability theorem is discharged by the explicit level-zero map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.negativeReference_stableObstructionValue_eq_zero {p : ℕ} (HPL : RefinedAffineMap.StableHomotopyInvarianceTheorem) (hp : Nat.Prime p) : stableObstructionValue hp (negativeReferenceZeroFreeMap hp) = 0

The stable negative-reference obstruction value vanishes.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPLPositiveRay.positiveReference_stableObstructionValue_ne_zero {p : ℕ} (HPL : RefinedAffineMap.StableHomotopyInvarianceTheorem) (hp : Nat.Prime p) : stableObstructionValue hp (positiveReferenceZeroFreeMap hp) ≠ 0

The stable positive-reference obstruction value is nonzero.