The joint critical Ashkin–Teller current limit

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Identifies the joint scaling limit of Ashkin–Teller heights and both complete current-cluster collections throughout the critical line, including the four-state Potts endpoint. In bounded Jordan domains with admissible lattice approximations and wired primal/free dual boundaries, the height converges to the predicted Gaussian free field, and the clusters to canonical recursive sets of that same field, retaining every nesting depth.

The release has no Lean statement for this family, so there is no formal statement to compare with the result described above.

One current paper; one replaced by a later edition.

What the papers state

Theorem 2.3 (Joint critical-line limit)

In The joint scaling limit of critical Ashkin-Teller currents

Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.

For every fixed pair J>0, U\le J with \sinh(2J)=e^{-2U}, every bounded Jordan domain D, and every admissible polygonal approximation as defined in Section 2.1,

\bigl(H_\delta,\cC_\delta^{\rm w},\cC_\delta^{\rm f}, C_{\partial,\delta}\bigr) \ \xrightarrow[\delta\downarrow0]{\mathrm{law}}\ \left(\frac{h}{\pi\sqrt g},\cC^{\rm w},\cC^{\rm f}, \TVS{a}{a}(h)\right).

The height converges in H^s_{\rm loc}(D) for every s<-1. Each cluster collection converges in the matching topology just defined, and the distinguished component converges in Hausdorff topology. The continuum collections are locally finite above every positive diameter. All convergences are joint, and the same GFF determines both continuum collections.

Theorem 6.1 (Flat-domain limit)

In The joint scaling limit of critical Ashkin-Teller currents

Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.

Let U_\delta be a single deterministic flat chamber, or a finite mesh-dependent union of independent chambers with pairwise disjoint interiors, as above. Suppose F_\delta converges in Hausdorff distance to F, and set U=B_0\setminus F. Then

K_\delta\ \Longrightarrow\ h_U/a \quad\text{in }H^s_{\mathrm{loc}}(U),\qquad s<-1,

where the restrictions of h_U to the components of U are independent zero-Dirichlet GFFs with logarithmic singularity -\log|x-y|. All finite joint smooth-test moments with supports in U converge. Different limiting components are independent even if their discrete precursors were the same chamber. Either wall parity and either atomic or interpolated smearing gives the same limit. The fields extended by zero off U_\delta are uniformly tight in H^s_{\mathrm{loc}}(B_0) for every s<-1.

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole, the closer match to the description’s wording first. The atlas has not reviewed either choice.

Reported proof verification: The release has no Lean statement for this family. The papers are available to read and assess.
Papers and explanations: One current paper, readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

The joint scaling limit of critical Ashkin-Teller currents

Undated, current edition.

Read it here PDF

This version corrects the transmission and boundary-collar arguments, replaces excursion convergence with a signed-loop-soup/GMC argument tied to the same limiting field, and updates the companion-paper citation; see the previous version.

Earlier editions: The-joint-scaling-limit-of-critical-Ashkin-Teller-currents-September-25-2026

For each fixed point on the critical Ashkin–Teller line, including the four-state Potts endpoint, we prove the conjectured joint scaling limit of the height and both current-cluster collections in every bounded Jordan domain, for every admissible polygonal approximation. The height converges to a Gaussian free field with the predicted coupling constant, and the clusters converge to canonical recursive two-valued local sets of that same field. The joint limit includes all nesting depths and the distinguished wired boundary cluster.

Previous editions

The joint scaling limit of critical Ashkin–Teller currents previous edition, PDF

Lean statements

The release has no Lean statement for this family. Its papers remain available to read, and contributors can propose a formal statement of a result. Suggest a change

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

The release contains no Lean statement for this family, so there is no formal statement to compare with OpenAI’s description.

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Papers elsewhere in the release that this family’s papers cite

The Gaussian free field limit of the balanced six-vertex model with variance multiplier 1/arcsin(c/2)Current edition; no accompanying Lean statement Family Gaussian free field limits throughout the balanced six-vertex regimeCited by The joint scaling limit of critical Ashkin-Teller currents.
The Gaussian free field limit of integer Lipschitz heights with two-arc boundary dataCurrent edition; no accompanying Lean statement Family Gaussian fields and interfaces for triangular-lattice Lipschitz heightsCited by The joint scaling limit of critical Ashkin-Teller currents.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

32 references in The joint scaling limit of critical Ashkin-Teller currents

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanation Suggest a source attribution Suggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Solid publication, could lead to tenure”. The page says that nothing on it is verified.
Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Identify the theorem the catalogue describes

Family 233 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

State the result in Lean

Family 233 The release has no Lean statement for this family. Open the form