Source and verification
This article explains family 226 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
Superposing two independent dimer coverings produces loops. Family 226 claims that the complete Temperleyan half-plane ensemble converges to nested CLE₄ as actual curves. The main issue is recovering excursions and traversal order that topological observables can miss.
🏷️ Preliminaries: dimers and the half-plane law
A dimer covering is a perfect matching: every vertex belongs to exactly one selected edge. Superpose two independent coverings. At each vertex there are two incident selected edges, counting multiplicity, so the components are doubled edges or alternating even cycles. Delete doubled edges and retain the cycles as unrooted, unoriented loops.
The manuscript works on the square lattice in with a specific Temperleyan law. Finite approximations use suitable lattice polygons with one boundary root vertex deleted. Their uniform matching laws converge as the polygons exhaust the half-plane and the root escapes to infinity. This boundary prescription is part of the model.
A nested conformal loop ensemble starts with the usual outermost CLE and recursively samples the corresponding ensembles inside its loops. Keeping only outermost loops would omit most of the target object.
🏷️ What convergence of loops means
To include the whole half-plane, map it into the unit disk using
Loop distances are measured after this fixed compactification. For parametrized loops in the closed disk, put
where ranges over circle homeomorphisms in either orientation. Passing to zero-distance equivalence permits pauses without forgetting the ordered traversal.
Two collections are close if their loops can be partially matched so that every loop above a small diameter threshold is matched to a nearby loop, while all unmatched loops are small. Multiplicities are retained. The diameter threshold is measured in the compactified disk, which also controls behavior near infinity.
Curve-level half-plane limit
The manuscript claims full-mesh convergence of the complete Temperleyan double-dimer loop ensemble to nested in this matching topology. Every macroscopic loop is represented as an unparametrized curve, with all nested generations retained. (OpenAI, 2026)
This statement is stronger than identifying the distribution of how many loops separate a few marked points.
🏷️ Why puncture data are insufficient
Consider a loop with a long thin excursion leaving its main body and returning almost along the same route. If a fixed finite set of marked points misses that excursion, the loop surrounds the same marked points before and after the excursion is removed. Yet the two curves can remain far apart in uniform distance.
Even convergence of traces as sets can miss repeated traversals of the same limiting segment. A curve topology therefore requires both a modulus of continuity after reparametrization and a mechanism excluding excursions that cancel in the tested topological observables.
This is the logical gap the source’s new geometric estimates are designed to close. A field limit or a loop-separation formula alone does not fill it.
🏷️ The two geometric estimates
The first estimate bounds the total number of disjoint traversals of a fixed-width slab, counting repeated traversals by the same loop. Large numbers of crossings would force a curve to oscillate rapidly. Controlling them supplies macroscopic loop-count bounds and tightness of parametrized representatives.
The second estimate retains signed crossings of arcs through the slab. The sign records crossing direction. On a shrinking transverse interval, the estimate rules out a subarc having a nonzero signed count inconsistent with its entire loop, and rules out simultaneous nonzero contributions from distinct loops in the relevant configuration. This prevents a long excursion from disappearing through cancellation against a return arc.
Both estimates come from a transfer matrix that counts matching configurations column by column. A boundary state records dimers crossing the current seam. After an occupancy change of variables, it becomes a particle configuration, and the transfer operator reduces to combinations of a one-particle operator.
Changing the particle number substantially incurs a quadratic spectral penalty, controlling many traversals. A localized two-particle insertion involves small minors of an interval projection; delocalized transverse modes make these contributions small as the interval shrinks. The proof must turn these signed matrix expressions into probability bounds with the correct boundary normalization.
🏷️ Completing the identification
Traversal estimates give subsequential compactness in the curve-matching topology. Localized signed-crossing estimates show that a subsequential curve cannot carry invisible macroscopic pieces. The previously available finite-puncture observables can then identify that geometric limit with CLE₄. Applying the argument throughout the nested collection retains every generation, and uniqueness of the identified law upgrades subsequential convergence to the full mesh limit.
The order matters: first obtain a geometric object with sufficient tightness, then prove that the observables distinguish it. Treating topological observables as already determining arbitrary curves would bypass the principal new obligation.
🏷️ Key steps and proof outlines
The new estimate must detect geometry that ordinary loop-separation observables cannot see. The proof builds a signed transfer observable, makes its complete color sum nonnegative by carefully chosen cap weights, and then turns its small expectation into a probability bound (OpenAI, 2026).
A quadratic spectral penalty controls repeated traversals
For a rectangle with transverse sites, the one-particle transfer has singular modes with factors , where
The corresponding orthonormal mode vectors have coordinates bounded by . Many-particle propagation multiplies the factors of the occupied modes. Moving particles across the preferred occupation boundary costs the sum of the first gaps, hence order . Across a slab of width proportional to , the normalized transfer cost is .
The source also computes the ordinary cap normalization. Its partition function includes a product , bounded away from zero when the rectangle’s aspect ratio stays positive. This prevents dividing the transfer estimate by a partition function that might erase its gain.
To connect modes to loops, forget matching colors inside the left and right caps. The remaining components are loops and seam-to-seam arches. An ordinary arch has opposite particle-difference signs at its endpoints. A formal “tear” prescribes equal signs and shifts the two replicas’ particle numbers in opposite directions. Marking eligible arches in a cap with at most choices changes its vector norm by at most . The proof expands the squared norm by pairs of uncolored diagrams: fixed endpoint signs reduce the number of compatible colorings, so no hidden exponential factor is lost.
If a slab has at least traversals, choose alternating left/right runs and tear their corresponding arches. The modified-to-ordinary color ratio is at least . Thus
Choose and recurse on the outer subslabs. At depth , the threshold is while slab width loses at most . The quadratic penalty beats both the marking entropy and the possible subslabs. On a fixed lattice recursion stops when the threshold exceeds the available seam sites, making the event empty. This closes tightness without assuming a crossing bound in advance.
A two-particle insertion gives a squared interval length
Fix a short interval on a middle seam. The insertion removes two occupied sites from one replica and inserts them in the other, preserving the uncolored edge multiplicity at each site. In the singular-mode basis , its coefficient between mode pairs is
by the two-by-two Cauchy–Binet identity. Here is the set of seam sites in . Mode delocalization makes every entry of at most . Its two-by-two minors therefore have size . Positive-width propagation on both sides makes the sum over modes convergent. After cap normalization, the marked contraction is bounded by .
The square is crucial: there are order tested intervals of length . A bound merely proportional to interval length would not vanish after their union bound.
Nesting weights turn a signed contraction into a detector
A same-loop marking contributes a nonnegative product of its two arc intersection numbers. Distinct-loop contributions can have either sign individually. They must be summed before estimating probabilities.
On the event of at most eligible arches per cap, give an arch weight , where counts eligible arches spanning it in that cap. Every positive weight is at least . If one separating loop is inside another, every eligible inner arch is spanned by an eligible outer arch. The extra factor and at most inner choices show that total mark weights decrease by a factor of at least two inward.
The loops separating the endpoints of form at most two nesting chains, with alternating crossing signs and opposite outermost signs. Weighted alternating sums then have their first term’s sign and at least half its magnitude. Grouping the distinct-loop terms by their outer member proves their complete sum nonnegative. Whenever the prohibited configuration occurs, it is at least . Thus the signed observable satisfies the pointwise bound
Combining this with the transfer estimate and gives
First take the lattice-mesh upper limit , then for fixed , and only then . Traversal tightness removes the remaining cap exception. This order avoids requiring uniform control of the rapidly growing constants .
From signed tests to the ordered limiting curves
A uniform localization coupling transfers these rectangle estimates to bounded half-plane windows. Slab traversal counts, together with the source’s disk-trip estimates near the compactification boundary, give tightness of parametrized representatives and of the number of macroscopic loops. Initially the limiting paths may still touch themselves or carry repeated traversals.
The known puncture observables identify visible loop signatures with nested CLE. To use shrinking intervals, the proof first fixes a finite family of tests, chooses its interval mesh, and only afterwards chooses the lattice-mesh threshold. A diagonal sequence with summable errors lets the family grow. No puncture theorem for colliding, mesh-dependent points is assumed.
The signed estimate now prevents cancellation among bounded opposite-side portions of a limiting path. Any actual movement across a generic coordinate line forces a change of inside indicator at nearby grid endpoints. An empty-signature nonconstant path is impossible, and a visible path cannot leave its corresponding CLE trace, where the indicator would be locally constant. Winding around an interior point gives degree or , hence surjectivity onto the trace.
Degree one still permits a forward passage followed by a reverse passage. The final argument excludes that pattern using opposite signed intersections with a generic line through the Jordan curve. The remaining traversal is weakly monotone, so it has zero curve distance from a once-around simple parametrization. Trace, multiplicity, and traversal order have now all been identified; uniqueness of the resulting nested law gives full-mesh convergence.
See Also
- Family 223 also distinguishes traces, ordered curves, full loop ensembles, and occupation measures.
- Family 225 explains Gaussian height convergence and the need for higher-moment and tightness estimates.
🏷️ Manuscripts and verification scope
- The Curve Scaling Limit of Half-Plane Double Dimers — pinned manuscript and companion source.
No family scope page was present at lean/docs/226.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.