Unconditional Route B perturbation on the affine-pullback full collar

This module combines the two concrete geometric certificates proved for the Step 4 collar:

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

The open-neighborhood theorem in RouteBSmallGenericPerturbation converts the second certificate into a positive-radius facet-regular perturbation ball. The generic Route B selection theorem then produces a small, frozen-boundary-preserving, prime-equivariant perturbation in full positive-ray general position while retaining half of the Step 5 origin margin.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.frozenPositiveSupportRaySafe_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) : ExplicitAffineRelativeCollar.RouteB.FrozenPositiveSupportRaySafe hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment

Item 3.1: the concrete affine-pullback full collar is safe whenever every positive-weight local vertex is frozen. This is the exact support-level hypothesis used by Route B; zero-weight movable vertices are intentionally irrelevant.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.safePerturbationBall_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) {eps : ℝ} (heps : 0 < eps) : Nonempty (ExplicitAffineRelativeCollar.RouteB.SafePerturbationBall hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment eps (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).margin)

Item 3.2: every positive requested perturbation size admits a genuine positive-radius neighborhood around a nearby generic center. Throughout this ball the reconstructed full assignment stays within the independent control radius min eps (margin / 2) of the Step 4 base assignment and every local facet remains regular.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.chosenSafePerturbationBallAffinePullback {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) {eps : ℝ} (heps : 0 < eps) : ExplicitAffineRelativeCollar.RouteB.SafePerturbationBall hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment eps (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).margin

A canonical safe perturbation ball, selected noncomputably from Item 3.2.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.chosenSafePerturbationBallAffinePullback hp F₀ F₁ H A₀ A₁ heps = Classical.choice ⋯

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.chosenSafePerturbationBall_affinePullback_radius_pos {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) {eps : ℝ} (heps : 0 < eps) : 0 < (chosenSafePerturbationBallAffinePullback hp F₀ F₁ H A₀ A₁ heps).radius

The selected Item 3.2 neighborhood has positive radius.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.chosenSafePerturbationBall_affinePullback_closeToBase {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) {eps : ℝ} (heps : 0 < eps) (x : ExplicitAffineRelativeCollar.RouteB.MovableParameterSpace hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells) (hx : x ∈ Metric.ball (chosenSafePerturbationBallAffinePullback hp F₀ F₁ H A₀ A₁ heps).center (chosenSafePerturbationBallAffinePullback hp F₀ F₁ H A₀ A₁ heps).radius) : EquivariantPrismGenericPerturbation.AssignmentClose (ExplicitAffineRelativeCollar.RouteB.assignmentOfMovableParameters hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment x) (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment (ExplicitAffineRelativeCollar.RouteB.perturbationControlRadius eps (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).margin)

Every point in the selected Item 3.2 neighborhood reconstructs an assignment within the required control radius of the Step 4 base assignment.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.chosenSafePerturbationBall_affinePullback_facetRegular {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) {eps : ℝ} (heps : 0 < eps) (x : ExplicitAffineRelativeCollar.RouteB.MovableParameterSpace hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells) (hx : x ∈ Metric.ball (chosenSafePerturbationBallAffinePullback hp F₀ F₁ H A₀ A₁ heps).center (chosenSafePerturbationBallAffinePullback hp F₀ F₁ H A₀ A₁ heps).radius) : ExplicitAffineRelativeCollar.RouteB.AllCellsFacetRegular hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment x

Every point in the selected Item 3.2 neighborhood is facet-regular on all cells of the concrete full collar.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.baseData_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) : StableFullCollarRouteB.GeometricInput hp F₀ F₁ H A₀ A₁

The concrete affine-pullback collar supplies every geometric input required by Route B.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.exists_smallGenericPerturbation_affinePullback_unconditional {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) {eps : ℝ} (heps : 0 < eps) : Nonempty (ExplicitAffineRelativeCollar.RouteB.SmallGenericPerturbationResult hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment eps (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).margin)

Steps 2 and 3 specialized to the concrete Step 4 collar: for every positive requested size, there is a small generic perturbation preserving the two horizontal boundary assignments, retaining a positive origin margin, and putting every collar cell in positive-ray general position.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.smallGenericPerturbation_affinePullback_exists {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) {eps : ℝ} (heps : 0 < eps) : ∃ (R : ExplicitAffineRelativeCollar.RouteB.SmallGenericPerturbationResult hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment eps (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).margin), (∀ {s : ExplicitAffineRelativeCollar.Parameters.Parameter hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells}, ExplicitAffineRelativeCollar.Parameters.IsFrozenParameter hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells s → ExplicitAffineRelativeCollar.RouteB.assignmentOfMovableParameters hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment R.move s = (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment s) ∧ ∀ (q : (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells.Cell), AffinePositiveRayBoundary.VertexMap.PositiveRayGeneralPosition hp (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (ExplicitAffineRelativeCollar.RouteB.assignmentOfMovableParameters hp (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).collar.cells (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).assignment R.move) q)

An explicit witness form of the unconditional Route B output.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBComplete.smallGenericPerturbation_affinePullback_retainedMargin_pos {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) : 0 < (StableFullCollarRouteB.baseData hp F₀ F₁ H A₀ A₁).margin / 2

The retained margin in the unconditional perturbation is strictly positive.