We prove a new rigorous lower bound on the critical density $\rho_c$ of the hard disk model. Specifically, we show that up to a certain density, a natural Markov chain that moves one disk at a time mixes rapidly, and that, moreover, positional correlations decay exponentially with distance. Our main tool is an optimized metric on neighboring pairs of configurations, i.e., configurations that differ in the position of a single disk: we define a metric that depends on the difference in these positions, and which approaches zero continuously as they coincide. This improves the previous rigorous bound on rapid mixing from $\rho_c \ge 1/8$ to $\rho_c \ge 0.154$, and shows that this a rigorous lower bound on the transition to the solid phase.
This is joint work with Tom Hayes.