= Solution
An exact-count form of the <Hanf locality lemma> is as follows. For every <quantifier rank> $q$, put $r=3^q$. If finite relational structures $A,B$ admit a bijection $f:A\to B$ such that
$$
(N_r^A(a),a)\cong(N_r^B(f(a)),f(a))\qquad\text{for every }a\in A,
$$
then $A$ and $B$ agree on every <first-order sentence> of <quantifier rank> at most $q$. Equivalently, they have the same number of occurrences of every marked radius-$r$ one-point neighbourhood type. The individual local isomorphisms need not be restrictions of $f$.
A bounded-degree threshold version permits the type counts to be different when both exceed a sufficiently large bound depending on the degree bound and $q$. We need only the exact-count form. Its locality content is that sufficiently large matching neighbourhoods and their multiplicities determine all sentences up to the prescribed <quantifier rank>.
Back to article page
