Exact counting of one-step refinements and parity completions

The interval between subspaces U ⊆ W whose ranks differ by two is equivalent to the projective line of W / U. We then prove that the choices in the k disjoint rank-two intervals of a parity partial flag are genuinely independent by constructing complete flags from arbitrary coordinate tuples. The resulting equivalences give the exact completion multiplicity (|K| + 1)^k; the neighbor-degree argument at the end deliberately remains an injection, since a graph neighbor need not have a unique common odd part.

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

structure MooreBound.DegreeDiameter.IntermediateSubspace {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (U W : Submodule K V) : Type u_2

Subspaces one rank above U and contained in W.

• space : Submodule K V

  The subspace between the fixed lower and upper endpoints.

• lower : U ≤ self.space
• upper : self.space ≤ W
• finrank_space : Module.finrank K ↥self.space = Module.finrank K ↥U + 1

theorem MooreBound.DegreeDiameter.IntermediateSubspace.ext {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {U W : Submodule K V} {L L' : IntermediateSubspace U W} (h : L.space = L'.space) : L = L'

theorem MooreBound.DegreeDiameter.IntermediateSubspace.ext_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {U W : Submodule K V} {L L' : IntermediateSubspace U W} : L = L' ↔ L.space = L'.space

instance MooreBound.DegreeDiameter.IntermediateSubspace.instFinite {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {U W : Submodule K V} [Finite V] : Finite (IntermediateSubspace U W)

theorem MooreBound.DegreeDiameter.finrank_map_mkQ_add {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U L : Submodule K V} (hUL : U ≤ L) : Module.finrank K ↥(Submodule.map U.mkQ L) + Module.finrank K ↥U = Module.finrank K ↥L

Rank-nullity for the image of L in the quotient by a contained U.

noncomputable def MooreBound.DegreeDiameter.intermediatePoint {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U W : Submodule K V} (_hUW : U ≤ W) (_hW : Module.finrank K ↥W = Module.finrank K ↥U + 2) (L : IntermediateSubspace U W) : Projectivization K ↥(Submodule.map U.mkQ W)

The image of an intermediate subspace in W / U, regarded as a one-dimensional subspace of the two-dimensional image of W.

Equations

• MooreBound.DegreeDiameter.intermediatePoint _hUW _hW L = Projectivization.mk'' (Submodule.comap (Submodule.map U.mkQ W).subtype (Submodule.map U.mkQ L.space)) ⋯

theorem MooreBound.DegreeDiameter.intermediatePoint_injective {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U W : Submodule K V} (hUW : U ≤ W) (hW : Module.finrank K ↥W = Module.finrank K ↥U + 2) : Function.Injective (intermediatePoint hUW hW)

noncomputable def MooreBound.DegreeDiameter.intermediateSubspaceOfPoint {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U W : Submodule K V} (hUW : U ≤ W) (p : Projectivization K ↥(Submodule.map U.mkQ W)) : IntermediateSubspace U W

Pull a projective point in W / U back to the unique intermediate subspace of V. This explicit pullback is inverse to intermediatePoint.

Equations

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

theorem MooreBound.DegreeDiameter.intermediatePoint_surjective {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U W : Submodule K V} (hUW : U ≤ W) (hW : Module.finrank K ↥W = Module.finrank K ↥U + 2) : Function.Surjective (intermediatePoint hUW hW)

The quotient-image construction and pullback construction are inverse: rank-two subspace intervals are exactly projective lines.

noncomputable def MooreBound.DegreeDiameter.intermediateSubspaceEquivProjectiveLine {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {U W : Submodule K V} (hUW : U ≤ W) (hW : Module.finrank K ↥W = Module.finrank K ↥U + 2) : IntermediateSubspace U W ≃ Projectivization K ↥(Submodule.map U.mkQ W)

The genuine bijection between a rank-two interval and its projective line.

Equations

• MooreBound.DegreeDiameter.intermediateSubspaceEquivProjectiveLine hUW hW = Equiv.ofBijective (MooreBound.DegreeDiameter.intermediatePoint hUW hW) ⋯

theorem MooreBound.DegreeDiameter.natCard_intermediate_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite K] [Finite V] {U W : Submodule K V} (hUW : U ≤ W) (hW : Module.finrank K ↥W = Module.finrank K ↥U + 2) : Nat.card (IntermediateSubspace U W) = Nat.card K + 1

Exactly |K| + 1 subspaces occur in a rank-two interval.

theorem MooreBound.DegreeDiameter.natCard_intermediate_le {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite K] [Finite V] {U W : Submodule K V} (hUW : U ≤ W) (hW : Module.finrank K ↥W = Module.finrank K ↥U + 2) : Nat.card (IntermediateSubspace U W) ≤ Nat.card K + 1

There are at most |K| + 1 possible intermediate subspaces.

def MooreBound.DegreeDiameter.evenLowerRank (k : ℕ) (j : Fin k) : Fin (2 * k + 1 + 1)

Consecutive retained even ranks surrounding the j-th missing odd rank.

Equations

• MooreBound.DegreeDiameter.evenLowerRank k j = ⟨2 * ↑j, ⋯⟩

def MooreBound.DegreeDiameter.oddMiddleRank (k : ℕ) (j : Fin k) : Fin (2 * k + 1 + 1)

The missing odd rank 2j+1 between consecutive retained even ranks.

Equations

• MooreBound.DegreeDiameter.oddMiddleRank k j = ⟨2 * ↑j + 1, ⋯⟩

def MooreBound.DegreeDiameter.evenUpperRank (k : ℕ) (j : Fin k) : Fin (2 * k + 1 + 1)

The upper even rank 2j+2 surrounding a missing odd rank.

Equations

• MooreBound.DegreeDiameter.evenUpperRank k j = ⟨2 * ↑j + 2, ⋯⟩

def MooreBound.DegreeDiameter.oddLowerRank (k : ℕ) (j : Fin k) : Fin (2 * k + 1 + 1)

Consecutive retained odd ranks surrounding the j-th missing positive even rank.

Equations

• MooreBound.DegreeDiameter.oddLowerRank k j = ⟨2 * ↑j + 1, ⋯⟩

def MooreBound.DegreeDiameter.evenMiddleRank (k : ℕ) (j : Fin k) : Fin (2 * k + 1 + 1)

The missing even rank 2j+2 between consecutive retained odd ranks.

Equations

• MooreBound.DegreeDiameter.evenMiddleRank k j = ⟨2 * ↑j + 2, ⋯⟩

def MooreBound.DegreeDiameter.oddUpperRank (k : ℕ) (j : Fin k) : Fin (2 * k + 1 + 1)

The upper odd rank 2j+3 surrounding a missing even rank.

Equations

• MooreBound.DegreeDiameter.oddUpperRank k j = ⟨2 * ↑j + 3, ⋯⟩

@[simp]

theorem MooreBound.DegreeDiameter.evenLowerRank_val (k : ℕ) (j : Fin k) : ↑(evenLowerRank k j) = 2 * ↑j

@[simp]

theorem MooreBound.DegreeDiameter.oddMiddleRank_val (k : ℕ) (j : Fin k) : ↑(oddMiddleRank k j) = 2 * ↑j + 1

@[simp]

theorem MooreBound.DegreeDiameter.evenUpperRank_val (k : ℕ) (j : Fin k) : ↑(evenUpperRank k j) = 2 * ↑j + 2

@[simp]

theorem MooreBound.DegreeDiameter.oddLowerRank_val (k : ℕ) (j : Fin k) : ↑(oddLowerRank k j) = 2 * ↑j + 1

@[simp]

theorem MooreBound.DegreeDiameter.evenMiddleRank_val (k : ℕ) (j : Fin k) : ↑(evenMiddleRank k j) = 2 * ↑j + 2

@[simp]

theorem MooreBound.DegreeDiameter.oddUpperRank_val (k : ℕ) (j : Fin k) : ↑(oddUpperRank k j) = 2 * ↑j + 3

theorem MooreBound.DegreeDiameter.ofComplete_space_eq_of_mod {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n parity : ℕ} {F : CompleteFlag K V n} {P : PartialFlag parity} (h : PartialFlag.ofComplete parity F = P) (i : Fin (n + 1)) (hi : ↑i % 2 = parity % 2) : F.space i = ↑P i

theorem MooreBound.DegreeDiameter.partialFlag_space_eq_bot_of_mod_ne {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n parity : ℕ} (P : PartialFlag parity) (i : Fin (n + 1)) (hi : ↑i % 2 ≠ parity % 2) : ↑P i = ⊥

A represented partial flag is bottom at every erased rank.

theorem MooreBound.DegreeDiameter.partialFlag_finrank_space_of_mod {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n parity : ℕ} (P : PartialFlag parity) (i : Fin (n + 1)) (hi : ↑i % 2 = parity % 2) : Module.finrank K ↥(↑P i) = ↑i

At every retained rank a partial flag has the prescribed dimension.

theorem MooreBound.DegreeDiameter.finrank_eq_of_partialFlag {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n parity : ℕ} (P : PartialFlag parity) : Module.finrank K V = n

The existence of a partial flag already fixes the dimension of the ambient space.

def MooreBound.DegreeDiameter.completeFlagOfRankedSpaces {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} (S : Fin (n + 1) → Submodule K V) (hrank : ∀ (i : Fin (n + 1)), Module.finrank K ↥(S i) = ↑i) (hstep : ∀ (i : Fin n), S i.castSucc ≤ S i.succ) (hzero : S 0 = ⊥) (hlast : S (Fin.last n) = ⊤) : CompleteFlag K V n

Package a ranked adjacent chain as a complete flag. Strictness follows from adjacent containment together with the one-rank dimension increase.

Equations

• MooreBound.DegreeDiameter.completeFlagOfRankedSpaces S hrank hstep hzero hlast = { space := S, strictMono_space := ⋯, finrank_space := hrank, space_zero := hzero, space_last := hlast }

@[simp]

theorem MooreBound.DegreeDiameter.completeFlagOfRankedSpaces_apply {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {n : ℕ} (S : Fin (n + 1) → Submodule K V) (hrank : ∀ (i : Fin (n + 1)), Module.finrank K ↥(S i) = ↑i) (hstep : ∀ (i : Fin n), S i.castSucc ≤ S i.succ) (hzero : S 0 = ⊥) (hlast : S (Fin.last n) = ⊤) (i : Fin (n + 1)) : (completeFlagOfRankedSpaces S hrank hstep hzero hlast).space i = S i

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.EvenCompletionCoordinates {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) : Type u_2

The product of the k projective-line intervals in which an even partial flag can be completed.

Equations

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

noncomputable def MooreBound.DegreeDiameter.completeOfEvenCompatibility {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (x : { Q : OddPartialFlag // Compatible P Q }) : CompleteFlag K V (2 * k + 1)

The common complete flag selected from a compatible pair. Its uniqueness was proved in compatible_unique; choice is used only to define the counting injection.

Equations

• MooreBound.DegreeDiameter.completeOfEvenCompatibility k P x = Classical.choose ⋯

theorem MooreBound.DegreeDiameter.completeOfEvenCompatibility_even {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (x : { Q : OddPartialFlag // Compatible P Q }) : PartialFlag.ofComplete 0 (completeOfEvenCompatibility k P x) = P

theorem MooreBound.DegreeDiameter.completeOfEvenCompatibility_odd {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (x : { Q : OddPartialFlag // Compatible P Q }) : PartialFlag.ofComplete 1 (completeOfEvenCompatibility k P x) = ↑x

noncomputable def MooreBound.DegreeDiameter.evenCompletionCoordinates {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) : { Q : OddPartialFlag // Compatible P Q } → EvenCompletionCoordinates k P

Extract each intermediate subspace from a compatible odd partial flag.

Equations

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

@[simp]

theorem MooreBound.DegreeDiameter.evenCompletionCoordinates_space {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (x : { Q : OddPartialFlag // Compatible P Q }) (j : Fin k) : (evenCompletionCoordinates k P x j).space = (completeOfEvenCompatibility k P x).space (oddMiddleRank k j)

theorem MooreBound.DegreeDiameter.evenCompletionCoordinates_injective {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) : Function.Injective (evenCompletionCoordinates k P)

theorem MooreBound.DegreeDiameter.evenBoundary_le {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (j : Fin k) : ↑P (evenLowerRank k j) ≤ ↑P (evenUpperRank k j)

theorem MooreBound.DegreeDiameter.evenBoundary_finrank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (j : Fin k) : Module.finrank K ↥(↑P (evenUpperRank k j)) = Module.finrank K ↥(↑P (evenLowerRank k j)) + 2

def MooreBound.DegreeDiameter.evenCompletedSpace {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (c : EvenCompletionCoordinates k P) : Fin (2 * k + 1 + 1) → Submodule K V

Interleave arbitrary rank-one choices in the rank-two intervals of an even partial flag; the final odd rank is the ambient top space.

Equations

• MooreBound.DegreeDiameter.evenCompletedSpace k P c i = if hi : ↑i % 2 = 0 then ↑P i else if _hlast : ↑i = 2 * k + 1 then ⊤ else (c ⟨↑i / 2, ⋯⟩).space

@[simp]

theorem MooreBound.DegreeDiameter.evenCompletedSpace_of_even {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (c : EvenCompletionCoordinates k P) (i : Fin (2 * k + 1 + 1)) (hi : ↑i % 2 = 0) : evenCompletedSpace k P c i = ↑P i

@[simp]

theorem MooreBound.DegreeDiameter.evenCompletedSpace_oddMiddle {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (c : EvenCompletionCoordinates k P) (j : Fin k) : evenCompletedSpace k P c (oddMiddleRank k j) = (c j).space

@[simp]

theorem MooreBound.DegreeDiameter.evenCompletedSpace_last {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (c : EvenCompletionCoordinates k P) : evenCompletedSpace k P c (Fin.last (2 * k + 1)) = ⊤

noncomputable def MooreBound.DegreeDiameter.completeFlagOfEvenCoordinates {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (c : EvenCompletionCoordinates k P) : CompleteFlag K V (2 * k + 1)

Every coordinate tuple over an even partial flag assembles into a complete flag. This is the formal independence assertion for the missing odd ranks.

Equations

• MooreBound.DegreeDiameter.completeFlagOfEvenCoordinates k P c = MooreBound.DegreeDiameter.completeFlagOfRankedSpaces (MooreBound.DegreeDiameter.evenCompletedSpace k P c) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem MooreBound.DegreeDiameter.completeFlagOfEvenCoordinates_apply {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (c : EvenCompletionCoordinates k P) (i : Fin (2 * k + 1 + 1)) : (completeFlagOfEvenCoordinates k P c).space i = evenCompletedSpace k P c i

theorem MooreBound.DegreeDiameter.completeFlagOfEvenCoordinates_evenPart {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (c : EvenCompletionCoordinates k P) : PartialFlag.ofComplete 0 (completeFlagOfEvenCoordinates k P c) = P

noncomputable def MooreBound.DegreeDiameter.oddCompatibleOfEvenCoordinates {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) (c : EvenCompletionCoordinates k P) : { Q : OddPartialFlag // Compatible P Q }

The compatible odd part assembled from an arbitrary coordinate tuple.

Equations

• MooreBound.DegreeDiameter.oddCompatibleOfEvenCoordinates k P c = ⟨MooreBound.DegreeDiameter.PartialFlag.ofComplete 1 (MooreBound.DegreeDiameter.completeFlagOfEvenCoordinates k P c), ⋯⟩

theorem MooreBound.DegreeDiameter.evenCompletionCoordinates_rightInverse {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) : Function.RightInverse (oddCompatibleOfEvenCoordinates k P) (evenCompletionCoordinates k P)

noncomputable def MooreBound.DegreeDiameter.evenCompletionEquiv {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) : { Q : OddPartialFlag // Compatible P Q } ≃ EvenCompletionCoordinates k P

Compatible odd parts are exactly independent products of the k rank-two intervals.

Equations

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

theorem MooreBound.DegreeDiameter.natCard_odd_compatible_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite K] [Finite V] (k : ℕ) (P : EvenPartialFlag) : Nat.card { Q : OddPartialFlag // Compatible P Q } = (Nat.card K + 1) ^ k

An even partial flag has exactly (q+1)^k compatible odd parts.

theorem MooreBound.DegreeDiameter.natCard_odd_compatible_le {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite K] [Finite V] (k : ℕ) (P : EvenPartialFlag) : Nat.card { Q : OddPartialFlag // Compatible P Q } ≤ (Nat.card K + 1) ^ k

The upper bound as a direct corollary of the exact completion count.

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.OddCompletionCoordinates {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) : Type u_2

Independent intermediate-subspace choices that complete an odd partial flag.

Equations

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

noncomputable def MooreBound.DegreeDiameter.completeOfOddCompatibility {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (x : { P : EvenPartialFlag // Compatible P Q }) : CompleteFlag K V (2 * k + 1)

Choose the complete flag witnessing compatibility with the given odd partial flag.

Equations

• MooreBound.DegreeDiameter.completeOfOddCompatibility k Q x = Classical.choose ⋯

theorem MooreBound.DegreeDiameter.completeOfOddCompatibility_even {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (x : { P : EvenPartialFlag // Compatible P Q }) : PartialFlag.ofComplete 0 (completeOfOddCompatibility k Q x) = ↑x

theorem MooreBound.DegreeDiameter.completeOfOddCompatibility_odd {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (x : { P : EvenPartialFlag // Compatible P Q }) : PartialFlag.ofComplete 1 (completeOfOddCompatibility k Q x) = Q

noncomputable def MooreBound.DegreeDiameter.oddCompletionCoordinates {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) : { P : EvenPartialFlag // Compatible P Q } → OddCompletionCoordinates k Q

Extract each intermediate subspace from a compatible even partial flag.

Equations

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

@[simp]

theorem MooreBound.DegreeDiameter.oddCompletionCoordinates_space {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (x : { P : EvenPartialFlag // Compatible P Q }) (j : Fin k) : (oddCompletionCoordinates k Q x j).space = (completeOfOddCompatibility k Q x).space (evenMiddleRank k j)

theorem MooreBound.DegreeDiameter.oddCompletionCoordinates_injective {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) : Function.Injective (oddCompletionCoordinates k Q)

theorem MooreBound.DegreeDiameter.oddBoundary_le {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (j : Fin k) : ↑Q (oddLowerRank k j) ≤ ↑Q (oddUpperRank k j)

theorem MooreBound.DegreeDiameter.oddBoundary_finrank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (j : Fin k) : Module.finrank K ↥(↑Q (oddUpperRank k j)) = Module.finrank K ↥(↑Q (oddLowerRank k j)) + 2

def MooreBound.DegreeDiameter.oddCompletedSpace {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (c : OddCompletionCoordinates k Q) : Fin (2 * k + 1 + 1) → Submodule K V

Interleave arbitrary positive-even-rank choices in the rank-two intervals of an odd partial flag; rank zero is the bottom space.

Equations

• MooreBound.DegreeDiameter.oddCompletedSpace k Q c i = if hi : ↑i % 2 = 1 then ↑Q i else if _hzero : ↑i = 0 then ⊥ else (c ⟨↑i / 2 - 1, ⋯⟩).space

@[simp]

theorem MooreBound.DegreeDiameter.oddCompletedSpace_of_odd {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (c : OddCompletionCoordinates k Q) (i : Fin (2 * k + 1 + 1)) (hi : ↑i % 2 = 1) : oddCompletedSpace k Q c i = ↑Q i

@[simp]

theorem MooreBound.DegreeDiameter.oddCompletedSpace_evenMiddle {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (c : OddCompletionCoordinates k Q) (j : Fin k) : oddCompletedSpace k Q c (evenMiddleRank k j) = (c j).space

@[simp]

theorem MooreBound.DegreeDiameter.oddCompletedSpace_zero {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (c : OddCompletionCoordinates k Q) : oddCompletedSpace k Q c 0 = ⊥

noncomputable def MooreBound.DegreeDiameter.completeFlagOfOddCoordinates {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (c : OddCompletionCoordinates k Q) : CompleteFlag K V (2 * k + 1)

Every coordinate tuple over an odd partial flag assembles into a complete flag. This is the dual formal independence assertion.

Equations

• MooreBound.DegreeDiameter.completeFlagOfOddCoordinates k Q c = MooreBound.DegreeDiameter.completeFlagOfRankedSpaces (MooreBound.DegreeDiameter.oddCompletedSpace k Q c) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem MooreBound.DegreeDiameter.completeFlagOfOddCoordinates_apply {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (c : OddCompletionCoordinates k Q) (i : Fin (2 * k + 1 + 1)) : (completeFlagOfOddCoordinates k Q c).space i = oddCompletedSpace k Q c i

theorem MooreBound.DegreeDiameter.completeFlagOfOddCoordinates_oddPart {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (c : OddCompletionCoordinates k Q) : PartialFlag.ofComplete 1 (completeFlagOfOddCoordinates k Q c) = Q

noncomputable def MooreBound.DegreeDiameter.evenCompatibleOfOddCoordinates {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) (c : OddCompletionCoordinates k Q) : { P : EvenPartialFlag // Compatible P Q }

The compatible even part assembled from an arbitrary coordinate tuple.

Equations

• MooreBound.DegreeDiameter.evenCompatibleOfOddCoordinates k Q c = ⟨MooreBound.DegreeDiameter.PartialFlag.ofComplete 0 (MooreBound.DegreeDiameter.completeFlagOfOddCoordinates k Q c), ⋯⟩

theorem MooreBound.DegreeDiameter.oddCompletionCoordinates_rightInverse {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) : Function.RightInverse (evenCompatibleOfOddCoordinates k Q) (oddCompletionCoordinates k Q)

noncomputable def MooreBound.DegreeDiameter.oddCompletionEquiv {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (Q : OddPartialFlag) : { P : EvenPartialFlag // Compatible P Q } ≃ OddCompletionCoordinates k Q

Compatible even parts are exactly independent products of the k rank-two intervals.

Equations

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

theorem MooreBound.DegreeDiameter.natCard_even_compatible_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite K] [Finite V] (k : ℕ) (Q : OddPartialFlag) : Nat.card { P : EvenPartialFlag // Compatible P Q } = (Nat.card K + 1) ^ k

An odd partial flag has exactly (q+1)^k compatible even parts.

theorem MooreBound.DegreeDiameter.natCard_even_compatible_le {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite K] [Finite V] (k : ℕ) (Q : OddPartialFlag) : Nat.card { P : EvenPartialFlag // Compatible P Q } ≤ (Nat.card K + 1) ^ k

The dual upper bound as a direct corollary of the exact completion count.

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.NeighborEncoding {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) : Type u_2

A neighbor is encoded by a compatible odd part and then by an even part compatible with that odd part. We deliberately keep all such pairs, rather than assuming that a neighbor has a unique common odd part.

Equations

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

noncomputable def MooreBound.DegreeDiameter.encodeNeighbor {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) : ↑(halvedFlagGraph.neighborSet P) → NeighborEncoding k P

Encode a graph neighbor by a shared odd flag and a distinct compatible even flag.

Equations

• MooreBound.DegreeDiameter.encodeNeighbor k P P' = ⟨⟨Classical.choose ⋯, ⋯⟩, ⟨↑P', ⋯⟩⟩

theorem MooreBound.DegreeDiameter.encodeNeighbor_injective {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (k : ℕ) (P : EvenPartialFlag) : Function.Injective (encodeNeighbor k P)

theorem MooreBound.DegreeDiameter.halvedFlagGraph_natCard_neighborSet_le_sharp {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite K] [Finite V] (k : ℕ) (P : EvenPartialFlag) : Nat.card ↑(halvedFlagGraph.neighborSet P) ≤ (Nat.card K + 1) ^ k * ((Nat.card K + 1) ^ k - 1)

The paper's neighbor-set cap A(A-1), where A = (q+1)^k. It does not count a neighbor twice or posit uniqueness of its common odd flag: the injection chooses one witness, and its second coordinate excludes the original vertex from the at-most-A compatible even parts.

theorem MooreBound.DegreeDiameter.halvedFlagGraph_natCard_neighborSet_le {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite K] [Finite V] (k : ℕ) (P : EvenPartialFlag) : Nat.card ↑(halvedFlagGraph.neighborSet P) ≤ (Nat.card K + 1) ^ k * (Nat.card K + 1) ^ k

The coarser square cap retained as a convenient corollary.

theorem MooreBound.DegreeDiameter.halvedFlagGraph_degree_le {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite K] [Finite V] (k : ℕ) (P : EvenPartialFlag) [Fintype ↑(halvedFlagGraph.neighborSet P)] : halvedFlagGraph.degree P ≤ (Nat.card K + 1) ^ k * (Nat.card K + 1) ^ k