Zero-free regular affine approximation after iterated subdivision

This module proves the quantitative approximation step used in S6. A zero-free continuous coordinate map on the compact Fox--Neuwirth realization has a positive uniform norm margin. Uniform continuity and diameter shrinking for iterated barycentric subdivision make the affine interpolation of vertex samples uniformly close to the original map. A small scalar perturbation toward the fixed positive S5 reference map avoids the finitely many determinant roots and hence makes every refined top simplex regular. The perturbation is chosen small enough that the entire straight-line homotopy from the original map to the refined affine interpolation remains zero-free.

The perturbation direction is a single global continuous map. Consequently values agree on every shared refined face and prime-symmetry equivariance is preserved.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.exists_positive_norm_margin {p : ℕ} (F : ContinuousCoordinateMap p) (hF : ∀ (x : Realization p), F x ≠ 0) : ∃ (m : ℝ), 0 < m ∧ ∀ (x : Realization p), m ≤ ‖F x‖

A uniform positive lower bound for the norm of a zero-free continuous map on the compact realization.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.exists_norm_upper_bound {p : ℕ} (F : ContinuousCoordinateMap p) : ∃ (B : ℝ), 0 < B ∧ ∀ (x : Realization p), ‖F x‖ < B

A uniform strict upper bound for a continuous map on the compact realization.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.exists_common_refinement_oscillation {p : ℕ} (hp : Nat.Prime p) (F : ContinuousCoordinateMap p) {eps : ℝ} (heps : 0 < eps) : ∃ (N : ℕ), ∀ (q : TopCell hp N) (u v : StandardSimplex (p - 1)), dist (F ((chart hp N q) (StandardSimplex.toDelta u))) (F ((chart hp N q) (StandardSimplex.toDelta v))) < eps

Uniform oscillation bound on every refined top simplex at one sufficiently deep common subdivision level.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.norm_value_sub_original_le_of_oscillation {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) (q : TopCell hp N) (eps : ℝ) (hosc : ∀ (u v : StandardSimplex (p - 1)), dist (F ((chart hp N q) (StandardSimplex.toDelta u))) (F ((chart hp N q) (StandardSimplex.toDelta v))) < eps) (w : StandardSimplex (p - 1)) : ‖value hp N F q w - F ((chart hp N q) (StandardSimplex.toDelta w))‖ ≤ eps

Affine interpolation of samples differs from the original map by at most the oscillation on the refined simplex.

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

A refined regular approximation of a zero-free continuous coordinate map. The stored global map is the small perturbation used for vertex sampling; zeroFreeStraightLine concerns the actual piecewise-affine interpolation of those samples.

• level : ℕ

  Common barycentric-subdivision level.

• map : ContinuousCoordinateMap p

  Global continuous map whose samples define the refined PL approximation.

• equivariant : IsEquivariantCoordinateMap p self.map

  The sampled map respects prime-symmetry relabelling.

• regular (q : TopCell hp self.level) : determinant hp self.level self.map q ≠ 0

  Every refined top simplex is transverse to the diagonal ray.

• 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

  The straight-line interpolation from the original map to the sampled affine map is zero-free on every refined simplex.

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

Positive orbit count represented by a regular refined approximation.

Equations

• A.zeroCount = NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.zeroCount hp A.level A.map

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.exists_regularApproximation {p : ℕ} (hp : Nat.Prime p) (F : ContinuousCoordinateMap p) (hEq : IsEquivariantCoordinateMap p F) (hF : ∀ (x : Realization p), F x ≠ 0) : Nonempty (RegularApproximation hp F)

Existence of a regular zero-free refined approximation.