The Fox--Neuwirth top chain modulo a prime, at the cell-orbit level

A codimension-one orbit is determined by a proper split 0 < k < p. Its coefficient in the boundary of the oriented top chain is the orientation of the lower-dimensional cell multiplied by the number p.choose k of order-preserving shuffles. For prime p this multiplicity is divisible by p, so every orbit boundary coefficient vanishes in ZMod p.

The module deliberately records the orbit-summed coefficient used in the pseudomanifold argument. It does not identify the disjoint simplex atlas with the glued Blagojevic--Ziegler polyhedron; that regular-cell realization and the subsequent separator construction are separate topological steps.

def NRR.FoxNeuwirth.ProperSplit (p : ℕ) : Type

A proper split of p labels into two nonempty consecutive blocks.

Equations

• NRR.FoxNeuwirth.ProperSplit p = { k : ℕ // 0 < k ∧ k < p }

@[simp]

theorem NRR.FoxNeuwirth.ProperSplit.positive {p : ℕ} (s : ProperSplit p) : 0 < ↑s

@[simp]

theorem NRR.FoxNeuwirth.ProperSplit.lt_total {p : ℕ} (s : ProperSplit p) : ↑s < p

def NRR.FoxNeuwirth.orientedTopCoefficient {p : ℕ} (b : BarredPermutation p) : ZMod p

Coefficient assigned to an oriented top cell. Multiplying by the signed facet incidence removes the top-cell orientation, leaving one copy of the facet orientation per shuffle.

Equations

• NRR.FoxNeuwirth.orientedTopCoefficient b = if b.IsTop then ↑b.orientationSign else 0

theorem NRR.FoxNeuwirth.orientedTopCoefficient_ne_zero_iff {p : ℕ} (hp : Nat.Prime p) (b : BarredPermutation p) : orientedTopCoefficient b ≠ 0 ↔ b.IsTop

The oriented top coefficient is supported exactly on top cells.

theorem NRR.FoxNeuwirth.signedIncidence_mul_orientedTopCoefficient {p : ℕ} (hp : Nat.Prime p) {a b : BarredPermutation p} (hab : a.IsFacet b) (hb : b.IsTop) : ↑(signedIncidence a b) * orientedTopCoefficient b = ↑a.orientationSign

A supported top cell contributes precisely the chosen orientation of its facet.

def NRR.FoxNeuwirth.orbitBoundaryCoefficient (p : ℕ) (s : ProperSplit p) : ZMod p

Unsigned orbit-summed boundary coefficient for a proper split.

Equations

• NRR.FoxNeuwirth.orbitBoundaryCoefficient p s = ↑(NRR.FoxNeuwirth.unsignedFacetCoefficient p ↑s)

theorem NRR.FoxNeuwirth.orbitBoundaryCoefficient_eq_zero {p : ℕ} (hp : Nat.Prime p) (s : ProperSplit p) : orbitBoundaryCoefficient p s = 0

Every proper-split orbit coefficient vanishes modulo a prime.

def NRR.FoxNeuwirth.orientedOrbitBoundaryCoefficient {p : ℕ} (a : BarredPermutation p) (s : ProperSplit p) : ZMod p

Oriented orbit-summed boundary coefficient at a codimension-one cell.

Equations

• NRR.FoxNeuwirth.orientedOrbitBoundaryCoefficient a s = ↑a.orientationSign * NRR.FoxNeuwirth.orbitBoundaryCoefficient p s

theorem NRR.FoxNeuwirth.orientedOrbitBoundaryCoefficient_eq_zero {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (s : ProperSplit p) : orientedOrbitBoundaryCoefficient a s = 0

The oriented coefficient also vanishes modulo p.