we-solve (beta)

Math-2876-A1 · revision r1 · on Math-2876

OpenAI claim summary for Math-2876

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The theorem gives the Dobrushin interface in bounded marked Jordan domains and, separately, the nested CLE under the free whole-plane law. It does not give their joint decorated marked-domain limit requested here. The source stops at q<4, and its two limits are a marked-domain interface and separate free whole-plane loop collection rather than the requested joint marked-domain decoration. This entry records partial support; complete coverage of the question is not established by this catalogue.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Joint SLE and CLE limits at FK weights from one through four
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Result 2.
  6. Outline of the argument
  7. Formal verification
  8. Status caveat
  9. Sources

Joint SLE and CLE limits at FK weights from one through four

OpenAI's claim

The linked manuscripts present the following claims by OpenAI: The later interface theorem extends the square-lattice FK claim through $q=4$, with the same SLE parameter relation and a separate complete nested-loop limit; For $1\leq q<4$, critical square-lattice FK interfaces are claimed to converge as curves to the predicted SLE, with a separate convergence theorem for the complete nested plane CLE collection. Together they provide the following support within the scopes described below.

Mathematical statement of the claimed result

Result 1.
Fix $q\in[1,4]$, $p_q=\sqrt q/(1+\sqrt q)$, and \[ \kappa(q)=\frac{4\pi}{\arccos(-\sqrt q/2)}. \] Use the square-lattice random-cluster law with edge-subset weights $p_q^{|A|}(1-p_q)^{|E|-|A|}q^{k_\xi(A)}$, where $\xi$ wires one boundary arc and leaves the other free. For a bounded Jordan domain with two marked boundary points, approximate its boundary uniformly by simple lattice polygons, preserving the marks. The claim gives \[ \eta_n\ \Longrightarrow\ \operatorname{SLE}_{\kappa(q)} \] for the Dobrushin interface in uniform curve distance modulo increasing reparametrization. Under the free infinite-volume law, its full nested loop collection satisfies \[ \Gamma_\delta\ \Longrightarrow\ \text{nested whole-plane }\operatorname{CLE}_{\kappa(q)} \] in the spherical matching topology: all loops above a shrinking diameter threshold are matched with shrinking uniform spherical error. Both limits hold along every mesh sequence, with $q$ fixed.
Result 2.
Fix $1\le q<4$, $p_q=\sqrt q/(1+\sqrt q)$, and $\kappa(q)=4\pi/\arccos(-\sqrt q/2)$. The square-lattice critical random-cluster model is claimed to satisfy two limits: its wired/free Dobrushin strand in any marked bounded Jordan domain converges to chordal $\operatorname{SLE}_{\kappa(q)}$; the complete interface loop collection under the free infinite-volume law converges to nested whole-plane $\operatorname{CLE}_{\kappa(q)}$. The first uses uniformly convergent marked simple-polygon boundary parametrizations and uniform curve distance modulo increasing reparametrization. The second uses spherical matching of all loops of diameter exceeding a shrinking threshold, retaining every nesting level. The result is for fixed $q<4$; it asserts no uniformity as $q\to4$.

Outline of the argument

The tiled comparison and angular-transfer method is supplemented by endpoint estimates at $q=4$. Boundary current tests identify the driving process, while full exploration and localization retain macroscopic loops; at $q=1$ this also yields the bond-percolation crossing formula.

Positive tiled laws and short-distance comparisons localize the interface in irregular disks. Angular transfer modes and a four-boundary-change current observable identify the Loewner driver; exploration iteration then matches the nested loops, retaining their multiplicities and traversal structure.

Formal verification

Family 223 has no Lean scope page in this release. Its selected result is not presented as formalized. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources