Route B, Step 3: decomposition of mixed-face positive-ray incidence

For a nonhorizontal codimension-two face, a positive-ray failure is split into finitely many cases by choosing a retained movable vertex whose barycentric coefficient is positive. The next stages will prove that each resulting bad parameter set is null.

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

Data selecting one codimension-two face and one retained local vertex whose scalar orbit is movable. The selected coordinate j is only used to certify that the vertex is genuinely movable; once one scalar coordinate at a vertex is movable, the corresponding vector value is controlled by movable orbit data.

• cell : C.Cell

  The collar cell containing the mixed face.

• omitted₀ : Fin (p + 1)

  The first vertex omitted from the codimension-two face.

• omitted₁ : Fin (p + 1)

  The second, distinct vertex omitted from the face.

• omitted_ne : self.omitted₀ ≠ self.omitted₁
• retained : Fin (p + 1)

  A vertex retained in the face whose selected coordinate is movable.

• retained_ne₀ : self.retained ≠ self.omitted₀
• retained_ne₁ : self.retained ≠ self.omitted₁
• coordinate : Fin p

  The selected scalar coordinate of the retained vertex.

• movable : ¬Parameters.IsFrozenParameter hp C (RelativeGenericity.localParameter hp C self.cell self.retained self.coordinate)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.mixedFaceBadSet {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 (MovableParameterSpace hp C)

The bad set attached to one distinguished positive movable vertex.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.HasPositiveMovableWitness {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (w : StandardSimplex p) (i j : Fin (p + 1)) : Prop

A positive-ray incidence on a codimension-two face has a positive movable witness when at least one retained vertex with positive barycentric weight has a movable local scalar parameter.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.mem_mixedFaceBadSet_of_incidence {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) (i j : Fin (p + 1)) (hij : i ≠ j) (hi : ↑w i = 0) (hj : ↑w j = 0) (hdev : ∀ (r : Fin (p - 1)), AffinePositiveRayBoundary.VertexMap.deviation hp ((Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base x) q).affineValue w) r = 0) (hmean : 0 < AffinePositiveRayBoundary.VertexMap.mean p ((Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base x) q).affineValue w)) (hmovable : HasPositiveMovableWitness hp C q w i j) : ∃ (κ : MixedFaceCase hp C), x ∈ mixedFaceBadSet hp C base κ

Every codimension-two positive-ray failure with a positive movable witness belongs to one of the finite bad sets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.incidence_of_mem_mixedFaceBadSet {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) (hx : x ∈ mixedFaceBadSet hp C base κ) : ∃ (w : StandardSimplex p), ↑w κ.omitted₀ = 0 ∧ ↑w κ.omitted₁ = 0 ∧ (∀ (r : Fin (p - 1)), AffinePositiveRayBoundary.VertexMap.deviation hp ((Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base x) κ.cell).affineValue w) r = 0) ∧ 0 < AffinePositiveRayBoundary.VertexMap.mean p ((Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base x) κ.cell).affineValue w)

Membership in a case bad set reconstructs an explicit positive-ray codimension-two incidence.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.exists_badCase_iff_incidence_with_movableWitness {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), 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

Exact finite-union characterization, under the geometric assertion that all relevant mixed incidences possess a positive movable witness.