Exact relative stable-collar interface

The polynomial package in StableCollarRelativeSubdivision is one sufficient route to the local positive-ray Stokes identity. It is not the mathematical interface consumed by the global argument. In particular, requiring an invertible (p-1) x (p-1) deviation matrix on every mixed codimension-two face is too strong when a retained frozen endpoint vertex has zero deviation.

This file records the exact, boundary-compatible interface. A construction supplies an actual prime-equivariant assignment, exact horizontal boundary values, and the cellwise Stokes identity. No discontinuous endpoint-adjusted sampler and no unnecessary codimension-two determinant are part of the certificate.

Boundary-compatible patched homotopy

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.ZeroFreeEndpointInterpolant {p : ℕ} (hp : Nat.Prime p) (F : EquivariantCoordinateHomotopy.ZeroFreeMap hp) : Type

A global zero-free equivariant endpoint interpolant, together with the straight-line safety that is stored simplexwise by a regular approximation. A gluing theorem builds this bundled map from the compatible local affine formulas.

• map : EquivariantCoordinateHomotopy.ZeroFreeMap hp

  The zero-free interpolating map joined to the original endpoint by a safe straight segment.

• zeroFreeStraightLine (x : Realization p) (t : ↑(Set.Icc 0 1)) : (1 - ↑t) • F.map x + ↑t • self.map.map x ≠ 0

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.patchedHomotopy {p : ℕ} {hp : Nat.Prime p} {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (I₀ : ZeroFreeEndpointInterpolant hp F₀) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (I₁ : ZeroFreeEndpointInterpolant hp F₁) : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp I₀.map I₁.map

Concatenate the safe segment from the lower interpolant to F₀, the supplied homotopy, and the safe segment from F₁ to the upper interpolant. Unlike endpointAdjustedAssignment, this is a continuous boundary-compatible zero-free target prescription on the entire cylinder.

Equations

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

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.ExactRelativeStableCollarData {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

Exact data consumed by finite affine Stokes. This is the correct target for a relative PL construction with independently triangulated endpoints.

• commonLevel : ℕ

  The common spatial level of the exact relative collar.

• timeLevel : ℕ

  The time-refinement level of the exact relative collar.

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

  The collar whose assignment agrees exactly with the horizontal endpoint data.

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

  The boundary-compatible assignment satisfying the local positive-ray Stokes identity.

• horizontalVertexFixed : ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ self.collar self.assignment
• localPositiveRayStokes : ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.LocalPositiveRayStokes hp self.collar.toFoxNeuwirthRelativeAffineCollar self.assignment

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.ExactRelativeStableCollarData.zeroCount_eq {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 : ExactRelativeStableCollarData hp H A₀ A₁) : A₀.zeroCount = A₁.zeroCount

The exact boundary-compatible collar data imply equality of the two supplied stable counts.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.ExactRelativeStableCollarData.ofExplicitRelativeStableCollarCertificate {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} (C : StableCollarRelativeSubdivision.ExplicitRelativeStableCollarCertificate hp H A₀ A₁) : ExactRelativeStableCollarData hp H A₀ A₁

Every certificate built through the older polynomial route satisfies the exact interface.

Equations

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

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.ExactRelativeStableCollarGeneralPositionData {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 convenient sufficient package: exact endpoint fixing together with the precise local positive-ray general-position predicate already proved sufficient by the affine Stokes module.

• commonLevel : ℕ

  The common spatial level of the collar in positive-ray general position.

• timeLevel : ℕ

  The time-refinement level of the collar in positive-ray general position.

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

  The endpoint-identified collar used for the exact general-position certificate.

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

  The boundary-compatible vertex assignment in positive-ray general position.

• horizontalVertexFixed : ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ self.collar self.assignment
• positiveRayGeneralPosition (q : self.collar.cells.Cell) : AffinePositiveRayBoundary.VertexMap.PositiveRayGeneralPosition hp (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp self.collar.cells self.assignment q)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.ExactRelativeStableCollarGeneralPositionData.toExactRelativeStableCollarData {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 : ExactRelativeStableCollarGeneralPositionData hp H A₀ A₁) : ExactRelativeStableCollarData hp H A₀ A₁

Exact positive-ray general position produces the exact Stokes certificate.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.ExactRelativeStableCollarConstructionTheorem : Prop

Existence proposition for the geometric construction.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.stableHomotopyInvariance_of_exactRelativeStableCollarConstruction (HC : ExactRelativeStableCollarConstructionTheorem) : RefinedAffineMap.StableHomotopyInvarianceTheorem

The exact construction theorem implies the project stable-homotopy-invariance interface.

Formal obstruction to the over-strong mixed-face minor condition

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.codimTwoDeviationMatrix_column_eq_zero_of_constantVertex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (q : C.Cell) (f : ExplicitAffineRelativeCollar.Polynomials.CodimTwoFace p) (c : Fin (p - 1)) (hconstant : ∀ (r : Fin (p - 1)), ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp C (q, ExplicitAffineRelativeCollar.Polynomials.codimTwoVertex hp f c)) (ReferenceAffineOrbitCount.coordinateLabel hp r) = ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp C (q, ExplicitAffineRelativeCollar.Polynomials.codimTwoVertex hp f c)) (ReferenceAffineOrbitCount.lastLabel hp)) (r : Fin (p - 1)) : ExplicitAffineRelativeCollar.Polynomials.codimTwoDeviationMatrix hp C a q f r c = 0

If one retained codimension-two vertex has all target coordinates equal, then the corresponding column of the deviation matrix is identically zero. Such a vertex is compatible with endpoint stability when its common coordinate is negative, but it makes the full deviation determinant condition impossible.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.codimTwoMinor_eq_zero_of_constantVertex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (q : C.Cell) (f : ExplicitAffineRelativeCollar.Polynomials.CodimTwoFace p) (c : Fin (p - 1)) (hconstant : ∀ (r : Fin (p - 1)), ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp C (q, ExplicitAffineRelativeCollar.Polynomials.codimTwoVertex hp f c)) (ReferenceAffineOrbitCount.coordinateLabel hp r) = ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp C (q, ExplicitAffineRelativeCollar.Polynomials.codimTwoVertex hp f c)) (ReferenceAffineOrbitCount.lastLabel hp)) : (ExplicitAffineRelativeCollar.Polynomials.codimTwoDeviationMatrix hp C a q f).det = 0

Consequently the full deviation minor required by the old mixed-face genericity family is zero. This is the formal algebraic obstruction to the manuscript's local-completion lemma.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivisionExact.mixedCodimTwo_genericityValue_eq_zero_of_constantVertex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (q : C.Cell) (f : ExplicitAffineRelativeCollar.Polynomials.CodimTwoFace p) (hnonpure : ¬ExplicitAffineRelativeCollar.Polynomials.IsPurelyHorizontalCodimTwo hp C q f) (c : Fin (p - 1)) (hconstant : ∀ (r : Fin (p - 1)), ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp C (q, ExplicitAffineRelativeCollar.Polynomials.codimTwoVertex hp f c)) (ReferenceAffineOrbitCount.coordinateLabel hp r) = ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp C (q, ExplicitAffineRelativeCollar.Polynomials.codimTwoVertex hp f c)) (ReferenceAffineOrbitCount.lastLabel hp)) : ExplicitAffineRelativeCollar.Polynomials.genericityValue hp C a (Sum.inr ⟨(q, f), hnonpure⟩) = 0

At a non-purely-horizontal face containing such a retained vertex, the corresponding old RelativeGenericityIndex can never have nonzero genericityValue.