Relative genericity for explicit affine collars

This module connects the boundary-restricted polynomial family of ExplicitAffineRelativeCollar to the weaker positive-ray general-position interface used by the finite Stokes theorem.

All facet determinant polynomials remain in the genericity family. Codimension-two minors are required only when the corresponding face is not purely horizontal. Purely horizontal codimension-two faces are handled by a separate endpoint-safety condition, which is the condition to be derived from the two stable endpoint approximations.

The final section packages finite multivariate perturbation on movable parameter orbits and proves that closeness there gives closeness of the reconstructed full assignment while retaining the horizontal boundary literally.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.IsRelativeGeneric {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) : Prop

Simultaneous nonvanishing of the complete boundary-restricted polynomial family.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.restrictedGenericityPolynomial_ne_zero_of_evaluation {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (i : Polynomials.RelativeGenericityIndex hp C) (move : Parameters.MovableParameter hp C → ℝ) (hvalue : Polynomials.genericityValue hp C (Parameters.replaceMovable hp C base move) i ≠ 0) : Polynomials.restrictedGenericityPolynomial hp C base i ≠ 0

A single explicit movable assignment at which a restricted genericity value is nonzero proves that the corresponding restricted polynomial is genuinely nonzero. This is the useful geometric form of the nontriviality obligation: collar constructions may provide a local witness rather than an equality proof in a multivariate polynomial ring.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.restrictedGenericityPolynomial_ne_zero_of_witnesses {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (hwitness : ∀ (i : Polynomials.RelativeGenericityIndex hp C), ∃ (move : Parameters.MovableParameter hp C → ℝ), Polynomials.genericityValue hp C (Parameters.replaceMovable hp C base move) i ≠ 0) (i : Polynomials.RelativeGenericityIndex hp C) : Polynomials.restrictedGenericityPolynomial hp C base i ≠ 0

Pointwise geometric witnesses imply nontriviality of the complete finite restricted polynomial family. Different indices may use different movable assignments.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.RequiresMovableGenericityWitness {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (i : Polynomials.RelativeGenericityIndex hp C) : Prop

Only nonhorizontal local facets and the retained codimension-two minors need a genuinely movable genericity witness. Horizontal facet determinants are fixed endpoint determinants.

Equations

• One or more equations did not get rendered due to their size.
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.RequiresMovableGenericityWitness hp C (Sum.inr val) = True

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.movableRestriction {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) : Parameters.MovableParameter hp C → ℝ

Restrict a full assignment to its movable parameter subtype.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.movableRestriction hp C base q = base ↑q

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.horizontalFacet_genericityValue_ne_zero {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (D : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp D.cells) (B : HorizontalVertexFixed hp A₀ A₁ D a) (q : D.cells.Cell) (k : Fin (p + 1)) (hhorizontal : D.cells.IsHorizontalFacet (D.cells.facetClass (q, k))) : Polynomials.genericityValue hp D.cells a (Sum.inl (q, k)) ≠ 0

A horizontal local facet of an endpoint-fixed collar has nonzero determinant because it is literally one of the two supplied stable endpoint facets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.horizontalFacet_genericityValue_ne_zero_endpointAdjusted {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) {M L : ℕ} (D : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (move : Parameters.MovableParameter hp D.cells → ℝ) (q : D.cells.Cell) (k : Fin (p + 1)) (hhorizontal : D.cells.IsHorizontalFacet (D.cells.facetClass (q, k))) : Polynomials.genericityValue hp D.cells (Parameters.replaceMovable hp D.cells (Parameters.endpointAdjustedAssignment hp D.cells H A₀.toRegularApproximation A₁.toRegularApproximation) move) (Sum.inl (q, k)) ≠ 0

For the endpoint-adjusted collar assignment, horizontal facet genericity is automatic after any movable perturbation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.all_relativeGenericityWitnesses_of_required {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) {M L : ℕ} (D : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (hwitness : ∀ (i : Polynomials.RelativeGenericityIndex hp D.cells), RequiresMovableGenericityWitness hp D.cells i → ∃ (move : Parameters.MovableParameter hp D.cells → ℝ), Polynomials.genericityValue hp D.cells (Parameters.replaceMovable hp D.cells (Parameters.endpointAdjustedAssignment hp D.cells H A₀.toRegularApproximation A₁.toRegularApproximation) move) i ≠ 0) (i : Polynomials.RelativeGenericityIndex hp D.cells) : ∃ (move : Parameters.MovableParameter hp D.cells → ℝ), Polynomials.genericityValue hp D.cells (Parameters.replaceMovable hp D.cells (Parameters.endpointAdjustedAssignment hp D.cells H A₀.toRegularApproximation A₁.toRegularApproximation) move) i ≠ 0

Geometric witnesses are required only for the nonhorizontal part of the relative genericity family; stable endpoint regularity supplies all horizontal facet witnesses automatically.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.facetRegular_of_relativeGeneric {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) (hgeneric : IsRelativeGeneric hp C base move) (q : C.Cell) : AffinePositiveRayBoundary.VertexMap.FacetRegular hp (Polynomials.localVertexMap hp C (Parameters.replaceMovable hp C base move) q)

Relative genericity gives facet regularity on every explicit top cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.codimTwoMinor_ne_zero_of_relativeGeneric {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) (hgeneric : IsRelativeGeneric hp C base move) (q : C.Cell) (f : Polynomials.CodimTwoFace p) (hf : ¬Polynomials.IsPurelyHorizontalCodimTwo hp C q f) : (Polynomials.codimTwoDeviationMatrix hp C (Parameters.replaceMovable hp C base move) q f).det ≠ 0

Relative genericity makes every non-purely-horizontal codimension-two deviation matrix nonsingular.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.HorizontalPositiveRayCodimTwoSafe {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) : Prop

Safety condition left for the frozen endpoint geometry. It is required only when the ordered codimension-two face determined by the two vanishing barycentric coordinates is purely horizontal.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.HorizontalEndpointSkeletonRepresentation {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (D : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp D.cells) : Prop

A purely horizontal codimension-two point is represented on the proper skeleton of one of the two actual endpoint triangulations, with exactly the same affine coordinate value. This is the geometric compatibility condition needed to transfer stable endpoint transversality to an arbitrary relative collar triangulation.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.horizontalPositiveRayCodimTwoSafe_of_endpointRepresentation {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (D : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp D.cells) (hrepresentation : HorizontalEndpointSkeletonRepresentation hp A₀ A₁ D a) : HorizontalPositiveRayCodimTwoSafe hp D.cells a

Stable endpoint skeleton transversality converts exact horizontal endpoint representation into the positive-ray safety property required by the relative local Stokes theorem.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.affineValue_replaceMovable_eq_of_purelyHorizontalCodimTwo {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) (q : C.Cell) (w : StandardSimplex p) (i j : Fin (p + 1)) (hij : i ≠ j) (hzeros : ↑w i = 0 ∧ ↑w j = 0) (hpure : Polynomials.IsPurelyHorizontalCodimTwo hp C q (i, EquivariantPrismGenericPerturbation.omittedIndex i j hij)) : (Polynomials.localVertexMap hp C (Parameters.replaceMovable hp C base move) q).affineValue w = (Polynomials.localVertexMap hp C base q).affineValue w

On a purely horizontal codimension-two face, changing movable parameters does not alter the represented affine value. The two omitted barycentric coordinates vanish, while every retained vertex belongs to a frozen endpoint boundary.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.horizontalPositiveRayCodimTwoSafe_replaceMovable {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) (hbase : HorizontalPositiveRayCodimTwoSafe hp C base) : HorizontalPositiveRayCodimTwoSafe hp C (Parameters.replaceMovable hp C base move)

Horizontal positive-ray safety depends only on frozen endpoint values and is therefore preserved by every replacement of the movable parameter orbits.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.avoidsPositiveRayCodimTwo_of_relativeGeneric {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) (hgeneric : IsRelativeGeneric hp C base move) (hhorizontal : HorizontalPositiveRayCodimTwoSafe hp C (Parameters.replaceMovable hp C base move)) (q : C.Cell) : AffinePositiveRayBoundary.VertexMap.AvoidsPositiveRayCodimTwo hp (Polynomials.localVertexMap hp C (Parameters.replaceMovable hp C base move) q)

Nonhorizontal minor regularity plus horizontal endpoint safety gives the exact positive-ray-relative codimension-two avoidance condition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.positiveRayGeneralPosition_of_relativeGeneric {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) (hgeneric : IsRelativeGeneric hp C base move) (hhorizontal : HorizontalPositiveRayCodimTwoSafe hp C (Parameters.replaceMovable hp C base move)) (havoid : ∀ (q : C.Cell), (Polynomials.localVertexMap hp C (Parameters.replaceMovable hp C base move) q).AvoidsOrigin) (q : C.Cell) : AffinePositiveRayBoundary.VertexMap.PositiveRayGeneralPosition hp (Polynomials.localVertexMap hp C (Parameters.replaceMovable hp C base move) q)

Relative genericity, horizontal endpoint safety, and origin avoidance give the local positive-ray general-position interface.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.localPositiveRayStokes_of_relativeGeneric {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (D : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (base : Parameters.Assignment hp D.cells) (move : Parameters.MovableParameter hp D.cells → ℝ) (hgeneric : IsRelativeGeneric hp D.cells base move) (hhorizontal : HorizontalPositiveRayCodimTwoSafe hp D.cells (Parameters.replaceMovable hp D.cells base move)) (havoid : ∀ (q : D.cells.Cell), (Polynomials.localVertexMap hp D.cells (Parameters.replaceMovable hp D.cells base move) q).AvoidsOrigin) : FoxNeuwirthRelativeAffineCollar.LocalPositiveRayStokes hp D (Parameters.replaceMovable hp D.cells base move)

The relative genericity package implies the exact cellwise positive-ray Stokes identity.

Finite perturbation on movable parameter orbits

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.exists_relativeGeneric_move_close {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (hpoly : ∀ (i : Polynomials.RelativeGenericityIndex hp C), Polynomials.restrictedGenericityPolynomial hp C base i ≠ 0) (move₀ : Parameters.MovableParameter hp C → ℝ) {eps : ℝ} (heps : 0 < eps) : ∃ (move : Parameters.MovableParameter hp C → ℝ), EquivariantPrismGenericPerturbation.AssignmentClose move move₀ eps ∧ IsRelativeGeneric hp C base move

A finite family of nonzero restricted polynomials admits a simultaneously generic movable assignment arbitrarily close to any prescribed movable assignment.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.replaceMovable_assignmentClose {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move move₀ : Parameters.MovableParameter hp C → ℝ) {eps : ℝ} (heps : 0 < eps) (hclose : EquivariantPrismGenericPerturbation.AssignmentClose move move₀ eps) : EquivariantPrismGenericPerturbation.AssignmentClose (Parameters.replaceMovable hp C base move) (Parameters.replaceMovable hp C base move₀) eps

Closeness on movable parameter orbits gives closeness of the reconstructed full assignments; frozen horizontal parameters agree exactly.

Quantitative origin-avoidance retention

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.replaceMovable_movableRestriction {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) : Parameters.replaceMovable hp C base (movableRestriction hp C base) = base

Replacing movable parameters by the restriction of the base assignment reconstructs the base assignment exactly.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.localParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (i : Fin (p + 1)) (j : Fin p) : Parameters.Parameter hp C

The full parameter represented by one local vertex coordinate.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.localVertexMap_value_apply_eq_assignment_localParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (q : C.Cell) (i : Fin (p + 1)) (j : Fin p) : (Polynomials.localVertexMap hp C a q).value i j = a (localParameter hp C q i j)

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.LocalAffineCoordinateNormMargin {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (m : ℝ) : Prop

A coordinate witness for a uniform lower bound on every local affine value.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.affineValue_coordinate_sub_abs_le_of_assignmentClose {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a' a : Parameters.Assignment hp C) {eps : ℝ} (hclose : EquivariantPrismGenericPerturbation.AssignmentClose a' a eps) (q : C.Cell) (w : StandardSimplex p) (j : Fin p) : |(Polynomials.localVertexMap hp C a' q).affineValue w j - (Polynomials.localVertexMap hp C a q).affineValue w j| ≤ eps

Coordinatewise closeness of full assignments bounds each coordinate of each local affine interpolation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.retain_localAffineCoordinateNormMargin {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a' a : Parameters.Assignment hp C) {m eps : ℝ} (hmargin : LocalAffineCoordinateNormMargin hp C a m) (hclose : EquivariantPrismGenericPerturbation.AssignmentClose a' a eps) : LocalAffineCoordinateNormMargin hp C a' (m - eps)

A coordinate norm margin decreases by at most the assignment perturbation size.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.avoidsOrigin_of_localAffineCoordinateNormMargin {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) {m : ℝ} (hm : 0 < m) (hmargin : LocalAffineCoordinateNormMargin hp C a m) (q : C.Cell) : (Polynomials.localVertexMap hp C a q).AvoidsOrigin

A positive coordinate norm margin implies local origin avoidance.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.exists_positive_localAffineCoordinateNormMargin {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (havoid : ∀ (q : C.Cell), (Polynomials.localVertexMap hp C a q).AvoidsOrigin) : ∃ (m : ℝ), 0 < m ∧ LocalAffineCoordinateNormMargin hp C a m

Cellwise origin avoidance on a finite relative collar automatically has a uniform positive coordinate margin. Compactness gives a positive norm minimum on each affine simplex; finiteness of the cell family gives one common minimum, and the finite-product sup norm is attained in a coordinate.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.PerturbationResult {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (m : ℝ) : Type

Output of a small boundary-relative generic perturbation retaining half of a supplied origin margin.

• move : Parameters.MovableParameter hp C → ℝ

  The selected values of the movable real coordinates.

• closeToBase : EquivariantPrismGenericPerturbation.AssignmentClose (Parameters.replaceMovable hp C base self.move) base (m / 2)
• relativeGeneric : IsRelativeGeneric hp C base self.move
• retainedMargin : LocalAffineCoordinateNormMargin hp C (Parameters.replaceMovable hp C base self.move) (m / 2)
• avoidsOrigin (q : C.Cell) : (Polynomials.localVertexMap hp C (Parameters.replaceMovable hp C base self.move) q).AvoidsOrigin

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeGenericity.exists_relativeGeneric_perturbation {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (hpoly : ∀ (i : Polynomials.RelativeGenericityIndex hp C), Polynomials.restrictedGenericityPolynomial hp C base i ≠ 0) {m : ℝ} (hm : 0 < m) (hmargin : LocalAffineCoordinateNormMargin hp C base m) : Nonempty (PerturbationResult hp C base m)

Simultaneously make all nontrivial boundary-relative genericity polynomials nonzero while retaining half of a positive affine origin margin.