Global signed cancellation for the refined equivariant prism

The compatible perturbation assigns one vector to every global sampled prism vertex. Hence the positive-ray index of a codimension-one face depends only on its ordered list of global vertices, not on the refined prism simplex in which that face is encountered.

This file turns the local affine boundary theorem into a single global finite cancellation identity. A facet occurrence is a pair consisting of a refined prism simplex and an omitted vertex. Its ordered global-vertex signature records the induced parametrized facet. Occurrences with the same signature have the same unsigned positive-ray index. After multiplying by the orbit-cycle, spatial-subdivision, staircase, prism-subdivision, and alternating face signs, the sum over all facet occurrences is zero.

The final section separates signatures in the lower horizontal layer, the upper horizontal layer, and the nonhorizontal part. The endpoint module proves vanishing of the nonhorizontal contribution and identifies the horizontal sums with the endpoint refined counts.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.unsignedFacetIndex {p : ℕ} (hp : Nat.Prime p) (V : AffinePositiveRayBoundary.VertexMap p) (k : Fin (p + 1)) : ZMod p

Positive-ray index of an oriented facet before multiplication by its alternating boundary sign.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetFaceIndex {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) : Fin (p - 1 + 2)

Transport an omitted facet vertex to the face-index type used by the simplicial boundary.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetFaceIndex hp k = Fin.cast ⋯ k

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetFaceIndex_val {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) : ↑(facetFaceIndex hp k) = ↑k

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetIndex_eq_faceSign_mul_unsignedFacetIndex {p : ℕ} (hp : Nat.Prime p) (V : AffinePositiveRayBoundary.VertexMap p) (k : Fin (p + 1)) : AffinePositiveRayBoundary.VertexMap.facetIndex hp V k = SimplicialChain.faceSign (facetFaceIndex hp k) * unsignedFacetIndex hp V k

The local signed facet index is the alternating face sign times the unsigned face index.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.unsignedFacetIndex_eq_of_facetValue_eq {p : ℕ} (hp : Nat.Prime p) (V W : AffinePositiveRayBoundary.VertexMap p) (k l : Fin (p + 1)) (hvalue : ∀ (i : Fin p), V.facetValue k i = W.facetValue l i) : unsignedFacetIndex hp V k = unsignedFacetIndex hp W l

If two oriented facets have the same ordered vertex values, their unsigned positive-ray indices agree.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.primeSmulVertexMap (p : ℕ) (g : ↥(PrimeSymmetry p)) (V : AffinePositiveRayBoundary.VertexMap p) : AffinePositiveRayBoundary.VertexMap p

Relabel every output coordinate vector of a local affine simplex by a prime symmetry.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.primeSmulVertexMap p g V = { value := fun (i : Fin (p + 1)) => g • V.value i }

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.primeSmulVertexMap_value (p : ℕ) (g : ↥(PrimeSymmetry p)) (V : AffinePositiveRayBoundary.VertexMap p) (i : Fin (p + 1)) : (primeSmulVertexMap p g V).value i = g • V.value i

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetDeterminant_primeSmul_ne_zero_iff {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (V : AffinePositiveRayBoundary.VertexMap p) (k : Fin (p + 1)) : AffinePositiveRayBoundary.VertexMap.facetDeterminant hp (primeSmulVertexMap p g V) k ≠ 0 ↔ AffinePositiveRayBoundary.VertexMap.facetDeterminant hp V k ≠ 0

Prime relabelling preserves nonvanishing of every oriented facet determinant.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.unsignedFacetIndex_primeSmul {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (V : AffinePositiveRayBoundary.VertexMap p) (k : Fin (p + 1)) : unsignedFacetIndex hp (primeSmulVertexMap p g V) k = unsignedFacetIndex hp V k

Prime relabelling preserves the unsigned positive-ray index. The open diagonal ray and the coordinate mean are invariant under coordinate permutation; the determinant changes by the sign of the selected prime permutation, whose image in ZMod p is one.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.unsignedFacetIndex_eq_of_facetValue_eq_primeSmul {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (V W : AffinePositiveRayBoundary.VertexMap p) (k l : Fin (p + 1)) (hvalue : ∀ (i : Fin p), W.facetValue l i = g • V.facetValue k i) : unsignedFacetIndex hp W l = unsignedFacetIndex hp V k

If the ordered values of one facet are a simultaneous prime relabelling of another, their unsigned positive-ray indices agree.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.FacetOccurrence {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

One codimension-one occurrence in the fully refined prism triangulation.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.FacetOccurrence hp N L = (NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.PrismCell hp N L × Fin (p + 1))

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.instFintypeFacetOccurrence {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Fintype (FacetOccurrence hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.instFintypeFacetOccurrence hp N L = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.instDecidableEqFacetOccurrence {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : DecidableEq (FacetOccurrence hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.instDecidableEqFacetOccurrence hp N L = inferInstance

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetSignature {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (o : FacetOccurrence hp N L) : Fin p → EquivariantPrismVertexParameters.GlobalVertex hp N L

Ordered global vertices of one induced prism facet. Equality of signatures means equality as an ordered sampled facet, which is the correct relation for oriented boundary cancellation.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetSignature hp N L o i = NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.sampleVertex hp N L (o.1, o.2.succAbove i)

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.FacetSignature {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

Finite type of possible ordered global-vertex signatures.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.FacetSignature hp N L = (Fin p → NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.GlobalVertex hp N L)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetSignatureFintype {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Fintype (FacetSignature hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetSignatureFintype hp N L = Fintype.ofFinite (NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.FacetSignature hp N L)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetSignatureDecidableEq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : DecidableEq (FacetSignature hp N L)

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.facetValue_eq_of_signature_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) {o o' : FacetOccurrence hp N L} (h : facetSignature hp N L o = facetSignature hp N L o') (i : Fin p) : (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a o.1).facetValue o.2 i = (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a o'.1).facetValue o'.2 i

Equal ordered facet signatures give equal ordered local vertex values.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.unsignedFacetIndex_eq_of_signature_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) {o o' : FacetOccurrence hp N L} (h : facetSignature hp N L o = facetSignature hp N L o') : unsignedFacetIndex hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a o.1) o.2 = unsignedFacetIndex hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a o'.1) o'.2

The unsigned index of a local occurrence depends only on its ordered global-vertex signature.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.signatureWeight {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (s : FacetSignature hp N L) : ZMod p

A chosen unsigned index for an ordered global facet signature. If the signature is not realized by the triangulation, its value is zero.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.signatureWeight_facetSignature {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (o : FacetOccurrence hp N L) : signatureWeight hp N L a (facetSignature hp N L o) = unsignedFacetIndex hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a o.1) o.2

On a realized signature, the chosen global weight is the unsigned index of every occurrence with that signature.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.prismCoefficient {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) : ZMod p

Coefficient of one fully refined prism simplex. It combines the original orbit-cycle coefficient, the spatial barycentric-subdivision sign, the staircase sign, and the further prism subdivision sign.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.occurrenceCoefficient {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (o : FacetOccurrence hp N L) : ZMod p

Signed incidence coefficient of one facet occurrence in the global refined prism chain.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.signatureBoundaryCoefficient {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : FacetSignature hp N L) : ZMod p

Total signed boundary coefficient of one ordered global facet signature.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.globalSignedFacetSum {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : ZMod p

Expanded global 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.EquivariantPrismGlobalCancellation.globalSignedFacetSum_eq_signature_sum {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : globalSignedFacetSum hp N L a = ∑ s : FacetSignature hp N L, signatureBoundaryCoefficient hp N L s * signatureWeight hp N L a s

The expanded occurrence sum is the sum over geometric ordered facet signatures of boundary coefficient times the common unsigned positive-ray index.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.globalSignedFacetSum_eq_local_boundary_sum {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : globalSignedFacetSum hp N L a = ∑ q : SubdivisionPrismCharts.PrismCell hp N L, prismCoefficient hp N L q * ∑ k : Fin (p + 1), AffinePositiveRayBoundary.VertexMap.facetIndex hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q) k

The global occurrence sum can equally be grouped by refined prism simplices and written using the local signed facet indices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.globalSignedFacetSum_eq_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hgp : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) : globalSignedFacetSum hp N L a = 0

Global signed prism-facet cancellation. Under local general position, every local affine boundary sum is zero, so the globally glued signed sum over all refined prism facets vanishes.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.global_signed_prism_facet_cancellation {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hgp : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) : globalSignedFacetSum hp N L a = 0

Public global signed prism-facet cancellation theorem. The sum ranges over every fully refined prism simplex and every oriented facet occurrence.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.signature_weighted_boundary_sum_eq_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hgp : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) : ∑ s : FacetSignature hp N L, signatureBoundaryCoefficient hp N L s * signatureWeight hp N L a s = 0

Signature-level form of global signed cancellation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.Result.global_signed_prism_facet_cancellation {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (m : ℝ) (R : EquivariantPrismGenericPerturbation.Result hp N L H m) : globalSignedFacetSum hp N L R.assignment = 0

Global occurrence-level cancellation specialized to the compatible generic perturbation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.Result.signature_weighted_boundary_sum_eq_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (m : ℝ) (R : EquivariantPrismGenericPerturbation.Result hp N L H m) : ∑ s : FacetSignature hp N L, signatureBoundaryCoefficient hp N L s * signatureWeight hp N L R.assignment s = 0

Cancellation specialized to the assignment produced by the generic perturbation theorem.

Horizontal and nonhorizontal decomposition

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.signatureTime {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : FacetSignature hp N L) (i : Fin p) : ℝ

Time coordinate of one vertex in an ordered global facet signature.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.signatureTime hp N L s i = ↑(NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalPoint hp N L (s i)).time

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.IsLowerHorizontal {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : FacetSignature hp N L) : Prop

A facet signature lies in the lower horizontal layer.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.IsUpperHorizontal {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : FacetSignature hp N L) : Prop

A facet signature lies in the upper horizontal layer.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.isLowerHorizontalDecidable {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : FacetSignature hp N L) : Decidable (IsLowerHorizontal hp N L s)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.isUpperHorizontalDecidable {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : FacetSignature hp N L) : Decidable (IsUpperHorizontal hp N L s)

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.lowerHorizontalContribution {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : ZMod p

Lower horizontal contribution to the global signed facet sum.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.upperHorizontalContribution {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : ZMod p

Upper horizontal contribution to the global signed facet sum.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.nonhorizontalContribution {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : ZMod p

Contribution of every signature not wholly contained in either horizontal layer.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.not_lower_and_upper {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : FacetSignature hp N L) : ¬(IsLowerHorizontal hp N L s ∧ IsUpperHorizontal hp N L s)

A signature cannot lie in both horizontal layers when the facet has a vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.signature_sum_eq_horizontal_add_nonhorizontal {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : ∑ s : FacetSignature hp N L, signatureBoundaryCoefficient hp N L s * signatureWeight hp N L a s = lowerHorizontalContribution hp N L a + upperHorizontalContribution hp N L a + nonhorizontalContribution hp N L a

The signature sum splits into lower-horizontal, upper-horizontal, and nonhorizontal pieces.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.horizontal_add_nonhorizontal_eq_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hgp : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) : lowerHorizontalContribution hp N L a + upperHorizontalContribution hp N L a + nonhorizontalContribution hp N L a = 0

The global local-boundary identity in horizontal/nonhorizontal form.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.Result.horizontal_add_nonhorizontal_eq_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (m : ℝ) (R : EquivariantPrismGenericPerturbation.Result hp N L H m) : lowerHorizontalContribution hp N L R.assignment + upperHorizontalContribution hp N L R.assignment + nonhorizontalContribution hp N L R.assignment = 0

Horizontal/nonhorizontal decomposition specialized to a generic perturbation result.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.lowerHorizontalContribution_eq_neg_upper_of_nonhorizontal_eq_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (hgp : ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), AffinePositiveRayBoundary.VertexMap.GeneralPosition hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a q)) (hside : nonhorizontalContribution hp N L a = 0) : lowerHorizontalContribution hp N L a = -upperHorizontalContribution hp N L a

Once internal and spatial-side signatures have been shown to cancel, the two horizontal contributions are opposite. This is the exact algebraic endpoint consumed by the refined homotopy-invariance theorem.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGlobalCancellation.Result.lowerHorizontalContribution_eq_neg_upper_of_nonhorizontal_eq_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (m : ℝ) (R : EquivariantPrismGenericPerturbation.Result hp N L H m) (hside : nonhorizontalContribution hp N L R.assignment = 0) : lowerHorizontalContribution hp N L R.assignment = -upperHorizontalContribution hp N L R.assignment

Horizontal balance specialized to a generic perturbation result.