Simultaneous generic perturbation of the equivariant refined prism

The orbit-parameter construction already enforces shared-face compatibility and prime equivariance. The polynomial layer records all local facet determinants and codimension-two deviation minors, and all of those polynomials are nonzero. This module applies the finite multivariate perturbation mechanism at the assignment obtained by sampling a zero-free equivariant homotopy.

There is one quantitative subtlety. The parameter t in FiniteMultivariateGenericPerturbation.exists_small_positive_generic is small, but its target assignment is not a priori bounded, so that statement alone does not imply that the resulting assignment is close to the base assignment. We therefore use it once to obtain a generic target, then apply the finite univariate root-avoidance theorem on the line from the base assignment to that generic target. The second parameter is chosen using the finite L¹ size of the direction. The result is genuinely coordinatewise close to the homotopy assignment.

The final theorem assumes a positive coordinate form of the zero-free norm margin for the affine interpolation of the unperturbed homotopy samples. This is the exact quantitative hypothesis that must later be supplied by sufficiently fine spatial and staircase subdivision. The perturbation retains half of that margin, while polynomial nonvanishing gives facet regularity and codimension-two avoidance on every refined prism simplex.

A genuinely small generic multivariate perturbation

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.AssignmentClose {J : Type u_1} (a b : J → ℝ) (eps : ℝ) : Prop

Pointwise coordinate closeness of two finite parameter assignments.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.AssignmentClose a b eps = ∀ (j : J), |a j - b j| < eps

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.exists_generic_assignment_close {J : Type u_1} {I : Type u_2} [Finite J] [Finite I] (P : I → MvPolynomial J ℝ) (hP : ∀ (i : I), P i ≠ 0) (a : J → ℝ) {eps : ℝ} (heps : 0 < eps) : ∃ (a' : J → ℝ), AssignmentClose a' a eps ∧ ∀ (i : I), (MvPolynomial.eval a') (P i) ≠ 0

A finite family of nonzero multivariate polynomials admits a simultaneously nonvanishing assignment which is genuinely pointwise close to any prescribed base assignment.

The first application of exists_small_positive_generic supplies a generic assignment. A second, univariate root-avoidance step moves an arbitrarily small positive distance from the base assignment toward that generic point.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.localVertexValue_apply_eq_assignment_localParameter {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) (j : Fin p) : EquivariantPrismVertexParameters.localVertexValue hp N L a q i j = a (EquivariantPrismGenericityNonzero.localParameter hp N L q i j)

A local scalar coordinate is exactly the corresponding global orbit parameter.

From polynomial nonvanishing to local general position

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.CodimTwoMinorRegular {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) : Prop

All ordered codimension-two deviation minors of one reconstructed local vertex map are nonsingular.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.facetRegular_of_generic {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hgeneric : ∀ (i : EquivariantPrismGenericityPolynomials.GenericityIndex hp N L), (MvPolynomial.eval a) (EquivariantPrismGenericityPolynomials.genericityPolynomial hp N L i) ≠ 0) (q : SubdivisionPrismCharts.PrismCell hp N L) : AffinePositiveRayBoundary.VertexMap.FacetRegular hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)

Nonvanishing of the facet part of the combined polynomial family gives facet regularity on one local refined prism simplex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.codimTwoMinorRegular_of_generic {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hgeneric : ∀ (i : EquivariantPrismGenericityPolynomials.GenericityIndex hp N L), (MvPolynomial.eval a) (EquivariantPrismGenericityPolynomials.genericityPolynomial hp N L i) ≠ 0) (q : SubdivisionPrismCharts.PrismCell hp N L) : CodimTwoMinorRegular hp N L a q

Nonvanishing of the minor part of the combined polynomial family gives nonsingularity of every ordered codimension-two deviation matrix on one local refined prism simplex.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.omittedIndex {p : ℕ} (i j : Fin (p + 1)) (hij : i ≠ j) : Fin p

The index of j after omitting the distinct index i.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.omittedIndex i j hij = Classical.choose ⋯

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.succAbove_omittedIndex {p : ℕ} (i j : Fin (p + 1)) (hij : i ≠ j) : i.succAbove (omittedIndex i j hij) = j

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.sum_codimTwoVertex {p : ℕ} (hp : Nat.Prime p) (F : Fin (p + 1) → ℝ) (i j : Fin (p + 1)) (hij : i ≠ j) (hi : F i = 0) (hj : F j = 0) : ∑ k : Fin (p + 1), F k = ∑ c : Fin (p - 1), F (EquivariantPrismGenericityPolynomials.codimTwoVertex hp (i, omittedIndex i j hij) c)

The ordered codimension-two vertex enumeration exhausts all vertices except the two omitted ones. This sum identity is the bridge from the minor determinant to barycentric avoidance.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.avoidsCodimTwo_of_minorRegular {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) (hminor : CodimTwoMinorRegular hp N L a q) : AffinePositiveRayBoundary.VertexMap.AvoidsCodimTwoDeviationZero hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)

Nonsingularity of every ordered codimension-two deviation matrix rules out a deviation-zero point on a codimension-two face.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.local_regular_and_avoidsCodimTwo_of_generic {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hgeneric : ∀ (i : EquivariantPrismGenericityPolynomials.GenericityIndex hp N L), (MvPolynomial.eval a) (EquivariantPrismGenericityPolynomials.genericityPolynomial hp N L i) ≠ 0) (q : SubdivisionPrismCharts.PrismCell hp N L) : AffinePositiveRayBoundary.VertexMap.FacetRegular hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q) ∧ AffinePositiveRayBoundary.VertexMap.AvoidsCodimTwoDeviationZero hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)

Combined polynomial nonvanishing gives the two combinatorial general-position conditions on every local refined prism simplex.

Quantitative retention of the zero-free affine margin

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.LocalAffineCoordinateNormMargin {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (m : ℝ) : Prop

A coordinate witness for a lower bound on the sup norm of every affine value. For the finite function space Fin p → Real, this is the concrete form needed to retain a zero-free norm margin under coordinatewise perturbation.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.affineValue_coordinate_sub_abs_le_of_assignmentClose {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a' a : EquivariantPrismVertexParameters.Assignment hp N L) {eps : ℝ} (hclose : AssignmentClose a' a eps) (q : SubdivisionPrismCharts.PrismCell hp N L) (w : StandardSimplex p) (j : Fin p) : |(EquivariantPrismGenericityPolynomials.localVertexMap hp N L a' q).affineValue w j - (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q).affineValue w j| ≤ eps

Coordinatewise assignment closeness bounds every coordinate of every local affine value.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.retain_localAffineCoordinateNormMargin {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a' a : EquivariantPrismVertexParameters.Assignment hp N L) {m eps : ℝ} (hmargin : LocalAffineCoordinateNormMargin hp N L a m) (hclose : AssignmentClose a' a eps) : LocalAffineCoordinateNormMargin hp N L a' (m - eps)

A perturbation by less than eps in every parameter coordinate retains the affine coordinate norm margin, reduced from m to m - eps.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.avoidsOrigin_of_coordinateNormMargin {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) {m : ℝ} (hm : 0 < m) (hmargin : LocalAffineCoordinateNormMargin hp N L a m) (q : SubdivisionPrismCharts.PrismCell hp N L) : (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q).AvoidsOrigin

A positive retained coordinate norm margin implies origin avoidance on every local affine simplex.

The prism perturbation theorem

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.Result {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (m : ℝ) : Type

Output of the compatible equivariant generic perturbation. Shared-face compatibility and prime equivariance are inherited automatically from the orbit parameter space.

• assignment : EquivariantPrismVertexParameters.Assignment hp N L

  The perturbed vertex assignment satisfying the prism's genericity and margin conditions.

• closeToHomotopy : AssignmentClose self.assignment (EquivariantPrismVertexParameters.homotopyAssignment hp N L H) (m / 2)
• facetRegular (q : SubdivisionPrismCharts.PrismCell hp N L) : AffinePositiveRayBoundary.VertexMap.FacetRegular hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L self.assignment q)
• avoidsCodimTwo (q : SubdivisionPrismCharts.PrismCell hp N L) : AffinePositiveRayBoundary.VertexMap.AvoidsCodimTwoDeviationZero hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L self.assignment q)
• retainedMargin : LocalAffineCoordinateNormMargin hp N L self.assignment (m / 2)
• avoidsOrigin (q : SubdivisionPrismCharts.PrismCell hp N L) : (EquivariantPrismGenericityPolynomials.localVertexMap hp N L self.assignment q).AvoidsOrigin
• generalPosition (q : SubdivisionPrismCharts.PrismCell hp N L) : AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L self.assignment q)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericPerturbation.exists_generic_perturbation {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) {m : ℝ} (hm : 0 < m) (hmargin : LocalAffineCoordinateNormMargin hp N L (EquivariantPrismVertexParameters.homotopyAssignment hp N L H) m) : Nonempty (Result hp N L H m)

Apply finite multivariate generic perturbation at the homotopy assignment. If the unperturbed piecewise-affine interpolation has positive coordinate norm margin m, the resulting compatible equivariant assignment has all facet determinants and codimension-two minors nonzero and retains margin m/2; hence every local prism simplex satisfies the full affine general-position interface.