Cancellation of the nonhorizontal refined-prism boundary

This file performs the finite reindexing in the refined prism argument. There are three layers.

• The boundary of an iterated barycentric subdivision is the corresponding iterated subdivision of the original boundary. The proof is used only after applying an arbitrary weight to the induced face map, so it is stated as a finite weighted identity.
• The standard staircase triangulation of Delta n x I has boundary equal to the upper copy minus the lower copy minus the staircase prism on the spatial boundary. Internal staircase faces pair with opposite signs.
• The spatial-side term is an equivariant function of an orbit facet. Reindexing by facet orbits turns it into the boundary pairing of PrimeOrbitCycle.orbitCycle, hence it vanishes.

Together these statements prove that the nonhorizontalContribution isolated in EquivariantPrismGlobalCancellation is zero. No geometric transgression hypothesis is introduced: the result is a consequence of the explicit subdivision signs, staircase signs, and the already proved orbit-cycle boundary identity.

Weighted boundary of iterated barycentric subdivision

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.cofacePoint (n : ℕ) (k : Fin (n + 2)) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))

Insert a zero barycentric coordinate at k.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.cofacePoint n k x = SphereOddDegree.FiniteSimplex.map k.succAbove x

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.deltaCast {m n : ℕ} (h : m = n) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta m) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)

Transport a standard-simplex point across an equality of dimensions.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.deltaCast h x = h ▸ x

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.deltaCast_rfl {n : ℕ} (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) : deltaCast ⋯ x = x

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.deltaCast_vertex {m n : ℕ} (h : m = n) (i : Fin (m + 1)) : deltaCast h (SphereOddDegree.FiniteSimplex.vertex i) = SphereOddDegree.FiniteSimplex.vertex (Fin.cast ⋯ i)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.cofacePoint_apply_succAbove (n : ℕ) (k : Fin (n + 2)) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) (i : Fin (n + 1)) : (cofacePoint n k x) (k.succAbove i) = x i

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.cofacePoint_apply_deleted (n : ℕ) (k : Fin (n + 2)) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) : (cofacePoint n k x) k = 0

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.cofacePoint_vertex (n : ℕ) (k : Fin (n + 2)) (i : Fin (n + 1)) : cofacePoint n k (SphereOddDegree.FiniteSimplex.vertex i) = SphereOddDegree.FiniteSimplex.vertex (k.succAbove i)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.fin_succAbove_val {n : ℕ} (k : Fin (n + 1)) (i : Fin n) : ↑(k.succAbove i) = if ↑i < ↑k then ↑i else ↑i + 1

The value of Fin.succAbove, exposed without proof-term-sensitive casts.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedSign {n : ℕ} (R : Type) [CommRing R] (N : ℕ) (rho : Fin N → Equiv.Perm (Fin (n + 1))) : R

Product of the orientation signs in an iterated subdivision word.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedSign R N rho = ∏ r : Fin N, SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R (rho r)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedSign_zero {n : ℕ} (R : Type) [CommRing R] (rho : Fin 0 → Equiv.Perm (Fin (n + 1))) : iteratedSign R 0 rho = 1

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedFacetMap {X : Type} (n N : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (rho : Fin N → Equiv.Perm (Fin (n + 2))) (k : Fin (n + 2)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X

The induced facet map of one simplex in an iterated subdivision.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedBoundaryMap {X : Type} (n N : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (k : Fin (n + 2)) (rho : Fin N → Equiv.Perm (Fin (n + 1))) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X

The iterated subdivision of an original boundary face.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.oneStep_internal_face_eq {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (pi : Equiv.Perm (Fin (n + 2))) (i : Fin (n + 1)) : iteratedFacetMap n 1 sigma (fun (x : Fin 1) => pi) i.castSucc = iteratedFacetMap n 1 sigma (fun (x : Fin 1) => Equiv.trans (Equiv.swap i.castSucc i.succ) pi) i.castSucc

One-step internal faces agree after the adjacent transposition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.oneStep_last_face_eq {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (j : Fin (n + 2)) (rho : Equiv.Perm (Fin (n + 1))) : iteratedFacetMap n 1 sigma (fun (x : Fin 1) => (SphereOddDegree.AffineBarycentricSubdivision.lastFaceEquiv n) (j, rho)) (Fin.last (n + 1)) = iteratedBoundaryMap n 1 sigma j fun (x : Fin 1) => rho

One-step final faces are precisely subdivisions of original boundary faces.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.oneStep_weighted_boundary {R X : Type} [CommRing R] (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) → R) : ∑ pi : Equiv.Perm (Fin (n + 2)), SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R pi * ∑ k : Fin (n + 2), SimplicialChain.faceSign k * W (iteratedFacetMap n 1 sigma (fun (x : Fin 1) => pi) k) = ∑ j : Fin (n + 2), SimplicialChain.faceSign j * ∑ rho : Equiv.Perm (Fin (n + 1)), SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R rho * W (iteratedBoundaryMap n 1 sigma j fun (x : Fin 1) => rho)

Weighted one-step subdivision boundary formula.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.wordSnocEquiv (N : ℕ) (A : Type) : (Fin N → A) × A ≃ (Fin (N + 1) → A)

Splitting a word into its prefix and last permutation.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedSign_snoc {n : ℕ} (R : Type) [CommRing R] (N : ℕ) (rho : Fin N → Equiv.Perm (Fin (n + 1))) (pi : Equiv.Perm (Fin (n + 1))) : iteratedSign R (N + 1) (Fin.snoc rho pi) = iteratedSign R N rho * SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R pi

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.sum_word_snoc {R A : Type} [AddCommMonoid R] [Fintype A] (N : ℕ) (f : (Fin (N + 1) → A) → R) : ∑ eta : Fin (N + 1) → A, f eta = ∑ rho : Fin N → A, ∑ a : A, f (Fin.snoc rho a)

Reindex a finite sum over words by their prefix and final letter.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.sum_cycle_left3 {R A B C : Type} [AddCommMonoid R] [Fintype A] [Fintype B] [Fintype C] (f : A → B → C → R) : ∑ a : A, ∑ b : B, ∑ c : C, f a b c = ∑ b : B, ∑ c : C, ∑ a : A, f a b c

Cycle three finite sums from a,b,c to b,c,a.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.sum_cycle_right3 {R A B C : Type} [AddCommMonoid R] [Fintype A] [Fintype B] [Fintype C] (f : A → B → C → R) : ∑ a : A, ∑ b : B, ∑ c : C, f a b c = ∑ c : C, ∑ a : A, ∑ b : B, f a b c

Cycle three finite sums from a,b,c to c,a,b.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedFacetMap_snoc {X : Type} (n N : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (rho : Fin N → Equiv.Perm (Fin (n + 2))) (pi : Equiv.Perm (Fin (n + 2))) (k : Fin (n + 2)) : iteratedFacetMap n (N + 1) sigma (Fin.snoc rho pi) k = iteratedFacetMap n 1 (fun (y : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) => sigma ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (n + 1) N rho) y)) (fun (x : Fin 1) => pi) k

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedBoundaryMap_snoc {X : Type} (n N : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (j : Fin (n + 2)) (eta : Fin N → Equiv.Perm (Fin (n + 1))) (theta : Equiv.Perm (Fin (n + 1))) : iteratedBoundaryMap n (N + 1) sigma j (Fin.snoc eta theta) = fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => iteratedBoundaryMap n N sigma j eta (SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap n theta x)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedFacetMap_zero {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (rho : Fin 0 → Equiv.Perm (Fin (n + 2))) (k : Fin (n + 2)) : iteratedFacetMap n 0 sigma rho k = fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => sigma (cofacePoint n k x)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedBoundaryMap_zero {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (j : Fin (n + 2)) (rho : Fin 0 → Equiv.Perm (Fin (n + 1))) : iteratedBoundaryMap n 0 sigma j rho = fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => sigma (cofacePoint n j x)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedBoundaryMap_one_after_prefix {X : Type} (n N : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (rho : Fin N → Equiv.Perm (Fin (n + 2))) (j : Fin (n + 2)) (theta : Equiv.Perm (Fin (n + 1))) : (iteratedBoundaryMap n 1 (fun (y : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) => sigma ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (n + 1) N rho) y)) j fun (x : Fin 1) => theta) = fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => iteratedFacetMap n N sigma rho j (SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap n theta x)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iterated_weighted_boundary {R X : Type} [CommRing R] (n N : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) → R) : ∑ rho : Fin N → Equiv.Perm (Fin (n + 2)), iteratedSign R N rho * ∑ k : Fin (n + 2), SimplicialChain.faceSign k * W (iteratedFacetMap n N sigma rho k) = ∑ j : Fin (n + 2), SimplicialChain.faceSign j * ∑ eta : Fin N → Equiv.Perm (Fin (n + 1)), iteratedSign R N eta * W (iteratedBoundaryMap n N sigma j eta)

Weighted boundary formula for an arbitrary number of barycentric subdivisions.

Staircase prism boundary

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseTime {n : ℕ} (k : Fin (n + 1)) (j : Fin (n + 2)) : Fin 2

Generic staircase time coordinate for a spatial n-simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseTime k j = if ↑j ≤ ↑k then 0 else 1

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatial {n : ℕ} (k : Fin (n + 1)) (j : Fin (n + 2)) : Fin (n + 1)

Generic staircase spatial vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatial k j = if h : ↑j ≤ ↑k then ⟨↑j, ⋯⟩ else ⟨↑j - 1, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatial_val {n : ℕ} (k : Fin (n + 1)) (j : Fin (n + 2)) : ↑(genericStaircaseSpatial k j) = if ↑j ≤ ↑k then ↑j else ↑j - 1

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatialPoint (n : ℕ) (k : Fin (n + 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)

Spatial barycentric point in the generic staircase simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseIntervalPoint (n : ℕ) (k : Fin (n + 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : ↑(Set.Icc 0 1)

Interval barycentric point in the generic staircase simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircasePrismMap {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) (k : Fin (n + 1)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → X × ↑(Set.Icc 0 1)

Generic staircase prism simplex over a spatial simplex map.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.lowerEndpointMap {n : ℕ} {X : Type} (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X × ↑(Set.Icc 0 1)

Lower endpoint copy of a spatial simplex map.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.upperEndpointMap {n : ℕ} {X : Type} (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X × ↑(Set.Icc 0 1)

Upper endpoint copy of a spatial simplex map.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.sidePrismMap {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) (r : Fin (n + 1)) (h : Fin n) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X × ↑(Set.Icc 0 1)

A side staircase simplex over an original spatial face.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatial_adjacent_of_ne {n : ℕ} (h : Fin n) (j : Fin (n + 2)) (hj : j ≠ h.succ.castSucc) : genericStaircaseSpatial h.castSucc j = genericStaircaseSpatial h.succ j

Away from the duplicated staircase vertex, adjacent staircase simplices have the same spatial label.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseTime_adjacent_of_ne {n : ℕ} (h : Fin n) (j : Fin (n + 2)) (hj : j ≠ h.succ.castSucc) : genericStaircaseTime h.castSucc j = genericStaircaseTime h.succ j

Away from the duplicated staircase vertex, adjacent staircase simplices have the same interval label.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatialPoint_internal_face (n : ℕ) (h : Fin n) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) : genericStaircaseSpatialPoint n h.castSucc (cofacePoint n h.succ.castSucc x) = genericStaircaseSpatialPoint n h.succ (cofacePoint n h.succ.castSucc x)

The spatial barycentric coordinates agree on the common internal face of two adjacent staircase simplices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseIntervalPoint_internal_face (n : ℕ) (h : Fin n) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) : genericStaircaseIntervalPoint n h.castSucc (cofacePoint n h.succ.castSucc x) = genericStaircaseIntervalPoint n h.succ (cofacePoint n h.succ.castSucc x)

The interval coordinate agrees on the common internal face of two adjacent staircase simplices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircase_internal_face_eq {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) (h : Fin n) : (fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => staircasePrismMap n sigma h.castSucc (cofacePoint n h.succ.castSucc x)) = fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => staircasePrismMap n sigma h.succ (cofacePoint n h.succ.castSucc x)

Pairing of the two internal facets between adjacent staircase simplices.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.StaircaseFacetClass (n : ℕ) : Type

Combinatorial classes of facets in the standard staircase triangulation. The two Unit summands are the upper and lower horizontal facets, the two Fin n summands are the two copies of each internal facet, and the final product indexes spatial-side facets.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.StaircaseFacetClass n = (Unit ⊕ Unit ⊕ (Fin n ⊕ Fin n) ⊕ Fin (n + 1) × Fin n)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircaseFacetClassify (n : ℕ) (z : Fin (n + 1) × Fin (n + 2)) : StaircaseFacetClass n

Classify a facet occurrence of a staircase simplex.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircaseFacetUnclassify (n : ℕ) : StaircaseFacetClass n → Fin (n + 1) × Fin (n + 2)

Recover the unique staircase-simplex facet occurrence from its combinatorial class.

Equations

• One or more equations did not get rendered due to their size.
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircaseFacetUnclassify n (Sum.inl val) = (0, 0)
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircaseFacetUnclassify n (Sum.inr (Sum.inl val)) = (Fin.last n, Fin.last (n + 1))
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircaseFacetUnclassify n (Sum.inr (Sum.inr (Sum.inl (Sum.inl h)))) = (h.succ, h.succ.castSucc)
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircaseFacetUnclassify n (Sum.inr (Sum.inr (Sum.inl (Sum.inr h)))) = (h.castSucc, h.succ.castSucc)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircaseFacetEquiv (n : ℕ) : Fin (n + 1) × Fin (n + 2) ≃ StaircaseFacetClass n

The complete finite partition of staircase facet occurrences.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatialPoint_eq_map (n : ℕ) (k : Fin (n + 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : genericStaircaseSpatialPoint n k w = SphereOddDegree.FiniteSimplex.map (genericStaircaseSpatial k) w

The explicit spatial barycentric formula is the standard-simplex pushforward.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseIntervalPoint_eq_map_apply_one (n : ℕ) (k : Fin (n + 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : ↑(genericStaircaseIntervalPoint n k w) = (SphereOddDegree.FiniteSimplex.map (genericStaircaseTime k) w) 1

The generic staircase interval coordinate is coordinate 1 of the simplex pushforward along genericStaircaseTime.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatial_succ_comp_sideCoface_of_le (n : ℕ) (r : Fin (n + 2)) (h : Fin (n + 1)) (hrh : ↑r ≤ ↑h) : genericStaircaseSpatial h.succ ∘ r.castSucc.succAbove = r.succAbove ∘ genericStaircaseSpatial h

Deleting a spatial vertex weakly before the staircase break commutes with the spatial staircase projection.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseTime_succ_comp_sideCoface_of_le (n : ℕ) (r : Fin (n + 2)) (h : Fin (n + 1)) (hrh : ↑r ≤ ↑h) : genericStaircaseTime h.succ ∘ r.castSucc.succAbove = genericStaircaseTime h

Deleting a spatial vertex weakly before the staircase break commutes with the interval staircase projection.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatial_castSucc_comp_sideCoface_of_gt (n : ℕ) (r : Fin (n + 2)) (h : Fin (n + 1)) (hrh : ↑h < ↑r) : genericStaircaseSpatial h.castSucc ∘ r.succ.succAbove = r.succAbove ∘ genericStaircaseSpatial h

Deleting a spatial vertex after the staircase break commutes with the spatial staircase projection.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseTime_castSucc_comp_sideCoface_of_gt (n : ℕ) (r : Fin (n + 2)) (h : Fin (n + 1)) (hrh : ↑h < ↑r) : genericStaircaseTime h.castSucc ∘ r.succ.succAbove = genericStaircaseTime h

Deleting a spatial vertex after the staircase break commutes with the interval staircase projection.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatialPoint_side_of_le (n : ℕ) (r : Fin (n + 2)) (h : Fin (n + 1)) (hrh : ↑r ≤ ↑h) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : genericStaircaseSpatialPoint (n + 1) h.succ (cofacePoint (n + 1) r.castSucc x) = cofacePoint n r (genericStaircaseSpatialPoint n h x)

Spatial-point naturality for a side face weakly before the staircase break.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseIntervalPoint_side_of_le (n : ℕ) (r : Fin (n + 2)) (h : Fin (n + 1)) (hrh : ↑r ≤ ↑h) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : genericStaircaseIntervalPoint (n + 1) h.succ (cofacePoint (n + 1) r.castSucc x) = genericStaircaseIntervalPoint n h x

Interval-point naturality for a side face weakly before the staircase break.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseSpatialPoint_side_of_gt (n : ℕ) (r : Fin (n + 2)) (h : Fin (n + 1)) (hrh : ↑h < ↑r) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : genericStaircaseSpatialPoint (n + 1) h.castSucc (cofacePoint (n + 1) r.succ x) = cofacePoint n r (genericStaircaseSpatialPoint n h x)

Spatial-point naturality for a side face after the staircase break.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericStaircaseIntervalPoint_side_of_gt (n : ℕ) (r : Fin (n + 2)) (h : Fin (n + 1)) (hrh : ↑h < ↑r) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) : genericStaircaseIntervalPoint (n + 1) h.castSucc (cofacePoint (n + 1) r.succ x) = genericStaircaseIntervalPoint n h x

Interval-point naturality for a side face after the staircase break.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircase_upper_face_eq {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) : (fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => staircasePrismMap n sigma 0 (cofacePoint n 0 x)) = upperEndpointMap sigma

The first facet of the first staircase simplex is the upper endpoint.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircase_lower_face_eq {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) : (fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => staircasePrismMap n sigma (Fin.last n) (cofacePoint n (Fin.last (n + 1)) x)) = lowerEndpointMap sigma

The last facet of the last staircase simplex is the lower endpoint.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircase_side_face_of_le {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) (r : Fin (n + 1)) (h : Fin n) (hrh : ↑r ≤ ↑h) : (fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => staircasePrismMap n sigma h.succ (cofacePoint n r.castSucc x)) = sidePrismMap n sigma r h

Side facet formula when the deleted spatial vertex occurs weakly before the staircase break.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircase_side_face_of_gt {X : Type} (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) (r : Fin (n + 1)) (h : Fin n) (hrh : ↑h < ↑r) : (fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => staircasePrismMap n sigma h.castSucc (cofacePoint n r.succ x)) = sidePrismMap n sigma r h

Side facet formula when the deleted spatial vertex occurs after the staircase break.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircaseFacet_sum_decomposition {M : Type} [AddCommMonoid M] (n : ℕ) (F : Fin (n + 1) → Fin (n + 2) → M) : ∑ k : Fin (n + 1), ∑ j : Fin (n + 2), F k j = F 0 0 + (F (Fin.last n) (Fin.last (n + 1)) + (∑ h : Fin n, F h.succ h.succ.castSucc + ∑ h : Fin n, F h.castSucc h.succ.castSucc) + ∑ r : Fin (n + 1), ∑ h : Fin n, if ↑r ≤ ↑h then F h.succ r.castSucc else F h.castSucc r.succ)

Sum decomposition induced by the staircase facet partition.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.negOnePow_mul_self {R : Type} [CommRing R] (m : ℕ) : (-1) ^ m * (-1) ^ m = 1

The square of every power of -1 is one.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.staircase_weighted_boundary {R X : Type} [CommRing R] (n : ℕ) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → X × ↑(Set.Icc 0 1)) → R) : (∑ k : Fin (n + 1), (-1) ^ ↑k * ∑ j : Fin (n + 2), SimplicialChain.faceSign j * W fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => staircasePrismMap n sigma k (cofacePoint n j x)) = W (upperEndpointMap sigma) - W (lowerEndpointMap sigma) - ∑ r : Fin (n + 1), (-1) ^ ↑r * ∑ h : Fin n, (-1) ^ ↑h * W (sidePrismMap n sigma r h)

Boundary formula for the staircase triangulation, after evaluation by an arbitrary weight.

From local occurrence sums to the orbit-cycle side sum

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.occurrenceCofacePoint {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)

The coface point of a facet occurrence, transported to the ambient p-simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (o : EquivariantPrismGlobalCancellation.FacetOccurrence hp N L) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)

The actual affine facet map of one local prism occurrence.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.occurrenceCofacePoint_vertex {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (i : Fin p) : occurrenceCofacePoint hp k (SphereOddDegree.FiniteSimplex.vertex (AffinePositiveRayBoundary.VertexMap.facetCoordinateIndex i)) = SphereOddDegree.FiniteSimplex.vertex (k.succAbove i)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap_vertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (o : EquivariantPrismGlobalCancellation.FacetOccurrence hp N L) (i : Fin p) : occurrenceFacetMap hp N L o (SphereOddDegree.FiniteSimplex.vertex (AffinePositiveRayBoundary.VertexMap.facetCoordinateIndex i)) = SubdivisionPrismCharts.vertex hp N L o.1 (o.2.succAbove i)

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.mapVertexSignature {p : ℕ} (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : Fin p → EquivariantPrismVertexParameters.CylinderPoint p

Ordered cylinder vertices of an arbitrary affine facet map.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.translateFacetMap (p : ℕ) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)

Prime translation of an affine facet map.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.translateFacetMap p g tau x = (g • (tau x).1, (tau x).2)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.mapVertexSignature_translateFacetMap (p : ℕ) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : mapVertexSignature (translateFacetMap p g tau) = fun (i : Fin p) => g • mapVertexSignature tau i

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

Ordered cylinder vertices of one actual facet occurrence.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.mapVertexSignature_occurrenceFacetMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (o : EquivariantPrismGlobalCancellation.FacetOccurrence hp N L) : mapVertexSignature (occurrenceFacetMap hp N L o) = occurrencePointSignature hp N L o

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.FacetMapIsRealizedUpToPrime {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : Prop

An affine facet map is realized when its ordered vertices are a simultaneous prime translate of the ordered vertices of an actual triangulation facet. Using the orbit closure, rather than literal function equality, is what makes the auxiliary weight equivariant on all maps appearing in the subdivision and staircase identities.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.occurrenceUnsignedFacetIndex_eq_of_pointSignature_eq_primeSmul {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (o o' : EquivariantPrismGlobalCancellation.FacetOccurrence hp N L) (g : ↥(PrimeSymmetry p)) (h : occurrencePointSignature hp N L o = fun (i : Fin p) => g • occurrencePointSignature hp N L o' i) : EquivariantPrismGlobalCancellation.unsignedFacetIndex hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a o.1) o.2 = EquivariantPrismGlobalCancellation.unsignedFacetIndex hp (EquivariantPrismGenericityPolynomials.localVertexMap hp N L a o'.1) o'.2

Prime-equivalent ordered geometric occurrence signatures have equal unsigned indices for every compatible assignment.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.realizedFacetWeight {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Unsigned index attached to a realized affine facet map. The chosen occurrence is immaterial by occurrenceUnsignedFacetIndex_eq_of_pointSignature_eq_primeSmul.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.realizedFacetWeight_occurrence {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (o : EquivariantPrismGlobalCancellation.FacetOccurrence hp N L) : realizedFacetWeight hp N L a (occurrenceFacetMap hp N L o) = EquivariantPrismGlobalCancellation.signatureWeight hp N L a (EquivariantPrismGlobalCancellation.facetSignature hp N L o)

The realized-map weight agrees with the signature weight of every occurrence.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.realizedFacetWeight_translateFacetMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : realizedFacetWeight hp N L a (translateFacetMap p g tau) = realizedFacetWeight hp N L a tau

The realized facet weight is invariant under simultaneous prime translation.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.MapIsLowerHorizontal {p : ℕ} (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : Prop

A facet map is lower horizontal when every one of its vertices has time zero.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.MapIsUpperHorizontal {p : ℕ} (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : Prop

A facet map is upper horizontal when every one of its vertices has time one.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.nonhorizontalMapWeight {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Weight used for the nonhorizontal part of the boundary.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.nonhorizontalMapWeight_lowerEndpointMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) : nonhorizontalMapWeight hp N L a (lowerEndpointMap sigma) = 0

The auxiliary nonhorizontal weight vanishes on every lower endpoint facet.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.nonhorizontalMapWeight_upperEndpointMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) : nonhorizontalMapWeight hp N L a (upperEndpointMap sigma) = 0

The auxiliary nonhorizontal weight vanishes on every upper endpoint facet.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.nonhorizontalContribution_eq_occurrence_sum {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : EquivariantPrismGlobalCancellation.nonhorizontalContribution hp N L a = ∑ o : EquivariantPrismGlobalCancellation.FacetOccurrence hp N L, EquivariantPrismGlobalCancellation.occurrenceCoefficient hp N L o * nonhorizontalMapWeight hp N L a (occurrenceFacetMap hp N L o)

Occurrence expansion of the nonhorizontal signature contribution.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.nonhorizontalMapWeight_smul {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : nonhorizontalMapWeight hp N L a (translateFacetMap p g tau) = nonhorizontalMapWeight hp N L a tau

Prime relabelling does not change the nonhorizontal facet weight.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFacetEquiv {p : ℕ} (hp : Nat.Prime p) : Fin p ≃ Fin (p - 2 + 2)

Transport from the ambient prime-cardinality index to the face index of a (p - 2)-simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFacetEquiv hp = finCongr ⋯

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFacetIndex {p : ℕ} (hp : Nat.Prime p) (k : Fin p) : Fin (p - 2 + 2)

The face index corresponding to a labelled facet of a prime orbit.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFacetIndex hp k = (NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFacetEquiv hp) k

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.simplicialIncidence_eq_orbitFace_sum {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (source : Simplex p (p - 2 + 1)) : SimplicialIncidence.incidence target source = ∑ k : Fin p, if source.restrict (FaceMap.delete (orbitFacetIndex hp k)) = target then SimplicialChain.faceSign (orbitFacetIndex hp k) else 0

Reindex simplicial incidence by the ambient prime-cardinality face indices.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitTopFace {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) (k : Fin p) : Simplex p (p - 2)

The facet of the chosen top representative obtained by deleting k.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFaceClass {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) (k : Fin p) : PrimeOrbitCycle.FacetOrbit hp

Orbit class of a face of the chosen top representative.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.exists_orbitFaceTransport {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) (k : Fin p) : ∃ (g : ↥(PrimeSymmetry p)), g • PrimeOrbitCycle.facetRepresentative hp (orbitFaceClass hp c k) = orbitTopFace hp c k

A face and the canonical representative of its orbit differ by a prime relabelling.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFaceTransport {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) (k : Fin p) : ↥(PrimeSymmetry p)

A chosen prime relabelling that sends the canonical representative of a face orbit to the actual face of the chosen top representative.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFaceTransport hp c k = Classical.choose ⋯

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFaceTransport_spec {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) (k : Fin p) : orbitFaceTransport hp c k • PrimeOrbitCycle.facetRepresentative hp (orbitFaceClass hp c k) = orbitTopFace hp c k

Specification of the chosen face transporter.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitTopCellOfFace {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) (k : Fin p) : ↑(MulAction.orbitRel.Quotient.orbit c)

The unique member of the chosen top orbit whose k-th face is the canonical representative of that face orbit.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitTopCellOfFace_restrict {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) (k : Fin p) : Simplex.restrict (↑(orbitTopCellOfFace hp c k)) (FaceMap.delete (orbitFacetIndex hp k)) = PrimeOrbitCycle.facetRepresentative hp (orbitFaceClass hp c k)

The selected top-orbit member has the canonical facet representative as its k-th face.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.OrbitFaceWitness {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) : Type

Incidence witnesses between one top orbit and the canonical facet representatives.

Equations

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

@[instance_reducible]

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.topOrbitMemberFintype {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) : Fintype ↑(MulAction.orbitRel.Quotient.orbit c)

Enumerate the members of a finite top-cell orbit.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.topOrbitMemberFintype hp c = Subtype.fintype (Membership.mem (MulAction.orbitRel.Quotient.orbit c))

@[instance_reducible]

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFaceWitnessFintype {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) : Fintype (OrbitFaceWitness hp c)

Enumerate the face witnesses of a fixed top-cell orbit.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFaceWitnessEquiv {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) : Fin p ≃ OrbitFaceWitness hp c

Every face of the chosen top representative determines exactly one nonzero orbit-incidence witness.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbitFaceWitness_sum {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) (W : Simplex p (p - 2) → ZMod p) : (∑ qf : PrimeOrbitCycle.FacetOrbit hp, ∑ s : ↑(MulAction.orbitRel.Quotient.orbit c), ∑ k : Fin p, if Simplex.restrict (↑s) (FaceMap.delete (orbitFacetIndex hp k)) = PrimeOrbitCycle.facetRepresentative hp qf then SimplicialChain.faceSign (orbitFacetIndex hp k) * W (PrimeOrbitCycle.facetRepresentative hp qf) else 0) = ∑ z : OrbitFaceWitness hp c, SimplicialChain.faceSign (orbitFacetIndex hp (↑z).2) * W (PrimeOrbitCycle.facetRepresentative hp (↑z).1.1)

Expand orbit incidence as a sum over its nonzero face witnesses.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbit_coboundary_eq_face_sum {p : ℕ} (hp : Nat.Prime p) (c : PrimeOrbitCycle.TopOrbit hp) (W : Simplex p (p - 2) → ZMod p) (hW : ∀ (g : ↥(PrimeSymmetry p)) (f : Simplex p (p - 2)), W (g • f) = W f) : ∑ qf : PrimeOrbitCycle.FacetOrbit hp, (PrimeOrbitCycle.orbitCycle hp).incidence qf c * W (PrimeOrbitCycle.facetRepresentative hp qf) = ∑ k : Fin p, SimplicialChain.faceSign (orbitFacetIndex hp k) * W (orbitTopFace hp c k)

The orbit coboundary at a chosen top representative is its ordinary weighted face sum.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.orbit_boundary_pairing_eq_zero {p : ℕ} (hp : Nat.Prime p) (W : Simplex p (p - 2) → ZMod p) (hW : ∀ (g : ↥(PrimeSymmetry p)) (f : Simplex p (p - 2)), W (g • f) = W f) : ∑ c : PrimeOrbitCycle.TopOrbit hp, (PrimeOrbitCycle.orbitCycle hp).coefficient c * ∑ k : Fin p, SimplicialChain.faceSign (orbitFacetIndex hp k) * W (Simplex.restrict (PrimeOrbitCycle.topRepresentative hp c) (FaceMap.delete (orbitFacetIndex hp k))) = 0

Weighted boundary pairing of the orbit cycle vanishes for every equivariant facet weight.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap_eq_iteratedFacetMap_succ {n : ℕ} (hp : Nat.Prime (n + 1)) (N L : ℕ) (base : RefinedAffineMap.TopCell hp N) (k : Fin (n + 1)) (rho : Fin L → Equiv.Perm (Fin (n + 2))) (j : Fin (n + 2)) : occurrenceFacetMap hp N L (((base, k), rho), j) = iteratedFacetMap n L (staircasePrismMap n (⇑(RefinedAffineMap.chart hp N base)) k) rho (EquivariantPrismGlobalCancellation.facetFaceIndex hp j)

In successor dimension, the concrete occurrence facet is the iterated facet map of the corresponding unrefined staircase prism.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.refined_chart_eq_affineCompMap {n : ℕ} (hp : Nat.Prime (n + 1)) (N : ℕ) (orbit : PrimeOrbitCycle.TopOrbit hp) (spatial : RefinementWord (n + 1) N) : ⇑(RefinedAffineMap.chart hp N (orbit, spatial)) = fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => (ReferenceAffineOrbitCount.topRepr hp orbit).realizationPoint (StandardSimplex.ofDelta ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n N spatial) x))

In positive successor dimension, the refined chart is the unrefined realization chart precomposed with the same spatial refinement word.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.realizationPoint_prime_smul_any {d : ℕ} (p : ℕ) (g : ↥(PrimeSymmetry p)) (s : Simplex p d) (w : StandardSimplex d) : (g • s).realizationPoint w = g • s.realizationPoint w

Relabelling any simplex commutes with its realization chart.

Shared spatial-side bridge

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.genericSpatialSideWeight {n : ℕ} (hp : Nat.Prime (n + 1)) (L : ℕ) (V : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → Realization (n + 1) × ↑(Set.Icc 0 1)) → ZMod (n + 1)) (eta : Fin L → Equiv.Perm (Fin (n + 1))) (h : Fin n) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n - 1)) → Realization (n + 1)) : ZMod (n + 1)

Weight of a staircase side simplex for any affine-facet weight.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.refined_side_eq_genericSpatialSideWeight {n : ℕ} (hp : Nat.Prime (n + 1)) (N L : ℕ) (V : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → Realization (n + 1) × ↑(Set.Icc 0 1)) → ZMod (n + 1)) (orbit : PrimeOrbitCycle.TopOrbit hp) (spatial : RefinementWord (n + 1) N) (eta : Fin L → Equiv.Perm (Fin (n + 1))) (r : Fin (n + 1)) (h : Fin n) : have hn := ⋯; have hd := ⋯; have spatial' := fun (k : Fin N) => ((Equiv.cast ⋯).trans (spatial k)).trans (Equiv.cast ⋯); have baseSimplex := fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n - 1 + 1))) => (ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap (deltaCast ⋯ x); (V fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => sidePrismMap n (⇑(RefinedAffineMap.chart hp N (orbit, spatial))) r h ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n L eta) x)) = genericSpatialSideWeight hp L V eta h (iteratedFacetMap (n - 1) N baseSimplex spatial' (Fin.cast ⋯ r))

A refined-chart side simplex is the generic weight of its spatial facet.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.spatialSideWeight {n : ℕ} (hp : Nat.Prime (n + 1)) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (eta : Fin L → Equiv.Perm (Fin (n + 1))) (h : Fin n) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n - 1)) → Realization (n + 1)) : ZMod (n + 1)

Weight of a staircase side simplex built over a spatial facet.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.refined_side_eq_spatialSideWeight {n : ℕ} (hp : Nat.Prime (n + 1)) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (orbit : PrimeOrbitCycle.TopOrbit hp) (spatial : RefinementWord (n + 1) N) (eta : Fin L → Equiv.Perm (Fin (n + 1))) (r : Fin (n + 1)) (h : Fin n) : have hn := ⋯; have hd := ⋯; have spatial' := fun (k : Fin N) => ((Equiv.cast ⋯).trans (spatial k)).trans (Equiv.cast ⋯); have baseSimplex := fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n - 1 + 1))) => (ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap (deltaCast ⋯ x); (nonhorizontalMapWeight hp N L a fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1 - 1))) => sidePrismMap n (⇑(RefinedAffineMap.chart hp N (orbit, spatial))) r h ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n L eta) x)) = spatialSideWeight hp N L a eta h (iteratedFacetMap (n - 1) N baseSimplex spatial' (Fin.cast ⋯ r))

A side simplex of a refined chart is the side weight of its iterated spatial facet.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.refined_side_eq_spatialSideWeight_succ {n : ℕ} (hp : Nat.Prime (n + 1 + 1)) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (orbit : PrimeOrbitCycle.TopOrbit hp) (spatial : RefinementWord (n + 1 + 1) N) (eta : Fin L → Equiv.Perm (Fin (n + 1 + 1))) (r : Fin (n + 1 + 1)) (h : Fin (n + 1)) : (nonhorizontalMapWeight hp N L a fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1 + 1 - 1))) => sidePrismMap (n + 1) (⇑(RefinedAffineMap.chart hp N (orbit, spatial))) r h ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (n + 1) L eta) x)) = spatialSideWeight hp N L a eta h (iteratedFacetMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) spatial r)

Successor-dimensional form of the refined side bridge, with transports normalized.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.spatialSide_weighted_boundary {n : ℕ} (hp : Nat.Prime (n + 1 + 1)) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (eta : Fin L → Equiv.Perm (Fin (n + 1 + 1))) (h : Fin (n + 1)) (orbit : PrimeOrbitCycle.TopOrbit hp) : ∑ spatial : RefinementWord (n + 1 + 1) N, iteratedSign (ZMod (n + 1 + 1)) N spatial * ∑ r : Fin (n + 1 + 1), SimplicialChain.faceSign r * spatialSideWeight hp N L a eta h (iteratedFacetMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) spatial r) = ∑ j : Fin (n + 1 + 1), SimplicialChain.faceSign j * ∑ theta : Fin N → Equiv.Perm (Fin (n + 1)), iteratedSign (ZMod (n + 1 + 1)) N theta * spatialSideWeight hp N L a eta h (iteratedBoundaryMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) j theta)

The spatial subdivision boundary identity specialized to a fixed side weight.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.spatialSide_scaled_boundary {n : ℕ} (hp : Nat.Prime (n + 1 + 1)) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (eta : Fin L → Equiv.Perm (Fin (n + 1 + 1))) (h : Fin (n + 1)) (orbit : PrimeOrbitCycle.TopOrbit hp) : ∑ spatial : RefinementWord (n + 1 + 1) N, ∑ r : Fin (n + 1 + 1), (PrimeOrbitCycle.orbitCycle hp).coefficient orbit * iteratedSign (ZMod (n + 1 + 1)) N spatial * (iteratedSign (ZMod (n + 1 + 1)) L eta * (SimplicialChain.faceSign r * ((-1) ^ ↑h * spatialSideWeight hp N L a eta h (iteratedFacetMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) spatial r)))) = (PrimeOrbitCycle.orbitCycle hp).coefficient orbit * iteratedSign (ZMod (n + 1 + 1)) L eta * (-1) ^ ↑h * ∑ j : Fin (n + 1 + 1), SimplicialChain.faceSign j * ∑ theta : Fin N → Equiv.Perm (Fin (n + 1)), iteratedSign (ZMod (n + 1 + 1)) N theta * spatialSideWeight hp N L a eta h (iteratedBoundaryMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) j theta)

The scaled form of the spatial side boundary identity used in the final sum.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.iteratedBoundaryMap_eq_orbitFaceRealization (n N : ℕ) (hp : Nat.Prime (n + 1 + 1)) (theta : Fin N → Equiv.Perm (Fin (n + 1))) (orbit : PrimeOrbitCycle.TopOrbit hp) (j : Fin (n + 1 + 1)) : iteratedBoundaryMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) j theta = fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => (Simplex.restrict (PrimeOrbitCycle.topRepresentative hp orbit) (FaceMap.delete j)).realizationPoint (StandardSimplex.ofDelta ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n N theta) x))

A refined orbit face map is the realization of the corresponding restricted simplex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.fixed_refined_orbit_pairing_cancels (N L n : ℕ) (hp : Nat.Prime (n + 1 + 1)) (W : Simplex (n + 1 + 1) n → ZMod (n + 1 + 1)) (hW : ∀ (g : ↥(PrimeSymmetry (n + 1 + 1))) (f : Simplex (n + 1 + 1) n), W (g • f) = W f) (eta : Fin L → Equiv.Perm (Fin (n + 1 + 1))) (h : Fin (n + 1)) (theta : Fin N → Equiv.Perm (Fin (n + 1))) : ∑ orbit : PrimeOrbitCycle.TopOrbit hp, ∑ j : Fin (n + 1 + 1), (PrimeOrbitCycle.orbitCycle hp).coefficient orbit * iteratedSign (ZMod (n + 1 + 1)) L eta * (-1) ^ ↑h * (SimplicialChain.faceSign j * (iteratedSign (ZMod (n + 1 + 1)) N theta * W (Simplex.restrict (PrimeOrbitCycle.topRepresentative hp orbit) (FaceMap.delete j)))) = 0

Fixed-refinement prime-orbit boundary cancellation for any invariant face weight.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.nonhorizontalContribution_eq_zero_core {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : EquivariantPrismGlobalCancellation.nonhorizontalContribution hp N L a = 0

The complete nonhorizontal refined-prism contribution vanishes.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.Result.nonhorizontalContribution_eq_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (m : ℝ) (R : EquivariantPrismGenericPerturbation.Result hp N L H m) : EquivariantPrismGlobalCancellation.nonhorizontalContribution hp N L R.assignment = 0

Nonhorizontal cancellation specialized to the compatible generic perturbation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismNonhorizontalCancellation.Result.lowerHorizontalContribution_eq_neg_upperHorizontalContribution {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F0 F1 : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F0 F1) (m : ℝ) (R : EquivariantPrismGenericPerturbation.Result hp N L H m) : EquivariantPrismGlobalCancellation.lowerHorizontalContribution hp N L R.assignment = -EquivariantPrismGlobalCancellation.upperHorizontalContribution hp N L R.assignment

The two horizontal contributions of a generic perturbation are opposite.