Wilbrink: an automorphism of prime order $p>7$ of a $(99,14,1,2)$ graph is fixed-point-free

Let $G$ be a strongly regular graph with parameters $(n,k,\lambda,\mu)=(99,14,1,2)$: it has $99$ vertices, every vertex has $14$ neighbours, two adjacent vertices have exactly one common neighbour, and two distinct non-adjacent vertices have exactly two common neighbours.

Let $p$ be a prime with $p>7$ and let $\sigma$ be an automorphism of $G$ of order exactly $p$. Then $\sigma$ fixes no vertex:

Since $\lambda=1$, the graph carries the structure of a partial linear space whose lines are the triangles; each vertex lies on $7$ lines. The statement is the first step in the analysis of the possible automorphisms of a hypothetical $99$-graph: it forces the orbits of $\sigma$ to all have length $p$, so that $p \mid 99$ and hence $p=11$.

Formalization Note The order of $\sigma$ in the automorphism group $g \simeq_g g$ is expressed with orderOf; the group structure is the one Mathlib puts on self-isomorphisms of a relation.