ESSENTIAL SINGULARITY OF THE CORRELATION LENGTH IN THE PLANAR XY MODEL
A self-contained account of the BKT essential singularity for the
nearest-neighbor cosine XY model on the square lattice

====================================================================
ABSTRACT
====================================================================

Put a unit-vector spin on each site of the square lattice, and let
neighboring spins prefer to point the same way with a Gibbs weight
proportional to exp( b cos(theta_u - theta_v) ), where b is the
inverse temperature.  There is a critical inverse temperature b_c in
(0, infinity).  Below b_c, the spin-spin correlations decay
exponentially along an axis with rate m(b) > 0, and xi(b) = 1/m(b) is
the correlation length in the massive phase.  Then

        lim_{b -> b_c^-}  sqrt(b_c - b) * log xi(b)  =  A_XY ,

with A_XY a finite, strictly positive constant that depends on the
model and on the choice of inverse temperature normalization, but not
on b.  In other words xi(b) grows like exp( A_XY / sqrt(b_c - b) ),
faster than any power of 1/sqrt(b_c - b) but slower than any
exponential of a positive power of it.  This is the celebrated
Berezinskii-Kosterlitz-Thouless (BKT) essential singularity.

We prove this for the original cosine XY model with the edge coupling b,
without any modification or approximation of the model.

====================================================================
READER'S GUIDE
====================================================================

Read Sections 1 and 2 first.  Section 1 states the theorem precisely and
sketches the structure of the proof.  Section 2 introduces the finite-
graph height laws and the comparison principles that underlie
everything else.

Sections 3 through 6 give the full proof.

  Section 3 (analytic entry):      at each scale s the model is described
                                   by a small activity in an explicit
                                   renormalization.  This uses the
                                   critical input from the companion
                                   paper [X], whose statements we
                                   recall as hypotheses H3.1-H3.4.

  Section 4 (temperature trajectory): the physical temperature per-
                                   turbation drives the activity away
                                   from criticality along a definite
                                   direction with a positive slope P.

  Section 5 (coefficient profile): turns the trajectory into a
                                   statement about the height
                                   coefficient on logarithmic scales.
                                   Below T = pi/sqrt(3P) the height
                                   coefficient equals the critical
                                   value a = 8 pi; above T it is zero.
                                   No value at the single scale T is
                                   needed.

  Section 6 (mass completion):     pinned covariance below T forces a
                                   lower bound on xi; a circulation
                                   estimate above T gives an upper
                                   bound.  The two bounds coincide at
                                   the same logarithmic scale, and
                                   A_XY = (log L) * T where L is the
                                   fixed block ratio in the
                                   renormalization.

All inputs imported from the two companion papers are stated as
explicit hypotheses in their sections.  Everything else is proved
from first principles.

Conventions.
  + inverse temperature is the coefficient b in the edge factor;
  + heights take values in 2 pi Z modulo common translations;
  + logarithms with subscript L mean log base L; plain log is natural;
  + O() and o() always refer to the limit named in the surrounding
    proposition;
  + constants written C, c, C_I, etc., are finite, positive, and
    uniform in whatever the surrounding statement permits; they are
    allowed to change from line to line.