Stable endpoint approximations and a boundary-relative prism perturbation

The unrestricted finite generic perturbation already produces transverse horizontal boundary data. This module turns those finite boundary samples into genuine continuous equivariant coordinate maps. The construction uses finite cardinal interpolation on the sampled horizontal vertices, followed by averaging over the prime symmetry group. It therefore has three properties simultaneously:

• it is continuous and prime-equivariant;
• it agrees exactly with the generic prism assignment at every horizontal sampled vertex;
• its refined affine samples inherit facet regularity and codimension-two avoidance from the prism.

The resulting lower and upper maps are StableRegularApproximations at the exact horizontal triangulation level. The original generic prism assignment is then a relative perturbation with those two boundary maps fixed by construction; no second generic perturbation is required.

inductive NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointSide : Type

The two horizontal components of the prism boundary.

• lower : EndpointSide
• upper : EndpointSide

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.instDecidableEqEndpointSide : DecidableEq EndpointSide

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.instDecidableEqEndpointSide x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.instFintypeEndpointSide : Fintype EndpointSide

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointSide.time : EndpointSide → ℝ

Numerical time attached to an endpoint side.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointSide.lower.time = 0
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointSide.upper.time = 1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointSide.time_lower : lower.time = 0

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointSide.time_upper : upper.time = 1

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointSide.zeroFreeMap {p : ℕ} (s : EndpointSide) {hp : Nat.Prime p} {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} : EquivariantCoordinateHomotopy.ZeroFreeMap hp

The endpoint map associated with a side.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointSide.lower.zeroFreeMap = F₀
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointSide.upper.zeroFreeMap = F₁

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.IsEndpointVertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (x : EquivariantPrismVertexParameters.GlobalVertex hp N L) : Prop

A sampled global prism vertex lies on a specified horizontal boundary.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.IsEndpointVertex hp N L s x = (↑(NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalPoint hp N L x).time = s.time)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointVertexDecidable {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (x : EquivariantPrismVertexParameters.GlobalVertex hp N L) : Decidable (IsEndpointVertex hp N L s x)

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointVertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) : Type

Finite set of global sampled vertices on one horizontal component.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointVertexFintype {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) : Fintype (EndpointVertex hp N L s)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointVertexDecidableEq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) : DecidableEq (EndpointVertex hp N L s)

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointSpatialPoint {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (x : EndpointVertex hp N L s) : Realization p

Spatial point represented by a horizontal sampled vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointSpatialPoint hp N L s x = (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalPoint hp N L ↑x).spatial

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointSpatialPoint_injective {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) : Function.Injective (endpointSpatialPoint hp N L s)

On a fixed horizontal component, the spatial point determines the global sampled vertex.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointCardinalWeight {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (v : EndpointVertex hp N L s) (x : Realization p) : ℝ

Cardinal interpolation weight for one horizontal sampled vertex.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointCardinalWeight_self {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (v : EndpointVertex hp N L s) : endpointCardinalWeight hp N L s v (endpointSpatialPoint hp N L s v) = 1

A cardinal weight is one at its own sampled vertex.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointCardinalWeight_other {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) {u v : EndpointVertex hp N L s} (huv : u ≠ v) : endpointCardinalWeight hp N L s v (endpointSpatialPoint hp N L s u) = 0

A cardinal weight vanishes at every other sampled vertex.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.rawEndpointInterpolant {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (a : EquivariantPrismVertexParameters.Assignment hp N L) (x : Realization p) : Fin p → ℝ

Raw finite cardinal interpolation of the boundary samples.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.rawEndpointInterpolant_sample {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (a : EquivariantPrismVertexParameters.Assignment hp N L) (v : EndpointVertex hp N L s) : rawEndpointInterpolant hp N L s a (endpointSpatialPoint hp N L s v) = EquivariantPrismVertexParameters.vectorValue hp N L a ↑v

The raw interpolant realizes every prescribed horizontal sample.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointInterpolant {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (a : EquivariantPrismVertexParameters.Assignment hp N L) : RefinedAffineMap.ContinuousCoordinateMap p

Prime-symmetrization of the raw interpolant. Averaging makes equivariance automatic while preserving all already-equivariant sampled values.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointInterpolant_equivariant {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (a : EquivariantPrismVertexParameters.Assignment hp N L) : IsEquivariantCoordinateMap p (endpointInterpolant hp N L s a)

The symmetrized endpoint interpolant is prime-equivariant.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointInterpolant_sample {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (a : EquivariantPrismVertexParameters.Assignment hp N L) (v : EndpointVertex hp N L s) : (endpointInterpolant hp N L s a) (endpointSpatialPoint hp N L s v) = EquivariantPrismVertexParameters.vectorValue hp N L a ↑v

The symmetrized interpolant still realizes every horizontal sample.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointPrismCell {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : SubdivisionPrismCharts.PrismCell hp N L

Canonical prism cell used to realize one endpoint simplex.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointOmittedIndex {p : ℕ} (L : ℕ) (s : EndpointSide) : Fin (p + 1)

Facet omitted from the canonical endpoint prism cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointOccurrence {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : EquivariantPrismGlobalCancellation.FacetOccurrence hp N L

Canonical facet occurrence realizing one endpoint simplex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointOccurrence_facetSignature {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) (i : Fin p) : (RelativeCollarMiddlePrism.cellSystem hp N L).facetSignature (endpointOccurrence hp N L s q eta) i = match s with | EndpointSide.lower => ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp (N + L) (EndpointFaceRefinement.endpointTopCell hp N L q eta) (Fin.cast ⋯ i)) | EndpointSide.upper => ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp (N + L) (EndpointFaceRefinement.endpointTopCell hp N L q eta) (Fin.cast ⋯ i))

The canonical endpoint occurrence has exactly the expected refined endpoint vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointInterpolant_vertexValue {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) (i : Fin p) : (endpointInterpolant hp N L s a) (EquivariantPrismHorizontalEndpointIdentification.endpointSpatialMap hp N L q eta (SphereOddDegree.FiniteSimplex.vertex (Fin.cast ⋯ i))) = EquivariantPrismVertexParameters.vectorValue hp N L a (EquivariantPrismVertexParameters.sampleVertex hp N L ((endpointOccurrence hp N L s q eta).1, (endpointOccurrence hp N L s q eta).2.succAbove i))

Boundary samples of an assignment agree with the corresponding endpoint interpolant.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointInterpolant_regular {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hregular : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.FacetRegular hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) (q : RefinedAffineMap.TopCell hp (N + L)) : RefinedAffineMap.determinant hp (N + L) (endpointInterpolant hp N L s a) q ≠ 0

Endpoint regularity inherited from the corresponding canonical horizontal facets of a generic prism assignment.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.DeviationSkeletonFree {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : RefinedAffineMap.ContinuousCoordinateMap p) : Prop

Strong skeleton transversality: no deviation-zero point lies on the boundary of a refined top simplex, without imposing a sign condition on the common coordinate mean.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointInterpolant_deviationSkeletonFree {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hcodim : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.AvoidsCodimTwoDeviationZero hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) : DeviationSkeletonFree hp (N + L) (endpointInterpolant hp N L s a)

Endpoint skeleton transversality inherited from prism codimension-two avoidance.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointInterpolant_skeletonFree {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hcodim : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.AvoidsCodimTwoDeviationZero hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) : RefinedAffineMap.PositiveRaySkeletonFree hp (N + L) (endpointInterpolant hp N L s a)

Endpoint skeleton transversality inherited from prism codimension-two avoidance.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStraightLineSafe {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (a : EquivariantPrismVertexParameters.Assignment hp N L) : Prop

Quantitative endpoint closeness needed for the stored zero-free straight-line field.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.stableEndpointApproximation {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : EndpointSide) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (a : EquivariantPrismVertexParameters.Assignment hp N L) (hregular : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.FacetRegular hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) (hcodim : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.AvoidsCodimTwoDeviationZero hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) (hsafe : EndpointStraightLineSafe hp N L s a) : RefinedAffineMap.StableRegularApproximation hp s.zeroFreeMap.map

Stable endpoint approximation extracted from one generic prism assignment.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.segment_ne_zero_of_norm_sub_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} {r : ℝ} (hr : r ≤ ‖x‖) (hxy : ‖y - x‖ < r) (u : ↑(Set.Icc 0 1)) : (1 - ↑u) • x + ↑u • y ≠ 0

A vector segment cannot hit the origin when its second endpoint is closer to the first than the norm of the first.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointControl {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (a : EquivariantPrismVertexParameters.Assignment hp N L) (r : ℝ) : Prop

Quantitative endpoint information used to construct stable approximations from a prism result.

• positive : 0 < r
• normLower (s : EndpointSide) (q : RefinedAffineMap.TopCell hp (N + L)) (w : StandardSimplex (p - 1)) : r ≤ ‖s.zeroFreeMap.map ((RefinedAffineMap.chart hp (N + L) q) (StandardSimplex.toDelta w))‖
• close (s : EndpointSide) (q : RefinedAffineMap.TopCell hp (N + L)) (w : StandardSimplex (p - 1)) : ‖RefinedAffineMap.value hp (N + L) (endpointInterpolant hp N L s a) q w - s.zeroFreeMap.map ((RefinedAffineMap.chart hp (N + L) q) (StandardSimplex.toDelta w))‖ < r

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointStraightLineSafe_of_control {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (a : EquivariantPrismVertexParameters.Assignment hp N L) {r : ℝ} (C : EndpointControl hp N L H a r) (s : EndpointSide) : EndpointStraightLineSafe hp N L s a

Endpoint control makes both straight-line interpolations zero-free.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.Result.lowerStableApproximation {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) {m r : ℝ} (R : EquivariantPrismGenericPerturbation.Result hp N L H m) (C : EndpointControl hp N L H R.assignment r) : RefinedAffineMap.StableRegularApproximation hp F₀.map

A generic prism result with controlled horizontal approximation determines a stable lower endpoint approximation at the exact horizontal triangulation level.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.Result.upperStableApproximation {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) {m r : ℝ} (R : EquivariantPrismGenericPerturbation.Result hp N L H m) (C : EndpointControl hp N L H R.assignment r) : RefinedAffineMap.StableRegularApproximation hp F₁.map

Stable upper endpoint approximation extracted from the same controlled prism result.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.BoundaryFixed {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) (a : EquivariantPrismVertexParameters.Assignment hp N L) : Prop

An assignment is relative to two endpoint approximations when its horizontal samples agree exactly with their sampled maps.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.Result.boundaryFixed {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) {m r : ℝ} (R : EquivariantPrismGenericPerturbation.Result hp N L H m) (C : EndpointControl hp N L H R.assignment r) : BoundaryFixed hp N L (lowerStableApproximation hp N L H R C) (upperStableApproximation hp N L H R C) R.assignment

The endpoint approximations extracted from a result are fixed boundaries for that same prism assignment.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeResult {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (m : ℝ) : Type

Complete boundary-relative output: two stable endpoint approximations and one compatible prime-equivariant prism assignment which keeps their horizontal samples fixed.

• prism : EquivariantPrismGenericPerturbation.Result hp N L H m

  The generic prism perturbation underlying the relative-boundary result.

• lower : RefinedAffineMap.StableRegularApproximation hp F₀.map

  The stable regular approximation fixed on the lower endpoint.

• upper : RefinedAffineMap.StableRegularApproximation hp F₁.map

  The stable regular approximation fixed on the upper endpoint.

• boundaryFixed : BoundaryFixed hp N L self.lower self.upper self.prism.assignment

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.Result.toRelativeResult {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) {m r : ℝ} (R : EquivariantPrismGenericPerturbation.Result hp N L H m) (C : EndpointControl hp N L H R.assignment r) : RelativeResult hp N L H m

Construct stable endpoint approximations and a generic prism perturbation relative to their fixed transverse horizontal boundaries.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.oscillation_further_refinement {p : ℕ} (hp : Nat.Prime p) (F : RefinedAffineMap.ContinuousCoordinateMap p) (N K : ℕ) {eps : ℝ} (hosc : ∀ (q : RefinedAffineMap.TopCell hp N) (u v : StandardSimplex (p - 1)), dist (F ((RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta u))) (F ((RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta v))) < eps) (q : RefinedAffineMap.TopCell hp (N + K)) (u v : StandardSimplex (p - 1)) : dist (F ((RefinedAffineMap.chart hp (N + K) q) (StandardSimplex.toDelta u))) (F ((RefinedAffineMap.chart hp (N + K) q) (StandardSimplex.toDelta v))) < eps

Oscillation on level N persists on every further barycentric refinement.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.exists_common_endpoint_oscillation {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) {eps : ℝ} (heps : 0 < eps) : ∃ (N : ℕ), (∀ (q : RefinedAffineMap.TopCell hp N) (u v : StandardSimplex (p - 1)), dist (F₀.map ((RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta u))) (F₀.map ((RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta v))) < eps) ∧ ∀ (q : RefinedAffineMap.TopCell hp N) (u v : StandardSimplex (p - 1)), dist (F₁.map ((RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta u))) (F₁.map ((RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta v))) < eps

One spatial level can be chosen so that both endpoint maps have small oscillation on every refined top simplex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.norm_endpoint_value_sub_homotopy_value_le {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (a : EquivariantPrismVertexParameters.Assignment hp N L) {eps : ℝ} (hclose : EquivariantPrismGenericPerturbation.AssignmentClose a (EquivariantPrismVertexParameters.homotopyAssignment hp N L H) eps) (s : EndpointSide) (q : RefinedAffineMap.TopCell hp (N + L)) (w : StandardSimplex (p - 1)) : ‖RefinedAffineMap.value hp (N + L) (endpointInterpolant hp N L s a) q w - RefinedAffineMap.value hp (N + L) (endpointInterpolant hp N L s (EquivariantPrismVertexParameters.homotopyAssignment hp N L H)) q w‖ ≤ eps

Coordinatewise closeness of global assignments bounds the endpoint affine interpolants in the finite product norm.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.endpointInterpolant_homotopyAssignment_value {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (s : EndpointSide) (q : RefinedAffineMap.TopCell hp (N + L)) (w : StandardSimplex (p - 1)) : RefinedAffineMap.value hp (N + L) (endpointInterpolant hp N L s (EquivariantPrismVertexParameters.homotopyAssignment hp N L H)) q w = RefinedAffineMap.value hp (N + L) s.zeroFreeMap.map q w

At a horizontal endpoint, the interpolant of the unperturbed homotopy assignment is the affine interpolation of the corresponding endpoint map samples.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.exists_controlled_generic_perturbation {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) : ∃ (N : ℕ) (L : ℕ) (m : ℝ) (r : ℝ), 0 < m ∧ ∃ (R : EquivariantPrismGenericPerturbation.Result hp N L H m), EndpointControl hp N L H R.assignment r

A sufficiently fine generic prism perturbation comes with quantitative endpoint control.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.exists_stable_relative_result {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) : ∃ (N : ℕ) (L : ℕ) (m : ℝ), 0 < m ∧ Nonempty (RelativeResult hp N L H m)

Stable endpoint approximations and a boundary-relative generic prism exist for every zero-free equivariant homotopy.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeResult.lower_zeroCount_eq_endpointRefinedCount {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (m : ℝ) (R : RelativeResult hp N L H m) : R.lower.zeroCount = EquivariantPrismHorizontalEndpointIdentification.lowerEndpointRefinedCount hp N L R.prism.assignment

The induced lower horizontal count is the stable lower approximation count.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeResult.upper_zeroCount_eq_endpointRefinedCount {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (m : ℝ) (R : RelativeResult hp N L H m) : R.upper.zeroCount = EquivariantPrismHorizontalEndpointIdentification.upperEndpointRefinedCount hp N L R.prism.assignment

The induced upper horizontal count is the stable upper approximation count.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeResult.stable_zeroCount_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (m : ℝ) (R : RelativeResult hp N L H m) : R.lower.zeroCount = R.upper.zeroCount

The two constructed stable endpoint approximations have equal positive-ray counts.