Quantitative zero-free margin after staircase refinement

For a fixed common spatial subdivision level, the finitely many unrefined staircase-prism charts are continuous maps from the compact standard p-simplex into the realization cylinder. A zero-free homotopy has a positive uniform norm margin on that compact cylinder. Uniform continuity, together with diameter shrinking under iterated barycentric subdivision of each staircase simplex, therefore makes the affine interpolation of homotopy samples uniformly close to the original homotopy.

Because the target Fin p → ℝ carries the finite product sup norm, one coordinate realizes at least the full vector norm. Consequently the sampled affine interpolation has a positive local coordinate norm margin. This is precisely the quantitative hypothesis required by EquivariantPrismGenericPerturbation.exists_generic_perturbation.

The main result is formulated for an arbitrary preselected spatial level N: only the staircase refinement level L must subsequently be increased. This permits later arguments to choose a common spatial subdivision for endpoint data first and then refine the entire homotopy prism.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismSubdivisionMargin.basePrismChart {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : SubdivisionPrismCharts.BasePrismCell hp N) : C(↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p), Realization p × ↑(Set.Icc 0 1))

The unrefined staircase chart over one fixed spatially refined top simplex.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismSubdivisionMargin.chart_eq_basePrismChart_affineCompMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : (SubdivisionPrismCharts.chart hp N L q) w = (basePrismChart hp N q.1) ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap p L q.2) w)

A fully refined prism chart factors through its unrefined staircase chart and the iterated barycentric subdivision map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismSubdivisionMargin.exists_positive_homotopy_norm_margin {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) : ∃ (M : ℝ), 0 < M ∧ ∀ (z : Realization p × ↑(Set.Icc 0 1)), M ≤ ‖H.map z‖

A zero-free homotopy has a uniform positive norm margin on the compact realization cylinder.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismSubdivisionMargin.exists_coordinate_abs_ge_norm {p : ℕ} (hp : Nat.Prime p) (x : Fin p → ℝ) : ∃ (j : Fin p), ‖x‖ ≤ |x j|

In a nonempty finite product, some coordinate has absolute value at least the product norm.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismSubdivisionMargin.exists_staircase_refinement_oscillation {p : ℕ} (hp : Nat.Prime p) (N : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) {eps : ℝ} (heps : 0 < eps) : ∃ (L : ℕ), ∀ (q : SubdivisionPrismCharts.PrismCell hp N L) (u v : StandardSimplex p), dist (H.map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta u))) (H.map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta v))) < eps

At every fixed spatial subdivision level, sufficiently deep staircase subdivision makes the homotopy oscillation on every refined prism simplex smaller than any prescribed positive bound.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismSubdivisionMargin.norm_affineValue_sub_homotopy_le_of_oscillation {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (q : SubdivisionPrismCharts.PrismCell hp N L) (eps : ℝ) (hosc : ∀ (u v : StandardSimplex p), dist (H.map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta u))) (H.map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta v))) < eps) (w : StandardSimplex p) : ‖(EquivariantPrismGenericityPolynomials.localVertexMap hp N L (EquivariantPrismVertexParameters.homotopyAssignment hp N L H) q).affineValue w - H.map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta w))‖ ≤ eps

If the homotopy oscillates by less than eps on one refined prism simplex, its affine interpolation from vertex samples differs from the original homotopy by at most eps.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismSubdivisionMargin.exists_staircase_refinement_coordinateNormMargin {p : ℕ} (hp : Nat.Prime p) (N : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) : ∃ (L : ℕ) (m : ℝ), 0 < m ∧ EquivariantPrismGenericPerturbation.LocalAffineCoordinateNormMargin hp N L (EquivariantPrismVertexParameters.homotopyAssignment hp N L H) m

For every fixed spatial level, some staircase refinement gives the homotopy assignment a strictly positive local affine coordinate norm margin.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismSubdivisionMargin.exists_generic_perturbation_after_staircase_refinement {p : ℕ} (hp : Nat.Prime p) (N : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) : ∃ (L : ℕ) (m : ℝ), 0 < m ∧ Nonempty (EquivariantPrismGenericPerturbation.Result hp N L H m)

After any preselected spatial subdivision, one can choose a staircase refinement and obtain a compatible equivariant generic perturbation satisfying full local general position and retaining a positive zero-free margin.