Front progression for the East model

The East model is a one-dimensional, non-attractive interacting particle system with Glauber dynamics, in which a flip is prohibited at a site $x$ if the right neighbour $x+1$ is occupied. Starting from a configuration entirely occupied on the left half-line, we prove a law of large numbers for the position of the left-most zero (the front), as well as ergodicity of the process seen from the front. For want of attractiveness, the one-dimensional shape theorem is not derived by the usual coupling arguments, but instead by quantifying the local relaxation to the non-equilibrium invariant measure for the process seen from the front. This is the first proof of a shape theorem for a kinetically constrained spin model.