Deza graphs

StructureDeza graph#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\), and let \(n, k, b, a\) be natural numbers. Then \(G\) is a Deza graph with parameters \((n, k, b, a)\) when \(a \le b \le k < n\), \(V\) has exactly \(n\) elements, every vertex of \(G\) has degree \(k\), and any two distinct vertices of \(G\) have exactly \(a\) or exactly \(b\) common neighbours, whether or not they are adjacent.

SimpleGraph.IsDezaWith · 15 lines

structure IsDezaWith (n k b a : ℕ) : Prop where
  /-- Lower parameter inequality `a ≤ b`. -/
  a_le_b : a ≤ b
  /-- Middle parameter inequality `b ≤ k`. -/
  b_le_k : b ≤ k
  /-- Strict parameter inequality `k < n`. -/
  k_lt_n : k < n
  /-- Exactly `n` vertices. -/
  card_eq : Fintype.card V = n
  /-- `k`-regularity. -/
  regular : G.IsRegularOfDegree k
  /-- Two-valued common-neighbour counts. -/
  common_eq : ∀ u v : V, u ≠ v →
    Fintype.card (G.commonNeighbors u v) = a ∨
      Fintype.card (G.commonNeighbors u v) = b

Sources

• Golubyatnikov, https://arxiv.org/abs/2608.13089v1, lines 163--164.

Used by 3

Used byParameter bound \(a \le k\) for Deza graphs · Parameter bound \(a < n\) for Deza graphs · Parameter bound \(b < n\) for Deza graphs

TheoremParameter bound \(a \le k\) for Deza graphs#✓fully proved

If a finite simple graph \(G\) is a Deza graph with parameters \((n, k, b, a)\), then \(a \le k\).

theorem IsDezaWith.a_le_k {n k b a : ℕ} (h : G.IsDezaWith n k b a) : a ≤ k

Uses 1 · Used by 1

Statement usesDeza graph

Used byParameter bound \(a < n\) for Deza graphs

TheoremParameter bound \(b < n\) for Deza graphs#✓fully proved

If a finite simple graph \(G\) is a Deza graph with parameters \((n, k, b, a)\), then \(b < n\).

theorem IsDezaWith.b_lt_n {n k b a : ℕ} (h : G.IsDezaWith n k b a) : b < n

Uses 1

Statement usesDeza graph

TheoremParameter bound \(a < n\) for Deza graphs#✓fully proved

If a finite simple graph \(G\) is a Deza graph with parameters \((n, k, b, a)\), then \(a < n\).

theorem IsDezaWith.a_lt_n {n k b a : ℕ} (h : G.IsDezaWith n k b a) : a < n

Uses 2

Statement usesDeza graph

Proof usesParameter bound \(a \le k\) for Deza graphs

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.