Route B, Step 4: one-coordinate affine fibers

A movable parameter is an orbit of scalar sites, so changing one parameter can alter several local coordinates simultaneously. The coefficient below is the total barycentric coefficient of that orbit in one deviation equation. This is the correct replacement for the invalid argument that used only the weight of one retained vertex.

For fixed barycentric data and all other movable parameters, every deviation is an affine function of the distinguished scalar parameter. If one total orbit coefficient is nonzero, the bad fiber is contained in a singleton and therefore has Lebesgue measure zero.

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

The movable parameter selected by a mixed-face case.

Equations

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

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

Indicator that a local scalar site belongs to the selected movable orbit.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.deviationOrbitCoefficient {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (w : StandardSimplex p) (r : Fin (p - 1)) : ℝ

Total coefficient of the selected scalar orbit in one deviation equation. It includes every local occurrence of the same quotient parameter.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.deviationFiberIntercept {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)) : ℝ

The deviation intercept obtained by setting the distinguished parameter to zero while retaining every other movable parameter.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.mixedFaceScalarFiber {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) : Set ℝ

Fixed-barycentric bad fiber in the distinguished scalar coordinate.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.assignment_replace_selected_apply {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) (t : ℝ) (i : Fin (p + 1)) (j : Fin p) : assignmentOfMovableParameters hp C base (replaceCoordinate hp C x (MixedFaceCase.selectedParameter hp C κ) t) (RelativeGenericity.localParameter hp C κ.cell i j) = if RelativeGenericity.localParameter hp C κ.cell i j = ↑(MixedFaceCase.selectedParameter hp C κ) then t else assignmentOfMovableParameters hp C base (replaceCoordinate hp C x (MixedFaceCase.selectedParameter hp C κ) 0) (RelativeGenericity.localParameter hp C κ.cell i j)

Replacing the selected coordinate evaluates a local scalar site by t exactly when that site belongs to the selected orbit.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.deviation_replace_selected {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)) (t : ℝ) : AffinePositiveRayBoundary.VertexMap.deviation hp ((Polynomials.localVertexMap hp C (assignmentOfMovableParameters hp C base (replaceCoordinate hp C x (MixedFaceCase.selectedParameter hp C κ) t)) κ.cell).affineValue w) r = deviationFiberIntercept hp C base x κ w r + t * deviationOrbitCoefficient hp C κ w r

Every deviation is affine in the selected scalar orbit, with the total orbit coefficient defined above.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.mixedFaceScalarFiber_subset_singleton {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) : mixedFaceScalarFiber hp C base x κ w ⊆ {-deviationFiberIntercept hp C base x κ w r / deviationOrbitCoefficient hp C κ w r}

A nonzero deviation coefficient forces every bad scalar to equal one explicit value.

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

Under one nonzero total orbit coefficient, the fixed-barycentric bad fiber has one-dimensional Lebesgue measure zero.