Concrete Route B assignment on the affine-pullback full collar

This module turns the unconditional existence theorem from StableFullCollarRouteBComplete into a canonical selected perturbation and a concrete perturbed assignment. The exported lemmas expose exactly the data needed by downstream collar/Stokes constructions:

• quantitative closeness to the Step 4 base assignment;
• literal preservation of every frozen parameter, hence both horizontal ends;
• prime equivariance;
• retention of half of the positive origin margin;
• cellwise facet regularity, codimension-two positive-ray avoidance, origin avoidance, and full positive-ray general position.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.routeBPerturbation {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) : ExplicitAffineRelativeCollar.RouteB.SmallGenericPerturbationResult hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).assignment eps (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).margin

A canonical Route B perturbation selected from the unconditional existence result for the concrete affine-pullback collar.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.routeBPerturbation hp F0 F1 H A0 A1 eps heps = Classical.choice ⋯

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.perturbedAssignment {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) : ExplicitAffineRelativeCollar.Parameters.Assignment hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells

The full collar assignment obtained by replacing exactly the movable parameters with the selected Route B perturbation.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.perturbedAssignment_closeToBase {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) : EquivariantPrismGenericPerturbation.AssignmentClose (perturbedAssignment hp F0 F1 H A0 A1 eps heps) (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).assignment eps

The selected assignment is pointwise eps-close to the Step 4 base assignment.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.perturbedAssignment_fixesFrozen {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) {s : ExplicitAffineRelativeCollar.Parameters.Parameter hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells} (hs : ExplicitAffineRelativeCollar.Parameters.IsFrozenParameter hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells s) : perturbedAssignment hp F0 F1 H A0 A1 eps heps s = (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).assignment s

Every frozen parameter is preserved literally.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.perturbedAssignment_equivariant {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) (g : ↥(PrimeSymmetry p)) (v : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (perturbedAssignment hp F0 F1 H A0 A1 eps heps) (g • v) = g • ExplicitAffineRelativeCollar.Parameters.vectorValue hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (perturbedAssignment hp F0 F1 H A0 A1 eps heps) v

The selected full assignment remains prime-equivariant.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.perturbedAssignment_retainedMargin {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) : ExplicitAffineRelativeCollar.RelativeGenericity.LocalAffineCoordinateNormMargin hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (perturbedAssignment hp F0 F1 H A0 A1 eps heps) ((StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).margin / 2)

Half of the Step 2 origin margin is retained by the selected assignment.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.perturbedAssignment_facetRegular {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) (q : (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells.Cell) : AffinePositiveRayBoundary.VertexMap.FacetRegular hp (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (perturbedAssignment hp F0 F1 H A0 A1 eps heps) q)

Every local cell is facet-regular after perturbation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.perturbedAssignment_avoidsPositiveRayCodimTwo {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) (q : (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells.Cell) : AffinePositiveRayBoundary.VertexMap.AvoidsPositiveRayCodimTwo hp (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (perturbedAssignment hp F0 F1 H A0 A1 eps heps) q)

Every local cell avoids the codimension-two positive-ray degeneracies.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.perturbedAssignment_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) (q : (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (perturbedAssignment hp F0 F1 H A0 A1 eps heps) q).AvoidsOrigin

Every local affine cell remains origin-free.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRouteBInstantiation.perturbedAssignment_positiveRayGeneralPosition {p : ℕ} (hp : Nat.Prime p) (F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) (eps : ℝ) (heps : 0 < eps) (q : (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells.Cell) : AffinePositiveRayBoundary.VertexMap.PositiveRayGeneralPosition hp (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (StableFullCollarRouteB.baseData hp F0 F1 H A0 A1).collar.cells (perturbedAssignment hp F0 F1 H A0 A1 eps heps) q)

The selected assignment is in full positive-ray general position on every cell of the new full collar.