Patched endpoint homotopy and exact frozen-boundary samples

The endpoint bridges provide genuine zero-free equivariant maps whose refined vertex values are exactly the two stable regular approximations. This file concatenates those bridges with the original zero-free homotopy and defines the corresponding relative-collar vertex assignment.

The assignment samples the patched homotopy at every nonhorizontal vertex and stores the supplied stable approximation values on the two horizontal layers. Exact endpoint fixing is therefore literal. On every vertex of an identified external endpoint facet, the stored value is also the actual value of the continuous patched homotopy; this follows from endpoint identification, prime equivariance, and the refined-vertex interpolation theorem.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.stablePatchedHomotopy {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) : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp (StableEndpointBridges.endpointInterpolant hp F₀ A₀).map (StableEndpointBridges.endpointInterpolant hp F₁ A₁).map

The continuous zero-free homotopy obtained by adjoining the two endpoint bridges to the original homotopy.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.stablePatchedHomotopy_zero_refinedVertex {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) (q : RefinedAffineMap.TopCell hp A₀.level) (i : Fin (p - 1 + 1)) : (stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map (RefinedAffineMap.vertex hp A₀.level q i, ⟨0, stablePatchedHomotopy_zero_refinedVertex._proof_1⟩) = A₀.map (RefinedAffineMap.vertex hp A₀.level q i)

At every lower refined endpoint vertex, the patched homotopy starts at exactly the stored stable approximation sample.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.stablePatchedHomotopy_one_refinedVertex {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) (q : RefinedAffineMap.TopCell hp A₁.level) (i : Fin (p - 1 + 1)) : (stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map (RefinedAffineMap.vertex hp A₁.level q i, ⟨1, stablePatchedHomotopy_one_refinedVertex._proof_1⟩) = A₁.map (RefinedAffineMap.vertex hp A₁.level q i)

At every upper refined endpoint vertex, the patched homotopy ends at exactly the stored stable approximation sample.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.patchedBoundarySiteValue {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) (s : ExplicitAffineRelativeCollar.Parameters.ScalarSite hp C) : ℝ

Scalar value used by the boundary-compatible sampling assignment. The horizontal values are stored literally from the stable approximations; every nonhorizontal value is sampled from the continuous patched homotopy.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.patchedBoundarySiteValue_eq_of_orbitRel {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) {a b : ExplicitAffineRelativeCollar.Parameters.ScalarSite hp C} (hab : (MulAction.orbitRel (↥(PrimeSymmetry p)) (ExplicitAffineRelativeCollar.Parameters.ScalarSite hp C)) a b) : patchedBoundarySiteValue hp C F₀ F₁ H A₀ A₁ a = patchedBoundarySiteValue hp C F₀ F₁ H A₀ A₁ b

Boundary-compatible patched samples are constant on diagonal prime orbits.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.patchedBoundaryAssignment {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) : ExplicitAffineRelativeCollar.Parameters.Assignment hp C

The boundary-compatible assignment associated with the patched homotopy.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.vectorValue_patchedBoundaryAssignment_lower {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C) (hx : ↑(ExplicitAffineRelativeCollar.Parameters.globalPoint hp C x).time = 0) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp C (patchedBoundaryAssignment hp C F₀ F₁ H A₀ A₁) x = A₀.map (ExplicitAffineRelativeCollar.Parameters.globalPoint hp C x).spatial

The patched assignment equals the lower stable approximation at every lower horizontal collar vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.vectorValue_patchedBoundaryAssignment_upper {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C) (hx : ↑(ExplicitAffineRelativeCollar.Parameters.globalPoint hp C x).time = 1) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp C (patchedBoundaryAssignment hp C F₀ F₁ H A₀ A₁) x = A₁.map (ExplicitAffineRelativeCollar.Parameters.globalPoint hp C x).spatial

The patched assignment equals the upper stable approximation at every upper horizontal collar vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.vectorValue_patchedBoundaryAssignment_interior {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp C) (hx₀ : ↑(ExplicitAffineRelativeCollar.Parameters.globalPoint hp C x).time ≠ 0) (hx₁ : ↑(ExplicitAffineRelativeCollar.Parameters.globalPoint hp C x).time ≠ 1) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp C (patchedBoundaryAssignment hp C F₀ F₁ H A₀ A₁) x = (stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map (ExplicitAffineRelativeCollar.Parameters.globalPoint hp C x).toProd

At every nonhorizontal sampled vertex, the patched assignment is the actual value of the continuous patched homotopy.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.horizontalVertexFixed_patchedBoundaryAssignment {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) {M L : ℕ} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) : ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ C (patchedBoundaryAssignment hp C.cells F₀ F₁ H A₀ A₁)

Exact frozen-boundary matching for every horizontal vertex slot of an endpoint-identified relative collar.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.horizontalVertexFixed_replaceMovable_patchedBoundaryAssignment {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) {M L : ℕ} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (move : ExplicitAffineRelativeCollar.Parameters.MovableParameter hp C.cells → ℝ) : ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ C (ExplicitAffineRelativeCollar.Parameters.replaceMovable hp C.cells (patchedBoundaryAssignment hp C.cells F₀ F₁ H A₀ A₁) move)

Replacing only movable parameters preserves the exact patched horizontal boundary values.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.lowerFacetVertex_eq_patchedHomotopySample {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) {M L : ℕ} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (q : RefinedAffineMap.TopCell hp A₀.level) (o : C.cells.FacetOccurrence) (ho : C.cells.facetClass o = C.lowerFacet q) (i : Fin p) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp C.cells (patchedBoundaryAssignment hp C.cells F₀ F₁ H A₀ A₁) o.1).facetValue o.2 i = (stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map (C.cells.facetSignature o i).toProd

On every lower external endpoint-facet vertex, the exact stored boundary value is also the actual value of the continuous patched homotopy.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StablePatchedHomotopyBoundary.upperFacetVertex_eq_patchedHomotopySample {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) {M L : ℕ} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (q : RefinedAffineMap.TopCell hp A₁.level) (o : C.cells.FacetOccurrence) (ho : C.cells.facetClass o = C.upperFacet q) (i : Fin p) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp C.cells (patchedBoundaryAssignment hp C.cells F₀ F₁ H A₀ A₁) o.1).facetValue o.2 i = (stablePatchedHomotopy hp F₀ F₁ H A₀ A₁).map (C.cells.facetSignature o i).toProd

On every upper external endpoint-facet vertex, the exact stored boundary value is also the actual value of the continuous patched homotopy.