Strongly regular graphs
TheoremTwo-edge paths close into triangles when μ = 0#✓fully proved
Let \(G\) be a finite strongly regular graph with parameters \((n, k, \ell, \mu)\) where \(\mu = 0\): \(G\) has \(n\) vertices, every vertex has degree \(k\), any two adjacent vertices have exactly \(\ell\) common neighbors, and any two distinct nonadjacent vertices have no common neighbor. If \(u\), \(v\), \(w\) are vertices of \(G\) such that \(u\) is adjacent to \(v\), \(v\) is adjacent to \(w\), and \(u \neq w\), then \(u\) is adjacent to \(w\).
public theorem _root_.SimpleGraph.IsSRGWith.adj_of_adj_of_adj_of_mu_zero
{V : Type*} [Fintype V] {n k ℓ : ℕ} {G : SimpleGraph V} [DecidableRel G.Adj]
(h : G.IsSRGWith n k ℓ 0) {u v w : V} (huv : G.Adj u v) (hvw : G.Adj v w)
(huw : u ≠ w) : G.Adj u wTheoremNon-principal eigenvalues of a strongly regular graph#✓fully proved
Let \(G\) be a finite strongly regular graph with parameters \((n, k, \ell, \mu)\): \(G\) has \(n\) vertices, every vertex has degree \(k\), any two adjacent vertices have exactly \(\ell\) common neighbors, and any two distinct nonadjacent vertices have exactly \(\mu\) common neighbors. Let \(A\) be the adjacency matrix of \(G\) over \(\mathbb{C}\). Then every eigenvalue \(x \in \mathbb{C}\) of \(A\) with \(x \neq k\) satisfies \(x^2 = (\ell - \mu) x + (k - \mu)\).
public theorem _root_.SimpleGraph.IsSRGWith.nonprincipal_eigenvalue_quadratic
{V : Type*} [Fintype V] {n k ℓ μ : ℕ} {G : SimpleGraph V}
[DecidableRel G.Adj] [DecidableEq V] (h : G.IsSRGWith n k ℓ μ) {x : ℂ}
(hx : x ≠ (k : ℂ))
(hEig : Module.End.HasEigenvalue (Matrix.toLin' (G.adjMatrix ℂ)) x) :
x ^ 2 = ((ℓ : ℂ) - (μ : ℂ)) * x + ((k : ℂ) - (μ : ℂ))TheoremConnected strongly regular graphs with μ = 0 are complete#✓fully proved
Let \(G\) be a finite strongly regular graph with parameters \((n, k, \ell, \mu)\) where \(\mu = 0\): \(G\) has \(n\) vertices, every vertex has degree \(k\), any two adjacent vertices have exactly \(\ell\) common neighbors, and any two distinct nonadjacent vertices have no common neighbor. If \(G\) is connected, then \(G\) is complete, that is, any two distinct vertices of \(G\) are adjacent.
Proof: The \(\mu = 0\) common-neighbor count makes every nontrivial two-edge walk a triangle, so walk induction makes each component a clique. Connectedness then gives completeness. Brouwer and Haemers, Section 9.1.4, state the component fact: \(\mu = 0\) makes the graph a disjoint union of complete graphs.
public theorem srg_connected_mu_zero_complete {V : Type*} [Fintype V]
{n k ℓ : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj]
(h : G.IsSRGWith n k ℓ 0) (hconn : G.Connected) : G = ⊤Sources
- A. E. Brouwer and W. H. Haemers, Spectra of Graphs, Springer 2012, Ch. 9 (disconnected and complete strongly regular graphs); C. Godsil and G. Royle, Algebraic Graph Theory, GTM 207, Ch. 10.
Uses 1
TheoremComponents of a strongly regular graph with μ = 0 are cliques#✓fully proved
Let \(G\) be a finite strongly regular graph with parameters \((n, k, \ell, \mu)\) where \(\mu = 0\): \(G\) has \(n\) vertices, every vertex has degree \(k\), any two adjacent vertices have exactly \(\ell\) common neighbors, and any two distinct nonadjacent vertices have no common neighbor. If \(v\) and \(w\) are vertices of \(G\) joined by a walk, then \(v = w\) or \(v\) and \(w\) are adjacent. Thus each connected component of \(G\) is a clique.
Without \(\mu = 0\) this is false: two nonadjacent vertices of the 5-cycle, a strongly regular graph with parameters \((5, 2, 0, 1)\), are joined by a walk but are neither equal nor adjacent.
Proof: Induct on a witnessing walk and close each two-edge segment using the zero common-neighbor count. Brouwer and Haemers, Section 9.1.4, state the result: \(\mu = 0\) makes the graph a disjoint union of complete graphs.
public theorem srg_reachable_eq_or_adj_mu_zero {V : Type*} [Fintype V]
{n k ℓ : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj]
(h : G.IsSRGWith n k ℓ 0) (v w : V) (hre : G.Reachable v w) :
v = w ∨ G.Adj v wSources
- A. E. Brouwer and W. H. Haemers, Spectra of Graphs, Springer 2012, Ch. 9 (a disconnected strongly regular graph is a disjoint union of complete graphs); C. Godsil and G. Royle, Algebraic Graph Theory, GTM 207, Ch. 10.
Uses 1
TheoremNon-principal eigenvalues of a connected non-complete strongly regular graph#✓fully proved
Let \(G\) be a finite strongly regular graph with parameters \((n, k, \ell, \mu)\): \(G\) has \(n\) vertices, every vertex has degree \(k\), any two adjacent vertices have exactly \(\ell\) common neighbors, and any two distinct nonadjacent vertices have exactly \(\mu\) common neighbors. Suppose that \(G\) is connected and not complete, and let \(A\) be its adjacency matrix over \(\mathbb{C}\). Then every eigenvalue \(x \in \mathbb{C}\) of \(A\) with \(x \neq k\) satisfies \(x^2 = (\ell - \mu) x + (k - \mu)\).
Proof: Apply the identity \(A^2 = kI + \ell A + \mu \bar{A}\), where \(I\) is the identity matrix and \(\bar{A}\) is the adjacency matrix of the complement of \(G\), to an eigenvector \(v\) for \(x\); regularity makes the coordinate sum of \(v\) zero, so \(\bar{A} v = -(1 + x) v\), and this gives the quadratic. This is the proof of Theorem 9.1.2, (ii) ⇒ (iii), in Brouwer and Haemers, Section 9.1.3.
public theorem srg_nonprincipal_eigenvalue_quadratic {V : Type*}
[Fintype V] {n k ℓ μ : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj]
[DecidableEq V] (h : G.IsSRGWith n k ℓ μ) (hconn : G.Connected)
(hncomp : G ≠ ⊤) (x : ℂ) (hx : x ≠ (k : ℂ))
(hEig : Module.End.HasEigenvalue (Matrix.toLin' (G.adjMatrix ℂ)) x) :
x ^ 2 = (((ℓ : ℂ) - (μ : ℂ)) * x + (((k : ℂ) - (μ : ℂ))))Sources
- A. E. Brouwer and W. H. Haemers, Spectra of Graphs, Springer 2012, Ch. 9, eigenvalues of strongly regular graphs; C. Godsil and G. Royle, Algebraic Graph Theory, GTM 207, Ch. 10 (eigenvalues of strongly regular graphs).
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.