The exact Moore bound

This module proves the standard breadth-first (Moore) bound used in the degree--diameter problem. Starting from a root, a shortest route has at most d choices for its first edge and at most d - 1 choices for each later edge: the edge just traversed cannot immediately be traversed backwards.

The route types below make that argument literal. In particular, the proof does not obtain the leading term indirectly from the coarser (d + 1)^k bound in Framework.

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.ForwardNeighbor {V : Type u} (G : SimpleGraph V) (previous current : V) : Type u

A possible next vertex after traversing previous -- current, excluding the immediate reverse step.

Equations

• MooreBound.DegreeDiameter.ForwardNeighbor G previous current = { next : V // G.Adj current next ∧ next ≠ previous }

instance MooreBound.DegreeDiameter.finite_forwardNeighbor {V : Type u} [Finite V] (G : SimpleGraph V) (previous current : V) : Finite (ForwardNeighbor G previous current)

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

An exact-length nonbacktracking continuation, after an initial directed edge previous -- current has already been traversed.

Equations

• MooreBound.DegreeDiameter.NBContinuation G x✝¹ x✝ 0 = PUnit.{?u.1 + 1}
• MooreBound.DegreeDiameter.NBContinuation G x✝¹ x✝ n.succ = ((next : MooreBound.DegreeDiameter.ForwardNeighbor G x✝¹ x✝) × MooreBound.DegreeDiameter.NBContinuation G x✝ (↑next) n)

instance MooreBound.DegreeDiameter.finite_nbContinuation {V : Type u} [Finite V] (G : SimpleGraph V) (previous current : V) (n : ℕ) : Finite (NBContinuation G previous current n)

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

An exact-length nonbacktracking route beginning at root.

Equations

• MooreBound.DegreeDiameter.ExactNBRoute G root 0 = PUnit.{?u.1 + 1}
• MooreBound.DegreeDiameter.ExactNBRoute G root n.succ = ((first : ↑(G.neighborSet root)) × MooreBound.DegreeDiameter.NBContinuation G root (↑first) n)

instance MooreBound.DegreeDiameter.finite_exactNBRoute {V : Type u} [Finite V] (G : SimpleGraph V) (root : V) (n : ℕ) : Finite (ExactNBRoute G root n)

def MooreBound.DegreeDiameter.NBContinuation.endpoint {V : Type u} (G : SimpleGraph V) {previous current : V} {n : ℕ} : NBContinuation G previous current n → V

The last vertex of a nonbacktracking continuation.

Equations

• MooreBound.DegreeDiameter.NBContinuation.endpoint G x_5 = x✝
• MooreBound.DegreeDiameter.NBContinuation.endpoint G route = MooreBound.DegreeDiameter.NBContinuation.endpoint G route.snd

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

The last vertex of an exact nonbacktracking route.

Equations

• MooreBound.DegreeDiameter.ExactNBRoute.endpoint G root x_2 = root
• MooreBound.DegreeDiameter.ExactNBRoute.endpoint G root route = MooreBound.DegreeDiameter.NBContinuation.endpoint G route.snd

theorem MooreBound.DegreeDiameter.ExactNBRoute.endpoint_cast {V : Type u} (G : SimpleGraph V) (root : V) {m n : ℕ} (h : m = n) (route : ExactNBRoute G root m) : endpoint G root (h ▸ route) = endpoint G root route

def MooreBound.DegreeDiameter.NBContinuation.ofPath {V : Type u} {G : SimpleGraph V} {previous current target : V} (p : G.Walk current target) : p.IsPath → previous ∉ p.support → NBContinuation G previous current p.length

Convert a path beginning at current, which avoids previous, into the corresponding nonbacktracking continuation.

Equations

• MooreBound.DegreeDiameter.NBContinuation.ofPath SimpleGraph.Walk.nil x_8 x_9 = PUnit.unit
• MooreBound.DegreeDiameter.NBContinuation.ofPath (SimpleGraph.Walk.cons hadj tail) hp hprevious = ⟨⟨v, ⋯⟩, MooreBound.DegreeDiameter.NBContinuation.ofPath tail ⋯ ⋯⟩

theorem MooreBound.DegreeDiameter.NBContinuation.endpoint_ofPath {V : Type u} {G : SimpleGraph V} {previous current target : V} (p : G.Walk current target) (hp : p.IsPath) (hprevious : previous ∉ p.support) : endpoint G (ofPath p hp hprevious) = target

def MooreBound.DegreeDiameter.ExactNBRoute.ofPath {V : Type u} {G : SimpleGraph V} {root target : V} (p : G.Walk root target) (hp : p.IsPath) : ExactNBRoute G root p.length

Every path gives an exact nonbacktracking route with the same endpoint.

Equations

• MooreBound.DegreeDiameter.ExactNBRoute.ofPath SimpleGraph.Walk.nil hp_2 = PUnit.unit
• MooreBound.DegreeDiameter.ExactNBRoute.ofPath (SimpleGraph.Walk.cons hadj tail) hp_2 = ⟨⟨v, hadj⟩, MooreBound.DegreeDiameter.NBContinuation.ofPath tail ⋯ ⋯⟩

theorem MooreBound.DegreeDiameter.ExactNBRoute.endpoint_ofPath {V : Type u} {G : SimpleGraph V} {root target : V} (p : G.Walk root target) (hp : p.IsPath) : endpoint G root (ofPath p hp) = target

theorem MooreBound.DegreeDiameter.natCard_forwardNeighbor_le {V : Type u} {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) {previous current : V} (hpc : G.Adj previous current) : Nat.card (ForwardNeighbor G previous current) ≤ d - 1

Removing the vertex just left leaves at most d - 1 choices.

theorem MooreBound.DegreeDiameter.natCard_nbContinuation_le {V : Type u} [Finite V] {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) {previous current : V} (hpc : G.Adj previous current) (n : ℕ) : Nat.card (NBContinuation G previous current n) ≤ (d - 1) ^ n

There are at most (d - 1)^n nonbacktracking continuations of length n after a directed edge.

theorem MooreBound.DegreeDiameter.natCard_exactNBRoute_succ_le {V : Type u} [Finite V] {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) (root : V) (n : ℕ) : Nat.card (ExactNBRoute G root (n + 1)) ≤ d * (d - 1) ^ n

The distance-n+1 route layer has at most d(d-1)^n members.

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

Routes of length at most k, presented recursively as the disjoint union of the earlier layers and the exact length-k layer.

Equations

• MooreBound.DegreeDiameter.BoundedNBRoute G root 0 = PUnit.{?u.1 + 1}
• MooreBound.DegreeDiameter.BoundedNBRoute G root n.succ = (MooreBound.DegreeDiameter.BoundedNBRoute G root n ⊕ MooreBound.DegreeDiameter.ExactNBRoute G root (n + 1))

instance MooreBound.DegreeDiameter.finite_boundedNBRoute {V : Type u} [Finite V] (G : SimpleGraph V) (root : V) (k : ℕ) : Finite (BoundedNBRoute G root k)

def MooreBound.DegreeDiameter.BoundedNBRoute.endpoint {V : Type u} (G : SimpleGraph V) (root : V) {k : ℕ} : BoundedNBRoute G root k → V

Endpoint of a route of length at most k.

Equations

• MooreBound.DegreeDiameter.BoundedNBRoute.endpoint G root x_2 = root
• MooreBound.DegreeDiameter.BoundedNBRoute.endpoint G root (Sum.inl route) = MooreBound.DegreeDiameter.BoundedNBRoute.endpoint G root route
• MooreBound.DegreeDiameter.BoundedNBRoute.endpoint G root (Sum.inr route) = MooreBound.DegreeDiameter.ExactNBRoute.endpoint G root route

theorem MooreBound.DegreeDiameter.exists_boundedNBRoute_endpoint_of_path {V : Type u} {G : SimpleGraph V} {root target : V} (p : G.Walk root target) (hp : p.IsPath) {k : ℕ} (hlength : p.length ≤ k) : ∃ (route : BoundedNBRoute G root k), BoundedNBRoute.endpoint G root route = target

A path of length at most k belongs to the bounded route type and keeps its endpoint. This is the formal shortest/nonbacktracking-route step in the standard Moore-bound proof.

theorem MooreBound.DegreeDiameter.natCard_boundedNBRoute_le {V : Type u} [Finite V] {G : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE G d) (root : V) (k : ℕ) : Nat.card (BoundedNBRoute G root k) ≤ mooreBound k d

The recursive bounded-route type has exactly the cardinality estimate in the Moore expression.

theorem MooreBound.DegreeDiameter.mooreBound_le_add_one_pow (k d : ℕ) : mooreBound k d ≤ (d + 1) ^ k

The exact Moore expression is bounded by the convenient leading-term comparison (d + 1)^k. This lemma is used only after the exact graph bound has been established.

theorem MooreBound.DegreeDiameter.natCard_le_mooreBound_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 ≤ mooreBound k d

Exact Moore bound for every finite graph of maximum degree at most d and extended diameter at most k.

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

The exact Moore bound, including the empty vertex type.

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

Every graph order admitted in the definition of nKD obeys the exact Moore bound.

theorem MooreBound.DegreeDiameter.nKD_le_mooreBound (k d : ℕ) : nKD k d ≤ mooreBound k d

The exact paper inequality n_k(d) ≤ 1 + d ∑_{j<k}(d-1)^j.