Finite Stokes theorem for explicit relative affine collars

This module proves the local-to-global cancellation theorem for the abstract finite affine-cell system introduced in ExplicitAffineRelativeCollar. It no longer relies on the standard product prism or on a common endpoint subdivision level.

For a compatible global vertex assignment, the unsigned positive-ray index of a local facet depends only on its ordered geometric facet class. Summing the local affine boundary identity over all top cells and regrouping by geometric facets gives the collar boundary pairing. The incidence formula of FoxNeuwirthRelativeAffineCollar then implies equality of the lower and upper horizontal contributions.

Endpoint identification with the two refined Fox--Neuwirth counts is deliberately separated from this finite Stokes theorem. It requires the boundary assignment to equal the two supplied stable endpoint maps on all frozen horizontal vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.facetValue_eq_primeSmul_of_facetClass_eq {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) {o o' : C.cells.FacetOccurrence} (h : C.cells.facetClass o = C.cells.facetClass o') : ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (Polynomials.localVertexMap hp C.cells a o'.1).facetValue o'.2 i = g • (Polynomials.localVertexMap hp C.cells a o.1).facetValue o.2 i

Equal ordered quotient-facet classes carry ordered local output values that differ by one simultaneous prime relabelling. This is the correct representative-independence statement for the prime-orbit facet quotient.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.occurrenceUnsignedFacetIndex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) (o : C.cells.FacetOccurrence) : ZMod p

The unsigned positive-ray index of a local facet occurrence.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.occurrenceUnsignedFacetIndex_eq_of_facetClass_eq {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) {o o' : C.cells.FacetOccurrence} (h : C.cells.facetClass o = C.cells.facetClass o') : occurrenceUnsignedFacetIndex hp C a o = occurrenceUnsignedFacetIndex hp C a o'

Equal geometric prime-orbit facet classes have equal unsigned positive-ray indices.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.facetWeight {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) (s : C.cells.Facet) : ZMod p

Common unsigned positive-ray weight of one ordered geometric facet class.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.facetWeight_facetClass {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) (o : C.cells.FacetOccurrence) : facetWeight hp C a (C.cells.facetClass o) = occurrenceUnsignedFacetIndex hp C a o

On a represented facet class, the common weight equals every occurrence index.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.globalSignedFacetSum {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) : ZMod p

Expanded signed positive-ray boundary sum over all local facet occurrences.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.globalSignedFacetSum_eq_facet_sum {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) : globalSignedFacetSum hp C a = ∑ s : C.cells.Facet, C.cells.facetIncidence s * facetWeight hp C a s

Regroup the expanded occurrence sum by ordered geometric facet classes.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.LocalPositiveRayStokes {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) : Prop

The exact local hypothesis consumed by finite affine Stokes: on every top cell, the signed positive-ray indices of the facets sum to zero.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.globalSignedFacetSum_eq_zero_of_localPositiveRayStokes {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) (hlocal : LocalPositiveRayStokes hp C a) : globalSignedFacetSum hp C a = 0

Cellwise positive-ray Stokes makes the expanded global signed facet sum vanish.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.localPositiveRayStokes_of_positiveRayGeneralPosition {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) (hgp : ∀ (q : C.cells.Cell), AffinePositiveRayBoundary.VertexMap.PositiveRayGeneralPosition hp (Polynomials.localVertexMap hp C.cells a q)) : LocalPositiveRayStokes hp C a

Positive-ray-relative general position is sufficient for the exact cellwise Stokes hypothesis.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.localPositiveRayStokes_of_generalPosition {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) (hgp : ∀ (q : C.cells.Cell), AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (Polynomials.localVertexMap hp C.cells a q)) : LocalPositiveRayStokes hp C a

Full local general position remains a sufficient way to obtain the exact local Stokes hypothesis.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.globalSignedFacetSum_eq_zero {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) (hgp : ∀ (q : C.cells.Cell), AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (Polynomials.localVertexMap hp C.cells a q)) : globalSignedFacetSum hp C a = 0

Local general position makes the expanded signed facet sum vanish.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.lowerHorizontalContribution {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) : ZMod p

Lower horizontal contribution of an explicit relative collar.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.upperHorizontalContribution {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) : ZMod p

Upper horizontal contribution of an explicit relative collar.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.facet_sum_eq_upper_sub_lower {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) : ∑ s : C.cells.Facet, C.cells.facetIncidence s * facetWeight hp C a s = upperHorizontalContribution hp C a - lowerHorizontalContribution hp C a

The collar incidence formula rewrites the geometric-facet sum as upper minus lower.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.lowerHorizontalContribution_eq_upperHorizontalContribution_of_localPositiveRayStokes {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) (hlocal : LocalPositiveRayStokes hp C a) : lowerHorizontalContribution hp C a = upperHorizontalContribution hp C a

Finite Stokes theorem from the exact cellwise positive-ray boundary identity.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.lowerHorizontalContribution_eq_upperHorizontalContribution {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (a : Parameters.Assignment hp C.cells) (hgp : ∀ (q : C.cells.Cell), AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (Polynomials.localVertexMap hp C.cells a q)) : lowerHorizontalContribution hp C a = upperHorizontalContribution hp C a

Finite Stokes theorem for an explicit relative affine collar under full local general position.

Identification of fixed horizontal facets with refined endpoint indices

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.refinedVertexEquiv {p : ℕ} (hp : Nat.Prime p) : Fin p ≃ Fin (p - 1 + 1)

Canonical identification of the p facet vertices with the vertex index type used by a (p - 1)-simplex. Keeping this transport named prevents repeated dependent casts.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.refinedVertexEquiv hp = NRR.AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.refinedVertexIndex {p : ℕ} (hp : Nat.Prime p) (i : Fin p) : Fin (p - 1 + 1)

The corresponding transported refined vertex index.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.refinedVertexEquiv_symm_apply_index {p : ℕ} (hp : Nat.Prime p) (i : Fin p) : (refinedVertexEquiv hp).symm (refinedVertexIndex hp i) = i

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.refinedVertexIndex_eq_facetCoordinateIndex {p : ℕ} (hp : Nat.Prime p) (i : Fin p) : refinedVertexIndex hp i = AffinePositiveRayBoundary.VertexMap.facetCoordinateIndex i

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.sum_refinedVertexIndex {p : ℕ} (hp : Nat.Prime p) {R : Type} [AddCommMonoid R] (f : Fin (p - 1 + 1) → R) : ∑ i : Fin p, f (refinedVertexIndex hp i) = ∑ j : Fin (p - 1 + 1), f j

Reindex a finite sum from refined simplex vertices to facet vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.facetDeterminant_eq_refinedDeterminant {p : ℕ} (hp : Nat.Prime p) (V : AffinePositiveRayBoundary.VertexMap p) (k : Fin (p + 1)) (N : ℕ) (F : RefinedAffineMap.ContinuousCoordinateMap p) (q : RefinedAffineMap.TopCell hp N) (hvertex : ∀ (i : Fin p), V.facetValue k i = RefinedAffineMap.vertexValue hp N F q (refinedVertexIndex hp i)) : AffinePositiveRayBoundary.VertexMap.facetDeterminant hp V k = RefinedAffineMap.determinant hp N F q

Matching ordered vertex values identify the affine facet determinant with the determinant of the corresponding refined Fox--Neuwirth top cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.facetDeterminant_ne_zero_of_eq_refined_primeSmul {p : ℕ} (hp : Nat.Prime p) (V : AffinePositiveRayBoundary.VertexMap p) (k : Fin (p + 1)) (N : ℕ) (F : RefinedAffineMap.ContinuousCoordinateMap p) (q : RefinedAffineMap.TopCell hp N) (g : ↥(PrimeSymmetry p)) (hvertex : ∀ (i : Fin p), V.facetValue k i = g • RefinedAffineMap.vertexValue hp N F q (refinedVertexIndex hp i)) (hregular : RefinedAffineMap.determinant hp N F q ≠ 0) : AffinePositiveRayBoundary.VertexMap.facetDeterminant hp V k ≠ 0

A simultaneous prime relabelling of a regular endpoint facet still has nonzero determinant.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.unsignedFacetIndex_eq_refinedLocalIndex {p : ℕ} (hp : Nat.Prime p) (V : AffinePositiveRayBoundary.VertexMap p) (k : Fin (p + 1)) (N : ℕ) (F : RefinedAffineMap.ContinuousCoordinateMap p) (q : RefinedAffineMap.TopCell hp N) (hvertex : ∀ (i : Fin p), V.facetValue k i = RefinedAffineMap.vertexValue hp N F q (refinedVertexIndex hp i)) (haffine : ∀ (w : StandardSimplex (p - 1)), V.facetAffineValue k w = RefinedAffineMap.value hp N F q w) : EquivariantPrismGlobalCancellation.unsignedFacetIndex hp V k = RefinedAffineMap.localIndex hp N F q

An ordered affine facet with the same vertex values and affine interpolation as a refined Fox--Neuwirth top cell has exactly that cell's unsigned positive-ray index.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.unsignedFacetIndex_eq_refinedLocalIndex_primeSmul {p : ℕ} (hp : Nat.Prime p) (V : AffinePositiveRayBoundary.VertexMap p) (k : Fin (p + 1)) (N : ℕ) (F : RefinedAffineMap.ContinuousCoordinateMap p) (q : RefinedAffineMap.TopCell hp N) (g : ↥(PrimeSymmetry p)) (hvertex : ∀ (i : Fin p), V.facetValue k i = g • RefinedAffineMap.vertexValue hp N F q (refinedVertexIndex hp i)) (haffine : ∀ (w : StandardSimplex (p - 1)), V.facetAffineValue k w = g • RefinedAffineMap.value hp N F q w) : EquivariantPrismGlobalCancellation.unsignedFacetIndex hp V k = RefinedAffineMap.localIndex hp N F q

A simultaneous prime relabelling of all ordered endpoint values has the same unsigned positive-ray index as the endpoint refined cell.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.EndpointBoundaryFixed {p : ℕ} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (hp : Nat.Prime p) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp C.cells) : Prop

Exact boundary fixing for an endpoint-identified relative affine collar. Every local representative of a prescribed horizontal quotient facet agrees with the endpoint data after one simultaneous prime relabelling.

• lowerData (q : RefinedAffineMap.TopCell hp A₀.level) (o : C.cells.FacetOccurrence) : C.cells.facetClass o = C.lowerFacet q → ∃ (g : ↥(PrimeSymmetry p)), (∀ (i : Fin p), (Polynomials.localVertexMap hp C.cells a o.1).facetValue o.2 i = g • RefinedAffineMap.vertexValue hp A₀.level A₀.map q (refinedVertexIndex hp i)) ∧ ∀ (w : StandardSimplex (p - 1)), (Polynomials.localVertexMap hp C.cells a o.1).facetAffineValue o.2 w = g • RefinedAffineMap.value hp A₀.level A₀.map q w
• upperData (q : RefinedAffineMap.TopCell hp A₁.level) (o : C.cells.FacetOccurrence) : C.cells.facetClass o = C.upperFacet q → ∃ (g : ↥(PrimeSymmetry p)), (∀ (i : Fin p), (Polynomials.localVertexMap hp C.cells a o.1).facetValue o.2 i = g • RefinedAffineMap.vertexValue hp A₁.level A₁.map q (refinedVertexIndex hp i)) ∧ ∀ (w : StandardSimplex (p - 1)), (Polynomials.localVertexMap hp C.cells a o.1).facetAffineValue o.2 w = g • RefinedAffineMap.value hp A₁.level A₁.map q w

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.HorizontalVertexFixed {p : ℕ} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (hp : Nat.Prime p) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp C.cells) : Prop

Implementable horizontal boundary condition: every local vertex lying in the lower or upper horizontal layer carries exactly the corresponding supplied endpoint value. Compatibility across shared vertices is already enforced by the global parameter quotient.

• lowerValue (s : C.cells.VertexSlot) : ↑(C.cells.slotPoint s).time = 0 → Parameters.vectorValue hp C.cells a (Parameters.sampleVertex hp C.cells s) = A₀.map (C.cells.slotPoint s).spatial
• upperValue (s : C.cells.VertexSlot) : ↑(C.cells.slotPoint s).time = 1 → Parameters.vectorValue hp C.cells a (Parameters.sampleVertex hp C.cells s) = A₁.map (C.cells.slotPoint s).spatial

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.HorizontalVertexFixed.lowerFacetVertexValuePrimeSmul {p : ℕ} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (hp : Nat.Prime p) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp C.cells) (B : HorizontalVertexFixed hp A₀ A₁ C a) (q : RefinedAffineMap.TopCell hp A₀.level) (o : C.cells.FacetOccurrence) (ho : C.cells.facetClass o = C.lowerFacet q) : ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (Polynomials.localVertexMap hp C.cells a o.1).facetValue o.2 i = g • RefinedAffineMap.vertexValue hp A₀.level A₀.map q (refinedVertexIndex hp i)

Slotwise lower boundary fixing gives the ordered endpoint values up to the simultaneous prime relabeling carried by the chosen quotient-facet representative.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.HorizontalVertexFixed.upperFacetVertexValuePrimeSmul {p : ℕ} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (hp : Nat.Prime p) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp C.cells) (B : HorizontalVertexFixed hp A₀ A₁ C a) (q : RefinedAffineMap.TopCell hp A₁.level) (o : C.cells.FacetOccurrence) (ho : C.cells.facetClass o = C.upperFacet q) : ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (Polynomials.localVertexMap hp C.cells a o.1).facetValue o.2 i = g • RefinedAffineMap.vertexValue hp A₁.level A₁.map q (refinedVertexIndex hp i)

Slotwise upper boundary fixing gives the ordered endpoint values up to the simultaneous prime relabeling carried by the chosen quotient-facet representative.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.HorizontalVertexFixed.toEndpointBoundaryFixed {p : ℕ} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (hp : Nat.Prime p) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp C.cells) (B : HorizontalVertexFixed hp A₀ A₁ C a) : EndpointBoundaryFixed hp A₀ A₁ C a

Slotwise horizontal boundary fixing induces the quotient-representative endpoint condition.

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

Every movable perturbation of the endpoint-adjusted base assignment fixes the two supplied endpoint approximations exactly on the horizontal vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.EndpointBoundaryFixed.lower_facetWeight_eq_localIndex {p : ℕ} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (hp : Nat.Prime p) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp C.cells) (B : EndpointBoundaryFixed hp A₀ A₁ C a) (q : RefinedAffineMap.TopCell hp A₀.level) : FoxNeuwirthRelativeAffineCollar.facetWeight hp C.toFoxNeuwirthRelativeAffineCollar a (C.lowerFacet q) = RefinedAffineMap.localIndex hp A₀.level A₀.map q

Weight of a lower horizontal facet is the refined local index of its prescribed endpoint cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.EndpointBoundaryFixed.upper_facetWeight_eq_localIndex {p : ℕ} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (hp : Nat.Prime p) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp C.cells) (B : EndpointBoundaryFixed hp A₀ A₁ C a) (q : RefinedAffineMap.TopCell hp A₁.level) : FoxNeuwirthRelativeAffineCollar.facetWeight hp C.toFoxNeuwirthRelativeAffineCollar a (C.upperFacet q) = RefinedAffineMap.localIndex hp A₁.level A₁.map q

Weight of an upper horizontal facet is the refined local index of its prescribed endpoint cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.EndpointBoundaryFixed.lowerHorizontalContribution_eq_zeroCount {p : ℕ} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (hp : Nat.Prime p) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp C.cells) (B : EndpointBoundaryFixed hp A₀ A₁ C a) : FoxNeuwirthRelativeAffineCollar.lowerHorizontalContribution hp C.toFoxNeuwirthRelativeAffineCollar a = A₀.zeroCount

The lower horizontal collar contribution is exactly the lower stable refined count.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.EndpointBoundaryFixed.upperHorizontalContribution_eq_zeroCount {p : ℕ} {F₀ F₁ : RefinedAffineMap.ContinuousCoordinateMap p} (hp : Nat.Prime p) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁) {M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp A₀.level A₁.level M L) (a : Parameters.Assignment hp C.cells) (B : EndpointBoundaryFixed hp A₀ A₁ C a) : FoxNeuwirthRelativeAffineCollar.upperHorizontalContribution hp C.toFoxNeuwirthRelativeAffineCollar a = A₁.zeroCount

The upper horizontal collar contribution is exactly the upper stable refined count.