The maximal-flag code-to-simplex bridge

This file completes the explicit bridge left open by MaximalFlagCode.

For a code z = (bottom, removal, top) and a stage j, the retained bars are those whose removal time is at least j. They determine an ordered block number for every label. The rank inside the stage cell is the ordinal rank of the lexicographic key

(stage block, final top rank).

Thus stage zero has the bottom singleton order, the final stage has the top order, and every intermediate stage orders its blocks from left to right while using the final top permutation inside each current block. This is the finite construction used by the exact regression checker.

The two internal pairings act transparently on this model:

• the bottom partner changes only stage zero, because its transposed labels lie on opposite sides of the first bar and that bar has disappeared at every later stage;
• the removal partner changes only the one intermediate stage between the two swapped removal times.

Consequently the paired maximal flags have literally equal deleted faces.

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removedBefore {p : ℕ} (z : Code p) (j : Fin p) : Finset (Fin (p - 1))

Bars already removed before stage j.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removedBefore z j = {r : Fin (p - 1) | ↑((Equiv.symm z.removal) r) < ↑j}

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedBars {p : ℕ} (z : Code p) (j : Fin p) : Finset (Fin (p - 1))

Bars still present at stage j.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedBars z j = Finset.univ \ NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removedBefore z j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.mem_retainedBars_iff {p : ℕ} (z : Code p) (j : Fin p) (r : Fin (p - 1)) : r ∈ retainedBars z j ↔ ↑j ≤ ↑((Equiv.symm z.removal) r)

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock {p : ℕ} (z : Code p) (j x : Fin p) : ℕ

Zero-based block number at one stage, computed in the bottom singleton order.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock z j x = {r ∈ NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedBars z j | ↑r < ↑(z.bottom x)}.card

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageKey {p : ℕ} (z : Code p) (j x : Fin p) : Lex (ℕ × ℕ)

Lexicographic key used to order labels at a stage.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageKey z j x = toLex (NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock z j x, ↑(z.top x))

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageKey_injective {p : ℕ} (z : Code p) (j : Fin p) : Function.Injective (stageKey z j)

The stage key is injective because its second coordinate is a permutation rank.

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ordinalRankNat {p : ℕ} (key : Fin p → Lex (ℕ × ℕ)) (x : Fin p) : ℕ

Ordinal rank of a key in a finite linear order.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ordinalRankNat key x = {y : Fin p | key y < key x}.card

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ordinalRankNat_lt {p : ℕ} (key : Fin p → Lex (ℕ × ℕ)) (x : Fin p) : ordinalRankNat key x < p

An ordinal rank is strictly smaller than the size of the finite type.

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ordinalRankFin {p : ℕ} (key : Fin p → Lex (ℕ × ℕ)) (x : Fin p) : Fin p

Fin-valued ordinal rank.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ordinalRankFin key x = ⟨NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ordinalRankNat key x, ⋯⟩

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ordinalRankFin_lt_of_lt {p : ℕ} {key : Fin p → Lex (ℕ × ℕ)} {x y : Fin p} (hxy : key x < key y) : ordinalRankFin key x < ordinalRankFin key y

Strictly ordered keys have strictly ordered ordinal ranks.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.ordinalRankFin_injective {p : ℕ} {key : Fin p → Lex (ℕ × ℕ)} (hkey : Function.Injective key) : Function.Injective (ordinalRankFin key)

For injective keys, ordinal rank is injective.

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageRank {p : ℕ} (z : Code p) (j : Fin p) : Equiv.Perm (Fin p)

The ordinal-rank permutation associated with a code stage.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageRank_apply {p : ℕ} (z : Code p) (j x : Fin p) : ↑((stageRank z j) x) = ordinalRankNat (stageKey z j) x

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageRank_lt_iff {p : ℕ} (z : Code p) (j x y : Fin p) : ↑((stageRank z j) x) < ↑((stageRank z j) y) ↔ stageKey z j x < stageKey z j y

Ordinal rank reflects the lexicographic key order.

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPrefix {p : ℕ} (z : Code p) (r : Fin (p - 1)) : Finset (Fin p)

Prefix of bottom positions ending at a cut.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomPrefix z r = {x : Fin p | ↑(z.bottom x) ≤ ↑r}

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.card_bottomPrefix {p : ℕ} (z : Code p) (r : Fin (p - 1)) : (bottomPrefix z r).card = ↑r + 1

A bottom prefix has the expected cardinality.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock_lt_of_bottom_le_cut_lt {p : ℕ} (z : Code p) (j : Fin p) (r : Fin (p - 1)) (hr : r ∈ retainedBars z j) (x y : Fin p) (hx : ↑(z.bottom x) ≤ ↑r) (hy : ↑r < ↑(z.bottom y)) : stageBlock z j x < stageBlock z j y

A retained cut separates stage block numbers strictly.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedCut_lt_stageRank_iff {p : ℕ} (z : Code p) (j : Fin p) (r : Fin (p - 1)) (hr : r ∈ retainedBars z j) (x : Fin p) : ↑r < ↑((stageRank z j) x) ↔ ↑r < ↑(z.bottom x)

A retained cut occurs before a stage rank exactly when it occurs before the bottom rank.

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageCell {p : ℕ} (z : Code p) (j : Fin p) : BarredPermutation p

The stage cell represented by a maximal-flag code.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageCell_blockIndex {p : ℕ} (z : Code p) (j x : Fin p) : (stageCell z j).blockIndex x = stageBlock z j x

The stage-cell block index is the block number used in its construction.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedBars_mono {p : ℕ} (z : Code p) {i j : Fin p} (hij : i ≤ j) : retainedBars z j ⊆ retainedBars z i

Retained bars decrease with the stage.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock_mono {p : ℕ} (z : Code p) (j : Fin p) {x y : Fin p} (hxy : ↑(z.bottom x) ≤ ↑(z.bottom y)) : stageBlock z j x ≤ stageBlock z j y

Stage blocks are monotone in the bottom position.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock_eq_of_le_of_eq {p : ℕ} (z : Code p) {i j : Fin p} (hij : i ≤ j) {x y : Fin p} (hxy : stageBlock z i x = stageBlock z i y) : stageBlock z j x = stageBlock z j y

Equality of blocks persists after further bar removals.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock_order_preserved {p : ℕ} (z : Code p) {i j : Fin p} (hij : i ≤ j) {x y : Fin p} (hxy : stageBlock z i x ≤ stageBlock z i y) : stageBlock z j x ≤ stageBlock z j y

Ordered blocks at an earlier stage remain ordered after further removals.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedBars_ssubset {p : ℕ} (z : Code p) {i j : Fin p} (hij : i < j) : retainedBars z j ⊂ retainedBars z i

A genuinely later stage has strictly fewer retained bars.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageCell_properFace {p : ℕ} (hp : Nat.Prime p) (z : Code p) {i j : Fin p} (hij : i < j) : ProperFace (stageCell z i) (stageCell z j)

Consecutive code stages form a strict Fox--Neuwirth face chain.

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

Cast a maximal-simplex vertex index to the stage index Fin p.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageIndex hp i = NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.maximalIndexCast hp i

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

Explicit strict flag associated with a maximal-flag code.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.toSimplex_apply {p : ℕ} (hp : Nat.Prime p) (z : Code p) (i : Fin (p - 1 + 1)) : ↑(toSimplex hp z) i = stageCell z (stageIndex hp i)

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageCell_ext {p : ℕ} {z w : Code p} {i j : Fin p} (hbars : retainedBars z i = retainedBars w j) (hblock : ∀ (x : Fin p), stageBlock z i x = stageBlock w j x) (htop : z.top = w.top) : stageCell z i = stageCell w j

A stage cell is determined by its retained bars, block numbers, and final permutation.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.firstCut_not_mem_retained {p : ℕ} (hp : Nat.Prime p) (z : Code p) {j : Fin p} (hj : 0 < ↑j) : z.removal (firstRemovalStep hp) ∉ retainedBars z j

The first removed bar is absent from every positive stage.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock_bottomPartner {p : ℕ} (hp : Nat.Prime p) (z : Code p) {j : Fin p} (hj : 0 < ↑j) (x : Fin p) : stageBlock (bottomPartner hp z) j x = stageBlock z j x

Swapping the two labels around the first removed cut preserves all positive-stage blocks.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageCell_bottomPartner {p : ℕ} (hp : Nat.Prime p) (z : Code p) {j : Fin p} (hj : 0 < ↑j) : stageCell (bottomPartner hp z) j = stageCell z j

The bottom partner gives the same cell at every positive stage.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedBars_removalPartner {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 2)) (z : Code p) (j : Fin p) (hj : ↑j ≠ ↑i + 1) : retainedBars (removalPartner hp i z) j = retainedBars z j

Swapping adjacent removal times preserves every prefix except the intermediate one.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageCell_removalPartner {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 2)) (z : Code p) (j : Fin p) (hj : ↑j ≠ ↑i + 1) : stageCell (removalPartner hp i z) j = stageCell z j

The removal partner gives the same cell away from its one changed intermediate stage.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.bottomFaceCompatibility {p : ℕ} (hp : Nat.Prime p) : BottomFaceCompatibility hp (toSimplex hp)

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removalFaceCompatibility {p : ℕ} (hp : Nat.Prime p) : RemovalFaceCompatibility hp (toSimplex hp)