Automorphism extension: an involution preserving the colours on $W$ and the colour degrees of $v$ preserves the colour of the pair with $e \notin W$

This is a general counting lemma for colourings of pairs: if an involution $J$ of a set $W$ keeps the colours of the pairs in $W$, and a point $v \in W$ and its image $J(v)$ have the same colour degrees in $W \cup \{e\}$, then the pairs $(v, e)$ and $(J(v), e)$ have the same colour.

Let $\alpha$ and $\gamma$ be types with decidable equality (points and colours), and let $\mathrm{col} : \alpha \to \alpha \to \gamma$ give each ordered pair $(x, y)$ a colour $\mathrm{col}(x, y)$. Let $W$ be a finite subset of $\alpha$, let $e \in \alpha$ with $e \notin W$, and let $J : \alpha \to \alpha$ satisfy, for all $x, y \in W$:

1. $J(x) \in W$;
2. $J(J(x)) = x$;
3. $\mathrm{col}(J(x), J(y)) = \mathrm{col}(x, y)$.

Let $v \in W$, and suppose that $v$ and $J(v)$ have the same number of neighbours of each colour in $W \cup \{e\}$: for every colour $i \in \gamma$,

Then

In the mission the lemma is applied with $W$ the central neighbourhood without its endpoint, $e = 2m + 1$, $J(x) = 2m - x$ and $\mathrm{col}(x, y) = c(|x - y|)$; the saturation theorem supplies the equal colour degrees, and the conclusion is the forced reflection.

Formalization Note. The colour function takes ordered pairs and need not be symmetric; the degrees of $v$ and $J(v)$ are counted with $v$ and $J(v)$ as first argument, and the pair of a point with itself is not counted. The types $\alpha$ and $\gamma$ are arbitrary (Lean Type* with DecidableEq), and $W$ is a Finset. The conditions on $J$ are required only on $W$. The case $J(v) = v$ is allowed, and the conclusion is then immediate.