Route B, Step 5: bad-set nullity certificates and finite avoidance

Step 4 proves that, after fixing a barycentric witness w and all movable coordinates except one selected scalar orbit, the corresponding scalar fiber is null whenever one total orbit coefficient is nonzero.

There is an important logical distinction between that statement and nullity of mixedFaceBadSet: the latter existentially quantifies over an uncountable simplex of witnesses. Projection of a null subset of a product need not be null. Consequently no theorem in this file silently promotes the Step 4 fixed-witness result to full bad-set nullity.

Instead this file does two things:

• packages the exact full-set nullity certificate needed by the perturbation selection argument;
• proves that a finite family of certified mixed-face bad sets can be avoided in every positive-volume parameter ball.

Full bad-set nullity requires an elimination theorem showing that each full mixedFaceBadSet is null. It must use the complete system of deviation equations (or an equivalent nonzero elimination polynomial), rather than only one fixed-witness scalar equation.

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

A checked nullity certificate for one complete mixed-face bad set.

This deliberately concerns mixedFaceBadSet itself, after existential quantification over all barycentric witnesses. A collection of merely fixed-witness fiber statements is not sufficient to construct this value.

• volume_eq_zero : MeasureTheory.volume (mixedFaceBadSet hp C base κ) = 0

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.allMixedFaceCases {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Finset (MixedFaceCase hp C)

The family of all mixed-face cases is finite.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.allMixedFaceCases hp C = Finset.univ

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.mem_allMixedFaceCases {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : κ ∈ allMixedFaceCases hp C

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.exists_mem_ball_avoiding_all_mixedFaceBadSets {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (center : MovableParameterSpace hp C) (radius : ℝ) (hball : MeasureTheory.volume (Metric.ball center radius) ≠ 0) (hnull : ∀ (κ : MixedFaceCase hp C), MixedFaceBadSetNullCertificate hp C base κ) : ∃ x ∈ Metric.ball center radius, ∀ (κ : MixedFaceCase hp C), x ∉ mixedFaceBadSet hp C base κ

Full-set nullity certificates imply simultaneous avoidance in any positive-volume parameter ball.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.no_incidence_with_movableWitness_of_avoids_all_badSets {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) (havoid : ∀ (κ : MixedFaceCase hp C), x ∉ mixedFaceBadSet hp C base κ) : ¬∃ (q : C.Cell) (w : StandardSimplex p) (i : Fin (p + 1)) (j : Fin (p + 1)), i ≠ j ∧ ↑w i = 0 ∧ ↑w j = 0 ∧ (∀ (r : Fin (p - 1)), AffinePositiveRayBoundary.VertexMap.deviation hp ((Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base x) q).affineValue w) r = 0) ∧ 0 < AffinePositiveRayBoundary.VertexMap.mean p ((Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base x) q).affineValue w) ∧ HasPositiveMovableWitness hp C q w i j

Avoiding every case excludes every mixed positive-ray incidence that has a positive movable witness.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.fixedWitness_scalarFiber_null {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) (κ : MixedFaceCase hp C) (w : StandardSimplex p) (r : Fin (p - 1)) (hr : deviationOrbitCoefficient hp C κ w r ≠ 0) : MeasureTheory.volume (mixedFaceScalarFiber hp C base x κ w) = 0

Step 4 supplies a null scalar fiber for every fixed witness carrying a nonzero selected-orbit coefficient. This theorem records the valid local input, without making the invalid projection inference.

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

The elimination property for a mixed-face case.

A proof of this proposition must control the existential barycentric witness. It can be obtained, for example, by deriving a nonzero polynomial obstruction in the remaining movable parameters whose zero set contains the complete bad set.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.certificate_of_hasNullElimination {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (h : HasNullElimination hp C base κ) : MixedFaceBadSetNullCertificate hp C base κ

The elimination property is exactly the certificate consumed by the finite avoidance theorem.