The edge-reduction construction

This file formalizes the bipartite graph B(H) used in Lemma 4.1 of the draft. An edge between the two copies of the vertex set records either equality or adjacency in H.

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.Linked {V : Type u} (H : SimpleGraph V) (x y : V) : Prop

Equality or adjacency in a simple graph (the reflexive closure of adjacency).

Equations

• MooreBound.DegreeDiameter.Linked H x y = (x = y ∨ H.Adj x y)

theorem MooreBound.DegreeDiameter.linked_refl {V : Type u} (H : SimpleGraph V) (x : V) : Linked H x x

theorem MooreBound.DegreeDiameter.linked_symm {V : Type u} {H : SimpleGraph V} {x y : V} : Linked H x y → Linked H y x

def MooreBound.DegreeDiameter.bipartiteExpansion {V : Type u} (H : SimpleGraph V) : SimpleGraph (V ⊕ V)

The graph B(H) from the draft. Its two parts are the two summands of V ⊕ V.

Equations

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

@[simp]

theorem MooreBound.DegreeDiameter.bipartiteExpansion_adj_inl_inr {V : Type u} (H : SimpleGraph V) (x y : V) : (bipartiteExpansion H).Adj (Sum.inl x) (Sum.inr y) ↔ Linked H x y

@[simp]

theorem MooreBound.DegreeDiameter.bipartiteExpansion_adj_inr_inl {V : Type u} (H : SimpleGraph V) (x y : V) : (bipartiteExpansion H).Adj (Sum.inr y) (Sum.inl x) ↔ Linked H x y

@[simp]

theorem MooreBound.DegreeDiameter.bipartiteExpansion_not_adj_inl_inl {V : Type u} (H : SimpleGraph V) (x y : V) : ¬(bipartiteExpansion H).Adj (Sum.inl x) (Sum.inl y)

@[simp]

theorem MooreBound.DegreeDiameter.bipartiteExpansion_not_adj_inr_inr {V : Type u} (H : SimpleGraph V) (x y : V) : ¬(bipartiteExpansion H).Adj (Sum.inr x) (Sum.inr y)

def MooreBound.DegreeDiameter.bipartiteEdge {V : Type u} (H : SimpleGraph V) (x y : V) (hxy : Linked H x y) : ↑(bipartiteExpansion H).edgeSet

The edge of B(H) represented in the draft by [x,y].

Equations

• MooreBound.DegreeDiameter.bipartiteEdge H x y hxy = ⟨s(Sum.inl x, Sum.inr y), ⋯⟩

@[simp]

theorem MooreBound.DegreeDiameter.bipartiteEdge_val {V : Type u} (H : SimpleGraph V) (x y : V) (hxy : Linked H x y) : ↑(bipartiteEdge H x y hxy) = s(Sum.inl x, Sum.inr y)

theorem MooreBound.DegreeDiameter.setOf_linked_eq_insert_neighborSet {V : Type u} (H : SimpleGraph V) (x : V) : {y : V | Linked H x y} = insert x (H.neighborSet x)

theorem MooreBound.DegreeDiameter.neighborSet_bipartiteExpansion_inl {V : Type u} (H : SimpleGraph V) (x : V) : (bipartiteExpansion H).neighborSet (Sum.inl x) = Sum.inr '' insert x (H.neighborSet x)

theorem MooreBound.DegreeDiameter.neighborSet_bipartiteExpansion_inr {V : Type u} (H : SimpleGraph V) (x : V) : (bipartiteExpansion H).neighborSet (Sum.inr x) = Sum.inl '' insert x (H.neighborSet x)

theorem MooreBound.DegreeDiameter.ncard_neighborSet_bipartiteExpansion_inl {V : Type u} [Finite V] (H : SimpleGraph V) (x : V) : ((bipartiteExpansion H).neighborSet (Sum.inl x)).ncard = (H.neighborSet x).ncard + 1

theorem MooreBound.DegreeDiameter.ncard_neighborSet_bipartiteExpansion_inr {V : Type u} [Finite V] (H : SimpleGraph V) (x : V) : ((bipartiteExpansion H).neighborSet (Sum.inr x)).ncard = (H.neighborSet x).ncard + 1

theorem MooreBound.DegreeDiameter.maxDegreeLE_bipartiteExpansion {V : Type u} [Finite V] {H : SimpleGraph V} {d : ℕ} (hdegree : MaxDegreeLE H d) : MaxDegreeLE (bipartiteExpansion H) (d + 1)

B(H) raises the maximum-degree bound by exactly one.

theorem MooreBound.DegreeDiameter.ncard_edgeSet_bipartiteExpansion_of_regular {V : Type u} [Finite V] (H : SimpleGraph V) (Delta : ℕ) (hregular : ∀ (x : V), (H.neighborSet x).ncard = Delta) : (bipartiteExpansion H).edgeSet.ncard = Nat.card V * (Delta + 1)

If every vertex of H has degree Delta, then the paper's graph B(H) has exactly |V(H)| * (Delta + 1) edges.

theorem MooreBound.DegreeDiameter.exists_eq_bipartiteEdge {V : Type u} (H : SimpleGraph V) (e : ↑(bipartiteExpansion H).edgeSet) : ∃ (x : V) (y : V) (hxy : Linked H x y), e = bipartiteEdge H x y hxy

Every edge of B(H) has a unique orientation from the left part to the right part.

theorem MooreBound.DegreeDiameter.lineGraph_edist_bipartiteEdge_le_one_of_left {V : Type u} (H : SimpleGraph V) (a b c : V) (hab : Linked H a b) (hac : Linked H a c) : (bipartiteExpansion H).lineGraph.edist (bipartiteEdge H a b hab) (bipartiteEdge H a c hac) ≤ 1

Two represented edges with the same left endpoint have line-graph distance at most one.

theorem MooreBound.DegreeDiameter.lineGraph_edist_bipartiteEdge_le_one_of_right {V : Type u} (H : SimpleGraph V) (a b c : V) (hac : Linked H a c) (hbc : Linked H b c) : (bipartiteExpansion H).lineGraph.edist (bipartiteEdge H a c hac) (bipartiteEdge H b c hbc) ≤ 1

Two represented edges with the same right endpoint have line-graph distance at most one.

inductive MooreBound.DegreeDiameter.Route {V : Type u} (H : SimpleGraph V) : V → V → ℕ → Type u

A route permits stationary steps as well as graph edges. It is indexed by its exact length; this is the formal counterpart of the padded sequences in the paper's proof of Lemma 4.1.

• nil {V : Type u} {H : SimpleGraph V} (x : V) : Route H x x 0
• cons {V : Type u} {H : SimpleGraph V} {x y z : V} {n : ℕ} (hxy : Linked H x y) (tail : Route H y z n) : Route H x z n.succ

def MooreBound.DegreeDiameter.Route.ofWalk {V : Type u} (H : SimpleGraph V) {x y : V} (p : H.Walk x y) : Route H x y p.length

Regard a graph walk as a route allowing both adjacency and stationary steps.

Equations

• MooreBound.DegreeDiameter.Route.ofWalk H SimpleGraph.Walk.nil = MooreBound.DegreeDiameter.Route.nil x
• MooreBound.DegreeDiameter.Route.ofWalk H (SimpleGraph.Walk.cons h p) = MooreBound.DegreeDiameter.Route.cons ⋯ (MooreBound.DegreeDiameter.Route.ofWalk H p)

def MooreBound.DegreeDiameter.Route.stay {V : Type u} (H : SimpleGraph V) (x : V) (n : ℕ) : Route H x x n

The route of the specified length that stays at one vertex.

Equations

• MooreBound.DegreeDiameter.Route.stay H x 0 = MooreBound.DegreeDiameter.Route.nil x
• MooreBound.DegreeDiameter.Route.stay H x n.succ = MooreBound.DegreeDiameter.Route.cons ⋯ (MooreBound.DegreeDiameter.Route.stay H x n)

def MooreBound.DegreeDiameter.Route.append {V : Type u} {H : SimpleGraph V} {x y z : V} {m n : ℕ} : Route H x y m → Route H y z n → Route H x z (n + m)

Concatenate routes. The length index is written in this order so the defining equations reduce without arithmetic casts when recursing through the first route.

Equations

• (MooreBound.DegreeDiameter.Route.nil x).append q = q
• (MooreBound.DegreeDiameter.Route.cons h p).append x✝ = MooreBound.DegreeDiameter.Route.cons h (p.append x✝)

def MooreBound.DegreeDiameter.Route.padWalk {V : Type u} (H : SimpleGraph V) {x y : V} (p : H.Walk x y) (k : ℕ) (hp : p.length ≤ k) : Route H x y k

Pad an ordinary graph walk by stationary steps to any prescribed larger length.

Equations

• MooreBound.DegreeDiameter.Route.padWalk H p k hp = ⋯ ▸ (MooreBound.DegreeDiameter.Route.ofWalk H p).append (MooreBound.DegreeDiameter.Route.stay H y (k - p.length))

def MooreBound.DegreeDiameter.zigEndpoints {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) : ((a : V) → Linked H a x → ↑(bipartiteExpansion H).edgeSet) × ((b : V) → Linked H x b → ↑(bipartiteExpansion H).edgeSet)

Compute both alternating edge endpoints by structural recursion on the route. The two functions record which coordinate is replaced first.

Equations

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

def MooreBound.DegreeDiameter.zigFirst {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) (a : V) (ha : Linked H a x) : ↑(bipartiteExpansion H).edgeSet

Follow a route by first replacing the left coordinate of a represented bipartite edge.

Equations

• MooreBound.DegreeDiameter.zigFirst H p a ha = (MooreBound.DegreeDiameter.zigEndpoints H p).1 a ha

def MooreBound.DegreeDiameter.zigSecond {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) (b : V) (hb : Linked H x b) : ↑(bipartiteExpansion H).edgeSet

Follow a route by first replacing the right coordinate of a represented bipartite edge.

Equations

• MooreBound.DegreeDiameter.zigSecond H p b hb = (MooreBound.DegreeDiameter.zigEndpoints H p).2 b hb

theorem MooreBound.DegreeDiameter.zig_terminal {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) : (∀ (a : V) (ha : Linked H a x), (Even n → ∃ (a' : V) (ha' : Linked H a' y), zigFirst H p a ha = bipartiteEdge H a' y ha') ∧ (Odd n → ∃ (b' : V) (hb' : Linked H y b'), zigFirst H p a ha = bipartiteEdge H y b' hb')) ∧ ∀ (b : V) (hb : Linked H x b), (Even n → ∃ (b' : V) (hb' : Linked H y b'), zigSecond H p b hb = bipartiteEdge H y b' hb') ∧ (Odd n → ∃ (a' : V) (ha' : Linked H a' y), zigSecond H p b hb = bipartiteEdge H a' y ha')

theorem MooreBound.DegreeDiameter.zigFirst_of_even {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) (a : V) (ha : Linked H a x) (hn : Even n) : ∃ (a' : V) (ha' : Linked H a' y), zigFirst H p a ha = bipartiteEdge H a' y ha'

theorem MooreBound.DegreeDiameter.zigFirst_of_odd {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) (a : V) (ha : Linked H a x) (hn : Odd n) : ∃ (b' : V) (hb' : Linked H y b'), zigFirst H p a ha = bipartiteEdge H y b' hb'

theorem MooreBound.DegreeDiameter.zigSecond_of_even {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) (b : V) (hb : Linked H x b) (hn : Even n) : ∃ (b' : V) (hb' : Linked H y b'), zigSecond H p b hb = bipartiteEdge H y b' hb'

theorem MooreBound.DegreeDiameter.zigSecond_of_odd {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) (b : V) (hb : Linked H x b) (hn : Odd n) : ∃ (a' : V) (ha' : Linked H a' y), zigSecond H p b hb = bipartiteEdge H a' y ha'

theorem MooreBound.DegreeDiameter.edist_zig_le {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) : (∀ (a : V) (ha : Linked H a x), (bipartiteExpansion H).lineGraph.edist (bipartiteEdge H a x ha) (zigFirst H p a ha) ≤ ↑n) ∧ ∀ (b : V) (hb : Linked H x b), (bipartiteExpansion H).lineGraph.edist (bipartiteEdge H x b hb) (zigSecond H p b hb) ≤ ↑n

Both alternating coordinate routes cost no more than one line-graph step per route step.

theorem MooreBound.DegreeDiameter.edist_zigFirst_le {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) (a : V) (ha : Linked H a x) : (bipartiteExpansion H).lineGraph.edist (bipartiteEdge H a x ha) (zigFirst H p a ha) ≤ ↑n

theorem MooreBound.DegreeDiameter.edist_zigSecond_le {V : Type u} (H : SimpleGraph V) {x y : V} {n : ℕ} (p : Route H x y n) (b : V) (hb : Linked H x b) : (bipartiteExpansion H).lineGraph.edist (bipartiteEdge H x b hb) (zigSecond H p b hb) ≤ ↑n

theorem MooreBound.DegreeDiameter.nonempty_route_of_ediam_le {V : Type u} (H : SimpleGraph V) (k : ℕ) (hdiam : H.ediam ≤ ↑k) (x y : V) : Nonempty (Route H x y k)

A diameter bound in H supplies an exact-length padded route between every two vertices.

theorem MooreBound.DegreeDiameter.lineGraph_edist_bipartiteExpansion_le {V : Type u} (H : SimpleGraph V) (k : ℕ) (hdiam : H.ediam ≤ ↑k) (e f : ↑(bipartiteExpansion H).edgeSet) : (bipartiteExpansion H).lineGraph.edist e f ≤ ↑(k + 1)

Pointwise distance form of Lemma 4.1.

theorem MooreBound.DegreeDiameter.lemma_4_1_le {V : Type u} (H : SimpleGraph V) (k : ℕ) (hdiam : H.ediam ≤ ↑k) : (bipartiteExpansion H).lineGraph.ediam ≤ ↑(k + 1)

Lemma 4.1 in bounded-diameter form. This formulation also handles empty vertex and edge types without adding nonemptiness hypotheses.

theorem MooreBound.DegreeDiameter.lemma_4_1 {V : Type u} (H : SimpleGraph V) : (bipartiteExpansion H).lineGraph.ediam ≤ H.ediam + 1

Lemma 4.1 exactly as an inequality of extended diameters.