Generic finite-graph framework for the degree--diameter preprint

This file contains only generic graph definitions and lemmas. In particular, it does not assume the flag-graph construction or any asymptotic input.

We use SimpleGraph.ediam, not SimpleGraph.diam: the latter is defined to be zero when the extended diameter is infinite, and would therefore allow disconnected graphs accidentally.

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

noncomputable def MooreBound.DegreeDiameter.MaxDegreeLE {V : Type u_1} (G : SimpleGraph V) (d : ℕ) : Prop

Every vertex of G has degree at most d, expressed without choosing a decidable adjacency relation. For a finite vertex type, Set.ncard (G.neighborSet v) is the ordinary vertex degree.

Equations

• MooreBound.DegreeDiameter.MaxDegreeLE G d = ∀ (v : V), (G.neighborSet v).ncard ≤ d

A coarse breadth-first bound

def MooreBound.DegreeDiameter.ClosedNeighbor {V : Type u} (G : SimpleGraph V) (x : V) : Type u

One legal breadth-first move: stay at the current vertex, or cross one edge.

Equations

• MooreBound.DegreeDiameter.ClosedNeighbor G x = { y : V // x = y ∨ G.Adj x y }

instance MooreBound.DegreeDiameter.finite_closedNeighbor {V : Type u} [Finite V] (G : SimpleGraph V) (x : V) : Finite (ClosedNeighbor G x)

theorem MooreBound.DegreeDiameter.setOf_closedNeighbor_eq_insert {V : Type u} (G : SimpleGraph V) (x : V) : {y : V | x = y ∨ G.Adj x y} = insert x (G.neighborSet x)

theorem MooreBound.DegreeDiameter.natCard_closedNeighbor_le {V : Type u} [Finite V] {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) (x : V) : Nat.card (ClosedNeighbor G x) ≤ d + 1

def MooreBound.DegreeDiameter.BFSCode (d : ℕ) : ℕ → Type

A uniform code space with d + 1 choices at each of n stages.

Equations

• MooreBound.DegreeDiameter.BFSCode d 0 = PUnit.{1}
• MooreBound.DegreeDiameter.BFSCode d n.succ = (Fin (d + 1) × MooreBound.DegreeDiameter.BFSCode d n)

instance MooreBound.DegreeDiameter.finite_bfsCode (d n : ℕ) : Finite (BFSCode d n)

@[simp]

theorem MooreBound.DegreeDiameter.natCard_bfsCode (d n : ℕ) : Nat.card (BFSCode d n) = (d + 1) ^ n

def MooreBound.DegreeDiameter.BFSRouteCode {V : Type u} (G : SimpleGraph V) : V → ℕ → Type u

Exact-length breadth-first routes. Unlike graph walks, these permit stationary moves.

Equations

• MooreBound.DegreeDiameter.BFSRouteCode G x✝ 0 = PUnit.{?u.1 + 1}
• MooreBound.DegreeDiameter.BFSRouteCode G x✝ n.succ = ((y : MooreBound.DegreeDiameter.ClosedNeighbor G x✝) × MooreBound.DegreeDiameter.BFSRouteCode G (↑y) n)

def MooreBound.DegreeDiameter.BFSRouteCode.endpoint {V : Type u} (G : SimpleGraph V) {x : V} {n : ℕ} : BFSRouteCode G x n → V

The endpoint of a breadth-first route code.

Equations

• MooreBound.DegreeDiameter.BFSRouteCode.endpoint G x_4 = x✝
• MooreBound.DegreeDiameter.BFSRouteCode.endpoint G c = MooreBound.DegreeDiameter.BFSRouteCode.endpoint G c.snd

theorem MooreBound.DegreeDiameter.exists_bfsRouteCode_endpoint_of_walk {V : Type u} {G : SimpleGraph V} {x y : V} (p : G.Walk x y) {n : ℕ} (hp : p.length ≤ n) : ∃ (c : BFSRouteCode G x n), BFSRouteCode.endpoint G c = y

A graph walk of length at most n can be padded by stationary moves to an exact-length breadth-first route code with the same endpoint.

noncomputable def MooreBound.DegreeDiameter.closedNeighborEmbedding {V : Type u} [Finite V] {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) (x : V) : ClosedNeighbor G x ↪ Fin (d + 1)

Each closed neighborhood embeds in the uniform alphabet of size d + 1.

Equations

• MooreBound.DegreeDiameter.closedNeighborEmbedding hdegree x = (Finite.equivFin (MooreBound.DegreeDiameter.ClosedNeighbor G x)).toEmbedding.trans (Fin.castLEEmb ⋯)

noncomputable def MooreBound.DegreeDiameter.encodeBFSRoute {V : Type u} [Finite V] {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) (n : ℕ) (x : V) : BFSRouteCode G x n → BFSCode d n

Encode a breadth-first route into a fixed-length word over Fin (d + 1).

Equations

• One or more equations did not get rendered due to their size.
• MooreBound.DegreeDiameter.encodeBFSRoute hdegree 0 x✝¹ x✝ = PUnit.unit

theorem MooreBound.DegreeDiameter.encodeBFSRoute_injective {V : Type u} [Finite V] {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) (n : ℕ) (x : V) : Function.Injective (encodeBFSRoute hdegree n x)

noncomputable def MooreBound.DegreeDiameter.bfsRouteEmbedding {V : Type u} [Finite V] {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) (n : ℕ) (x : V) : BFSRouteCode G x n ↪ BFSCode d n

Embed length-n routes into the finite set of degree-bounded BFS codes.

Equations

• MooreBound.DegreeDiameter.bfsRouteEmbedding hdegree n x = { toFun := MooreBound.DegreeDiameter.encodeBFSRoute hdegree n x, inj' := ⋯ }

theorem MooreBound.DegreeDiameter.natCard_le_add_one_pow_of_ediam_le {V : Type u} [Finite V] [Nonempty V] {G : SimpleGraph V} {d k : ℕ} (hdegree : MaxDegreeLE G d) (hdiam : G.ediam ≤ ↑k) : Nat.card V ≤ (d + 1) ^ k

Coarse breadth-first bound. Its leading term is still d^k, so it is sufficient for the upper asymptotic in Theorem 1.1.

theorem MooreBound.DegreeDiameter.natCard_le_add_one_pow_of_ediam_le' {V : Type u} [Finite V] {G : SimpleGraph V} {d k : ℕ} (hdegree : MaxDegreeLE G d) (hdiam : G.ediam ≤ ↑k) : Nat.card V ≤ (d + 1) ^ k

A coarse degree bound for line graphs

noncomputable def MooreBound.DegreeDiameter.lineGraphSharedVertex {V : Type u} {G : SimpleGraph V} (e : ↑G.edgeSet) (f : ↑(G.lineGraph.neighborSet e)) : V

Choose the common endpoint of two adjacent edges of the original graph.

Equations

• MooreBound.DegreeDiameter.lineGraphSharedVertex e f = Classical.choose ⋯

theorem MooreBound.DegreeDiameter.lineGraphSharedVertex_mem_left {V : Type u} {G : SimpleGraph V} (e : ↑G.edgeSet) (f : ↑(G.lineGraph.neighborSet e)) : lineGraphSharedVertex e f ∈ ↑e

theorem MooreBound.DegreeDiameter.lineGraphSharedVertex_mem_right {V : Type u} {G : SimpleGraph V} (e : ↑G.edgeSet) (f : ↑(G.lineGraph.neighborSet e)) : lineGraphSharedVertex e f ∈ ↑↑f

noncomputable def MooreBound.DegreeDiameter.lineGraphNeighborCode {V : Type u} {G : SimpleGraph V} (e : ↑G.edgeSet) : ↑(G.lineGraph.neighborSet e) → (v : ↥↑e) × ↑(G.neighborSet ↑v)

Encode an edge neighboring e in the line graph by a shared endpoint of e and the other endpoint of the neighboring edge.

Equations

• MooreBound.DegreeDiameter.lineGraphNeighborCode e f = ⟨⟨MooreBound.DegreeDiameter.lineGraphSharedVertex e f, ⋯⟩, ⟨Sym2.Mem.other ⋯, ⋯⟩⟩

def MooreBound.DegreeDiameter.edgeOfLineGraphNeighborCode {V : Type u} {G : SimpleGraph V} {e : ↑G.edgeSet} (c : (v : ↥↑e) × ↑(G.neighborSet ↑v)) : ↑G.edgeSet

Recover the encoded neighboring edge.

Equations

• MooreBound.DegreeDiameter.edgeOfLineGraphNeighborCode c = ⟨s(↑c.fst, ↑c.snd), ⋯⟩

theorem MooreBound.DegreeDiameter.edgeOfLineGraphNeighborCode_code {V : Type u} {G : SimpleGraph V} (e : ↑G.edgeSet) (f : ↑(G.lineGraph.neighborSet e)) : edgeOfLineGraphNeighborCode (lineGraphNeighborCode e f) = ↑f

theorem MooreBound.DegreeDiameter.lineGraphNeighborCode_injective {V : Type u} {G : SimpleGraph V} (e : ↑G.edgeSet) : Function.Injective (lineGraphNeighborCode e)

theorem MooreBound.DegreeDiameter.natCard_endpoints_eq_two {V : Type u} {G : SimpleGraph V} (e : ↑G.edgeSet) : Nat.card ↥↑e = 2

theorem MooreBound.DegreeDiameter.maxDegreeLE_lineGraph {V : Type u} [Finite V] {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) : MaxDegreeLE G.lineGraph (2 * d)

A coarse line-graph maximum-degree bound. The sharper standard estimate is 2 * (d - 1); 2 * d is enough to establish finite boundedness of the edge extremum.

noncomputable def MooreBound.DegreeDiameter.OrderAdmissible (k d n : ℕ) : Prop

A finite simple graph of order n, maximum degree at most d, and diameter at most k.

The quantified vertex type is kept native instead of transporting every construction to Fin n. Finite V makes Nat.card V and the set cardinalities mathematically meaningful.

Equations

• MooreBound.DegreeDiameter.OrderAdmissible k d n = ∃ (V : Type) (G : SimpleGraph V), Finite V ∧ Nat.card V = n ∧ MooreBound.DegreeDiameter.MaxDegreeLE G d ∧ G.ediam ≤ ↑k

theorem MooreBound.DegreeDiameter.orderAdmissible_le_coarseBound {k d n : ℕ} (hn : OrderAdmissible k d n) : n ≤ (d + 1) ^ k

theorem MooreBound.DegreeDiameter.orderAdmissible_set_bddAbove (k d : ℕ) : BddAbove {n : ℕ | OrderAdmissible k d n}

The defining set for nKD is bounded, unconditionally.

noncomputable def MooreBound.DegreeDiameter.nKD (k d : ℕ) : ℕ

The degree--diameter extremal order. The specification lemmas below require (and later the Moore bound supplies) boundedness of the defining set.

Equations

• MooreBound.DegreeDiameter.nKD k d = sSup {n : ℕ | MooreBound.DegreeDiameter.OrderAdmissible k d n}

noncomputable def MooreBound.DegreeDiameter.EdgeAdmissible (ell d m : ℕ) : Prop

A finite simple graph with m edges, maximum degree at most d, and line-graph diameter at most ell.

Equations

• MooreBound.DegreeDiameter.EdgeAdmissible ell d m = ∃ (V : Type) (G : SimpleGraph V), Finite V ∧ G.edgeSet.ncard = m ∧ MooreBound.DegreeDiameter.MaxDegreeLE G d ∧ G.lineGraph.ediam ≤ ↑ell

theorem MooreBound.DegreeDiameter.edgeAdmissible_le_coarseBound {ell d m : ℕ} (hm : EdgeAdmissible ell d m) : m ≤ (2 * d + 1) ^ ell

theorem MooreBound.DegreeDiameter.edgeAdmissible_set_bddAbove (ell d : ℕ) : BddAbove {m : ℕ | EdgeAdmissible ell d m}

The defining edge-count set is bounded, unconditionally.

noncomputable def MooreBound.DegreeDiameter.h (ell d : ℕ) : ℕ

The paper defines h_ell(d) - 1 as the maximum admissible edge count, so we define h to be one plus that maximum.

Equations

• MooreBound.DegreeDiameter.h ell d = 1 + sSup {m : ℕ | MooreBound.DegreeDiameter.EdgeAdmissible ell d m}

def MooreBound.DegreeDiameter.mooreBound (k d : ℕ) : ℕ

The exact Moore expression.

Equations

• MooreBound.DegreeDiameter.mooreBound k d = 1 + d * ∑ j ∈ Finset.range k, (d - 1) ^ j

theorem MooreBound.DegreeDiameter.maxDegreeLE_mono {V : Type u_1} {G : SimpleGraph V} {d d' : ℕ} (hdd' : d ≤ d') (hG : MaxDegreeLE G d) : MaxDegreeLE G d'

theorem MooreBound.DegreeDiameter.orderAdmissible_mono_degree {k d d' n : ℕ} (hdd' : d ≤ d') (hn : OrderAdmissible k d n) : OrderAdmissible k d' n

theorem MooreBound.DegreeDiameter.orderAdmissible_mono_diameter {k k' d n : ℕ} (hkk' : k ≤ k') (hn : OrderAdmissible k d n) : OrderAdmissible k' d n

theorem MooreBound.DegreeDiameter.edgeAdmissible_mono_degree {ell d d' m : ℕ} (hdd' : d ≤ d') (hm : EdgeAdmissible ell d m) : EdgeAdmissible ell d' m

theorem MooreBound.DegreeDiameter.edgeAdmissible_mono_diameter {ell ell' d m : ℕ} (hell : ell ≤ ell') (hm : EdgeAdmissible ell d m) : EdgeAdmissible ell' d m

theorem MooreBound.DegreeDiameter.orderAdmissible_set_nonempty (k d : ℕ) : {n : ℕ | OrderAdmissible k d n}.Nonempty

The admissible-order set is always nonempty; the one-vertex edgeless graph is a witness.

theorem MooreBound.DegreeDiameter.edgeAdmissible_set_nonempty (ell d : ℕ) : {m : ℕ | EdgeAdmissible ell d m}.Nonempty

The admissible-edge-count set is always nonempty; an edgeless graph is a witness.

theorem MooreBound.DegreeDiameter.le_nKD_of_bddAbove {k d n : ℕ} (hbdd : BddAbove {n : ℕ | OrderAdmissible k d n}) (hn : OrderAdmissible k d n) : n ≤ nKD k d

Any admissible order is at most the extremal value, once boundedness has been established.

theorem MooreBound.DegreeDiameter.nKD_admissible_of_bddAbove (k d : ℕ) (hbdd : BddAbove {n : ℕ | OrderAdmissible k d n}) : OrderAdmissible k d (nKD k d)

Under boundedness, nKD is itself attained by a finite simple graph.

theorem MooreBound.DegreeDiameter.nKD_isGreatest_of_bddAbove (k d : ℕ) (hbdd : BddAbove {n : ℕ | OrderAdmissible k d n}) : IsGreatest {n : ℕ | OrderAdmissible k d n} (nKD k d)

Conditional maximum specification for nKD.

theorem MooreBound.DegreeDiameter.le_nKD {k d n : ℕ} (hn : OrderAdmissible k d n) : n ≤ nKD k d

Unconditional extremal specification, using the coarse breadth-first bound above.

theorem MooreBound.DegreeDiameter.nKD_admissible (k d : ℕ) : OrderAdmissible k d (nKD k d)

theorem MooreBound.DegreeDiameter.nKD_isGreatest (k d : ℕ) : IsGreatest {n : ℕ | OrderAdmissible k d n} (nKD k d)

theorem MooreBound.DegreeDiameter.le_h_sub_one_of_bddAbove {ell d m : ℕ} (hbdd : BddAbove {m : ℕ | EdgeAdmissible ell d m}) (hm : EdgeAdmissible ell d m) : m ≤ h ell d - 1

Any admissible edge count is at most h ell d - 1, once boundedness has been established.

theorem MooreBound.DegreeDiameter.h_sub_one_admissible_of_bddAbove (ell d : ℕ) (hbdd : BddAbove {m : ℕ | EdgeAdmissible ell d m}) : EdgeAdmissible ell d (h ell d - 1)

Under boundedness, h ell d - 1 is itself attained.

theorem MooreBound.DegreeDiameter.h_sub_one_isGreatest_of_bddAbove (ell d : ℕ) (hbdd : BddAbove {m : ℕ | EdgeAdmissible ell d m}) : IsGreatest {m : ℕ | EdgeAdmissible ell d m} (h ell d - 1)

Conditional maximum specification for the paper's edge extremum h ell d - 1.

theorem MooreBound.DegreeDiameter.le_h_sub_one {ell d m : ℕ} (hm : EdgeAdmissible ell d m) : m ≤ h ell d - 1

Unconditional edge-extremum specifications, using the coarse line-graph bound above.

theorem MooreBound.DegreeDiameter.h_sub_one_admissible (ell d : ℕ) : EdgeAdmissible ell d (h ell d - 1)

theorem MooreBound.DegreeDiameter.h_sub_one_isGreatest (ell d : ℕ) : IsGreatest {m : ℕ | EdgeAdmissible ell d m} (h ell d - 1)

theorem MooreBound.DegreeDiameter.h_sub_one_le_coarseBound (ell d : ℕ) : h ell d - 1 ≤ (2 * d + 1) ^ ell