The rank-potential lower bound for the halved flag graph

This file follows the reverse inequality in the diameter paragraph of Proposition 3.1. Relative to a fixed nonzero vector e, evenEntryBlock records the first retained even rank containing e (with k + 1 as the sentinel when no retained even rank contains it). The paper's potential is exactly 2 * (evenEntryBlock - 1).

Compatibility with one odd partial flag lets the entry block move by at most one. The standard and reverse basis flags have entry blocks 1 and k + 1; hence every walk between them has at least k edges. Combined with the odd--even route upper bound, this proves exact extended diameter k.

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.evenRank (k j : ℕ) (hj : j ≤ k) : Fin (2 * k + 1 + 1)

The retained even rank 2*j in dimension 2*k+1.

Equations

• MooreBound.DegreeDiameter.evenRank k j hj = ⟨2 * j, ⋯⟩

def MooreBound.DegreeDiameter.EvenEntryCandidate {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (P : EvenPartialFlag) (j : ℕ) : Prop

A candidate entry block: either a positive retained even rank containing e, or the sentinel k+1.

Equations

• MooreBound.DegreeDiameter.EvenEntryCandidate k e P j = ((1 ≤ j ∧ ∃ (hj : j ≤ k), e ∈ ↑P (MooreBound.DegreeDiameter.evenRank k j hj)) ∨ j = k + 1)

theorem MooreBound.DegreeDiameter.exists_evenEntryCandidate {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (P : EvenPartialFlag) : ∃ (j : ℕ), EvenEntryCandidate k e P j

noncomputable def MooreBound.DegreeDiameter.evenEntryBlock {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (P : EvenPartialFlag) : ℕ

The first positive retained even rank containing e, numbered in blocks; the value is k+1 if no retained even rank contains e.

Equations

• MooreBound.DegreeDiameter.evenEntryBlock k e P = Nat.find ⋯

theorem MooreBound.DegreeDiameter.evenEntryBlock_spec {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (P : EvenPartialFlag) : EvenEntryCandidate k e P (evenEntryBlock k e P)

theorem MooreBound.DegreeDiameter.one_le_evenEntryBlock {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (P : EvenPartialFlag) : 1 ≤ evenEntryBlock k e P

theorem MooreBound.DegreeDiameter.evenEntryBlock_le_sentinel {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (P : EvenPartialFlag) : evenEntryBlock k e P ≤ k + 1

theorem MooreBound.DegreeDiameter.evenEntryBlock_le_of_mem {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (P : EvenPartialFlag) (j : ℕ) (hj1 : 1 ≤ j) (hjk : j ≤ k) (hmem : e ∈ ↑P (evenRank k j hjk)) : evenEntryBlock k e P ≤ j

theorem MooreBound.DegreeDiameter.evenEntryBlock_mem {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (P : EvenPartialFlag) (hblock : evenEntryBlock k e P ≤ k) : e ∈ ↑P (evenRank k (evenEntryBlock k e P) hblock)

theorem MooreBound.DegreeDiameter.evenEntryBlock_ofComplete_le_of_mem {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (F : CompleteFlag K V (2 * k + 1)) (j : ℕ) (hj1 : 1 ≤ j) (hjk : j ≤ k) (hmem : e ∈ F.space (evenRank k j hjk)) : evenEntryBlock k e (PartialFlag.ofComplete 0 F) ≤ j

theorem MooreBound.DegreeDiameter.evenEntryBlock_le_add_one_of_common_compatible {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) {P P' : EvenPartialFlag} {Q : OddPartialFlag} (hPQ : Compatible P Q) (hP'Q : Compatible P' Q) : evenEntryBlock k e P' ≤ evenEntryBlock k e P + 1

Compatibility with a common odd partial flag makes the first even entry block move by at most one. This is the paper's rank-potential estimate.

theorem MooreBound.DegreeDiameter.evenEntryBlock_adjacent {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) {P P' : EvenPartialFlag} (h : halvedFlagGraph.Adj P P') : evenEntryBlock k e P' ≤ evenEntryBlock k e P + 1

noncomputable def MooreBound.DegreeDiameter.rankPotential {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) (P : EvenPartialFlag) : ℕ

The rank potential lambda from the paper.

Equations

• MooreBound.DegreeDiameter.rankPotential k e P = 2 * (MooreBound.DegreeDiameter.evenEntryBlock k e P - 1)

theorem MooreBound.DegreeDiameter.rankPotential_dist_adjacent {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) {P P' : EvenPartialFlag} (h : halvedFlagGraph.Adj P P') : (rankPotential k e P).dist (rankPotential k e P') ≤ 2

Adjacent vertices have paper-potential values differing by at most two.

theorem MooreBound.DegreeDiameter.evenEntryBlock_walk_le {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) {P P' : EvenPartialFlag} (p : halvedFlagGraph.Walk P P') : evenEntryBlock k e P' ≤ evenEntryBlock k e P + p.length

Along a walk, the entry block changes by no more than its length.

theorem MooreBound.DegreeDiameter.rankPotential_walk_le {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (e : V) {P P' : EvenPartialFlag} (p : halvedFlagGraph.Walk P P') : rankPotential k e P' ≤ rankPotential k e P + 2 * p.length

The rank potential can increase by at most two per edge along a walk.

theorem MooreBound.DegreeDiameter.evenEntryBlock_standard_basis {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin (2 * k + 1)) K V) : evenEntryBlock k (b 0) (PartialFlag.ofComplete 0 (CompleteFlag.ofBasis b)) = 1

theorem MooreBound.DegreeDiameter.evenEntryBlock_opposite_basis {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (b : Module.Basis (Fin (2 * k + 1)) K V) : evenEntryBlock k (b 0) (PartialFlag.ofComplete 0 (CompleteFlag.ofBasis (b.reindex Fin.revPerm))) = k + 1

theorem MooreBound.DegreeDiameter.rankPotential_standard_basis {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin (2 * k + 1)) K V) : rankPotential k (b 0) (PartialFlag.ofComplete 0 (CompleteFlag.ofBasis b)) = 0

theorem MooreBound.DegreeDiameter.rankPotential_opposite_basis {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (b : Module.Basis (Fin (2 * k + 1)) K V) : rankPotential k (b 0) (PartialFlag.ofComplete 0 (CompleteFlag.ofBasis (b.reindex Fin.revPerm))) = 2 * k

theorem MooreBound.DegreeDiameter.standard_to_opposite_walk_length {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin (2 * k + 1)) K V) (p : halvedFlagGraph.Walk (PartialFlag.ofComplete 0 (CompleteFlag.ofBasis b)) (PartialFlag.ofComplete 0 (CompleteFlag.ofBasis (b.reindex Fin.revPerm)))) : k ≤ p.length

Every walk from the standard flag to the opposite flag has at least k edges, exactly as in the potential argument in Proposition 3.1.

theorem MooreBound.DegreeDiameter.halvedFlagGraph_ediam_ge_ofBasis {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin (2 * k + 1)) K V) : ↑k ≤ halvedFlagGraph.ediam

The reverse inequality k ≤ ediam, witnessed by the standard and opposite complete flags and proved with the paper's rank potential.

theorem MooreBound.DegreeDiameter.halvedFlagGraph_ediam_eq_ofBasis {K : Type u_1} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin (2 * k + 1)) K V) : halvedFlagGraph.ediam = ↑k

The exact diameter assertion diam H_{k,q}=k from Proposition 3.1, in extended-diameter form.

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.CoordinateFlagSpace (K : Type u_2) (k : ℕ) : Type u_2

The coordinate space used for the concrete graph H_{k,q}.

Equations

• MooreBound.DegreeDiameter.CoordinateFlagSpace K k = (Fin (2 * k + 1) → K)

noncomputable def MooreBound.DegreeDiameter.coordinateBasis {K : Type u_1} [DivisionRing K] (k : ℕ) : Module.Basis (Fin (2 * k + 1)) K (CoordinateFlagSpace K k)

The standard coordinate basis e₁,...,eₜ.

Equations

• MooreBound.DegreeDiameter.coordinateBasis k = Pi.basisFun K (Fin (2 * k + 1))

noncomputable def MooreBound.DegreeDiameter.firstCoordinate {K : Type u_1} [DivisionRing K] (k : ℕ) : CoordinateFlagSpace K k

The vector called e₁ in the paper.

Equations

• MooreBound.DegreeDiameter.firstCoordinate k = (MooreBound.DegreeDiameter.coordinateBasis k) 0

noncomputable def MooreBound.DegreeDiameter.standardEvenFlag {K : Type u_1} [DivisionRing K] (k : ℕ) : EvenPartialFlag

The even part of the standard complete flag A.

Equations

• MooreBound.DegreeDiameter.standardEvenFlag k = MooreBound.DegreeDiameter.PartialFlag.ofComplete 0 (MooreBound.DegreeDiameter.CompleteFlag.ofBasis (MooreBound.DegreeDiameter.coordinateBasis k))

noncomputable def MooreBound.DegreeDiameter.oppositeEvenFlag {K : Type u_1} [DivisionRing K] (k : ℕ) : EvenPartialFlag

The even part of the reverse-coordinate complete flag C.

Equations

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

theorem MooreBound.DegreeDiameter.coordinate_halvedFlagGraph_ediam_eq {K : Type u_1} [DivisionRing K] (k : ℕ) (hk : 1 ≤ k) : halvedFlagGraph.ediam = ↑k