Strongly regular graphs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

G.is_SRG_with n k ℓ μ (see simple_graph.is_SRG_with) is a structure for a simple_graph satisfying the following conditions:
- The cardinality of the vertex set is n
- G is a regular graph with degree k
- The number of common neighbors between any two adjacent vertices in G is ℓ
- The number of common neighbors between any two nonadjacent vertices in G is μ

TODO #

Prove that the parameters of a strongly regular graph obey the relation (n - k - 1) * μ = k * (k - ℓ - 1)
Prove that if I is the identity matrix and J is the all-one matrix, then the adj matrix A of SRG obeys relation A^2 = kI + ℓA + μ(J - I - A)

structure simple_graph.is_SRG_with {V : Type u} [fintype V] [decidable_eq V] (G : simple_graph V) [decidable_rel G.adj] (n k ℓ μ : ℕ) :

Prop

card : fintype.card V = n
regular : G.is_regular_of_degree k
of_adj : ∀ (v w : V), G.adj v w → fintype.card ↥(G.common_neighbors v w) = ℓ
of_not_adj : ∀ (v w : V), v ≠ w → ¬G.adj v w → fintype.card ↥(G.common_neighbors v w) = μ

A graph is strongly regular with parameters n k ℓ μ if

its vertex set has cardinality n
it is regular with degree k
every pair of adjacent vertices has ℓ common neighbors
every pair of nonadjacent vertices has μ common neighbors

source

theorem simple_graph.bot_strongly_regular {V : Type u} [fintype V] [decidable_eq V] {ℓ : ℕ} :

⊥.is_SRG_with (fintype.card V) 0 ℓ 0

Empty graphs are strongly regular. Note that ℓ can take any value for empty graphs, since there are no pairs of adjacent vertices.

source

theorem simple_graph.is_SRG_with.top {V : Type u} [fintype V] [decidable_eq V] {μ : ℕ} :

⊤.is_SRG_with (fintype.card V) (fintype.card V - 1) (fintype.card V - 2) μ

Complete graphs are strongly regular. Note that μ can take any value for complete graphs, since there are no distinct pairs of non-adjacent vertices.

source

theorem simple_graph.is_SRG_with.card_neighbor_finset_union_eq {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : ℕ} {v w : V} (h : G.is_SRG_with n k ℓ μ) :

(G.neighbor_finset v ∪ G.neighbor_finset w).card = 2 * k - fintype.card ↥(G.common_neighbors v w)

source

theorem simple_graph.is_SRG_with.card_neighbor_finset_union_of_not_adj {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : ℕ} {v w : V} (h : G.is_SRG_with n k ℓ μ) (hne : v ≠ w) (ha : ¬G.adj v w) :

(G.neighbor_finset v ∪ G.neighbor_finset w).card = 2 * k - μ

Assuming G is strongly regular, 2*(k + 1) - m in G is the number of vertices that are adjacent to either v or w when ¬G.adj v w. So it's the cardinality of G.neighbor_set v ∪ G.neighbor_set w.

source

theorem simple_graph.is_SRG_with.card_neighbor_finset_union_of_adj {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : ℕ} {v w : V} (h : G.is_SRG_with n k ℓ μ) (ha : G.adj v w) :

(G.neighbor_finset v ∪ G.neighbor_finset w).card = 2 * k - ℓ

source

theorem simple_graph.compl_neighbor_finset_sdiff_inter_eq {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {v w : V} :

(G.neighbor_finset v)ᶜ \ {v} ∩ ((G.neighbor_finset w)ᶜ \ {w}) = (G.neighbor_finset v)ᶜ ∩ (G.neighbor_finset w)ᶜ \ ({w} ∪ {v})

source

theorem simple_graph.sdiff_compl_neighbor_finset_inter_eq {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {v w : V} (h : G.adj v w) :

(G.neighbor_finset v)ᶜ ∩ (G.neighbor_finset w)ᶜ \ ({w} ∪ {v}) = (G.neighbor_finset v)ᶜ ∩ (G.neighbor_finset w)ᶜ

source

theorem simple_graph.is_SRG_with.compl_is_regular {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : ℕ} (h : G.is_SRG_with n k ℓ μ) :

Gᶜ.is_regular_of_degree (n - k - 1)

source

theorem simple_graph.is_SRG_with.card_common_neighbors_eq_of_adj_compl {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : ℕ} (h : G.is_SRG_with n k ℓ μ) {v w : V} (ha : Gᶜ.adj v w) :

fintype.card ↥(Gᶜ.common_neighbors v w) = n - (2 * k - μ) - 2

source

theorem simple_graph.is_SRG_with.card_common_neighbors_eq_of_not_adj_compl {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : ℕ} (h : G.is_SRG_with n k ℓ μ) {v w : V} (hn : v ≠ w) (hna : ¬Gᶜ.adj v w) :

fintype.card ↥(Gᶜ.common_neighbors v w) = n - (2 * k - ℓ)

source

theorem simple_graph.is_SRG_with.compl {V : Type u} [fintype V] [decidable_eq V] {G : simple_graph V} [decidable_rel G.adj] {n k ℓ μ : ℕ} (h : G.is_SRG_with n k ℓ μ) :

Gᶜ.is_SRG_with n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ℓ))

The complement of a strongly regular graph is strongly regular.