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

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.

🐻  OpenAI 2026a. BKT universality for height and planar spin fields.
🐻  OpenAI 2026b. Critical Center Magnetization in the Planar XY Model.
🐻  OpenAI 2026c. Essential Singularity of the Correlation Length in the Planar XY Model.
🐻  OpenAI 2026d. The critical correlation exponent of the planar XY model.
🐻  OpenAI 2026e. The critical logarithmic correction for the planar XY model.
🐻  OpenAI 2026f. The Critical Spin Field of the Planar XY Model.