Relative subdivision cobordisms for stable endpoint counts

The relative stable-collar construction allows the lower and upper horizontal boundaries to use independently chosen barycentric-subdivision levels. It is represented by a relative finite-chain cobordism. For a cycle c, the difference of the two accumulated barycentric-subdivision homotopies has boundary

sd^N₀(c) - sd^N₁(c).

Thus the two horizontal chains retain their independently chosen levels. The module also defines a proof-carrying relative stable-collar certificate: a linear positive-ray boundary functional which vanishes on the collar boundary and evaluates to the two supplied stable counts on the two horizontal chains. Finite Stokes then proves equality of the endpoint counts without assuming that the endpoint levels coincide.

The geometric construction realizes the finite support of the relative chain by compatible prime-equivariant affine cells, freeze the two horizontal parameter subsets, and use strong general position only on movable interior and side cells. The fixed horizontal boundaries require only the PositiveRaySkeletonFree property already carried by StableRegularApproximation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.iterHomotopy_boundary_of_cycle (R : Type) [CommRing R] (X : TopCat) (N n : ℕ) (c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)) (hc : match n, c with | 0, c => True | m.succ, c => (ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X m)) c = 0) : (ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X n)) ((SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyLinearMap R X N n) c) = c - (SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap R X N n) c

The accumulated barycentric-subdivision homotopy has boundary c - sd^N(c) on a cycle.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.relativeSubdivisionChain (R : Type) [CommRing R] (X : TopCat) (N₀ N₁ n : ℕ) (c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X (n + 1))

Relative subdivision collar between two independently chosen subdivision levels. Its order is chosen so that the boundary is sd^N₀(c) - sd^N₁(c).

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.relativeSubdivisionChain_boundary (R : Type) [CommRing R] (X : TopCat) (N₀ N₁ n : ℕ) (c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)) (hc : match n, c with | 0, c => True | m.succ, c => (ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X m)) c = 0) : (ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X n)) (relativeSubdivisionChain R X N₀ N₁ n c) = (SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap R X N₀ n) c - (SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap R X N₁ n) c

Boundary formula for the relative subdivision collar. Neither horizontal chain is replaced by an additional common refinement.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : Type

Proof-carrying relative boundary chain. This is the algebraic domain required by a stable collar whose endpoint triangulations may have distinct levels.

• baseCycle : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)

  The closed singular chain whose two subdivisions are connected by the collar.

• baseCycle_closed : match n, self.baseCycle with | 0, baseCycle => True | m.succ, baseCycle => (ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X m)) baseCycle = 0
• lowerLevel : ℕ

  The subdivision level of the lower endpoint chain.

• upperLevel : ℕ

  The subdivision level of the upper endpoint chain.

• collarChain : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X (n + 1))

  The relative subdivision chain connecting the two endpoint subdivisions.

• collar_boundary : (ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X n)) self.collarChain = (SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap R X self.lowerLevel n) self.baseCycle - (SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap R X self.upperLevel n) self.baseCycle

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeSubdivisionBoundary.ofCycle (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)) (hc : match n, c with | 0, c => True | m.succ, c => (ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X m)) c = 0) (N₀ N₁ : ℕ) : RelativeSubdivisionBoundary R X n

Canonical relative boundary object associated with a cycle and two subdivision levels.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeSubdivisionBoundary.lowerChain {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (B : RelativeSubdivisionBoundary R X n) : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)

Lower horizontal chain of a relative subdivision boundary.

Equations

• B.lowerChain = (SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap R X B.lowerLevel n) B.baseCycle

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeSubdivisionBoundary.upperChain {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (B : RelativeSubdivisionBoundary R X n) : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)

Upper horizontal chain of a relative subdivision boundary.

Equations

• B.upperChain = (SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap R X B.upperLevel n) B.baseCycle

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeSubdivisionBoundary.collar_boundary_eq_lower_sub_upper {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (B : RelativeSubdivisionBoundary R X n) : (ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X n)) B.collarChain = B.lowerChain - B.upperChain

The collar boundary is lower minus upper.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeBoundaryFunctional {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (B : RelativeSubdivisionBoundary R X n) : Type

A linear boundary functional which vanishes on the boundary of a relative collar. In the geometric application this functional is obtained by summing the local positive-ray facet indices. Interior and side general position are used to prove collarBoundaryWeightZero; no stronger transversality is required on the two fixed horizontal chains.

• weight : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n) →ₗ[R] R

  The linear functional that evaluates boundary chains in the coefficient ring.

• collarBoundaryWeightZero : self.weight ((ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X n)) B.collarChain) = 0

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeBoundaryFunctional.lower_eq_upper {R : Type} [CommRing R] {X : TopCat} {n : ℕ} {B : RelativeSubdivisionBoundary R X n} (W : RelativeBoundaryFunctional B) : W.weight B.lowerChain = W.weight B.upperChain

Relative finite Stokes: a boundary functional vanishing on the collar boundary takes the same value on the independently subdivided lower and upper chains.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeStableCollarCertificate {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) (X : TopCat) (n : ℕ) : Type

Finite-chain replacement for the old common-level StableCollar. The two endpoint levels are independent. The structure contains no endpoint count equality field: equality follows from the relative boundary formula and the vanishing boundary functional.

A geometric constructor must realize boundary.collarChain by compatible affine cells. The supplied stable approximations already provide the only fixed-boundary condition needed here, namely positive-ray skeleton transversality.

• boundary : RelativeSubdivisionBoundary (ZMod p) X n

  The relative subdivision boundary carrying the stable collar comparison.

• lowerLevel_eq : self.boundary.lowerLevel = A₀.level
• upperLevel_eq : self.boundary.upperLevel = A₁.level
• functional : RelativeBoundaryFunctional self.boundary

  The boundary functional identifying the endpoint weights with their zero counts.

• lowerWeight_eq : self.functional.weight self.boundary.lowerChain = A₀.zeroCount
• upperWeight_eq : self.functional.weight self.boundary.upperChain = A₁.zeroCount

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeStableCollarCertificate.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} {X : TopCat} {n : ℕ} (C : RelativeStableCollarCertificate hp H A₀ A₁ X n) : A₀.zeroCount = A₁.zeroCount

A relative finite-chain stable collar compares arbitrary stable endpoint levels.

Geometric relative-collar certificate

The singular-chain certificate above records the algebraic Stokes pattern, but by itself it does not require its abstract chain or functional to arise from the Fox--Neuwirth collar. The main formalization therefore uses the following geometric certificate instead. Its finite affine cells have exactly the two prescribed refined endpoint boundaries, and count equality is derived from the actual local affine boundary theorem and the actual signed facet-incidence formula.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.ExplicitRelativeStableCollarCertificate {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 genuine boundary-fixed relative affine collar between two supplied stable approximations. The base assignment is no longer arbitrary: it is the endpoint-adjusted homotopy assignment. The certificate chooses only the movable parameter values, so exact agreement with both horizontal endpoint approximations follows automatically from the parameter construction. The comparison itself is proved by finite affine Stokes and is not stored as data.

• commonLevel : ℕ

  The common spatial level of the explicit stable collar certificate.

• timeLevel : ℕ

  The time-refinement level of the explicit stable collar certificate.

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

  The endpoint-identified collar carrying the local positive-ray Stokes data.

• movableAssignment : ExplicitAffineRelativeCollar.Parameters.MovableParameter hp self.collar.cells → ℝ

  The movable vertex coordinates used in the explicit collar certificate.

• localPositiveRayStokes : ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.LocalPositiveRayStokes hp self.collar.toFoxNeuwirthRelativeAffineCollar (ExplicitAffineRelativeCollar.Parameters.replaceMovable hp self.collar.cells (ExplicitAffineRelativeCollar.Parameters.endpointAdjustedAssignment hp self.collar.cells H A₀.toRegularApproximation A₁.toRegularApproximation) self.movableAssignment)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.ExplicitRelativeStableCollarCertificate.ofRelativeGeneric {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) (commonLevel timeLevel : ℕ) (collar : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level commonLevel timeLevel) (move : ExplicitAffineRelativeCollar.Parameters.MovableParameter hp collar.cells → ℝ) (hgeneric : ExplicitAffineRelativeCollar.RelativeGenericity.IsRelativeGeneric hp collar.cells (ExplicitAffineRelativeCollar.Parameters.endpointAdjustedAssignment hp collar.cells H A₀.toRegularApproximation A₁.toRegularApproximation) move) (hhorizontal : ExplicitAffineRelativeCollar.RelativeGenericity.HorizontalPositiveRayCodimTwoSafe hp collar.cells (ExplicitAffineRelativeCollar.Parameters.replaceMovable hp collar.cells (ExplicitAffineRelativeCollar.Parameters.endpointAdjustedAssignment hp collar.cells H A₀.toRegularApproximation A₁.toRegularApproximation) move)) (havoid : ∀ (q : collar.cells.Cell), (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp collar.cells (ExplicitAffineRelativeCollar.Parameters.replaceMovable hp collar.cells (ExplicitAffineRelativeCollar.Parameters.endpointAdjustedAssignment hp collar.cells H A₀.toRegularApproximation A₁.toRegularApproximation) move) q).AvoidsOrigin) : ExplicitRelativeStableCollarCertificate hp H A₀ A₁

Build a stable-collar certificate from the boundary-restricted polynomial package, horizontal endpoint safety, and local origin avoidance.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.ExplicitRelativeStableCollarCertificate.assignment {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 : ExplicitRelativeStableCollarCertificate hp H A₀ A₁) : ExplicitAffineRelativeCollar.Parameters.Assignment hp C.collar.cells

The actual compatible assignment represented by a geometric stable-collar certificate.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.ExplicitRelativeStableCollarCertificate.horizontalVertexFixed {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 : ExplicitRelativeStableCollarCertificate hp H A₀ A₁) : ExplicitAffineRelativeCollar.HorizontalVertexFixed hp A₀ A₁ C.collar C.assignment

The represented assignment fixes both horizontal endpoint approximations automatically.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.ExplicitRelativeStableCollarCertificate.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} (C : ExplicitRelativeStableCollarCertificate hp H A₀ A₁) : A₀.zeroCount = A₁.zeroCount

Finite affine Stokes compares the two prescribed stable endpoint counts.

Concrete construction package

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeStableCollarConstructionData {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 data for a stable relative collar.

The base assignment is forced to be the endpoint-adjusted sampling of the supplied homotopy. The proof fields record the required geometry: cellwise origin avoidance, a geometric movable-assignment witness for every nonhorizontal genericity condition, and exact representation of every purely horizontal codimension-two point on the frozen endpoint skeletons. Horizontal facet regularity, polynomial nontriviality, finite perturbation, and finite Stokes are consequences, not additional assumptions.

• commonLevel : ℕ

  The common spatial level chosen for constructing the relative stable collar.

• timeLevel : ℕ

  The time-refinement level chosen for constructing the relative stable collar.

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

  The endpoint-identified collar whose base assignment avoids the origin cellwise.

• baseAvoidsOrigin (q : self.collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp self.collar.cells (ExplicitAffineRelativeCollar.Parameters.endpointAdjustedAssignment hp self.collar.cells H A₀.toRegularApproximation A₁.toRegularApproximation) q).AvoidsOrigin
• requiredGenericityWitness (i : ExplicitAffineRelativeCollar.Polynomials.RelativeGenericityIndex hp self.collar.cells) : ExplicitAffineRelativeCollar.RelativeGenericity.RequiresMovableGenericityWitness hp self.collar.cells i → ∃ (move : ExplicitAffineRelativeCollar.Parameters.MovableParameter hp self.collar.cells → ℝ), ExplicitAffineRelativeCollar.Polynomials.genericityValue hp self.collar.cells (ExplicitAffineRelativeCollar.Parameters.replaceMovable hp self.collar.cells (ExplicitAffineRelativeCollar.Parameters.endpointAdjustedAssignment hp self.collar.cells H A₀.toRegularApproximation A₁.toRegularApproximation) move) i ≠ 0
• horizontalEndpointRepresentation : ExplicitAffineRelativeCollar.RelativeGenericity.HorizontalEndpointSkeletonRepresentation hp A₀ A₁ self.collar (ExplicitAffineRelativeCollar.Parameters.endpointAdjustedAssignment hp self.collar.cells H A₀.toRegularApproximation A₁.toRegularApproximation)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeStableCollarConstructionData.certificate_nonempty {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 : RelativeStableCollarConstructionData hp H A₀ A₁) : Nonempty (ExplicitRelativeStableCollarCertificate hp H A₀ A₁)

A geometric construction package yields a boundary-fixed generic collar certificate. The movable perturbation is chosen automatically, retains a positive compactness-derived norm margin, and cannot change the horizontal positive-ray safety condition.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeStableCollarConstructionTheorem : Prop

Existence of the explicit geometric construction package for every stable pair of endpoints.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.RelativeStableCollarExistenceTheorem : Prop

Arbitrary-endpoint existence proposition. A witness contains a finite endpoint-identified affine collar and movable parameter data whose assignment satisfies the exact cellwise positive-ray Stokes identity. Horizontal boundary fixing is derived from the certificate.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.relativeStableCollarExistence_of_construction (HC : RelativeStableCollarConstructionTheorem) : RelativeStableCollarExistenceTheorem

The concrete geometric construction package implies the stable-collar existence theorem.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableCollarRelativeSubdivision.stableHomotopyInvariance_of_relative_collarExistence (HC : RelativeStableCollarExistenceTheorem) : RefinedAffineMap.StableHomotopyInvarianceTheorem

Relative stable-collar existence implies stable homotopy invariance.