 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 thatthen $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.