Exact order of the halved flag graph

This file carries out the double count in Proposition 3.1. A complete flag is the same thing as an even partial flag together with a compatible odd partial flag. The equivalence is explicit, and the fibre over every even partial flag has the exact cardinality (q + 1)^k proved in CompletionCount. Combining that equality with the exact q-factorial enumeration of complete flags gives both the multiplication form and the division form of the paper's vertex-count formula.

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.CompatiblePartialFlagPair {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) : Type u_2

The dependent type of compatible even/odd partial-flag pairs.

Equations

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

noncomputable def MooreBound.DegreeDiameter.completeFlagEquivCompatiblePartialFlagPair {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) : CompleteFlag K V (2 * k + 1) ≃ CompatiblePartialFlagPair k

Splitting a complete flag into its parity parts is an equivalence onto the type of compatible pairs. This is the precise bijection used in the double count.

Equations

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

theorem MooreBound.DegreeDiameter.natCard_completeFlag_eq_evenPartialFlag_mul_completion {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] [Finite V] [FiniteDimensional K V] (k : ℕ) : Nat.card (CompleteFlag K V (2 * k + 1)) = Nat.card EvenPartialFlag * (Nat.card K + 1) ^ k

Exact double-counting identity before inserting the q-factorial formula: the number of complete flags is the number of even partial flags times the constant compatible-completion multiplicity.

theorem MooreBound.DegreeDiameter.natCard_evenPartialFlag_mul_completion_eq_qFactorial {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] [Finite V] [FiniteDimensional K V] (k : ℕ) (hV : Module.finrank K V = 2 * k + 1) : Nat.card EvenPartialFlag * (Nat.card K + 1) ^ k = qFactorial (Nat.card K) (2 * k + 1)

Equation (6) of the write-up in multiplication form. This form records the exact double count without relying on truncated natural-number division.

theorem MooreBound.DegreeDiameter.natCard_evenPartialFlag_eq_qFactorial_div {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] [Finite V] [FiniteDimensional K V] (k : ℕ) (hV : Module.finrank K V = 2 * k + 1) : Nat.card EvenPartialFlag = qFactorial (Nat.card K) (2 * k + 1) / (Nat.card K + 1) ^ k

Equation (6) of the write-up in its displayed division form.

theorem MooreBound.DegreeDiameter.natCard_flagSpaceEvenPartialFlag_eq_qFactorial_div {K : Type u_1} [Field K] [Finite K] (k : ℕ) : Nat.card EvenPartialFlag = qFactorial (Nat.card K) (2 * k + 1) / (Nat.card K + 1) ^ k

The same exact formula for the recursively split coordinate model used by the big-cell construction.