Classification of maximal Fox--Neuwirth flags

This file proves the surjectivity theorem for maximal-flag codes. The central observation is that if a.IsFace b, then every prefix cut defined by a bar of b contains exactly the same labels in a and b. Hence b.bars ⊆ a.bars. Along a maximal strict flag the dual dimension at vertex i is exactly i, so consecutive bar sets differ by one element. Those unique removed bars form a permutation of Fin (p - 1).

The first and last ranks, together with this removal permutation, reconstruct every intermediate cell: the bottom rank fixes the block order and the final rank fixes the order inside each block. This yields the explicit inverse simplexToCode and proves that toSimplex is bijective.

def NRR.BarredPermutation.rankPrefix {p : ℕ} (c : BarredPermutation p) (r : Fin (p - 1)) : Finset (Fin p)

Rank-prefix labels through position r.

Equations

• c.rankPrefix r = {x : Fin p | ↑(c.rank x) ≤ ↑r}

theorem NRR.BarredPermutation.mem_rankPrefix {p : ℕ} {c : BarredPermutation p} {r : Fin (p - 1)} {x : Fin p} : x ∈ c.rankPrefix r ↔ ↑(c.rank x) ≤ ↑r

def NRR.BarredPermutation.barLeft {p : ℕ} (r : Fin (p - 1)) : Fin p

The displayed position immediately to the left of a bar.

Using an explicit constructor avoids relying on the non-definitional arithmetic identity p - 1 + 1 = p.

Equations

• NRR.BarredPermutation.barLeft r = ⟨↑r, ⋯⟩

def NRR.BarredPermutation.barRight {p : ℕ} (r : Fin (p - 1)) : Fin p

The displayed position immediately to the right of a bar.

Equations

• NRR.BarredPermutation.barRight r = ⟨↑r + 1, ⋯⟩

@[simp]

theorem NRR.BarredPermutation.barLeft_val {p : ℕ} (r : Fin (p - 1)) : ↑(barLeft r) = ↑r

@[simp]

theorem NRR.BarredPermutation.barRight_val {p : ℕ} (r : Fin (p - 1)) : ↑(barRight r) = ↑r + 1

theorem NRR.BarredPermutation.card_rankPrefix {p : ℕ} (c : BarredPermutation p) (r : Fin (p - 1)) : (c.rankPrefix r).card = ↑r + 1

Every rank prefix has its evident size.

theorem NRR.BarredPermutation.blockIndex_mono_rank {p : ℕ} (c : BarredPermutation p) {x y : Fin p} (hxy : ↑(c.rank x) ≤ ↑(c.rank y)) : c.blockIndex x ≤ c.blockIndex y

Block indices are monotone in the displayed rank.

theorem NRR.BarredPermutation.blockIndex_lt_of_rank_le_bar_lt {p : ℕ} (c : BarredPermutation p) (r : Fin (p - 1)) (hr : r ∈ c.bars) {x y : Fin p} (hx : ↑(c.rank x) ≤ ↑r) (hy : ↑r < ↑(c.rank y)) : c.blockIndex x < c.blockIndex y

A bar separates every label on its left from every label on its right.

theorem NRR.BarredPermutation.mem_bars_iff_adjacent_blockIndex_lt {p : ℕ} (c : BarredPermutation p) (r : Fin (p - 1)) : r ∈ c.bars ↔ c.blockIndex ((Equiv.symm c.rank) (barLeft r)) < c.blockIndex ((Equiv.symm c.rank) (barRight r))

A bar is characterized by a strict block jump between its two adjacent displayed positions.

theorem NRR.BarredPermutation.rank_lt_of_mem_prefix_of_not_mem_prefix {p : ℕ} {a b : BarredPermutation p} (hface : a.IsFace b) (r : Fin (p - 1)) (hr : r ∈ b.bars) {x y : Fin p} (hx : x ∈ b.rankPrefix r) (hy : y ∉ b.rankPrefix r) : ↑(a.rank x) < ↑(a.rank y)

Across a bar of a coarser face, all prefix labels precede all complementary labels in every refinement.

theorem NRR.BarredPermutation.rankPrefix_eq_of_isFace {p : ℕ} {a b : BarredPermutation p} (hface : a.IsFace b) (r : Fin (p - 1)) (hr : r ∈ b.bars) : a.rankPrefix r = b.rankPrefix r

A face relation preserves the label set lying in every bar-defined rank prefix of the coarser cell.

theorem NRR.BarredPermutation.bars_subset_of_isFace {p : ℕ} {a b : BarredPermutation p} (hface : a.IsFace b) : b.bars ⊆ a.bars

Bars can only disappear when passing to a coarser face.

theorem NRR.BarredPermutation.blockIndex_eq_barCount_before_vertexRank {p : ℕ} {a b : BarredPermutation p} (hface : a.IsFace b) (x : Fin p) : b.blockIndex x = {r ∈ b.bars | ↑r < ↑(a.rank x)}.card

Along a face, the coarser block index counts the bars lying before the finer cell's rank.

The first-stage vertex is the intended finer cell, but only the face relation is needed.

noncomputable def NRR.FoxNeuwirthOrderComplex.Simplex.maximalDimensionOrderIso {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : Fin p ≃o Fin p

Dual dimension as an order isomorphism along a maximal strict flag.

Equations

• NRR.FoxNeuwirthOrderComplex.Simplex.maximalDimensionOrderIso hp s = { toEquiv := Equiv.ofBijective (fun (i : Fin p) => ⟨(↑s (Fin.cast ⋯ i)).dualDimension, ⋯⟩) ⋯, map_rel_iff' := ⋯ }

theorem NRR.FoxNeuwirthOrderComplex.Simplex.maximal_dualDimension {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (i : Fin p) : (↑s (Fin.cast ⋯ i)).dualDimension = ↑i

The dual dimension of vertex i in a maximal strict flag is exactly i.

theorem NRR.FoxNeuwirthOrderComplex.Simplex.maximal_bars_card {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (i : Fin p) : (↑s (Fin.cast ⋯ i)).bars.card = p - 1 - ↑i

Bar cardinality at a maximal-flag stage.

theorem NRR.FoxNeuwirthOrderComplex.Simplex.maximal_zero_isVertex {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : (↑s (MaximalFlagCode.simplexIndex hp (MaximalFlagCode.firstStage hp))).IsVertex

The initial vertex of a maximal strict flag is all-singleton.

theorem NRR.FoxNeuwirthOrderComplex.Simplex.maximal_last_isTop {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : (↑s (MaximalFlagCode.simplexIndex hp (MaximalFlagCode.lastStage hp))).IsTop

The final vertex of a maximal strict flag is top-dimensional.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.consecutive_sdiff_card {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (q : Fin (p - 1)) : ((↑s (simplexIndex hp (stageIndex hp q.castSucc))).bars \ (↑s (simplexIndex hp (stageIndex hp q.succ))).bars).card = 1

The bar difference between two consecutive maximal-flag stages is a singleton.

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removedBarAt {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (q : Fin (p - 1)) : Fin (p - 1)

The unique bar removed between two consecutive stages of a maximal strict flag.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removedBarAt hp s q = Classical.choose ⋯

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removedBarAt_spec {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (q : Fin (p - 1)) : (↑s (simplexIndex hp (stageIndex hp q.castSucc))).bars \ (↑s (simplexIndex hp (stageIndex hp q.succ))).bars = {removedBarAt hp s q}

The defining singleton difference for removedBarAt.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.maximal_bars_mono {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) {i j : Fin p} (hij : i ≤ j) : (↑s (simplexIndex hp j)).bars ⊆ (↑s (simplexIndex hp i)).bars

Bar sets are nested along any two stages of a maximal flag.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removedBarAt_injective {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : Function.Injective (removedBarAt hp s)

Distinct removal steps remove distinct bars.

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.decodedRemoval {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : Equiv.Perm (Fin (p - 1))

Canonical removal permutation recovered from a maximal strict flag.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.decodedRemoval hp s = Equiv.ofBijective (NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removedBarAt hp s) ⋯

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.decodedRemoval_apply {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (q : Fin (p - 1)) : (decodedRemoval hp s) q = removedBarAt hp s q

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.simplexToCode {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : Code p

Canonical code extracted from an arbitrary maximal strict flag.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.card_removedBefore {p : ℕ} (z : Code p) (j : Fin p) : (removedBefore z j).card = ↑j

Cardinality of the removed-before set for any removal permutation.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.card_retainedBars {p : ℕ} (z : Code p) (j : Fin p) : (retainedBars z j).card = p - 1 - ↑j

Cardinality of the retained-bar set at one coded stage.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedBars_simplexToCode {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (j : Fin p) : retainedBars (simplexToCode hp s) j = (↑s (simplexIndex hp j)).bars

The recovered removal schedule has exactly the original stage bar sets.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock_simplexToCode {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (j x : Fin p) : stageBlock (simplexToCode hp s) j x = (↑s (simplexIndex hp j)).blockIndex x

The stage block number reconstructed from the bottom vertex equals the original block index.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.rank_lt_iff_blockIndex_topRank {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (j x y : Fin p) : ↑((↑s (simplexIndex hp j)).rank x) < ↑((↑s (simplexIndex hp j)).rank y) ↔ toLex ((↑s (simplexIndex hp j)).blockIndex x, ↑((↑s (simplexIndex hp (lastStage hp))).rank x)) < toLex ((↑s (simplexIndex hp j)).blockIndex y, ↑((↑s (simplexIndex hp (lastStage hp))).rank y))

A cell rank is lexicographically determined by its block index and the final top rank.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageCell_simplexToCode {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (j : Fin p) : stageCell (simplexToCode hp s) j = ↑s (simplexIndex hp j)

Every reconstructed stage cell is the original simplex vertex.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.toSimplex_simplexToCode {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : toSimplex hp (simplexToCode hp s) = s

The canonical inverse reconstructs every maximal strict flag.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.simplexToCode_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : Code p) : simplexToCode hp (toSimplex hp z) = z

The canonical inverse also recovers every explicit code.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.everyMaximalFlagEncoded {p : ℕ} (hp : Nat.Prime p) : EveryMaximalFlagEncoded hp

Every maximal strict flag is encoded by the explicit stage construction.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.toSimplex_bijective {p : ℕ} (hp : Nat.Prime p) : Function.Bijective (toSimplex hp)

The explicit code map is bijective onto all maximal strict flags.

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

Unconditional equivalence between maximal-flag codes and all maximal strict flags.

Equations

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

theorem NRR.AAK.simplestRoute_maximalFlagEncoding_complete {p : ℕ} (hp : Nat.Prime p) : FoxNeuwirthOrderComplex.MaximalFlagCode.EveryMaximalFlagEncoded hp

Step 1 of the simplest route: maximal flags are unconditionally classified by explicit codes.