Local linearity: a strongly regular graph with $\lambda = 1$ has no $K_4$

A strongly regular graph with $\lambda = 1$ is $K_4$-free.

Let $G$ be strongly regular with parameters $(n, k, 1, \mu)$, so that any two adjacent vertices have exactly one common neighbour. Then $G$ contains no clique on four vertices:

Indeed, if $a, b, c, d$ were four pairwise adjacent vertices, then $c$ and $d$ would be two distinct common neighbours of the adjacent pair $a, b$, contradicting $\lambda = 1$.

For Conway's 99-graph problem this says that a hypothetical $(99,14,1,2)$ graph has clique number exactly $3$: its maximal cliques are the $231$ triangles that form the lines of the associated partial linear space. The statement is the local-linearity constraint that a search over such graphs must respect, and it holds for every parameter set with $\lambda = 1$, in particular for the realised cases $(9,4,1,2)$ and $(243,22,1,2)$.

Formalization note. The vertex type is an arbitrary finite type with decidable equality, and the parameters $n$, $k$, $\mu$ are unconstrained; only $\lambda = 1$ is used.