Faster-than-power-law decay of order parameter correlations in the two-dimensional RP$^2$ model: a rigorous result by vibe-proving
Masaki Oshikawa
cond-mat.stat-mech
Oct 30, 2026 · v1
hep-lat math-ph
TL;DR
AI-generated proof of super-polynomial correlation decay in RP^2 and RP^3 lattice models, fully formalized in Lean 4 against pinned Mathlib and archived on Zenodo.
Abstract
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 $π_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_β\exp{(-c_β[\log(2+r)]^2)}$ for any finite inverse temperature $β\ge0$, with positive constants $C_β$ and $c_β$ depending only on $β$. 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 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.
Problem
Whether the two-dimensional RP^2 (and RP^3) director model on the square lattice has a critical phase with power-law quadrupolar correlations, possibly driven by Z_2 vortices, has been an open and contested question.
Approach
An AI system (ChatGPT 6 Astra) generated a rigorous proof of an upper bound on the quadrupolar two-point function, building on a prior Lean-verified O(n) exponential-decay result. The AI was then asked to write a complete Lean 4 formalization against a pinned Mathlib commit. That formalization was cross-checked by separate AI instances and by an automated verification registry. A heuristic effective-theory argument, which is not formalized, interprets the bound physically.
Results
The authors prove, and verify in Lean, that |C_Q(r)| ≤ C_β exp(-c_β (log(2+r))^2) for every finite β, so correlations decay faster than any power of r. They also prove a high-temperature exponential bound. The heuristic argument suggests, without proof, that Z_2 vortices are unbound at all nonzero temperatures.
