Proposition 3.1 over arbitrary finite fields

The definitions below name the concrete graph in the write-up: its vertices are the even partial flags in the recursively split (2k+1)-dimensional coordinate model FlagSpace K k, and adjacency means sharing a compatible odd partial flag. The degree is the cardinality of the neighbor set of the standard coordinate flag; transitivity then proves that this is the degree of every vertex.

proposition_3_1_over_finite_field packages the exact order formula, the sharp degree cap, regularity, and exact diameter for this one graph. The prime-power theorem is a genuine instance obtained from a finite field of the requested cardinality, rather than a separate prime-only construction.

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

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.Proposition31Vertex (K : Type u_1) [Field K] (k : ℕ) : Type u_1

The vertex type of the graph H_{k,K} in Proposition 3.1.

Equations

• MooreBound.DegreeDiameter.Proposition31Vertex K k = MooreBound.DegreeDiameter.EvenPartialFlag

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.Proposition31Graph (K : Type u_1) [Field K] (k : ℕ) : SimpleGraph (Proposition31Vertex K k)

The concrete halved flag graph H_{k,K}.

Equations

• MooreBound.DegreeDiameter.Proposition31Graph K k = MooreBound.DegreeDiameter.halvedFlagGraph

noncomputable def MooreBound.DegreeDiameter.proposition31Basis (K : Type u_1) [Field K] (k : ℕ) : Module.Basis (Fin (2 * k + 1)) K (FlagSpace K k)

A coordinate basis of the recursively split model.

Equations

• MooreBound.DegreeDiameter.proposition31Basis K k = Module.finBasisOfFinrankEq K (MooreBound.DegreeDiameter.FlagSpace K k) ⋯

noncomputable def MooreBound.DegreeDiameter.proposition31StandardEven (K : Type u_1) [Field K] (k : ℕ) : Proposition31Vertex K k

The standard vertex used to name the actual common degree.

Equations

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

noncomputable def MooreBound.DegreeDiameter.proposition31Degree (K : Type u_1) [Field K] (k : ℕ) : ℕ

The actual degree of H_{k,K}, measured at the standard coordinate flag. Regularity below proves that this is independent of the vertex.

Equations

• MooreBound.DegreeDiameter.proposition31Degree K k = Nat.card ↑((MooreBound.DegreeDiameter.Proposition31Graph K k).neighborSet (MooreBound.DegreeDiameter.proposition31StandardEven K k))

theorem MooreBound.DegreeDiameter.proposition31_regular (K : Type u_1) [Field K] (k : ℕ) (P : Proposition31Vertex K k) : Nat.card ↑((Proposition31Graph K k).neighborSet P) = proposition31Degree K k

All vertices of the concrete graph have its named actual degree.

theorem MooreBound.DegreeDiameter.proposition_3_1_over_finite_field (K : Type u_1) [Field K] [Finite K] (k : ℕ) (hk : 0 < k) : (∀ (P : Proposition31Vertex K k), Nat.card ↑((Proposition31Graph K k).neighborSet P) = proposition31Degree K k) ∧ Nat.card (Proposition31Vertex K k) * (Nat.card K + 1) ^ k = qFactorial (Nat.card K) (2 * k + 1) ∧ Nat.card (Proposition31Vertex K k) = qFactorial (Nat.card K) (2 * k + 1) / (Nat.card K + 1) ^ k ∧ proposition31Degree K k ≤ (Nat.card K + 1) ^ k * ((Nat.card K + 1) ^ k - 1) ∧ (Proposition31Graph K k).ediam = ↑k

Proposition 3.1 (finite-field form). For every finite field K and positive k, the same concrete graph is regular, has the exact q-factorial order in both multiplication and division form, obeys the paper's sharp degree cap, and has extended diameter exactly k.

theorem MooreBound.DegreeDiameter.proposition_3_1_for_prime_power (q : PrimePowerIndex) (k : ℕ) (hk : 0 < k) : (∀ (P : Proposition31Vertex (PrimePowerField q) k), Nat.card ↑((Proposition31Graph (PrimePowerField q) k).neighborSet P) = proposition31Degree (PrimePowerField q) k) ∧ Nat.card (Proposition31Vertex (PrimePowerField q) k) * (↑q + 1) ^ k = qFactorial (↑q) (2 * k + 1) ∧ Nat.card (Proposition31Vertex (PrimePowerField q) k) = qFactorial (↑q) (2 * k + 1) / (↑q + 1) ^ k ∧ proposition31Degree (PrimePowerField q) k ≤ (↑q + 1) ^ k * ((↑q + 1) ^ k - 1) ∧ (Proposition31Graph (PrimePowerField q) k).ediam = ↑k

Proposition 3.1 (prime-power form). Every prime power q supplies a finite field of cardinality exactly q, and hence the graph with exactly the numerical parameters stated in the write-up.