Fine middle-prism control and quantitative origin margins

The endpoint-identified collar is assembled from two relative subdivision stacks and a common-level middle prism. This file supplies the quantitative part of the middle-prism construction for the continuous patched homotopy.

For every preselected spatial level, sufficiently deep staircase subdivision makes the patched homotopy oscillate by less than any prescribed positive amount on every middle-prism simplex. The assignment obtained by sampling the patched homotopy at the relative-cell vertices is then uniformly close to the continuous patched homotopy on each simplex. Compact zero-freeness therefore gives a strict positive coordinate margin. Any full assignment, in particular any boundary-fixed movable replacement, within half that margin remains origin-free on every middle-prism cell.

The lower and upper relative subdivision stacks require their separate endpoint-control argument; that assembly is intentionally not hidden in the middle-prism theorem below.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.middleHomotopySiteValue {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {G₀ G₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (K : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp G₀ G₁) (s : ExplicitAffineRelativeCollar.Parameters.ScalarSite hp (RelativeCollarMiddlePrism.cellSystem hp N L)) : ℝ

Scalar sample of a zero-free homotopy on one relative middle-prism parameter site.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.middleHomotopySiteValue_eq_of_orbitRel {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {G₀ G₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (K : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp G₀ G₁) {a b : ExplicitAffineRelativeCollar.Parameters.ScalarSite hp (RelativeCollarMiddlePrism.cellSystem hp N L)} (hab : (MulAction.orbitRel (↥(PrimeSymmetry p)) (ExplicitAffineRelativeCollar.Parameters.ScalarSite hp (RelativeCollarMiddlePrism.cellSystem hp N L))) a b) : middleHomotopySiteValue hp N L K a = middleHomotopySiteValue hp N L K b

Middle-prism homotopy samples are constant on diagonal prime orbits.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.middleHomotopyAssignment {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {G₀ G₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (K : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp G₀ G₁) : ExplicitAffineRelativeCollar.Parameters.Assignment hp (RelativeCollarMiddlePrism.cellSystem hp N L)

Relative-cell assignment obtained by sampling a zero-free homotopy on every middle-prism vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.vectorValue_middleHomotopyAssignment {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {G₀ G₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (K : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp G₀ G₁) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (RelativeCollarMiddlePrism.cellSystem hp N L)) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (RelativeCollarMiddlePrism.cellSystem hp N L) (middleHomotopyAssignment hp N L K) x = K.map (ExplicitAffineRelativeCollar.Parameters.globalPoint hp (RelativeCollarMiddlePrism.cellSystem hp N L) x).toProd

Reconstructing the relative middle-prism assignment gives the original homotopy sample at every sampled global vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.localVertexMap_middleHomotopyAssignment {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {G₀ G₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (K : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp G₀ G₁) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (RelativeCollarMiddlePrism.cellSystem hp N L) (middleHomotopyAssignment hp N L K) q).value i = K.map (SubdivisionPrismCharts.vertex hp N L q i)

On every local relative middle-prism vertex, the sampled assignment is exactly the homotopy value at the corresponding staircase-prism vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.exists_patchedMiddle_refinement_oscillation {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (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) : ∃ (L : ℕ), ∀ (q : SubdivisionPrismCharts.PrismCell hp N L) (u v : StandardSimplex p), dist ((StablePatchedHomotopyBoundary.stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta u))) ((StablePatchedHomotopyBoundary.stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta v))) < eps

Fine-middle oscillation for the patched homotopy at a prescribed initial spatial level.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.norm_middleAffineValue_sub_homotopy_le_of_oscillation {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {G₀ G₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (K : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp G₀ G₁) (q : SubdivisionPrismCharts.PrismCell hp N L) (eps : ℝ) (hosc : ∀ (u v : StandardSimplex p), dist (K.map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta u))) (K.map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta v))) < eps) (w : StandardSimplex p) : ‖(ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (RelativeCollarMiddlePrism.cellSystem hp N L) (middleHomotopyAssignment hp N L K) q).affineValue w - K.map ((SubdivisionPrismCharts.chart hp N L q) (StandardSimplex.toDelta w))‖ ≤ eps

On one middle-prism simplex, an oscillation bound controls the error between affine vertex interpolation and the continuous homotopy.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.exists_patchedMiddle_refinement_coordinateNormMargin {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) : ∃ (L : ℕ) (m : ℝ), 0 < m ∧ ExplicitAffineRelativeCollar.RelativeGenericity.LocalAffineCoordinateNormMargin hp (RelativeCollarMiddlePrism.cellSystem hp N L) (middleHomotopyAssignment hp N L (StablePatchedHomotopyBoundary.stablePatchedHomotopy hp F₀ F₁ H A₀ A₁)) m

For every prescribed initial spatial level, some fully refined middle prism has a positive coordinate margin for the sampled patched homotopy.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.avoidsOrigin_of_assignmentClose_half_margin {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (base perturbed : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) {margin : ℝ} (hmargin : 0 < margin) (hbase : ExplicitAffineRelativeCollar.RelativeGenericity.LocalAffineCoordinateNormMargin hp C base margin) (hclose : EquivariantPrismGenericPerturbation.AssignmentClose perturbed base (margin / 2)) (q : C.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp C perturbed q).AvoidsOrigin

Any assignment within half of a positive local coordinate margin remains origin-free on every cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyFineMargin.middle_replaceMovable_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {G₀ G₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (K : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp G₀ G₁) {margin : ℝ} (hmargin : 0 < margin) (hbase : ExplicitAffineRelativeCollar.RelativeGenericity.LocalAffineCoordinateNormMargin hp (RelativeCollarMiddlePrism.cellSystem hp N L) (middleHomotopyAssignment hp N L K) margin) (move : ExplicitAffineRelativeCollar.Parameters.MovableParameter hp (RelativeCollarMiddlePrism.cellSystem hp N L) → ℝ) (hclose : EquivariantPrismGenericPerturbation.AssignmentClose (ExplicitAffineRelativeCollar.Parameters.replaceMovable hp (RelativeCollarMiddlePrism.cellSystem hp N L) (middleHomotopyAssignment hp N L K) move) (middleHomotopyAssignment hp N L K) (margin / 2)) (q : SubdivisionPrismCharts.PrismCell hp N L) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (RelativeCollarMiddlePrism.cellSystem hp N L) (ExplicitAffineRelativeCollar.Parameters.replaceMovable hp (RelativeCollarMiddlePrism.cellSystem hp N L) (middleHomotopyAssignment hp N L K) move) q).AvoidsOrigin

In particular, a boundary-fixed movable replacement within half of the middle-prism margin remains origin-free cellwise.