Masaki Oshikawa

math-ph — Mathematical Physics

Faster-than-power-law decay of order parameter correlations in the two-dimensional RP2 model: a rigorous result by vibe-proving

Contributed by Masaki Oshikawa

We consider the $RP^2$ model on the two-dimensional square lattice with nearest-neighbor interactions. It is obtained by replacing the spin in the standard classical Heisenberg model with a director, which does not distinguish two opposite directions. Unlike the standard classical Heisenberg model or the O(3) nonlinear sigma model, the $RP^2$ (and its cousin $RP^3$) model allows point vortex defects classified by $\pi_1(RP^2)=Z_2$ in two dimensions. It is tempting to expect the $Z_2$ vortices to induce a phase transition analogous to the well-established Berezinskii-Kosterlitz-Thouless transition in the O(2) model (XY model) in two dimensions. Indeed, the possibilities of a critical phase or a critical point with power-law correlations of the order parameter in the $RP^2$ and $RP^3$ models have been discussed in the literature. However, the challenging nature of the problem has prevented a definitive conclusion on the phase diagram so far. In this paper, we report a rigorous mathematical proof by Artificial Intelligence (ChatGPT 6 Astra) that the absolute value of the two-point correlation function of order parameters at distance $r$ in the $RP^2$ and $RP^3$ models on the two-dimensional square lattice is bounded above by $C_\beta \exp\{-c_\beta[\log(2+r)]^2\}$ for any finite inverse temperature $\beta\ge0$, with positive constants $C_\beta$ and $c_\beta$ depending only on $\beta$. Namely, the correlation function decays faster than any power of $r$. The proof is formalized and verified in Lean; the formalization is publicly available at \href{https://doi.org/10.5281/zenodo.23548847}{doi:10.5281/zenodo.23548847}. A heuristic argument based on a one-parameter effective theory ansatz at large distances combined with the rigorous correlation bound suggests (but does not prove) that the $Z_2$ vortices are always unbound at any nonzero temperature.