Explicit codes and internal pairings for maximal Fox--Neuwirth flags

A maximal flag is combinatorially controlled by three permutations:

• the bottom singleton order;
• the order in which the p - 1 bars are removed;
• the final top-cell order.

This module implements the sign-reversing part of that description. Deleting the bottom vertex is paired by swapping the two bottom labels separated by the first removed bar. Deleting any other internal vertex is paired by swapping the two adjacent removal steps around that vertex. Both operations are fixed-point-free involutions and negate the canonical product sign.

The geometric/combinatorial bridge constructs the associated strict flag and proves that paired codes have the same deleted face. The finite involution lemma then proves RankTwoCancellationTheorem.

Index conventions. The bar-removal permutation lives on Fin (p - 1). Because Lean's natural subtraction does not make p - 2 + 1 and p - 1 definitionally equal, the removal-step pairing uses the explicit reindexing equivalence eQ hp : Fin (p - 2 + 1) ≃ Fin (p - 1), and the first-cut labels use ePp hp : Fin (p - 1 + 1) ≃ Fin p.

structure NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.Code (p : ℕ) : Type

Finite code for a maximal flag.

• bottom : Equiv.Perm (Fin p)

  The label permutation at the bottom of the encoded maximal flag.

• removal : Equiv.Perm (Fin (p - 1))

  The order in which the bars are removed along the maximal flag.

• top : Equiv.Perm (Fin p)

  The label permutation at the top of the encoded maximal flag.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.Code.ext {p : ℕ} {x y : Code p} (bottom : x.bottom = y.bottom) (removal : x.removal = y.removal) (top : x.top = y.top) : x = y

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.Code.ext_iff {p : ℕ} {x y : Code p} : x = y ↔ x.bottom = y.bottom ∧ x.removal = y.removal ∧ x.top = y.top

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instFintypeCode {p✝ : ℕ} : Fintype (Code p✝)

Equations

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

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instDecidableEqCode.decEq {p✝ : ℕ} (x✝ x✝¹ : Code p✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instDecidableEqCode {p✝ : ℕ} : DecidableEq (Code p✝)

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instDecidableEqCode = NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instDecidableEqCode.decEq

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.permSignInt {n : ℕ} (sigma : Equiv.Perm (Fin n)) : ℤ

Integer sign of a finite permutation.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.permSignInt sigma = ↑(Equiv.Perm.sign sigma)

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.coefficient {p : ℕ} (z : Code p) : ℤ

Canonical sign of a maximal-flag code.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.coefficient z = NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.permSignInt z.bottom * NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.permSignInt z.removal

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.firstRemovalStep {p : ℕ} (hp : Nat.Prime p) : Fin (p - 1)

First bar-removal step; prime cardinality guarantees that Fin (p - 1) is nonempty.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.firstRemovalStep hp = ⟨0, ⋯⟩

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomDeletionIndex {p : ℕ} (hp : Nat.Prime p) : Fin p

Bottom vertex index in a maximal flag.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomDeletionIndex hp = ⟨0, ⋯⟩

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ePp {p : ℕ} (hp : Nat.Prime p) : Fin (p - 1 + 1) ≃ Fin p

Reindexing equivalence Fin (p - 1 + 1) ≃ Fin p, used to view a bar-adjacent position as a bottom label position.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ePp hp = finCongr ⋯

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.eQ {p : ℕ} (hp : Nat.Prime p) : Fin (p - 2 + 1) ≃ Fin (p - 1)

Reindexing equivalence Fin (p - 2 + 1) ≃ Fin (p - 1), used to view an internal removal-step index as a bar position.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.eQ hp = finCongr ⋯

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.firstCutLeftLabel {p : ℕ} (hp : Nat.Prime p) (z : Code p) : Fin p

Label occupying the position immediately before the first removed bar.

Equations

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

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.firstCutRightLabel {p : ℕ} (hp : Nat.Prime p) (z : Code p) : Fin p

Label occupying the position immediately after the first removed bar.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.firstCutLabels_ne {p : ℕ} (hp : Nat.Prime p) (z : Code p) : firstCutLeftLabel hp z ≠ firstCutRightLabel hp z

The two labels around the first removed bar are distinct.

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPartner {p : ℕ} (hp : Nat.Prime p) (z : Code p) : Code p

Pairing for deletion of the bottom vertex: swap the two labels which become identified after removing the first bar.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPartner_removal {p : ℕ} (hp : Nat.Prime p) (z : Code p) : (bottomPartner hp z).removal = z.removal

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPartner_top {p : ℕ} (hp : Nat.Prime p) (z : Code p) : (bottomPartner hp z).top = z.top

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPartner_bottom_apply {p : ℕ} (hp : Nat.Prime p) (z : Code p) (i : Fin p) : (bottomPartner hp z).bottom i = z.bottom ((Equiv.swap (firstCutLeftLabel hp z) (firstCutRightLabel hp z)) i)

The bottom pairing swaps the ranks of the two labels and fixes every other rank.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPartner_leftLabel {p : ℕ} (hp : Nat.Prime p) (z : Code p) : firstCutLeftLabel hp (bottomPartner hp z) = firstCutRightLabel hp z

After the swap, the labels occupying the two first-cut positions are exchanged.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPartner_rightLabel {p : ℕ} (hp : Nat.Prime p) (z : Code p) : firstCutRightLabel hp (bottomPartner hp z) = firstCutLeftLabel hp z

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPartner_involutive {p : ℕ} (hp : Nat.Prime p) : Function.Involutive (bottomPartner hp)

Bottom pairing is an involution.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPartner_ne {p : ℕ} (hp : Nat.Prime p) (z : Code p) : bottomPartner hp z ≠ z

Bottom pairing has no fixed points.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.permSignInt_swap_trans {n : ℕ} (sigma : Equiv.Perm (Fin n)) (i j : Fin n) (hij : i ≠ j) : permSignInt (Equiv.trans (Equiv.swap i j) sigma) = -permSignInt sigma

Any nontrivial transposition negates the integer permutation sign.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.coefficient_bottomPartner {p : ℕ} (hp : Nat.Prime p) (z : Code p) : coefficient (bottomPartner hp z) = -coefficient z

Bottom pairing reverses the code orientation.

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removalPartner {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 2)) (z : Code p) : Code p

Pairing for a positive internal deleted position: swap the adjacent bar-removal steps on the left and right of that position.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removalPartner_bottom {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 2)) (z : Code p) : (removalPartner hp i z).bottom = z.bottom

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removalPartner_top {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 2)) (z : Code p) : (removalPartner hp i z).top = z.top

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.eQ_castSucc_ne_succ {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 2)) : (eQ hp) i.castSucc ≠ (eQ hp) i.succ

The two removal steps around an internal position are distinct after reindexing.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removalPartner_involutive {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 2)) : Function.Involutive (removalPartner hp i)

Removal-step pairing is an involution.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removalPartner_ne {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 2)) (z : Code p) : removalPartner hp i z ≠ z

Removal-step pairing has no fixed points.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.coefficient_removalPartner {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 2)) (z : Code p) : coefficient (removalPartner hp i z) = -coefficient z

Removal-step pairing reverses the code orientation.

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.deleteFace {p : ℕ} (hp : Nat.Prime p) (k : Fin (p - 1 + 1)) : FaceMap (p - 2) (p - 1)

The order-preserving face map that deletes a chosen maximal-flag vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.deleteFace hp k = { toFun := fun (i : Fin (p - 2 + 1)) => k.succAbove (Fin.cast ⋯ i), strictMono := ⋯ }

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.BottomFaceCompatibility {p : ℕ} (hp : Nat.Prime p) (toSimplex : Code p → Simplex p (p - 1)) : Prop

Bottom-partner flag codes represent the same simplex face after the bottom deletion.

Equations

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

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.RemovalFaceCompatibility {p : ℕ} (hp : Nat.Prime p) (toSimplex : Code p → Simplex p (p - 1)) : Prop

Removal-partner flag codes represent the same simplex face at the chosen internal deletion.

Equations

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

theorem NRR.AAK.simplestRoute_internalPairingKernel {p : ℕ} (hp : Nat.Prime p) : Function.Involutive (FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPartner hp)

The explicit sign-reversing internal pairing kernel is available.