theorem GLnBuilding.existsUnique_step_jump {n : ℕ} (g : Fin (n + 1) → ℕ) (hmono : Monotone g) (hstep : ∀ (j : Fin n), g ⟨↑j + 1, ⋯⟩ ≤ g ⟨↑j, ⋯⟩ + 1) (htotal : g ⟨n, ⋯⟩ = g ⟨0, ⋯⟩ + 1) : ∃! j : Fin n, g ⟨↑j + 1, ⋯⟩ = g ⟨↑j, ⋯⟩ + 1

For any monotone $g : \{0, \dots, n\} \to \mathbb{N}$ with step increments $\le 1$ and total increase $g(n) = g(0) + 1$, there is a unique index $j$ where $g$ jumps by $1$.

theorem GLnBuilding.schreierCell_finrank_mono {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (i : Fin (n + 1)) (hi : 0 < ↑i) (j j' : Fin (n + 1)) (hjj' : j ≤ j') : Module.finrank k ↥(schreierCell σ τ i hi j) ≤ Module.finrank k ↥(schreierCell σ τ i hi j')

Monotonicity of the Schreier cell dimensions along the second index.

theorem GLnBuilding.existsUnique_jump_col {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : ∃! j : Fin n, Module.finrank k ↥(schreierCell σ τ i hi ⟨↑j + 1, ⋯⟩) = Module.finrank k ↥(schreierCell σ τ i hi ⟨↑j, ⋯⟩) + 1

For each row $i > 0$ of the Schreier refinement of $\sigma$ by $\tau$, there is a unique column $j$ where the dimension jumps from $\dim(\sigma_{i-1} + \sigma_i \cap \tau_j)$ to $\dim(\sigma_{i-1} + \sigma_i \cap \tau_{j+1})$ by exactly $1$.

noncomputable def GLnBuilding.jumpCol {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : Fin n

The Schreier refinement permutation: for each row $i$, jumpCol returns the unique column $j$ where the refinement increases in dimension, giving the bijection between the composition factors of $\sigma$ and those of $\tau$.

theorem GLnBuilding.jumpCol_spec {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : Module.finrank k ↥(schreierCell σ τ i hi ⟨↑(jumpCol σ τ hσ hτ i hi) + 1, ⋯⟩) = Module.finrank k ↥(schreierCell σ τ i hi ⟨↑(jumpCol σ τ hσ hτ i hi), ⋯⟩) + 1

Defining property: at column $j = $ jumpCol, the Schreier cell dimension jumps by exactly $1$.

theorem GLnBuilding.jumpCol_unique {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) (j : Fin n) (hj : Module.finrank k ↥(schreierCell σ τ i hi ⟨↑j + 1, ⋯⟩) = Module.finrank k ↥(schreierCell σ τ i hi ⟨↑j, ⋯⟩) + 1) : j = jumpCol σ τ hσ hτ i hi

Uniqueness: any column where the Schreier cell dimension jumps must equal jumpCol.

theorem GLnBuilding.schreierCell_lt_at_jumpCol {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : schreierCell σ τ i hi ⟨↑(jumpCol σ τ hσ hτ i hi), ⋯⟩ < schreierCell σ τ i hi ⟨↑(jumpCol σ τ hσ hτ i hi) + 1, ⋯⟩

At the jump column, the Schreier cell strictly increases.

theorem GLnBuilding.vi_inter_wj_not_le_vim1 {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : ¬σ.spaces i ⊓ τ.spaces ⟨↑(jumpCol σ τ hσ hτ i hi) + 1, ⋯⟩ ≤ σ.spaces ⟨↑i - 1, ⋯⟩

Key non-containment: $V_i \cap W_{j+1}$ is not contained in $V_{i-1}$ at the jump column $j$, ensuring existence of the Jordan-Hölder gap vector.

theorem GLnBuilding.exists_jhGapVector {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : ∃ v ∈ σ.spaces i ⊓ τ.spaces ⟨↑(jumpCol σ τ hσ hτ i hi) + 1, ⋯⟩, v ∉ σ.spaces ⟨↑i - 1, ⋯⟩

Existence of a Jordan-Hölder gap vector: a vector $v \in V_i \cap W_{j+1}$ with $v \notin V_{i-1}$.

noncomputable def GLnBuilding.jhGapVector {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : Vec k n

Choice of the Jordan-Hölder gap vector at row $i$: an explicit witness in $V_i \cap W_{j+1} \setminus V_{i-1}$ where $j$ is the jump column.

theorem GLnBuilding.jhGapVector_mem_inf {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : jhGapVector σ τ hσ hτ i hi ∈ σ.spaces i ⊓ τ.spaces ⟨↑(jumpCol σ τ hσ hτ i hi) + 1, ⋯⟩

The Jordan-Hölder gap vector lies in $V_i \cap W_{j+1}$.

theorem GLnBuilding.jhGapVector_not_mem_lower {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : jhGapVector σ τ hσ hτ i hi ∉ σ.spaces ⟨↑i - 1, ⋯⟩

The Jordan-Hölder gap vector does not lie in $V_{i-1}$.

theorem GLnBuilding.jhGapVector_mem_Vi {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : jhGapVector σ τ hσ hτ i hi ∈ σ.spaces i

The Jordan-Hölder gap vector lies in $V_i$.

theorem GLnBuilding.jhGapVector_mem_Wj {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : jhGapVector σ τ hσ hτ i hi ∈ τ.spaces ⟨↑(jumpCol σ τ hσ hτ i hi) + 1, ⋯⟩

The Jordan-Hölder gap vector lies in $W_{j+1}$, where $j$ is the jump column.

theorem GLnBuilding.jhGapVector_ne_zero {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : jhGapVector σ τ hσ hτ i hi ≠ 0

The Jordan-Hölder gap vector is nonzero.