{c}

For a finite relational signature and quantifier rank $q$, matching the numbers of all marked radius-$3^q$ one-point neighbourhood types suffices for two finite structures to satisfy the same first-order sentences of rank at most $q$. Equivalently, a bijection can match the isomorphism types of these marked neighbourhoods point by point. On bounded-degree structures, a threshold version permits large neighbourhood-type counts to differ once both exceed a fixed bound. Long cycles of equal total size give useful exact-count applications.


 Hanf locality lemma (source code)