Top-flag subdivision of the Fox--Neuwirth cellular cycle

This module implements the concrete simplicial chain required by Step S3 of the simplest route. A maximal order-complex flag has p vertices and p - 1 successive transitions. For each transition we record the change of the bar-indicator vector. The determinant of the resulting square matrix is the sign of the order in which the initial bars are removed. Multiplying by the orientation of the bottom vertex gives the canonical orientation of the subdivided top cell.

The construction has two advantages over the earlier affine block determinant:

• it depends only on the finite barred-permutation data;
• its coefficient is independent of the final top-cell permutation once the preceding flag is fixed, so the terminal boundary is governed directly by the top-extension multiplicity proved in FacetShuffleEquiv.

The local boundary theorem is rank-two internal cancellation. It is isolated below as an explicit finite statement about the actual chain, rather than hidden in a geometric certificate.

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.barIndicator {p : ℕ} (c : BarredPermutation p) (r : Fin (p - 1)) : ℤ

Integer indicator of a bar position.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.barIndicator c r = if r ∈ c.bars then 1 else 0

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.barIndicator_of_mem {p : ℕ} (c : BarredPermutation p) (r : Fin (p - 1)) (hr : r ∈ c.bars) : barIndicator c r = 1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.barIndicator_of_not_mem {p : ℕ} (c : BarredPermutation p) (r : Fin (p - 1)) (hr : r ∉ c.bars) : barIndicator c r = 0

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.barDifferenceMatrix {p : ℕ} (s : Simplex p (p - 1)) : Matrix (Fin (p - 1)) (Fin (p - 1)) ℤ

Matrix of successive bar-removal vectors along a maximal strict flag.

Equations

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

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.barRemovalDeterminant {p : ℕ} (s : Simplex p (p - 1)) : ℤ

Orientation of the order in which bars disappear along a maximal flag.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.barRemovalDeterminant s = (NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.barDifferenceMatrix s).det

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.permutationOrientationSign {p : ℕ} (c : BarredPermutation p) : ℤ

Canonical permutation orientation of a Fox--Neuwirth cell.

This is the Mathlib permutation sign of the displayed rank. It is the same parity orientation used by BarredPermutation.orientationSign, but using the library sign directly avoids carrying a second inversion-parity implementation into the subdivision determinant calculation.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.permutationOrientationSign c = ↑(Equiv.Perm.sign c.rank)

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.integralCoefficient {p : ℕ} (s : Simplex p (p - 1)) : ℤ

Integral coefficient of a maximal flag in the subdivision chain.

Equations

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

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.chain {p : ℕ} : SimplicialChain (ZMod p) p (p - 1)

The concrete top-flag subdivision chain over ZMod p.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.chain s = ↑(NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.integralCoefficient s)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.chain_apply {p : ℕ} (s : Simplex p (p - 1)) : chain s = ↑(integralCoefficient s)

noncomputable def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.boundary {p : ℕ} (hp : Nat.Prime p) : SimplicialChain (ZMod p) p (p - 2)

The actual simplicial boundary of the top-flag subdivision chain.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.boundary hp = (⋯ ▸ NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.chain).boundary

noncomputable def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.deletionCoefficient {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (k : Fin (p - 2 + 2)) : ZMod p

Contribution obtained by deleting one fixed position from a maximal flag.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.boundary_apply_eq_sum_deletionCoefficient {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) : boundary hp target = ∑ k : Fin (p - 2 + 2), deletionCoefficient hp target k

Boundary coefficients split as the sum over deleted positions.

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.InternalCancellation {p : ℕ} (hp : Nat.Prime p) : Prop

Internal deletion positions, including deletion of the bottom vertex, cancel locally.

Equations

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

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.TerminalCancellation {p : ℕ} (hp : Nat.Prime p) : Prop

The terminal deletion removes the final top-dimensional cell.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.boundary_eq_zero_of_internal_terminal {p : ℕ} (hp : Nat.Prime p) (hint : InternalCancellation hp) (hterminal : TerminalCancellation hp) : boundary hp = 0

Internal and terminal cancellation imply that the concrete flag chain is a cycle.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.integralCoefficient_eq_of_initial_and_bars_eq {p : ℕ} (s t : Simplex p (p - 1)) (hzero : ↑s 0 = ↑t 0) (hbars : ∀ (i : Fin (p - 1 + 1)), (↑s i).bars = (↑t i).bars) : integralCoefficient s = integralCoefficient t

A maximal flag's coefficient only depends on its bottom cell and its sequence of bar sets. In particular, changing only the final top cell does not change the coefficient.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.integralCoefficient_eq_of_init_eq_of_final_top {p : ℕ} (hp : Nat.Prime p) (s t : Simplex p (p - 1)) (hinit : ∀ (i : Fin (p - 1)), ↑s i.castSucc = ↑t i.castSucc) (hs : (↑s (Fin.last (p - 1))).IsTop) (ht : (↑t (Fin.last (p - 1))).IsTop) : integralCoefficient s = integralCoefficient t

Special case used for terminal faces: once all preceding vertices agree and both final vertices are top cells, the flag coefficients agree.

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.RankTwoCancellationTheorem : Prop

The exact internal combinatorics: every nonterminal deleted face has total signed extension coefficient zero. This is a finite rank-two interval statement for ordered partitions.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.RankTwoCancellationTheorem = ∀ {p : ℕ} (hp : Nat.Prime p), NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.InternalCancellation hp

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.TerminalMultiplicityTheorem : Prop

The exact terminal reindexing statement. The coefficient independence theorem above reduces this to the already proved facet--shuffle multiplicity.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.TerminalMultiplicityTheorem = ∀ {p : ℕ} (hp : Nat.Prime p), NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.TerminalCancellation hp

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.cycle_of_rankTwo_and_terminal (hrank : RankTwoCancellationTheorem) (hterminal : TerminalMultiplicityTheorem) {p : ℕ} (hp : Nat.Prime p) : boundary hp = 0

If the two finite local cancellation theorems are proved, the concrete chain is an unconditional simplicial cycle.

theorem NRR.AAK.simplestRoute_topFlagSubdivision_defined : Nonempty (FoxNeuwirthOrderComplex.SimplicialChain (ZMod 2) 2 1)

Step S3 now has a concrete maximal-flag chain on the glued order complex.