Zero-free endpoint bridges for stable regular approximations

A stable regular approximation stores a finite family of refined vertex samples and a zero-free straight-line comparison between the original map and their affine interpolation on every refined top simplex. For the relative collar we need a genuine global endpoint map whose values at those refined vertices are exactly the stored samples.

The construction below does not attempt to glue the local affine formulas globally. Instead it uses a finite, localized correction of the original map.

• Include every prime translate of every refined endpoint vertex in a finite sample family.
• Around each sample point, the straight segment from the original map to the approximation's global sampling map remains zero-free on a sufficiently small ball.
• A finite continuous bump is one at every sample point and supported in the union of those safe balls.
• Averaging the bump over the prime group makes it invariant without changing its value on the invariant sample family or enlarging its support outside the safe locus.
• Blending the original map with the sampling map by this invariant bump gives a continuous, equivariant, zero-free global map. It agrees exactly with the approximation at every refined vertex, and the straight line from the original map to the blended map is zero-free.

Thus every StableRegularApproximation canonically determines the ZeroFreeEndpointInterpolant required by the exact relative-collar interface.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.SegmentSafe {p : ℕ} (F G : RefinedAffineMap.ContinuousCoordinateMap p) (x : Realization p) : Prop

Pointwise straight-segment safety between two coordinate maps.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.SegmentSafe F G x = ∀ (t : ↑(Set.Icc 0 1)), (1 - ↑t) • F x + ↑t • G x ≠ 0

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.segmentFamily {p : ℕ} (F G : RefinedAffineMap.ContinuousCoordinateMap p) : C(Realization p × ↑(Set.Icc 0 1), Fin p → ℝ)

The jointly continuous straight-segment evaluation map.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.exists_positive_segment_margin_at {p : ℕ} (F G : RefinedAffineMap.ContinuousCoordinateMap p) (x : Realization p) (hsafe : SegmentSafe F G x) : ∃ (m : ℝ), 0 < m ∧ ∀ (t : ↑(Set.Icc 0 1)), m ≤ ‖(1 - ↑t) • F x + ↑t • G x‖

A safe segment at one point has a positive norm margin, uniformly in the segment parameter.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.exists_segmentSafe_ball {p : ℕ} (F G : RefinedAffineMap.ContinuousCoordinateMap p) (x : Realization p) (hsafe : SegmentSafe F G x) : ∃ (r : ℝ), 0 < r ∧ ∀ y ∈ Metric.ball x r, SegmentSafe F G y

Segment safety persists on a metric neighborhood of a safe point.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.SampleIndex {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : Type

One finite index for every prime translate of every refined endpoint vertex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.samplePoint {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (z : SampleIndex hp N) : Realization p

Spatial point represented by a sample index.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.samplePoint hp N z = z.1 • NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.vertex hp N z.2.1 z.2.2

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.samplePoint_mul {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (h : ↥(PrimeSymmetry p)) (z : SampleIndex hp N) : samplePoint hp N (h * z.1, z.2) = h • samplePoint hp N z

Left multiplication on the group coordinate realizes the prime action on sample points.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.segmentSafe_smul (p : ℕ) (F G : RefinedAffineMap.ContinuousCoordinateMap p) (hF : IsEquivariantCoordinateMap p F) (hG : IsEquivariantCoordinateMap p G) {x : Realization p} (hx : SegmentSafe F G x) (g : ↥(PrimeSymmetry p)) : SegmentSafe F G (g • x)

Segment safety is transported by prime equivariance.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.segmentSafe_smul_iff (p : ℕ) (F G : RefinedAffineMap.ContinuousCoordinateMap p) (hF : IsEquivariantCoordinateMap p F) (hG : IsEquivariantCoordinateMap p G) (x : Realization p) (g : ↥(PrimeSymmetry p)) : SegmentSafe F G (g • x) ↔ SegmentSafe F G x

Segment safety is equivalent along a prime orbit.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.segmentSafe_refinedVertex {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (q : RefinedAffineMap.TopCell hp A.level) (i : Fin (p - 1 + 1)) : SegmentSafe F.map A.map (RefinedAffineMap.vertex hp A.level q i)

The stored simplexwise straight-line condition is safe at every refined vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.segmentSafe_samplePoint {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) : SegmentSafe F.map A.map (samplePoint hp A.level z)

Every translated endpoint sample has a safe segment to the approximation's sampling map.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.sampleRadius {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) : ℝ

A chosen positive radius on which one sample's full segment remains safe.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.sampleRadius hp F A z = Classical.choose ⋯

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.sampleRadius_pos {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) : 0 < sampleRadius hp F A z

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.segmentSafe_of_mem_sampleBall {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) (x : Realization p) (hx : x ∈ Metric.ball (samplePoint hp A.level z) (sampleRadius hp F A z)) : SegmentSafe F.map A.map x

The chosen ball around a sample lies in the pointwise safe locus.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.sampleBump {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) (x : Realization p) : ℝ

Continuous radial bump supported in one chosen safe ball.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.sampleBump_self {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) : sampleBump hp F A z (samplePoint hp A.level z) = 1

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.sampleBump_nonneg {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) (x : Realization p) : 0 ≤ sampleBump hp F A z x

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.sampleBump_le_one {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) (x : Realization p) : sampleBump hp F A z x ≤ 1

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.continuous_sampleBump {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) : Continuous (sampleBump hp F A z)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.mem_sampleBall_of_sampleBump_pos {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) (x : Realization p) (hx : 0 < sampleBump hp F A z x) : x ∈ Metric.ball (samplePoint hp A.level z) (sampleRadius hp F A z)

A positive sample bump certifies membership in its safe ball.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.rawBridgeWeight {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (x : Realization p) : ℝ

Unsymmetrized finite bump: one on every endpoint sample and supported in the union of safe sample balls.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.continuous_rawBridgeWeight {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) : Continuous (rawBridgeWeight hp F A)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.rawBridgeWeight_nonneg {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (x : Realization p) : 0 ≤ rawBridgeWeight hp F A x

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.rawBridgeWeight_le_one {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (x : Realization p) : rawBridgeWeight hp F A x ≤ 1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.rawBridgeWeight_sample {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z0 : SampleIndex hp A.level) : rawBridgeWeight hp F A (samplePoint hp A.level z0) = 1

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.segmentSafe_of_rawBridgeWeight_pos {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (x : Realization p) (hx : 0 < rawBridgeWeight hp F A x) : SegmentSafe F.map A.map x

Positivity of the raw bump implies full pointwise segment safety.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.bridgeWeight {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (x : Realization p) : ℝ

Prime-invariant average of the raw bridge weight.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.continuous_bridgeWeight {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) : Continuous (bridgeWeight hp F A)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.bridgeWeight_nonneg {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (x : Realization p) : 0 ≤ bridgeWeight hp F A x

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.bridgeWeight_le_one {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (x : Realization p) : bridgeWeight hp F A x ≤ 1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.bridgeWeight_smul {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (h : ↥(PrimeSymmetry p)) (x : Realization p) : bridgeWeight hp F A (h • x) = bridgeWeight hp F A x

The averaged bridge weight is prime-invariant.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.bridgeWeight_sample {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) : bridgeWeight hp F A (samplePoint hp A.level z) = 1

The averaged weight remains one on every translated refined endpoint vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.segmentSafe_of_bridgeWeight_pos {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (x : Realization p) (hx : 0 < bridgeWeight hp F A x) : SegmentSafe F.map A.map x

A positive averaged weight still lies in the full safe locus.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.bridgedMap {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) : EquivariantCoordinateHomotopy.ZeroFreeMap hp

Global localized endpoint map. It agrees with the approximation's sampling map at every refined endpoint vertex, but returns to the original map away from the finite safe neighborhood.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.bridgedMap_sample {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (z : SampleIndex hp A.level) : (bridgedMap hp F A).map (samplePoint hp A.level z) = A.map (samplePoint hp A.level z)

The bridged map has exactly the stored approximation value at every translated refined vertex.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.bridgedMap_refinedVertex {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (q : RefinedAffineMap.TopCell hp A.level) (i : Fin (p - 1 + 1)) : (bridgedMap hp F A).map (RefinedAffineMap.vertex hp A.level q i) = A.map (RefinedAffineMap.vertex hp A.level q i)

In particular, every canonical refined vertex is fixed to the stored endpoint sample.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.bridgedMap_zeroFreeStraightLine {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (x : Realization p) (t : ↑(Set.Icc 0 1)) : (1 - ↑t) • F.map x + ↑t • (bridgedMap hp F A).map x ≠ 0

The straight line from the original map to the localized bridged map is zero-free.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.endpointInterpolant {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) : StableCollarRelativeSubdivisionExact.ZeroFreeEndpointInterpolant hp F

Every stable regular approximation supplies the global zero-free endpoint interpolant required by the exact relative-collar construction.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.endpointInterpolant_refinedVertex {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (q : RefinedAffineMap.TopCell hp A.level) (i : Fin (p - 1 + 1)) : (endpointInterpolant hp F A).map.map (RefinedAffineMap.vertex hp A.level q i) = A.map (RefinedAffineMap.vertex hp A.level q i)

The endpoint interpolant has exactly the approximation's refined vertex samples.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableEndpointBridges.endpointBridgePair {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) : StableCollarRelativeSubdivisionExact.ZeroFreeEndpointInterpolant hp F₀ × StableCollarRelativeSubdivisionExact.ZeroFreeEndpointInterpolant hp F₁

Simultaneous lower and upper endpoint bridges.

Equations

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