Terminal cancellation for the top-flag subdivision

This module proves the terminal half of Step S3. A terminal boundary face is a strict flag whose last vertex is a Fox--Neuwirth facet. Appending a top cell to that flag is equivalent to choosing a top-cell extension of the final facet. The coefficient of the resulting maximal flag is independent of the chosen extension, while the number of extensions is divisible by the prime by the facet--shuffle equivalence.

The proof is deliberately separated from the internal rank-two cancellation. No classification of rank-two intervals is used here.

theorem NRR.FoxNeuwirthOrderComplex.Simplex.index_le_dualDimension {p d : ℕ} (s : Simplex p d) (i : Fin (d + 1)) : ↑i ≤ (↑s i).dualDimension

The index of a vertex in a strict chain is bounded by its dual dimension.

def NRR.FoxNeuwirthOrderComplex.Simplex.snoc {p d : ℕ} (s : Simplex p d) (c : BarredPermutation p) (hc : ∀ (i : Fin (d + 1)), ProperFace (↑s i) c) : Simplex p (d + 1)

Append one cell above every vertex of a strict flag.

Equations

• s.snoc c hc = ⟨fun (i : Fin (d + 1 + 1)) => Fin.lastCases c (fun (i : Fin (d + 1)) => ↑s i) i, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.snoc_last {p d : ℕ} (s : Simplex p d) (c : BarredPermutation p) (hc : ∀ (i : Fin (d + 1)), ProperFace (↑s i) c) : ↑(s.snoc c hc) (Fin.last (d + 1)) = c

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.snoc_castSucc {p d : ℕ} (s : Simplex p d) (c : BarredPermutation p) (hc : ∀ (i : Fin (d + 1)), ProperFace (↑s i) c) (i : Fin (d + 1)) : ↑(s.snoc c hc) i.castSucc = ↑s i

theorem NRR.FoxNeuwirthOrderComplex.Simplex.snoc_restrict_omit_last {p d : ℕ} (s : Simplex p d) (c : BarredPermutation p) (hc : ∀ (i : Fin (d + 1)), ProperFace (↑s i) c) : (s.snoc c hc).restrict (FaceMap.delete (Fin.last (d + 1))) = s

Deleting the appended final vertex recovers the original simplex.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.dualDimension_le_top {p : ℕ} (hp0 : 0 < p) (c : BarredPermutation p) : c.dualDimension ≤ p - 1

Every Fox--Neuwirth dual dimension is at most p - 1 when p is positive.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.isTop_of_dualDimension_eq_top {p : ℕ} (hp0 : 0 < p) (c : BarredPermutation p) (hc : c.dualDimension = p - 1) : c.IsTop

A cell of maximal dual dimension is a top cell.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.maximal_last_dualDimension {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : (↑s (Fin.last (p - 1))).dualDimension = p - 1

The final vertex of a maximal strict flag has top dual dimension.

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalIndex {p : ℕ} (hp : Nat.Prime p) : Fin (p - 2 + 2)

The terminal deletion index in the arithmetic presentation used by deletionCoefficient.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalIndex hp = ⟨p - 1, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalIndex_val {p : ℕ} (hp : Nat.Prime p) : ↑(terminalIndex hp) = p - 1

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalIndex_eq_last {p : ℕ} (hp : Nat.Prime p) : terminalIndex hp = Fin.last (p - 2 + 1)

The terminal index is the last index of the maximal flag.

def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.TerminalSource {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) : Type

Maximal flags whose terminal face is a fixed codimension-one flag.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.instFintypeTerminalSource {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) : Fintype (TerminalSource hp target)

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.instFintypeTerminalSource hp target = id inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.instDecidableEqTerminalSource {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) : DecidableEq (TerminalSource hp target)

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.instDecidableEqTerminalSource hp target = id inferInstance

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalSource_castSucc {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (u : TerminalSource hp target) (i : Fin (p - 2 + 1)) : ↑↑u i.castSucc = ↑target i

Initial vertices of a terminal source agree with the target flag.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalSource_last_dualDimension {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (u : TerminalSource hp target) : (↑↑u (Fin.last (p - 2 + 1))).dualDimension = p - 1

The last vertex of a terminal source has maximal dimension.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalSource_target_last_dualDimension {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (u : TerminalSource hp target) : (↑target (Fin.last (p - 2))).dualDimension = p - 2

If a terminal source exists, the last target vertex is a facet-dimensional cell.

noncomputable def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalSourceToTopExtension {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (u : TerminalSource hp target) : FoxNeuwirth.TopExtension (↑target (Fin.last (p - 2)))

A terminal source determines a top-cell extension of the final target facet.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalSourceToTopExtension hp target u = ⟨⟨↑↑u (Fin.last (p - 2 + 1)), ⋯⟩, ⋯⟩

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.properFace_topExtension {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (ha : (↑target (Fin.last (p - 2))).dualDimension = p - 2) (c : FoxNeuwirth.TopExtension (↑target (Fin.last (p - 2)))) (i : Fin (p - 2 + 1)) : ProperFace (↑target i) ↑↑c

Every vertex of the target lies properly below any top extension of its final facet.

noncomputable def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.topExtensionToTerminalSource {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (ha : (↑target (Fin.last (p - 2))).dualDimension = p - 2) (c : FoxNeuwirth.TopExtension (↑target (Fin.last (p - 2)))) : TerminalSource hp target

Append a chosen top extension to the target flag.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.topExtensionToTerminalSource hp target ha c = ⟨target.snoc ↑↑c ⋯, ⋯⟩

noncomputable def NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalSourceEquivTopExtension {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (u0 : TerminalSource hp target) : TerminalSource hp target ≃ FoxNeuwirth.TopExtension (↑target (Fin.last (p - 2)))

Terminal source flags are exactly top-cell extensions of the final facet.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.chain_eq_of_head_matrix {p : ℕ} (w w' : Simplex p (p - 1)) (h0 : ↑w 0 = ↑w' 0) (hm : barDifferenceMatrix w = barDifferenceMatrix w') : chain w = chain w'

Cast-free core: the subdivision chain value depends only on the head vertex and the bar-difference matrix.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.simplicialChain_cast_apply {p d d' : ℕ} (h : d = d') (f : SimplicialChain (ZMod p) p d) (w : Simplex p d') : (h ▸ f) w = f (⋯ ▸ w)

Applying a dimension-transported simplicial chain equals the chain applied to the transported simplex.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.simplex_cast_apply {p d d' : ℕ} (h : d = d') (s : Simplex p d) (j : Fin (d' + 1)) : ↑(h ▸ s) j = ↑s (Fin.cast ⋯ j)

Evaluating a dimension-transported simplex is evaluation at the reindexed vertex.

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

chain transported to the index (p - 2) + 1 used by the terminal deletion.

Equations

• NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.liftedTerminalChain hp = ⋯ ▸ NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.chain

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.liftedTerminalChain_eq_of_terminalSource {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (u v : TerminalSource hp target) : liftedTerminalChain hp ↑u = liftedTerminalChain hp ↑v

Any two terminal sources of the same target flag carry the same transported chain value: their initial faces agree (both restrict to target) and their final vertices are top cells, so the subdivision coefficient is independent of the terminal source.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.deletionCoefficient_terminal_eq_source_sum {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) : deletionCoefficient hp target (terminalIndex hp) = ∑ u : TerminalSource hp target, SimplicialChain.faceSign (terminalIndex hp) * liftedTerminalChain hp ↑u

Reindex the terminal deletion sum by the actual terminal source subtype.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.topExtension_card_cast_eq_zero {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) : ↑(Fintype.card (FoxNeuwirth.TopExtension a)) = 0

The cardinality of the top-extension type vanishes in ZMod p.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalCancellation {p : ℕ} (hp : Nat.Prime p) : TerminalCancellation hp

Terminal deleted faces cancel modulo the prime.

theorem NRR.FoxNeuwirthOrderComplex.TopFlagSubdivision.terminalMultiplicityTheorem : TerminalMultiplicityTheorem

The terminal local theorem required by the top-flag subdivision is unconditional.

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

After terminal reindexing, only the rank-two internal pairing remains for the simplicial cycle.

theorem NRR.AAK.simplestRoute_terminalCancellation_complete : FoxNeuwirthOrderComplex.TopFlagSubdivision.TerminalMultiplicityTheorem

Step S3 terminal reindexing is complete.