Full-collar origin-margin packaging

The quantitative middle-prism estimates and the generic compactness theorem reduce the full origin-margin stage to one geometric input: an endpoint-identified collar assignment which already avoids the origin on every cell. This file packages that input separately from the later positive- ray perturbation argument and proves that it automatically has a uniform positive coordinate margin. Every sufficiently small movable replacement then remains origin-free while retaining the horizontal boundary literally.

The structure FineFullCollarData packages a compatible simplicial retraction/PL assignment on the lower and upper subdivision stacks together with the controlled middle prism. All results in this file are theorem-level consequences of that data.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMargin.FineFullCollarData {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) : Type 1

Geometric output required from the completed fine-collar construction, before extracting a numerical uniform margin. The endpoint values are literal, and origin avoidance is required on the entire glued collar, not only on its middle-prism summand.

• commonLevel : ℕ

  The common spatial level of the fine full collar.

• timeLevel : ℕ

  The time-refinement level of the fine full collar.

• collar : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level self.commonLevel self.timeLevel

  The fine endpoint-identified collar on which the cellwise origin avoidance is verified.

• assignment : ExplicitAffineRelativeCollar.Parameters.Assignment hp self.collar.cells

  The horizontal-boundary-compatible assignment that avoids the origin on each cell.

• horizontalVertexFixed : ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ self.collar self.assignment
• baseAvoidsOrigin (q : self.collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp self.collar.cells self.assignment q).AvoidsOrigin

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMargin.FineFullCollarConstructionTheorem : Prop

Item 4, expressed as the exact construction proposition still required from the endpoint-stack geometry. This is a named target, not an assumed theorem and not a field of the final AAK result.

Equations

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

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMargin.FullCollarOriginMarginData {p : ℕ} (hp : Nat.Prime p) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) extends NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMargin.FineFullCollarData hp H A₀ A₁ : Type 1

Full quantitative output of item 5.

• commonLevel : ℕ
• timeLevel : ℕ
• collar : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level self.commonLevel self.timeLevel
• assignment : ExplicitAffineRelativeCollar.Parameters.Assignment hp self.collar.cells
• horizontalVertexFixed : ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ self.collar self.assignment
• baseAvoidsOrigin (q : self.collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp self.collar.cells self.assignment q).AvoidsOrigin
• margin : ℝ

  A positive lower bound for the norm of every affine collar value.

• margin_pos : 0 < self.margin
• coordinateNormMargin : ExplicitAffineRelativeCollar.RelativeGenericity.LocalAffineCoordinateNormMargin hp self.collar.cells self.assignment self.margin

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMargin.FullCollarOriginMarginData.ofFineFullCollarData {p : ℕ} {hp : Nat.Prime p} {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} {H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁} {A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map} {A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map} (D : FineFullCollarData hp H A₀ A₁) : FullCollarOriginMarginData hp H A₀ A₁

Every finite full-collar assignment which avoids the origin cellwise has a single positive coordinate margin valid on all cells.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMargin.FullCollarOriginMarginData.assignment_avoidsOrigin {p : ℕ} {hp : Nat.Prime p} {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} {H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁} {A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map} {A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map} (D : FullCollarOriginMarginData hp H A₀ A₁) (q : D.collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp D.collar.cells D.assignment q).AvoidsOrigin

The stored assignment is origin-free, now as an immediate consequence of its quantitative margin.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMargin.FullCollarOriginMarginData.perturbed_avoidsOrigin {p : ℕ} {hp : Nat.Prime p} {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} {H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁} {A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map} {A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map} (D : FullCollarOriginMarginData hp H A₀ A₁) (perturbed : ExplicitAffineRelativeCollar.Parameters.Assignment hp D.collar.cells) (hclose : EquivariantPrismGenericPerturbation.AssignmentClose perturbed D.assignment (D.margin / 2)) (q : D.collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp D.collar.cells perturbed q).AvoidsOrigin

Any full assignment within half of the global collar margin remains origin-free on every collar cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMargin.FullCollarOriginMarginData.replaceMovable_avoidsOrigin {p : ℕ} {hp : Nat.Prime p} {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} {H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁} {A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map} {A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map} (D : FullCollarOriginMarginData hp H A₀ A₁) (move : ExplicitAffineRelativeCollar.Parameters.MovableParameter hp D.collar.cells → ℝ) (hclose : EquivariantPrismGenericPerturbation.AssignmentClose (ExplicitAffineRelativeCollar.Parameters.replaceMovable hp D.collar.cells D.assignment move) D.assignment (D.margin / 2)) (q : D.collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp D.collar.cells (ExplicitAffineRelativeCollar.Parameters.replaceMovable hp D.collar.cells D.assignment move) q).AvoidsOrigin

In particular, a boundary-fixed movable replacement within half of the global margin remains origin-free. Exact endpoint values are retained by the definition of replaceMovable.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMargin.fullCollarOriginMargin_of_fineFullCollarConstruction (HC : FineFullCollarConstructionTheorem) {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) : Nonempty (FullCollarOriginMarginData hp H A₀ A₁)

Once item 4 constructs the full fine collar, item 5 follows without any further geometric hypothesis.