Only five feasible degrees:
ProvedConway99.srg_lambda_one_mu_two_degree_memcombinatoricsgraph-theorystrongly-regular-graphs
Let be a strongly regular graph with parameters on a finite vertex set with at least two vertices. Then
Together with the counting identity these degrees correspond to the parameter tuples (the triangle , where the condition on non-adjacent pairs is vacuous), , , , and . Beyond the complete case, the restriction comes from the integrality conditions: the adjacency matrix has eigenvalues and the two roots of , so must be a perfect square , and the multiplicities of the two non-principal eigenvalues are integers only when divides . This is the classical argument showing that the family , contains only five non-degenerate feasible parameter tuples, two of which are realised and three of which — including — are open.
Preamble
import Mathlib.Combinatorics.SimpleGraph.StronglyRegular open SimpleGraph
Formal statement
namespace Conway99
theorem srg_lambda_one_mu_two_degree_mem {V : Type*} [Fintype V] {g : SimpleGraph V}
[DecidableRel g.Adj] {n k : ℕ} (h : g.IsSRGWith n k 1 2) (hn : 1 < n) :
k = 2 ∨ k = 4 ∨ k = 14 ∨ k = 22 ∨ k = 112 ∨ k = 994 := by sorry
end Conway99Source
Classical feasibility (integrality) conditions for strongly regular graphs with lambda = 1, mu = 2; the list of five feasible parameter tuples is as recorded in https://en.wikipedia.org/wiki/Conway%27s_99-graph_problem (section 'Related graphs'), citing Makhnev & Minakova, Discrete Math. Appl. 14 (2004), no. 2
Human review
Confirmed by the mission captain (proposal self-audit).