Route B on the concrete affine-pullback full collar

This file specializes the finite-dimensional Route B selection theorem to the Step 4 collar and its compactness-derived origin margin. The generic perturbation is then completely automatic from two geometric certificates on the concrete collar:

• positive-ray safety when every positive-support vertex is frozen; and
• nontriviality of every boundary-restricted facet determinant polynomial.

The latter is converted internally into a genuine positive-radius facet-regular neighborhood by RouteB.exists_safePerturbationBall.

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteB.baseData {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) : StableFullCollarOriginMargin.FullCollarOriginMarginData hp H A₀ A₁

Concrete Step 4/5 data used as the base point for Route B.

Equations

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

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteB.GeometricInput {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) : Prop

Exact geometric input still required to run Route B on the concrete collar. The safe ball is not stored: it is constructed from facetPolynomialsNonzero by the open-neighborhood theorem.

• frozenSupportSafe : ExplicitAffineRelativeCollar.RouteB.FrozenPositiveSupportRaySafe hp (baseData hp F₀ F₁ H A₀ A₁).collar.cells (baseData hp F₀ F₁ H A₀ A₁).assignment
• facetPolynomialsNonzero : ExplicitAffineRelativeCollar.RouteB.AllRestrictedFacetPolynomialsNonzero hp (baseData hp F₀ F₁ H A₀ A₁).collar.cells (baseData hp F₀ F₁ H A₀ A₁).assignment

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteB.exists_smallGenericPerturbation_affinePullback {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) (G : GeometricInput hp F₀ F₁ H A₀ A₁) {eps : ℝ} (heps : 0 < eps) : Nonempty (ExplicitAffineRelativeCollar.RouteB.SmallGenericPerturbationResult hp (baseData hp F₀ F₁ H A₀ A₁).collar.cells (baseData hp F₀ F₁ H A₀ A₁).assignment eps (baseData hp F₀ F₁ H A₀ A₁).margin)

Route B instantiated on the Step 4 collar and Step 5 margin.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteB.smallGenericPerturbation_fixesHorizontal {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) (G : GeometricInput hp F₀ F₁ H A₀ A₁) {eps : ℝ} (heps : 0 < eps) : ∃ (R : ExplicitAffineRelativeCollar.RouteB.SmallGenericPerturbationResult hp (baseData hp F₀ F₁ H A₀ A₁).collar.cells (baseData hp F₀ F₁ H A₀ A₁).assignment eps (baseData hp F₀ F₁ H A₀ A₁).margin), ∀ {s : ExplicitAffineRelativeCollar.Parameters.Parameter hp (baseData hp F₀ F₁ H A₀ A₁).collar.cells}, ExplicitAffineRelativeCollar.Parameters.IsFrozenParameter hp (baseData hp F₀ F₁ H A₀ A₁).collar.cells s → ExplicitAffineRelativeCollar.RouteB.assignmentOfMovableParameters hp (baseData hp F₀ F₁ H A₀ A₁).collar.cells (baseData hp F₀ F₁ H A₀ A₁).assignment R.move s = (baseData hp F₀ F₁ H A₀ A₁).assignment s

The selected perturbation fixes the two horizontal endpoint assignments literally.