Alternating routes between complete flags

This file proves Lemma 2.1 in the same three visible stages as the paper:

1. invoke the separately proved common-basis theorem from CommonBasis.lean;
2. apply the separately proved n-round odd--even transposition route;
3. take prefix spans and verify that only ranks of the active parity change.

Indices are zero based in Lean: rank i is space i, while paper step s + 1 has Lean index s.

Lean Pool port of wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022. The port adds a namespace and adapts proofs to the current Mathlib APIs and repository style.

def MooreBound.DegreeDiameter.OrderingStep {n : ℕ} (s : Fin n) (σ τ : Equiv.Perm (Fin n)) : Prop

A purely combinatorial alternating layer. At layer s + 1, all prefix sets of parity opposite to s + 1 are unchanged.

Equations

• MooreBound.DegreeDiameter.OrderingStep s σ τ = ∀ (i : Fin (n + 1)), ↑i % 2 ≠ (↑s + 1) % 2 → MooreBound.DegreeDiameter.PrefixSet σ i = MooreBound.DegreeDiameter.PrefixSet τ i

theorem MooreBound.DegreeDiameter.oddEvenRoute {n : ℕ} (π : Equiv.Perm (Fin n)) : ∃ (route : Fin (n + 1) → Equiv.Perm (Fin n)), route 0 = 1 ∧ route (Fin.last n) = π ∧ ∀ (s : Fin n), OrderingStep s (route s.castSucc) (route s.succ)

Odd--even transposition routing, stated independently of linear algebra.

theorem MooreBound.DegreeDiameter.ofBasis_reindex_eq_at_of_prefixSet_eq (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (b : Module.Basis (Fin n) K V) {σ τ : Equiv.Perm (Fin n)} {i : Fin (n + 1)} (h : PrefixSet σ i = PrefixSet τ i) : (CompleteFlag.ofBasis (b.reindex (Equiv.symm σ))).space i = (CompleteFlag.ofBasis (b.reindex (Equiv.symm τ))).space i

def MooreBound.DegreeDiameter.AlternatingStep (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (s : Fin n) (F G : CompleteFlag K V n) : Prop

Step s + 1 may change only ranks with the same parity as s + 1. Equivalently, every rank of the other parity is frozen.

Equations

• MooreBound.DegreeDiameter.AlternatingStep K V s F G = ∀ (i : Fin (n + 1)), ↑i % 2 ≠ (↑s + 1) % 2 → F.space i = G.space i

theorem MooreBound.DegreeDiameter.alternating_route (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} (F F' : CompleteFlag K V n) : ∃ (route : Fin (n + 1) → CompleteFlag K V n), route 0 = F ∧ route (Fin.last n) = F' ∧ ∀ (s : Fin n), AlternatingStep K V s (route s.castSucc) (route s.succ)

Exact statement of Lemma 2.1: route 0 = F, route n = F', and the transition from route s to route (s+1) changes only ranks of the parity prescribed by the one-based step number s+1.