Source and verification
This article explains family 216 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.
Overview
The planar XY model has circle-valued spins and a transition driven by marginal scale evolution. Family 216 connects its critical power law, logarithmic correction, spin field, and rapidly diverging correlation length. Some companions explicitly use field-limit and renormalization inputs supplied elsewhere in the family.
π·οΈ Preliminaries: correlations, length scales, and dual heights
Write a spin as , with . The square-lattice cosine model has Gibbs density proportional to
Let be the infinite-volume free-boundary expectation of , taking the box limit before . In the massive phase define the inverse correlation length and its reciprocal by
A Gaussian free field (GFF) is specified through Gaussian averages against test functions and the inverse-Laplacian covariance. It has no pointwise values in two dimensions. Expressions such as its imaginary exponential require their own renormalization.
Fourier expansion of the XY edge weight gives modified Bessel coefficients . Integrating the angles imposes a conservation law on integer edge currents, which can be represented by dual heights. Spin insertions introduce nontrivial circulation in this representation. Consequently, convergence of smooth height averages alone does not determine spin correlations at microscopic insertion points.
π·οΈ The claims, ordered by strength
The critical-exponent companion claims . (OpenAI, 2026) The logarithmic companion strengthens this to
An exponent with an error permits arbitrary slowly varying factors; the positive amplitude statement is substantially sharper. (OpenAI, 2026b)
Approaching from the massive side, another companion claims
Neither the lattice amplitude nor is asserted to be a universal numerical constant. (OpenAI, 2026a)
For a square of radius with boundary angles fixed to zero, let be the center magnetization. Its dedicated companion gives, under specified critical-height, local-renormalization, and spin-field inputs, the asymptotic . (OpenAI, 2026a) The spin-field companion uses its Bessel-height and puncture inputs to identify a normalized imaginary exponential of a zero-boundary GFF, including distributional convergence and moments. (OpenAI, 2026e)
The height-universality paper also treats discrete Gaussian heights throughout the rough regime and low-temperature Villain spin fields. These quadratic or periodic-Gaussian models supply related mechanisms; their conclusions must not be silently substituted for a proof for the cosine model at criticality. (OpenAI, 2026a)
π·οΈ Why a marginal flow produces a logarithm
Here is the main calculational mechanism in the logarithmic companion. Fix a block ratio , so physical length corresponds to scale steps. The controlled critical gradient coordinate satisfies
The source compares center insertions at successive geometric sizes using the same intermediate scale history. After cancelling source-independent factors, its estimate takes the form
where the remainder consists of absolutely summable errors and convergent telescoping Green-function corrections. Summing the constant produces ; summing produces . Exponentiation therefore yields the center logarithm with power and a finite nonzero amplitude. A positive limiting comparison doubles that power to .
The harmonic sum is elementary. The hard work is deriving the coordinate coefficient, preserving the marked insertion during blocking, and making the remaining errors summable. An error merely tending to zero at each step would not suffice for a limiting amplitude.
π·οΈ The essential singularity and the continuum field
Near criticality, the leading two-coordinate flow separates trajectories by a parameter of order . The trajectory stays near the critical regime for order scale steps. Since length grows exponentially with the number of steps, this predicts the displayed essential singularity. The manuscript must additionally prove a nonzero response to changing temperature and relate exit from the scale regime to the physical correlation length.
For the spin field, the proof first keeps punctures at positive macroscopic radius. Annular conditional kernels compare the exterior field with the microscopic insertion, and exact center normalization removes the shared microscopic factor. This order of limits prevents a Gaussian height theorem from being applied where it gives no control.
π·οΈ Key steps and proof outlines
Locating the marginal coefficient without assuming continuity
The critical-exponent manuscript constructs a height-covariance coefficient for the original dual law and proves the alternative
When it is positive, upper and lower magnetic estimates identify the spin power exponent as . These estimates keep opposite spin insertions through the height construction; a theorem only about smooth height averages would not supply them.
Two arguments identify the coefficient at the threshold. The imported polynomial lower bound on critical spin correlations excludes , since the zero-coefficient case gives arbitrarily fast polynomial decay. To exclude , the source proves an openness theorem: such a value would imply positivity of on a whole neighborhood of , including points on the massive side.
The openness proof does not assume continuity of . It first strengthens the law by adding positive precision on block averages. That gives a Gaussian large-field bound while retaining a coefficient above . Entry into the controlled activity norm and stability of the gapped flow then give a torus variance diagnostic, which transfers positivity back to the original model. Hence and the exponent is . (OpenAI, 2026d)
A ratio estimate must control the microscopic insertion relatively
The center-magnetization companion compares size with size after blocking both through a common history. Source-independent partition factors and the common microscopic magnetic scalar cancel exactly in their logarithmic ratio. The terminal calculation leaves the Green-energy increment multiplied by the running gradient coordinate, plus an error bounded by
where is the scale index and an auxiliary terminal-window size. Choosing of order makes the first two terms and , both summable. The critical trajectory then gives
for some and .
Define the centered logarithm
Its increments on the geometric sequence are absolutely summable, so it converges to a finite real value. Positivity of the finite-volume magnetization makes exponentiation legitimate and gives a positive finite amplitude.
There is still a step from geometric sizes to all integers. For , extract a subsequence with . The stated regular-variation input gives . This cancels the corresponding change in the power normalization, while the log-log correction changes by . Thus every subsequence has the same limit for . The logarithmic-correlation companion combines its controlled insertion comparison with a positive limit for , giving the doubled logarithmic exponent. The center companionβs additional inputs remain assumptions of that manuscript. (OpenAI, 2026b) (OpenAI, 2026e)
Solving the bottleneck flow and relating it to physical length
Put and . The essential-singularity manuscript proves a strictly positive temperature-response constant . After matching the perturbed trajectory to the critical one, rescale its two coordinates by and time by . The limiting equations are
They preserve . The matched left-end behavior fixes this invariant to , with . The relevant solution is
Direct differentiation checks the equations and the common behavior near zero. The second pole occurs at . The source controls the discrete error and the irrelevant coordinates to show that exit from a fixed small-activity region occurs at indices with .
An exit time in renormalization coordinates is not yet a spin correlation length. Before exit, separated height covariance supplies a lower bound on that length. Beyond the transition in the height profile, the source proves arbitrarily strong polynomial spin decay. It then uses the finite-size criterion
For its proof, repeatedly apply the boundary correlation inequality in translated squares. Each step moves the center by at most , and multiplies the total bound by . A target at distance therefore costs at least factors. Taking the logarithmic rate proves the criterion. Applying it at for every , then letting , matches the lower bound. This yields
The limit uses the axis mass with the prescribed thermodynamic-limit convention. (OpenAI, 2026c)
From separated spin correlations to a random distribution
The spin-field proof first identifies correlations at separated insertions. Extending them through collisions and obtaining a law requires uniform absolute moments. For a finite positive-boundary XY system and nonnegative weights, put
Rotate all spins by an independent uniform angle and let . The imported LeeβYang theorem places the zeros of its Laplace transform on the imaginary axis. Its product representation and give
The imaginary part has the same law, so Chernoffβs bound yields , hence . Complex test weights are split into four nonnegative parts.
For a square of side , the normalized field has second moment at most . The nonnegative current expansion proves positivity of every signed lattice spin correlation. This lets the restricted collision sum be bounded by full box moments after replacing test weights by their absolute values. Cover configurations with a colliding pair by enlarged squares. HΓΆlderβs inequality and the absolute-moment bound make the contribution of each square . After the mesh limit, the total collision contribution is and vanishes. Repeated sites are included. Away from collisions, the separated-point theorem gives ordinary Riemann-sum convergence. This proves convergence of all smeared mixed moments; the moment bounds identify their laws, and local Sobolev estimates give tightness.
The broader BKT-universality companion carries out a related transfer for Villain spins using exact current duality, marked defects, and a location-independent amplitude. That is a separate model-specific construction: the common moment-and-collision argument becomes available only after each modelβs signed correlations and normalizations have been established. (OpenAI, 2026f) (OpenAI, 2026a)
See Also
- Family 215 concerns sphere-valued spins with at least three components and a different mass behavior.
- Family 225 gives a height-field limit with an explicitly normalized covariance.
π·οΈ Manuscripts and verification scope
- The critical logarithmic correction for the planar XY model β pinned manuscript and companion source.
- Critical Center Magnetization in the Planar XY Model β pinned manuscript and companion source.
- The Critical Spin Field of the Planar XY Model β pinned manuscript and companion source.
- Essential Singularity of the Correlation Length in the Planar XY Model β pinned manuscript and companion source.
- The critical correlation exponent of the planar XY model β pinned manuscript and companion source.
- BKT universality for height and planar spin fields β pinned manuscript and companion source.
No family scope page was present at lean/docs/216.md in the pinned snapshot. This does not establish that all related formalization code is absent. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.
OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.