Route B: full mixed-face bad-set nullity

This is the concrete completion of Step 5. After the canonical coordinate split, fix all parameters except the complete p-coordinate value at the selected retained vertex. Any positive-ray incidence forces that selected block into the linear span of the diagonal vector and the other p - 2 retained vertex blocks. The span has dimension at most p - 1 in a p-dimensional real vector space, hence has zero Lebesgue measure. Fubini and the measure-preserving coordinate split give nullity of the original complete bad set, including its existential simplex witness.

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

Local vertices retained after deleting the two face omissions and the selected vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.card_otherRetainedIndices {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : (otherRetainedIndices hp C κ).card = p - 2

There are exactly p - 2 other retained vertices.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.OtherRetainedIndex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : Type

Finite type of the other retained local vertices.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.card_selectedVectorParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : Fintype.card (SelectedVectorParameter hp C κ) = p

The selected block has cardinality p.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.card_option_otherRetainedIndex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : Fintype.card (Option (OtherRetainedIndex hp C κ)) = p - 1

The index type consisting of the diagonal generator and the other retained vertices has cardinality p - 1.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.mergedParameters {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (u : SelectedVectorParameter hp C κ → ℝ) (rest : RemainingMovableParameter hp C κ → ℝ) : MovableParameterSpace hp C

Reconstruct the complete movable assignment from selected and remaining blocks.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.localVertexBlock {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (u : SelectedVectorParameter hp C κ → ℝ) (rest : RemainingMovableParameter hp C κ → ℝ) (i : Fin (p + 1)) : SelectedVectorParameter hp C κ → ℝ

Value of a local vertex, represented in selected-block coordinate order.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.localVertexBlock_retained {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (u : SelectedVectorParameter hp C κ → ℝ) (rest : RemainingMovableParameter hp C κ → ℝ) : localVertexBlock hp C base κ u rest κ.retained = u

At the selected retained vertex, the local vertex block is exactly the selected coordinate variable.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.localVertexBlock_eq_zeroSelected_of_ne {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (u : SelectedVectorParameter hp C κ → ℝ) (rest : RemainingMovableParameter hp C κ → ℝ) (i : Fin (p + 1)) (hi : i ≠ κ.retained) : localVertexBlock hp C base κ u rest i = localVertexBlock hp C base κ 0 rest i

At every other local vertex, the selected block has no influence.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.diagonalBlock {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : SelectedVectorParameter hp C κ → ℝ

The constant diagonal vector in selected-block coordinates.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.diagonalBlock hp C κ x✝ = 1

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.fiberGenerator {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (rest : RemainingMovableParameter hp C κ → ℝ) : Option (OtherRetainedIndex hp C κ) → SelectedVectorParameter hp C κ → ℝ

The finite generating family for the bad selected-vector fiber.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.badFiberSubmodule {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (rest : RemainingMovableParameter hp C κ → ℝ) : Submodule ℝ (SelectedVectorParameter hp C κ → ℝ)

The proper linear subspace containing the complete selected-vector bad fiber for fixed complementary parameters.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.badFiberSubmodule_ne_top {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (rest : RemainingMovableParameter hp C κ → ℝ) : badFiberSubmodule hp C base κ rest ≠ ⊤

The fiber subspace is proper.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.weightedSum_eq_selected_add_other {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (w : StandardSimplex p) (V : Fin (p + 1) → SelectedVectorParameter hp C κ → ℝ) (h0 : ↑w κ.omitted₀ = 0) (h1 : ↑w κ.omitted₁ = 0) : ∑ i : Fin (p + 1), ↑w i • V i = ↑w κ.retained • V κ.retained + ∑ i ∈ otherRetainedIndices hp C κ, ↑w i • V i

Decomposition of a barycentric vector sum after deleting the two zero weights and isolating the selected retained vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.selectedFiber_subset_badFiberSubmodule {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (rest : RemainingMovableParameter hp C κ → ℝ) : {u : SelectedVectorParameter hp C κ → ℝ | mergedParameters hp C κ u rest ∈ mixedFaceBadSet hp C base κ} ⊆ ↑(badFiberSubmodule hp C base κ rest)

A complete bad selected-vector fiber is contained in its proper span.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.volume_selectedFiber_eq_zero {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (rest : RemainingMovableParameter hp C κ → ℝ) : MeasureTheory.volume {u : SelectedVectorParameter hp C κ → ℝ | mergedParameters hp C κ u rest ∈ mixedFaceBadSet hp C base κ} = 0

Each selected-vector fiber has zero volume.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.splitMixedFaceBadSetCanonical {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) : Set ((MixedFaceCase.SelectedVectorParameter hp C κ → ℝ) × (MixedFaceCase.RemainingMovableParameter hp C κ → ℝ))

The complete bad set in canonical split coordinates.

Equations

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

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

The split bad set is measurable.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.volume_splitMixedFaceBadSetCanonical_eq_zero {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) : MeasureTheory.volume (splitMixedFaceBadSetCanonical hp C base κ) = 0

Fubini proves nullity in split coordinates.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.volume_mixedFaceBadSet_eq_zero {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) : MeasureTheory.volume (mixedFaceBadSet hp C base κ) = 0

Concrete full-set nullity theorem for every mixed-face case.

theorem 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) : MixedFaceBadSetNullCertificate hp C base κ

Concrete Step 5 certificate.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.exists_mem_ball_avoiding_all_mixedFaceBadSets_unconditional {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) : ∃ x ∈ Metric.ball center radius, ∀ (κ : MixedFaceCase hp C), x ∉ mixedFaceBadSet hp C base κ

Every positive-volume ball contains a parameter avoiding all mixed-face bad sets, with no external nullity hypotheses.