Compatible refined-chart maps and PL-ended homotopies

A regular endpoint approximation supplies a zero-free affine interpolation on every refined top simplex. The carrier theorem proves that these local formulas agree on shared faces, including prime-translated chart occurrences. This module packages those formulas as compatible chart maps and constructs a chartwise zero-free homotopy

PL(A₀) -> F₀ -> H -> F₁ -> PL(A₁).

The package is deliberately chart-local: Step 4 only samples finitely many affine collar vertices, so no global quotient-map construction is required. Decorated compatibility is exactly the condition needed for those samples to descend to global collar vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.continuous_toDelta {d : ℕ} : Continuous StandardSimplex.toDelta

The project simplex presentation maps continuously to the topological simplex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.continuous_ofDelta {d : ℕ} : Continuous StandardSimplex.ofDelta

The topological simplex maps continuously to the project simplex presentation.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartMap {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : Type

A prime-compatible zero-free map written in every refined top-simplex chart.

• value : RefinedAffineMap.TopCell hp N → StandardSimplex (p - 1) → Fin p → ℝ

  Coordinate values in each refined top-simplex chart.

• continuous_value (q : RefinedAffineMap.TopCell hp N) : Continuous (self.value q)
• decorated_compatible (g h : ↥(PrimeSymmetry p)) (q r : RefinedAffineMap.TopCell hp N) (w v : StandardSimplex (p - 1)) : g • (RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta w) = h • (RefinedAffineMap.chart hp N r) (StandardSimplex.toDelta v) → g • self.value q w = h • self.value r v
• zeroFree (q : RefinedAffineMap.TopCell hp N) (w : StandardSimplex (p - 1)) : self.value q w ≠ 0

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartHomotopy {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (K0 K1 : ChartMap hp N) : Type

A compatible chart homotopy between two compatible chart maps.

• value : RefinedAffineMap.TopCell hp N → StandardSimplex (p - 1) → ↑(Set.Icc 0 1) → Fin p → ℝ

  The time-dependent coordinate values in each refined chart.

• continuous_value (q : RefinedAffineMap.TopCell hp N) : Continuous fun (z : StandardSimplex (p - 1) × ↑(Set.Icc 0 1)) => self.value q z.1 z.2
• value_zero (q : RefinedAffineMap.TopCell hp N) (w : StandardSimplex (p - 1)) : self.value q w ⟨0, _proof_1⟩ = K0.value q w
• value_one (q : RefinedAffineMap.TopCell hp N) (w : StandardSimplex (p - 1)) : self.value q w ⟨1, _proof_2⟩ = K1.value q w
• decorated_compatible (g h : ↥(PrimeSymmetry p)) (q r : RefinedAffineMap.TopCell hp N) (w v : StandardSimplex (p - 1)) (t : ↑(Set.Icc 0 1)) : g • (RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta w) = h • (RefinedAffineMap.chart hp N r) (StandardSimplex.toDelta v) → g • self.value q w t = h • self.value r v t
• zeroFree (q : RefinedAffineMap.TopCell hp N) (w : StandardSimplex (p - 1)) (t : ↑(Set.Icc 0 1)) : self.value q w t ≠ 0

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ancestorTopCell {p : ℕ} (hp : Nat.Prime p) (N k : ℕ) (q : RefinedAffineMap.TopCell hp (N + k)) : RefinedAffineMap.TopCell hp N

Prefix top cell of a chart after k additional subdivision stages.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ancestorTail {p : ℕ} {hp : Nat.Prime p} (N k : ℕ) (q : RefinedAffineMap.TopCell hp (N + k)) : RefinementWord p k

Tail subdivision word of a chart after splitting off its first N stages.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ancestorWeight {p : ℕ} {hp : Nat.Prime p} (N k : ℕ) (q : RefinedAffineMap.TopCell hp (N + k)) (w : StandardSimplex (p - 1)) : StandardSimplex (p - 1)

Pull a standard-simplex coordinate back to the ancestor chart.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.chart_eq_ancestor {p : ℕ} (hp : Nat.Prime p) (N k : ℕ) (q : RefinedAffineMap.TopCell hp (N + k)) (w : StandardSimplex (p - 1)) : (RefinedAffineMap.chart hp (N + k) q) (StandardSimplex.toDelta w) = (RefinedAffineMap.chart hp N (ancestorTopCell hp N k q)) (StandardSimplex.toDelta (ancestorWeight N k q w))

A refined chart factors through its ancestor chart.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.continuous_ancestorWeight {p : ℕ} {hp : Nat.Prime p} (N k : ℕ) (q : RefinedAffineMap.TopCell hp (N + k)) : Continuous fun (w : StandardSimplex (p - 1)) => ancestorWeight N k q w

Pullback of standard-simplex coordinates to an ancestor chart is continuous.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartMap.refine {p : ℕ} {hp : Nat.Prime p} {N : ℕ} (K : ChartMap hp N) (k : ℕ) : ChartMap hp (N + k)

Further spatial refinement of a compatible chart map.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartHomotopy.refine {p : ℕ} {hp : Nat.Prime p} {N : ℕ} {K0 K1 : ChartMap hp N} (J : ChartHomotopy hp N K0 K1) (k : ℕ) : ChartHomotopy hp (N + k) (K0.refine k) (K1.refine k)

Further spatial refinement of a compatible chart homotopy.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.baseOriginalPLMap {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) : ChartMap hp A.level

The affine interpolation stored by one regular approximation, as a compatible chart map.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.originalPLMap {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (k : ℕ) : ChartMap hp (A.level + k)

The same original PL interpolation represented on a further subdivision.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ofGlobalMap {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) : ChartMap hp N

A compatible chart map induced by one global zero-free equivariant map.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.clampUnit (x : ℝ) : ↑(Set.Icc 0 1)

Clamp a real number into the unit interval.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.clampUnit x = ⟨min 1 (max 0 x), ⋯⟩

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.continuous_clampUnit : Continuous clampUnit

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartHomotopy.refl {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (K : ChartMap hp N) : ChartHomotopy hp N K K

Constant compatible chart homotopy.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartHomotopy.symm {p : ℕ} {hp : Nat.Prime p} {N : ℕ} {K0 K1 : ChartMap hp N} (J : ChartHomotopy hp N K0 K1) : ChartHomotopy hp N K1 K0

Reverse a compatible chart homotopy.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartHomotopy.trans {p : ℕ} {hp : Nat.Prime p} {N : ℕ} {K0 K1 K2 : ChartMap hp N} (J01 : ChartHomotopy hp N K0 K1) (J12 : ChartHomotopy hp N K1 K2) : ChartHomotopy hp N K0 K2

Concatenate compatible chart homotopies.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ofGlobalHomotopy {p : ℕ} (hp : Nat.Prime p) (N : ℕ) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) : ChartHomotopy hp N (ofGlobalMap hp N F0) (ofGlobalMap hp N F1)

Restrict a global zero-free equivariant homotopy to every refined chart.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.originalPLToGlobal {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (k : ℕ) : ChartHomotopy hp (A.level + k) (originalPLMap hp A.toRegularApproximation k) (ofGlobalMap hp (A.level + k) F)

Zero-free chart homotopy from the original PL interpolation to the global endpoint map.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.globalToOriginalPL {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (A : RefinedAffineMap.StableRegularApproximation hp F.map) (k : ℕ) : ChartHomotopy hp (A.level + k) (ofGlobalMap hp (A.level + k) F) (originalPLMap hp A.toRegularApproximation k)

Zero-free chart homotopy from the global endpoint map to the original PL interpolation.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartMap.castLevel {p : ℕ} {hp : Nat.Prime p} {N M : ℕ} (h : N = M) (K : ChartMap hp N) : ChartMap hp M

Transport a compatible chart map along an equality of subdivision levels.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartMap.castLevel h K = h ▸ K

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartMap.castLevel_ofGlobalMap {p : ℕ} {hp : Nat.Prime p} {N M : ℕ} (h : N = M) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) : castLevel h (ofGlobalMap hp N F) = ofGlobalMap hp M F

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartHomotopy.castLevel {p : ℕ} {hp : Nat.Prime p} {N M : ℕ} (h : N = M) {K0 K1 : ChartMap hp N} (J : ChartHomotopy hp N K0 K1) : ChartHomotopy hp M (ChartMap.castLevel h K0) (ChartMap.castLevel h K1)

Transport a compatible chart homotopy along an equality of subdivision levels.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.ChartHomotopy.castLevel h J = h ▸ J

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.baseCommonLevel {p : ℕ} {hp : Nat.Prime p} {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) : ℕ

Canonical common spatial level used by the PL-ended middle homotopy.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.baseCommonLevel A0 A1 = A0.level + A1.level + 1

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.upperLevel_eq_baseCommonLevel {p : ℕ} {hp : Nat.Prime p} {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (A0 : RefinedAffineMap.StableRegularApproximation hp F0.map) (A1 : RefinedAffineMap.StableRegularApproximation hp F1.map) : A1.level + (A0.level + 1) = baseCommonLevel A0 A1

The two component levels agree with the common level after reassociation.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopy.plEndedHomotopy {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) : ChartHomotopy hp (baseCommonLevel A0 A1) (originalPLMap hp A0.toRegularApproximation (A1.level + 1)) (ChartMap.castLevel ⋯ (originalPLMap hp A1.toRegularApproximation (A0.level + 1)))

The chartwise middle homotopy with exact endpoint PL maps.

Equations

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