Berlekamp–van Lint–Seidel graph: existence at
ProvedConway99.srg_243_22_1_2combinatoricsgraph-theorystrongly-regular-graphs
There exists a strongly regular graph with parameters .
The Berlekamp–van Lint–Seidel graph is such a graph: its vertices are the cosets of the perfect ternary Golay code in , with two cosets adjacent when their difference contains a vector of Hamming weight . Equivalently it is the Cayley graph on whose connection set consists of the syndromes of the weight-one vectors, where are the columns of a parity check matrix of the code. It is the largest member of the family , known to exist, and the only known example that is not the trivial one on vertices.
Preamble
import Mathlib.Combinatorics.SimpleGraph.StronglyRegular open SimpleGraph
Formal statement
namespace Conway99
theorem srg_243_22_1_2 : ∃ (α : Type) (_ : Fintype α) (g : SimpleGraph α)
(_ : DecidableRel g.Adj), IsSRGWith g 243 22 1 2 := by sorry
end Conway99Source
E. R. Berlekamp, J. H. van Lint, J. J. Seidel, 'A strongly regular graph derived from the perfect ternary Golay code', in: A Survey of Combinatorial Theory, North-Holland, 1973, pp. 25-30; see also https://en.wikipedia.org/wiki/Berlekamp%E2%80%93van_Lint%E2%80%93Seidel_graph
Human review
Confirmed by the mission captain (proposal self-audit).