Relative-mesh completion of the fine full collar

This module isolates the geometric certificate for a boundary-preserving fine relative mesh. The assignment is the globally defined patched homotopy assignment. A relative mesh certificate records:

• exact agreement of every local vertex sample with the patched zero-free homotopy;
• a positive global norm margin for that homotopy; and
• sufficiently small oscillation on every affine collar cell.

The affine interpolation estimate is independent of the particular middle-prism cell system. Consequently any endpoint-identified relative collar satisfying this certificate yields an actual FineFullCollarData term, including literal horizontal endpoint values and cellwise origin avoidance.

The construction problem is geometric: construct a boundary-preserving relative triangulation fine enough to satisfy cellOscillation and prove its local vertices have the stated patched-sample representation. No overlap or seam assumption is hidden in the adapter.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.patchedHomotopyMargin {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) : ℝ

A fixed positive global norm margin for the patched homotopy.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.patchedHomotopyMargin hp F₀ F₁ H A₀ A₁ = Classical.choose ⋯

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.patchedHomotopyMargin_pos {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) : 0 < patchedHomotopyMargin hp F₀ F₁ H A₀ A₁

The chosen patched-homotopy margin is positive.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.patchedHomotopyMargin_le_norm {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) (z : Realization p × ↑(Set.Icc 0 1)) : patchedHomotopyMargin hp F₀ F₁ H A₀ A₁ ≤ ‖(StablePatchedHomotopyBoundary.stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map z‖

The chosen margin bounds the norm of every patched-homotopy value.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.norm_localAffineValue_sub_homotopy_le_of_oscillation {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) {G₀ G₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (K : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp G₀ G₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (q : C.Cell) (eps : ℝ) (hsample : ∀ (i : Fin (p + 1)), (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp C a q).value i = K.map (C.vertex q i).toProd) (hosc : ∀ (u v : StandardSimplex p), dist (K.map (C.chart q (StandardSimplex.toDelta u)).toProd) (K.map (C.chart q (StandardSimplex.toDelta v)).toProd) < eps) (w : StandardSimplex p) : ‖(ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp C a q).affineValue w - K.map (C.chart q (StandardSimplex.toDelta w)).toProd‖ ≤ eps

On an arbitrary affine collar cell, vertexwise samples of a continuous homotopy are uniformly close to the homotopy value whenever the homotopy oscillates by less than eps on that cell.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.FineFullCollarReferenceControlData {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

A cellwise reference-control certificate for the exact fine full collar.

This is the robust analytic interface for item 4. Different classes of collar cells may use different zero-free reference maps: endpoint cells can be compared with the already constructed endpoint PL maps, while interior cells can be compared with the patched homotopy. This avoids the false requirement that one global continuous reference have arbitrarily small oscillation across an unsplit horizontal boundary facet.

• commonLevel : ℕ

  The common spatial level of the collar equipped with reference control.

• timeLevel : ℕ

  The time-refinement level of the collar equipped with reference control.

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

  The endpoint-identified collar carrying the reference-value estimates.

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

  The collar assignment whose affine values stay close to the reference values.

• horizontalVertexFixed : ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ self.collar self.assignment
• margin : ℝ

  The positive norm margin used to compare affine values with the reference prescription.

• margin_pos : 0 < self.margin
• referenceValue : self.collar.cells.Cell → StandardSimplex p → Fin p → ℝ

  The reference coordinate vector at every point of each collar cell.

• referenceNormMargin (q : self.collar.cells.Cell) (w : StandardSimplex p) : self.margin ≤ ‖self.referenceValue q w‖
• affineClose (q : self.collar.cells.Cell) (w : StandardSimplex p) : ‖(ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp self.collar.cells self.assignment q).affineValue w - self.referenceValue q w‖ ≤ self.margin / 2

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.FineFullCollarReferenceControlData.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 : FineFullCollarReferenceControlData hp H A₀ A₁) (q : D.collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp D.collar.cells D.assignment q).AvoidsOrigin

Half-margin closeness to a cellwise zero-free reference implies origin avoidance.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.FineFullCollarReferenceControlData.toFineFullCollarData {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 : FineFullCollarReferenceControlData hp H A₀ A₁) : StableFullCollarOriginMargin.FineFullCollarData hp H A₀ A₁

A reference-controlled collar is already the exact item-4 output.

Equations

• D.toFineFullCollarData = { commonLevel := D.commonLevel, timeLevel := D.timeLevel, collar := D.collar, assignment := D.assignment, horizontalVertexFixed := ⋯, baseAvoidsOrigin := ⋯ }

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.FineRelativePatchedMeshData {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

Concrete relative-mesh certificate sufficient for the full fine-collar construction.

Unlike the earlier one-step last-vertex interface, this certificate is stable under gluing: every local value is the value of one global patched homotopy at the represented cylinder vertex.

• commonLevel : ℕ

  The common spatial level of the fine mesh for the patched homotopy.

• timeLevel : ℕ

  The time-refinement level of the fine mesh for the patched homotopy.

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

  The collar whose sampled vertex values agree with the stable patched homotopy.

• localSampleAgreement (q : self.collar.cells.Cell) (i : Fin (p + 1)) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp self.collar.cells (StablePatchedHomotopyBoundary.patchedBoundaryAssignment hp self.collar.cells F₀ F₁ H A₀ A₁) q).value i = (StablePatchedHomotopyBoundary.stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map (self.collar.cells.vertex q i).toProd
• cellOscillation (q : self.collar.cells.Cell) (u v : StandardSimplex p) : dist ((StablePatchedHomotopyBoundary.stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map (self.collar.cells.chart q (StandardSimplex.toDelta u)).toProd) ((StablePatchedHomotopyBoundary.stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map (self.collar.cells.chart q (StandardSimplex.toDelta v)).toProd) < patchedHomotopyMargin hp F₀ F₁ H A₀ A₁ / 2

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.FineRelativePatchedMeshData.toReferenceControlData {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 : FineRelativePatchedMeshData hp H A₀ A₁) : FineFullCollarReferenceControlData hp H A₀ A₁

A globally sampled patched mesh is a special case of cellwise reference control.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.FineRelativePatchedMeshData.patchedAssignment_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 : FineRelativePatchedMeshData hp H A₀ A₁) (q : D.collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp D.collar.cells (StablePatchedHomotopyBoundary.patchedBoundaryAssignment hp D.collar.cells F₀ F₁ H A₀ A₁) q).AvoidsOrigin

The patched affine assignment on every certified relative-mesh cell avoids the origin.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.FineRelativePatchedMeshData.toFineFullCollarData {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 : FineRelativePatchedMeshData hp H A₀ A₁) : StableFullCollarOriginMargin.FineFullCollarData hp H A₀ A₁

A certified fine relative mesh produces the exact item-4 output.

Equations

• D.toFineFullCollarData = D.toReferenceControlData.toFineFullCollarData

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.FineFullCollarReferenceControlConstructionTheorem : Prop

General construction target for the relative mesh. The geometric proof may use the endpoint PL maps as references on boundary-adjacent cells and the patched homotopy on interior cells.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.fineFullCollarConstruction_of_referenceControl (HR : FineFullCollarReferenceControlConstructionTheorem) : StableFullCollarOriginMargin.FineFullCollarConstructionTheorem

Cellwise reference control is sufficient for the original item-4 proposition.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.FineRelativePatchedMeshConstructionTheorem : Prop

A stronger, globally sampled relative-mesh existence target. It is useful for a collar whose boundary cells are also sufficiently fine, but is not required by the general reference-control formulation.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarRelativeMesh.fineFullCollarConstruction_of_relativePatchedMesh (HM : FineRelativePatchedMeshConstructionTheorem) : StableFullCollarOriginMargin.FineFullCollarConstructionTheorem

The concrete relative-mesh theorem closes the original item-4 construction proposition.