Step 1: recovering maximal-flag codes

This file implements the unconditional part of the maximal-flag encoding theorem.

The explicit map

MaximalFlagCode.toSimplex hp : Code p → Simplex p (p - 1)

is proved injective. The proof recovers the bottom and top permutations from the endpoint vertices and recovers the bar-removal permutation from the successive retained-bar sets. Consequently Code p is equivalent to the subtype of maximal strict flags lying in the image of the explicit stage construction.

The surjectivity statement is isolated as EveryMaximalFlagEncoded hp. From this classification the file constructs simplexToCode, proves both inverse identities, and packages the requested equivalence with all maximal strict flags. No cycle, coefficient, or cancellation statement is included in that classification hypothesis.

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

The first (bottom) stage index, in Fin p.

Equations

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

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

The last (top) stage index, in Fin p.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.lastStage hp = ⟨p - 1, ⋯⟩

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

Cast a stage index back to the arithmetic index used by a maximal simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.simplexIndex hp j = Fin.cast ⋯ j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageIndex_simplexIndex {p : ℕ} (hp : Nat.Prime p) (j : Fin p) : stageIndex hp (simplexIndex hp j) = j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageIndex_last {p : ℕ} (hp : Nat.Prime p) : stageIndex hp (Fin.last (p - 1)) = lastStage hp

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedBars_zero {p : ℕ} (hp : Nat.Prime p) (z : Code p) : retainedBars z (firstStage hp) = Finset.univ

At stage zero every original bar is retained.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.retainedBars_last {p : ℕ} (hp : Nat.Prime p) (z : Code p) : retainedBars z (lastStage hp) = ∅

At the final stage every bar has been removed.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock_zero {p : ℕ} (hp : Nat.Prime p) (z : Code p) (x : Fin p) : stageBlock z (firstStage hp) x = ↑(z.bottom x)

At stage zero the block number is the bottom-permutation rank.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageBlock_last {p : ℕ} (hp : Nat.Prime p) (z : Code p) (x : Fin p) : stageBlock z (lastStage hp) x = 0

At the final stage every label has block number zero.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.perm_eq_of_lt_iff {n : ℕ} (sigma tau : Equiv.Perm (Fin n)) (horder : ∀ (x y : Fin n), sigma x < sigma y ↔ tau x < tau y) : sigma = tau

A finite permutation is determined by the strict order it induces.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageRank_zero {p : ℕ} (hp : Nat.Prime p) (z : Code p) : stageRank z (firstStage hp) = z.bottom

The first stage rank is exactly the coded bottom permutation.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageRank_last {p : ℕ} (hp : Nat.Prime p) (z : Code p) : stageRank z (lastStage hp) = z.top

The final stage rank is exactly the coded top permutation.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageCell_zero {p : ℕ} (hp : Nat.Prime p) (z : Code p) : stageCell z (firstStage hp) = { rank := z.bottom, bars := Finset.univ }

The first stage cell is the all-singleton cell determined by bottom.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.stageCell_last {p : ℕ} (hp : Nat.Prime p) (z : Code p) : stageCell z (lastStage hp) = { rank := z.top, bars := ∅ }

The final stage cell is the top cell determined by top.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removal_mem_retained_castSucc {p : ℕ} (hp : Nat.Prime p) (z : Code p) (q : Fin (p - 1)) : z.removal q ∈ retainedBars z (stageIndex hp q.castSucc)

A bar removed at step q is present immediately before that step.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removal_not_mem_retained_succ {p : ℕ} (hp : Nat.Prime p) (z : Code p) (q : Fin (p - 1)) : z.removal q ∉ retainedBars z (stageIndex hp q.succ)

A bar removed at step q is absent immediately after that step.

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.removal_eq_of_retainedBars_eq {p : ℕ} (hp : Nat.Prime p) {z w : Code p} (hbars : ∀ (j : Fin p), retainedBars z j = retainedBars w j) : z.removal = w.removal

Equality of every retained-bar stage determines the removal permutation.

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

The explicit maximal-flag code map is injective.

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.EncodedSimplex {p : ℕ} (hp : Nat.Prime p) : Type

Maximal strict flags produced by the explicit stage construction.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.EncodedSimplex hp = { s : NRR.FoxNeuwirthOrderComplex.Simplex p (p - 1) // s ∈ Set.range (NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.toSimplex hp) }

instance NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instFiniteEncodedSimplex {p : ℕ} (hp : Nat.Prime p) : Finite (EncodedSimplex hp)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instFintypeEncodedSimplex {p : ℕ} (hp : Nat.Prime p) : Fintype (EncodedSimplex hp)

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instFintypeEncodedSimplex hp = Fintype.ofFinite (NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.EncodedSimplex hp)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instDecidableEqEncodedSimplex {p : ℕ} (hp : Nat.Prime p) : DecidableEq (EncodedSimplex hp)

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.instDecidableEqEncodedSimplex hp = Classical.decEq (NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.EncodedSimplex hp)

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.encodedSimplexToCode {p : ℕ} (hp : Nat.Prime p) (s : EncodedSimplex hp) : Code p

Recover the unique code of an encoded maximal flag.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.encodedSimplexToCode hp s = Classical.choose ⋯

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.toSimplex_encodedSimplexToCode {p : ℕ} (hp : Nat.Prime p) (s : EncodedSimplex hp) : toSimplex hp (encodedSimplexToCode hp s) = ↑s

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.encodedSimplexToCode_toSimplex {p : ℕ} (hp : Nat.Prime p) (z : Code p) : encodedSimplexToCode hp ⟨toSimplex hp z, ⋯⟩ = z

noncomputable def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.codeEquivEncodedSimplex {p : ℕ} (hp : Nat.Prime p) : Code p ≃ EncodedSimplex hp

Unconditional equivalence between codes and the image of the explicit stage construction.

Equations

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

def NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.EveryMaximalFlagEncoded {p : ℕ} (hp : Nat.Prime p) : Prop

The classification statement for Step 1: every maximal strict flag is encoded.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.EveryMaximalFlagEncoded hp = Function.Surjective (NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.toSimplex hp)

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

Recover a code from an arbitrary maximal flag once the classification theorem is available.

Equations

• NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.simplexToCodeOfSurjective hp hall s = Classical.choose ⋯

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.toSimplex_simplexToCodeOfSurjective {p : ℕ} (hp : Nat.Prime p) (hall : EveryMaximalFlagEncoded hp) (s : Simplex p (p - 1)) : toSimplex hp (simplexToCodeOfSurjective hp hall s) = s

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.MaximalFlagCode.simplexToCodeOfSurjective_toSimplex {p : ℕ} (hp : Nat.Prime p) (hall : EveryMaximalFlagEncoded hp) (z : Code p) : simplexToCodeOfSurjective hp hall (toSimplex hp z) = z

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

Equivalence with all maximal strict flags, conditional on the surjectivity/classification theorem.

Equations

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

theorem NRR.AAK.simplestRoute_maximalFlagEncoding_injective {p : ℕ} (hp : Nat.Prime p) : Function.Injective (FoxNeuwirthOrderComplex.MaximalFlagCode.toSimplex hp)

Step 1 is unconditional on the image of the explicit maximal-flag construction.