Route B, Step 6: small generic relative perturbation

The incidence analysis is organized by positive support:

• if a positive-weight retained vertex has a movable scalar coordinate, the incidence belongs to one of the finite null bad sets;
• otherwise every positive-weight vertex is frozen, and the incidence is excluded by a support-level frozen safety hypothesis inherited exactly from the base assignment.

Step 5 supplies the bad-set nullity certificates internally.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.assignmentClose_mono {J : Type u_1} {a b : J → ℝ} {r s : ℝ} (h : EquivariantPrismGenericPerturbation.AssignmentClose a b r) (hrs : r ≤ s) : EquivariantPrismGenericPerturbation.AssignmentClose a b s

Monotonicity of coordinatewise assignment closeness in its radius.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.perturbationControlRadius (eps margin : ℝ) : ℝ

Coordinatewise control radius used for both the requested perturbation size and retention of half of the origin margin. The geometric radius of a neighborhood around a generic center is kept separate: a displaced center cannot in general have a ball of radius r entirely contained in the radius-r ball around the base assignment.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.perturbationControlRadius eps margin = min eps (margin / 2)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.perturbationControlRadius_pos {eps margin : ℝ} (heps : 0 < eps) (hmargin : 0 < margin) : 0 < perturbationControlRadius eps margin

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.perturbationControlRadius_le_eps (eps margin : ℝ) : perturbationControlRadius eps margin ≤ eps

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.perturbationControlRadius_le_half_margin (eps margin : ℝ) : perturbationControlRadius eps margin ≤ margin / 2

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.AllCellsFacetRegular {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x : MovableParameterSpace hp C) : Prop

Facet regularity of every local vertex map reconstructed from one movable assignment.

Equations

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

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

Support-level endpoint safety. It is invoked only when every vertex with positive barycentric weight is frozen. Zero-weight nonhorizontal vertices do not affect this condition.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.affineValue_assignmentOfMovableParameters_eq_base_of_frozenSupport {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x : MovableParameterSpace hp C) (q : C.Cell) (w : StandardSimplex p) (hsupport : ∀ (k : Fin (p + 1)), 0 < ↑w k → ∀ (c : Fin p), Parameters.IsFrozenParameter hp C (RelativeGenericity.localParameter hp C q k c)) : (Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base x) q).affineValue w = (Polynomials.localVertexMap hp C base q).affineValue w

Replacing movable parameters leaves an affine value unchanged whenever all positive-weight local vertices are frozen.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.frozenPositiveSupportRaySafe_assignmentOfMovableParameters {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x : MovableParameterSpace hp C) (hsafe : FrozenPositiveSupportRaySafe hp C base) : FrozenPositiveSupportRaySafe hp C (assignmentOfMovableParameters hp C base x)

Frozen-support safety is inherited exactly by every movable replacement.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.avoidsPositiveRayCodimTwo_of_avoids_all_mixedFaceBadSets {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (x : MovableParameterSpace hp C) (hfrozen : FrozenPositiveSupportRaySafe hp C (assignmentOfMovableParameters hp C base x)) (havoid : ∀ (κ : MixedFaceCase hp C), x ∉ mixedFaceBadSet hp C base κ) (q : C.Cell) : AffinePositiveRayBoundary.VertexMap.AvoidsPositiveRayCodimTwo hp (Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base x) q)

Avoidance of all mixed-face bad sets plus frozen-support safety gives the direct codimension-two positive-ray condition.

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

A positive-volume perturbation neighborhood on which full-assignment closeness and facet regularity are controlled. radius is the radius around the generic center; the assignment closeness conclusion uses the independent control radius min eps (margin / 2).

• center : MovableParameterSpace hp C

  The center of a ball of admissible movable parameters.

• radius : ℝ

  The positive radius on which the perturbation bounds and genericity remain valid.

• radius_pos : 0 < self.radius
• closeToBase (x : MovableParameterSpace hp C) : x ∈ Metric.ball self.center self.radius → EquivariantPrismGenericPerturbation.AssignmentClose (assignmentOfMovableParameters hp C base x) base (perturbationControlRadius eps margin)
• facetRegular (x : MovableParameterSpace hp C) : x ∈ Metric.ball self.center self.radius → AllCellsFacetRegular hp C base x

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

Nontriviality of every boundary-restricted facet determinant polynomial. This is the exact algebraic input needed to find a nearby facet-regular center; codimension-two minors are handled by the Route B bad-set argument and are intentionally absent.

Equations

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

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

Geometric form of facet-polynomial nontriviality. Different local facets may use different movable assignments.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.allRestrictedFacetPolynomialsNonzero_of_witnesses {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (h : AllFacetRegularityWitnesses hp C base) : AllRestrictedFacetPolynomialsNonzero hp C base

Pointwise facet witnesses prove nontriviality of every restricted facet polynomial.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.continuous_restrictedFacetDeterminant_eval {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (q : C.Cell) (k : Fin (p + 1)) : Continuous fun (x : MovableParameterSpace hp C) => (MvPolynomial.eval x) (Polynomials.restrictedFacetDeterminantPolynomial hp C base q k)

Evaluation of every restricted facet determinant is continuous in the finite movable parameter space.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.isOpen_allCellsFacetRegular {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) : IsOpen {x : MovableParameterSpace hp C | AllCellsFacetRegular hp C base x}

Facet regularity is an open condition in the movable parameter space.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.exists_safePerturbationBall {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) {eps margin : ℝ} (heps : 0 < eps) (hmargin : 0 < margin) (hfacetPoly : AllRestrictedFacetPolynomialsNonzero hp C base) : Nonempty (SafePerturbationBall hp C base eps margin)

Nonzero restricted facet polynomials produce a genuine positive-radius safe neighborhood. The center is chosen close to the base movable parameters, then the neighborhood radius is shrunk both to remain facet-regular and to keep every reconstructed full assignment inside the independent control radius.

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

Complete Step 6 output.

• move : MovableParameterSpace hp C

  The chosen movable parameters realizing the small generic perturbation.

• closeToBase : EquivariantPrismGenericPerturbation.AssignmentClose (assignmentOfMovableParameters hp C base self.move) base eps
• fixesFrozen {s : Parameters.Parameter hp C} : Parameters.IsFrozenParameter hp C s → assignmentOfMovableParameters hp C base self.move s = base s
• equivariant (g : ↥(PrimeSymmetry p)) (v : Parameters.GlobalVertex hp C) : Parameters.vectorValue hp C (assignmentOfMovableParameters hp C base self.move) (g • v) = g • Parameters.vectorValue hp C (assignmentOfMovableParameters hp C base self.move) v
• retainedMargin : RelativeGenericity.LocalAffineCoordinateNormMargin hp C (assignmentOfMovableParameters hp C base self.move) (margin / 2)
• facetRegular (q : C.Cell) : AffinePositiveRayBoundary.VertexMap.FacetRegular hp (Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base self.move) q)
• avoidsPositiveRayCodimTwo (q : C.Cell) : AffinePositiveRayBoundary.VertexMap.AvoidsPositiveRayCodimTwo hp (Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base self.move) q)
• avoidsOrigin (q : C.Cell) : (Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base self.move) q).AvoidsOrigin
• positiveRayGeneralPosition (q : C.Cell) : AffinePositiveRayBoundary.VertexMap.PositiveRayGeneralPosition hp (Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base self.move) q)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.exists_smallGenericPerturbation {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) {eps margin : ℝ} (hmargin : 0 < margin) (hbaseMargin : RelativeGenericity.LocalAffineCoordinateNormMargin hp C base margin) (hfrozenBase : FrozenPositiveSupportRaySafe hp C base) (B : SafePerturbationBall hp C base eps margin) : Nonempty (SmallGenericPerturbationResult hp C base eps margin)

Step 6 selection theorem. Full mixed-face bad-set nullity is supplied by Step 5 and is no longer an external hypothesis.