Stable regular approximations for endpoint cobordism

The raw RegularApproximation interface records top-simplex determinant regularity but permits a positive-ray intersection on a proper face of the chosen refined triangulation. Since RegularApproximation.zeroCount counts only relative-interior intersections, that datum is not sufficient for a boundary-relative prism comparison.

This module introduces the transversality condition required by the endpoint-comparison stage. Existence and comparison are established by the downstream collar modules.

def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.PositiveRaySkeletonFree {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) : Prop

The sampled affine map has no positive-ray intersection on the boundary of any refined top simplex. Equivalently, every positive deviation-zero barycentric point is in the relative interior.

Equations

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

structure NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.StableRegularApproximation {p : ℕ} (hp : Nat.Prime p) (F : ContinuousCoordinateMap p) extends NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.RegularApproximation hp F : Type

A regular approximation whose positive-ray intersections are transverse to the chosen triangulation skeleton. This is the appropriate endpoint object for a boundary-relative prism cobordism.

• level : ℕ
• map : ContinuousCoordinateMap p
• equivariant : IsEquivariantCoordinateMap p self.map
• regular (q : TopCell hp self.level) : determinant hp self.level self.map q ≠ 0
• zeroFreeStraightLine (q : TopCell hp self.level) (w : StandardSimplex (p - 1)) (u : ↑(Set.Icc 0 1)) : (1 - ↑u) • F ((chart hp self.level q) (StandardSimplex.toDelta w)) + ↑u • value hp self.level self.map q w ≠ 0
• positiveRaySkeletonFree : PositiveRaySkeletonFree hp self.level self.map

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.StableRegularApproximation.zeroCount {p : ℕ} {hp : Nat.Prime p} {F : ContinuousCoordinateMap p} (A : StableRegularApproximation hp F) : ZMod p

The stable count is the existing refined count; stability is supplied by the additional transversality field, not by changing the numerical definition.

Equations

• A.zeroCount = A.zeroCount

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.StableRegularApproximation.positive_coordinate {p : ℕ} {hp : Nat.Prime p} {F : ContinuousCoordinateMap p} (A : StableRegularApproximation hp F) (q : TopCell hp A.level) (w : StandardSimplex (p - 1)) (hdev : ∀ (r : Fin (p - 1)), value hp A.level A.map q w (ReferenceAffineOrbitCount.coordinateLabel hp r) = value hp A.level A.map q w (ReferenceAffineOrbitCount.lastLabel hp)) (hmean : 0 < (coordinateMean p) (value hp A.level A.map q w)) (i : Fin p) : 0 < ↑w (Fin.cast ⋯ i)

A positive-ray intersection of a stable approximation cannot have a zero barycentric coordinate.

def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.StableHomotopyInvarianceTheorem : Prop

Finite-PL endpoint comparison proposition. This proposition requires boundary-transverse endpoint approximations.

Equations

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