Actual Fox--Neuwirth top-cell boundary

The orbit coefficient calculation in ModPOrbitCycle records the expected binomial answer, but it is not itself the boundary of a finite chain. This module defines the genuine finite incidence sum over all oriented top cells.

For a barred permutation a, topExtensions a is the finite set of top cells having a as a codimension-one face. The main reduction proves that the actual boundary coefficient is the cardinality of this extension set, multiplied by the chosen orientation of a. Consequently the prime cycle theorem reduces to the concrete shuffle-cardinality statement for codimension-one cells.

noncomputable def NRR.FoxNeuwirth.topExtensions {p : ℕ} (a : BarredPermutation p) : Finset (BarredPermutation.TopCell p)

Top cells containing a as a codimension-one face.

Equations

• NRR.FoxNeuwirth.topExtensions a = {c : NRR.BarredPermutation.TopCell p | a.IsFacet ↑c}

@[simp]

theorem NRR.FoxNeuwirth.mem_topExtensions_iff {p : ℕ} (a : BarredPermutation p) (c : BarredPermutation.TopCell p) : c ∈ topExtensions a ↔ a.IsFacet ↑c

noncomputable def NRR.FoxNeuwirth.topExtensionMultiplicity {p : ℕ} (a : BarredPermutation p) : ℕ

Number of top cells containing a given barred permutation as a facet.

Equations

• NRR.FoxNeuwirth.topExtensionMultiplicity a = (NRR.FoxNeuwirth.topExtensions a).card

noncomputable def NRR.FoxNeuwirth.actualTopBoundaryCoefficient {p : ℕ} (a : BarredPermutation p) : ZMod p

The actual coefficient of a in the boundary of the oriented top-cell sum.

Equations

• NRR.FoxNeuwirth.actualTopBoundaryCoefficient a = ∑ c : NRR.BarredPermutation.TopCell p, ↑(NRR.FoxNeuwirth.signedIncidence a ↑c) * NRR.FoxNeuwirth.orientedTopCoefficient ↑c

theorem NRR.FoxNeuwirth.actualTopBoundary_summand {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (c : BarredPermutation.TopCell p) : ↑(signedIncidence a ↑c) * orientedTopCoefficient ↑c = if a.IsFacet ↑c then ↑a.orientationSign else 0

One top-cell summand is the orientation of the facet when the incidence is present, and zero otherwise.

theorem NRR.FoxNeuwirth.actualTopBoundaryCoefficient_eq_multiplicity {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) : actualTopBoundaryCoefficient a = ↑(topExtensionMultiplicity a) * ↑a.orientationSign

The genuine boundary coefficient is the extension multiplicity times one common orientation sign.

theorem NRR.FoxNeuwirth.topExtensions_eq_empty_of_dimension_ne {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension ≠ p - 2) : topExtensions a = ∅

A cell outside codimension one has no top-cell extensions.

theorem NRR.FoxNeuwirth.topExtensionMultiplicity_eq_zero_of_dimension_ne {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension ≠ p - 2) : topExtensionMultiplicity a = 0

Multiplicity vanishes away from codimension one.

theorem NRR.FoxNeuwirth.bars_card_eq_one_of_codimOne {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : a.bars.card = 1

A codimension-one cell has exactly one bar.

noncomputable def NRR.FoxNeuwirth.facetBar {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : Fin (p - 1)

The unique bar of a codimension-one barred permutation.

Equations

• NRR.FoxNeuwirth.facetBar hp a ha = Classical.choose ⋯

theorem NRR.FoxNeuwirth.bars_eq_singleton_facetBar {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : a.bars = {facetBar hp a ha}

The bar set of a codimension-one cell is the singleton containing facetBar.

noncomputable def NRR.FoxNeuwirth.facetLeftSize {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : ℕ

Size of the first ordered block of a codimension-one cell.

Equations

• NRR.FoxNeuwirth.facetLeftSize hp a ha = ↑(NRR.FoxNeuwirth.facetBar hp a ha) + 1

@[simp]

theorem NRR.FoxNeuwirth.facetLeftSize_pos {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : 0 < facetLeftSize hp a ha

@[simp]

theorem NRR.FoxNeuwirth.facetLeftSize_lt {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : facetLeftSize hp a ha < p

def NRR.FoxNeuwirth.FirstBlockLabel {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : Type

Labels in the first ordered block, expressed directly by their rank before the unique bar.

Equations

• NRR.FoxNeuwirth.FirstBlockLabel hp a ha = { i : Fin p // ↑(a.rank i) < NRR.FoxNeuwirth.facetLeftSize hp a ha }

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirth.instFintypeFirstBlockLabel {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : Fintype (FirstBlockLabel hp a ha)

Equations

• NRR.FoxNeuwirth.instFintypeFirstBlockLabel hp a ha = id (Fintype.ofFinite { i : Fin p // ↑(a.rank i) < NRR.FoxNeuwirth.facetLeftSize hp a ha })

noncomputable def NRR.FoxNeuwirth.firstBlockEquivFin {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : FirstBlockLabel hp a ha ≃ Fin (facetLeftSize hp a ha)

The first block has the expected finite cardinality.

Equations

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

@[simp]

theorem NRR.FoxNeuwirth.card_firstBlockLabel {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : Fintype.card (FirstBlockLabel hp a ha) = facetLeftSize hp a ha

def NRR.FoxNeuwirth.TopExtension {p : ℕ} (a : BarredPermutation p) : Type

Top-cell extensions as a finite subtype.

Equations

• NRR.FoxNeuwirth.TopExtension a = { c : NRR.BarredPermutation.TopCell p // a.IsFacet ↑c }

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirth.instFintypeTopExtension {p : ℕ} (a : BarredPermutation p) : Fintype (TopExtension a)

Equations

• NRR.FoxNeuwirth.instFintypeTopExtension a = id (Fintype.ofFinite { c : NRR.BarredPermutation.TopCell p // a.IsFacet ↑c })

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirth.instDecidableEqTopExtension {p : ℕ} (a : BarredPermutation p) : DecidableEq (TopExtension a)

Equations

• NRR.FoxNeuwirth.instDecidableEqTopExtension a = Classical.decEq (NRR.FoxNeuwirth.TopExtension a)

@[simp]

theorem NRR.FoxNeuwirth.card_topExtension {p : ℕ} (a : BarredPermutation p) : Fintype.card (TopExtension a) = topExtensionMultiplicity a

noncomputable def NRR.FoxNeuwirth.firstBlockPositions {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : BarredPermutation.TopCell p) : Finset (Fin p)

Positions occupied by the first block inside a candidate top-cell order.

Equations

• NRR.FoxNeuwirth.firstBlockPositions hp a ha c = Finset.image (fun (i : NRR.FoxNeuwirth.FirstBlockLabel hp a ha) => (↑c).rank ↑i) Finset.univ

@[simp]

theorem NRR.FoxNeuwirth.card_firstBlockPositions {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : BarredPermutation.TopCell p) : (firstBlockPositions hp a ha c).card = facetLeftSize hp a ha

noncomputable def NRR.FoxNeuwirth.topExtensionToShuffle {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : TopExtension a → ShuffleIndex p (facetLeftSize hp a ha)

Canonical map sending a top-cell extension to the positions occupied by the first block.

Equations

• NRR.FoxNeuwirth.topExtensionToShuffle hp a ha c = ⟨NRR.FoxNeuwirth.firstBlockPositions hp a ha ↑c, ⋯⟩

def NRR.FoxNeuwirth.FacetShuffleCardinality (p : ℕ) : Prop

Exact finite combinatorial statement needed to identify every genuine facet boundary with a proper shuffle coefficient.

Equations

• NRR.FoxNeuwirth.FacetShuffleCardinality p = ∀ (a : NRR.BarredPermutation p), a.dualDimension = p - 2 → ∃ (k : ℕ), 0 < k ∧ k < p ∧ NRR.FoxNeuwirth.topExtensionMultiplicity a = p.choose k

def NRR.FoxNeuwirth.FacetShuffleBijection {p : ℕ} (hp : Nat.Prime p) : Prop

Concrete bijectivity statement for the canonical extension-to-shuffle map.

Equations

• NRR.FoxNeuwirth.FacetShuffleBijection hp = ∀ (a : NRR.BarredPermutation p) (ha : a.dualDimension = p - 2), Function.Bijective (NRR.FoxNeuwirth.topExtensionToShuffle hp a ha)

theorem NRR.FoxNeuwirth.facetShuffleCardinality_of_bijection {p : ℕ} (hp : Nat.Prime p) (H : FacetShuffleBijection hp) : FacetShuffleCardinality p

The canonical shuffle bijection implies the required cardinality formula.

theorem NRR.FoxNeuwirth.prime_dvd_topExtensionMultiplicity {p : ℕ} (hp : Nat.Prime p) (H : FacetShuffleCardinality p) (a : BarredPermutation p) : p ∣ topExtensionMultiplicity a

The shuffle-cardinality theorem implies divisibility of every actual top-extension multiplicity by the prime.

theorem NRR.FoxNeuwirth.actualTopBoundaryCoefficient_eq_zero {p : ℕ} (hp : Nat.Prime p) (H : FacetShuffleCardinality p) (a : BarredPermutation p) : actualTopBoundaryCoefficient a = 0

The shuffle-cardinality theorem proves that the actual oriented top-cell sum has zero boundary modulo p.

noncomputable def NRR.FoxNeuwirth.actualFiniteIncidenceCycle {p : ℕ} (hp : Nat.Prime p) (H : FacetShuffleCardinality p) : FiniteIncidenceCycle (ZMod p)

The genuine finite incidence cycle obtained from the actual top-cell boundary.

Equations

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