Asymmetric coloring of locally finite graphs and profinite permutation groups: Tucker's Conjecture confirmed

An asymmetric coloring of a graph is a coloring of its vertices that is not preserved by any non-identity automorphism of the graph. The motion of a graph is the minimal degree of its automorphism group, i.e., the minimum number of elements displaced by any non-identity automorphism. In this paper we confirm Tom Tucker's "Infinite Motion Conjecture" that connected locally finite graphs with infinite motion admit an asymmetric 2-coloring. We infer this from the more general result that the inverse limit of a sequence of finite permutation groups with disjoint domains, viewed as a permutation group on the union of those domains, admits an asymmetric 2-coloring. The proof is based on the study of the interaction between epimorphisms of finite permutation groups and the structure of the setwise stabilizers of subsets of their domains.
Comment: V.2 updates: Choi 1972 ref. added, Sec. 8.3 (Mathieu groups) updated, question about $M_{24}$ deleted from "Open questions." New material: New Sec. 14 added, incl. two conjectures. Minor changes made for improved clarity throughout the paper. None of the updates affects the main results or their proofs