Source-sum cancellation for maximal Fox--Neuwirth flags

This module performs the finite source-sum reindexing left open after the explicit maximal-flag bridge. Rather than classifying a rank-two interval abstractly, it works with the concrete code

(bottom permutation, bar-removal permutation, top permutation).

For the bottom deleted face, the source sum is paired by bottomPartner. For every positive internal deleted face, it is paired by the corresponding removalPartner. The bridge theorems from MaximalFlagBridge show that paired codes produce the same deleted simplex, while the code orientation changes sign. Mathlib's finite fixed-point-free involution cancellation theorem then makes each code-indexed internal source sum vanish.

The deleted-face index carried through this module is k : Fin ((p - 2) + 2), matching the index type of TopFlagSubdivision.deletionCoefficient. Restriction of a (p - 1)-dimensional flag toSimplex hp z along that index uses the built-in-cast coface map deleteFace, which absorbs the (p - 2) + 2 vs p - 1 + 1 reindexing.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.faceDimEq {p : ℕ} (hp : Nat.Prime p) : p - 2 + 2 = p - 1 + 1

The face-dimension reindexing used to view a deletion index Fin ((p - 2) + 2) as a coface index Fin (p - 1 + 1).

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomDelIdx {p : ℕ} : Fin (p - 2 + 2)

The bottom deletion index, in the deletion-index type Fin ((p - 2) + 2).

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomDelIdx = ⟨0, ⋯⟩

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.codedFaceTerm {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (k : Fin (p - 2 + 2)) (z : Code p) : ZMod p

Contribution of one maximal-flag code to one fixed deleted face.

Equations

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

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

Code-indexed source sum for one fixed deleted position.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.codedFaceTerm_bottomPartner {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (z : Code p) : codedFaceTerm hp target bottomDelIdx (bottomPartner hp z) = -codedFaceTerm hp target bottomDelIdx z

The bottom partner negates the complete bottom-face summand, including its support predicate.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.codedDeletionCoefficient_bottom_eq_zero {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) : codedDeletionCoefficient hp target bottomDelIdx = 0

The code-indexed bottom-face source sum vanishes.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.codedFaceTerm_removalPartner {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (i : Fin (p - 2)) (z : Code p) : codedFaceTerm hp target i.succ.castSucc (removalPartner hp i z) = -codedFaceTerm hp target i.succ.castSucc z

A removal partner negates the complete positive-internal-face summand.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.codedDeletionCoefficient_removal_eq_zero {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (i : Fin (p - 2)) : codedDeletionCoefficient hp target i.succ.castSucc = 0

Every code-indexed positive internal source sum vanishes.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.codedDeletionCoefficient_internal_eq_zero {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (k : Fin (p - 2 + 2)) (hk : ↑k < p - 1) : codedDeletionCoefficient hp target k = 0

Every nonterminal code-indexed deleted-position sum vanishes.

structure NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.CompleteEncoding {p : ℕ} (hp : Nat.Prime p) : Prop

The two purely enumerative facts needed to identify code-indexed sums with the original maximal-simplex sums. This structure contains no cancellation or boundary assertion.

• bijective_toSimplex : Function.Bijective (toSimplex hp)
• coefficient_eq (z : Code p) : TopFlagSubdivision.integralCoefficient (toSimplex hp z) = coefficient z

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.codeEquivSimplex {p : ℕ} (hp : Nat.Prime p) (henc : CompleteEncoding hp) : Code p ≃ Simplex p (p - 1)

The explicit code map as an equivalence, once completeness of the enumeration is known.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.codeEquivSimplex hp henc = Equiv.ofBijective (NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.toSimplex hp) ⋯

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.transport_chain_apply {p a b : ℕ} (h : a = b) (f : Simplex p a → ZMod p) (s : Simplex p a) : Eq.rec (motive := fun (x : ℕ) (h : a = x) => Simplex p x → ZMod p) f h ((Equiv.cast ⋯) s) = f s

Transporting a chain along a dimension equality and evaluating it on the correspondingly transported simplex recovers the original evaluation.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.cast_simplex_apply {p a b : ℕ} (h : a = b) (s : Simplex p a) (i : Fin (b + 1)) : ↑((Equiv.cast ⋯) s) i = ↑s (Fin.cast ⋯ i)

Evaluation of a dimension-cast simplex at a vertex index.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.val_succAbove_eq {n : ℕ} (k : Fin (n + 1)) (j : Fin n) : ↑(k.succAbove j) = if ↑j < ↑k then ↑j else ↑j + 1

The value of Fin.succAbove as an explicit if.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.deletionCoefficient_eq_codedDeletionCoefficient {p : ℕ} (hp : Nat.Prime p) (henc : CompleteEncoding hp) (target : Simplex p (p - 2)) (k : Fin (p - 2 + 2)) : TopFlagSubdivision.deletionCoefficient hp target k = codedDeletionCoefficient hp target k

Reindex an actual fixed-position simplicial source sum by maximal-flag codes.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.rankTwoCancellation_of_completeEncoding (henc : ∀ {p : ℕ} (hp : Nat.Prime p), CompleteEncoding hp) : TopFlagSubdivision.RankTwoCancellationTheorem

The completed finite source-sum reindexing proves the original rank-two cancellation as soon as the explicit maximal-flag enumeration is identified with all maximal simplices.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.topFlagCycle_of_completeEncoding (henc : ∀ {p : ℕ} (hp : Nat.Prime p), CompleteEncoding hp) {p : ℕ} (hp : Nat.Prime p) : TopFlagSubdivision.boundary hp = 0

With the terminal theorem already proved, complete encoding yields the full simplicial cycle.

theorem NRR.AAK.simplestRoute_codeIndexedInternalCancellation {p : ℕ} (hp : Nat.Prime p) (target : FoxNeuwirthOrderComplex.Simplex p (p - 2)) (k : Fin (p - 2 + 2)) : ↑k < p - 1 → FoxNeuwirthOrderComplex.MaximalFlagCode.codedDeletionCoefficient hp target k = 0

The finite source-sum cancellation step is unconditional at the explicit code level.