The proof in the paper. For each symmetric $R ⊆ Π^s × Π^s$ let $φ_R(z̄ x, y)$ express distance at most $r$ in $G ⊕ (z̄, R)$, using the quantifier-free edge formula of the flip. Let $k$ exceed all the bounds on $φ_R$-patterns and put $t = Q(k · 9^s)$. For every $R$, every $N ∈ {E, ¬E}$ and every base $b̄ ∈ A^k$ fix a $(φ_R, N)$-pattern of maximum height (less than $k$), and let $A*$ consist of $A$ and all their grid points. If a ball $B = Ball^H_r[v]$ in $H = G ⊕ (p̄, R)$ avoids $A*$ but realizes more than $t$ atomic types over $A$, the matching theorem gives atomically matched tuples in $B$ and $A$ of length $k · 9^s$. By pigeonhole $k$ of the pairs have the same pair of atomic types over $p̄$, so on them $H$ agrees with $G$ or with its complement, and this yields $N$ such that the tuple $w̄$ from $A$ and the tuple ū from $B$ satisfy $N(wⱼ, uⱼ)$ and $¬N(wⱼ', uⱼ)$ for $j < j'$. Then $p̄ v$ and ū extend the chosen pattern with base $w̄$ by a row, as ū lies in $B$ and the old grid points do not, contradicting maximality.

The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.