Local linearity: $\lambda = 1$ forces the degree $k$ to be even

Proved

Conway99.srg_lambda_one_degree_even

by Gabewhigham · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsgraph-theorystrongly-regular-graphs

Let $g$ be a strongly regular graph on a nonempty finite vertex set with parameters $(n, k, 1, \mu)$ for an arbitrary $\mu$ , so that every edge lies in exactly one triangle. Then the degree $k$ is even.

The reason is local: for a vertex $v$ , each neighbour $w$ of $v$ has exactly one neighbour inside $N(v)$ , namely the unique common neighbour of $v$ and $w$ . Hence the graph induced on the $k$ -element set $N(v)$ is $1$ -regular, i.e. a perfect matching, and a finite graph admitting a perfect matching has an even number of vertices. Graphs with $\lambda = 1$ are called locally linear for exactly this reason; for the parameters of Conway's problem the neighbourhood of every vertex is a perfect matching on $14$ vertices, i.e. $7$ disjoint edges.

Preamble

import Mathlib.Combinatorics.SimpleGraph.StronglyRegular

open SimpleGraph

Formal statement

namespace Conway99

theorem srg_lambda_one_degree_even {V : Type*} [Fintype V] {g : SimpleGraph V}
    [DecidableRel g.Adj] {n k m : ℕ} (h : g.IsSRGWith n k 1 m) (hn : 0 < n) :
    Even k := by sorry

end Conway99

Source

Local linearity of strongly regular graphs with lambda = 1; https://en.wikipedia.org/wiki/Conway%27s_99-graph_problem and https://en.wikipedia.org/wiki/Locally_linear_graph

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by Gabewhigham · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Local linearity: λ=1\lambda = 1λ=1 forces the degree kkk to be even

Local linearity: $\lambda = 1$ forces the degree $k$ to be even