we-solve (beta)

Math-2939 · mathematics · Probability

Finite conditional resolution of critical planar Ising stopping bands

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For the critical nearest-neighbor zero-field Ising model on square lattices of mesh delta, with plus boundary in a fixed larger square $Q_L={z:||z||_infinity<L}$, fix $0<u<v<L$. In the inward case choose a compact target K inside $Q_u$; in the outward case choose K inside $Q_L$ minus the closure of $Q_v$. Require strictly positive distances from K to the band and fixed square boundary. Allow the two contour levels to be chosen in fixed open windows with disjoint closures, preserving these clearances. Fix a triangulation of each lattice face, linearly interpolate spins, and explore zero-level strands meeting the starting contour until their first return to that contour or first hit of the other contour, revealing the traversed triangle spins and starting-contour spins. Initially reveal the outside of the outer contour for an inward exploration, or the inside of the inner contour for an outward exploration. Is it true that for every $\epsilon ,\eta >0$ one can choose the levels and a finite list of deterministic regular Jordan barriers with finitely many plus/minus boundary arcs, all independent of the mesh, and a finite-valued descriptor of the band spins, so that for every sufficiently small delta the exceptional descriptor has probability at most epsilon, while for every realizable nonexceptional transcript inserting its descriptor-specific plus pins and then minus pins changes the entire conditional target spin law by summed total variation at most eta and yields the same final target-side law for every transcript with that descriptor? Require the descriptors of any fixed finite list of such bands to have convergent joint laws. Clearances and barriers are fixed before the mesh threshold, and the approximation is uniform over all bounded, including mesh-dependent, target observables.

Short English statement

For the critical nearest-neighbor zero-field Ising model on square lattices of mesh delta, with plus boundary in a fixed larger square $Q_L={z:||z||_infinity<L}$, fix $0<u<v<L$. In the inward case choose a compact target K inside $Q_u$; in the outward case choose K inside $Q_L$ minus the closure of $Q_v$. Require strictly positive distances from K to the band and fixed square boundary. Allow the two contour levels to be chosen in fixed open windows with disjoint closures, preserving these clearances. Fix a triangulation of each lattice face, linearly interpolate spins, and explore zero-level strands meeting the starting contour until their first return to that contour or first hit of the other contour, revealing the traversed triangle spins and starting-contour spins. Initially reveal the outside of the outer contour for an inward exploration, or the inside of the inner contour for an outward exploration. Is it true that for every $\epsilon ,\eta >0$ one can choose the levels and a finite list of deterministic regular Jordan barriers with finitely many plus/minus boundary arcs, all independent of the mesh, and a finite-valued descriptor of the band spins, so that for every sufficiently small delta the exceptional descriptor has probability at most epsilon, while for every realizable nonexceptional transcript inserting its descriptor-specific plus pins and then minus pins changes the entire conditional target spin law by summed total variation at most eta and yields the same final target-side law for every transcript with that descriptor? Require the descriptors of any fixed finite list of such bands to have convergent joint laws. Clearances and barriers are fixed before the mesh threshold, and the approximation is uniform over all bounded, including mesh-dependent, target observables.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2939-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2939

The stopping-band transfer theorem, together with the specified stopping observation, proves the whole question for fixed positive clearances and critical nearest-neighbor zero-field plus-boundary reference law. It chooses generic contour levels, finitely many mesh-independent signed barriers and band-spin descriptor values, exceptional probability at most epsilon, and transcript-uniform summed target total variation at most eta. It also states joint descriptor convergence for every fixed finite list of bands and uniformity over all bounded mesh-dependent observables. Lean Scope 218 expressly covers finite-graph likelihood comparison and excludes this finite stopping-band approximation theorem. Within these assumptions, this is a claimed affirmative answer to the stated question.

Finite conditional resolution of critical planar Ising stopping bands

OpenAI's claim

OpenAI presents a proof in the selected manuscript. Critical Ising target laws are claimed to obey buffered pointwise comparisons with common pins, and finite regular signed barriers approximate stopping-band target laws in total variation.

Mathematical statement of the claimed result

Result 1.
Let $Q_r=\{z:\|z\|_\infty<r\}$ and fix $0<u<v$, with a compact target and the annular band $\overline Q_v\setminus Q_u$ separated by positive macroscopic distances from one another and the ambient square boundary. Inward exploration begins with spins outside $Q_v$ and traces zero-contour strands towards $Q_u$, with target strictly inside $Q_u$. Outward exploration begins inside $Q_u$ and traces towards $Q_v$, with target outside $Q_v$ and inside a more distant prescribed-sign wall. Resolve contours by fixed diagonal affine interpolation of critical Ising spins, retaining each strand until its first return to the initial contour or first hit of the opposite contour. Fix a larger square as reference and impose plus boundary there. Given $\epsilon,\eta>0$, choose generic contour radii inside any fixed separated radius windows and finitely many descriptor states \[ Z^\delta\in\{0,1,\ldots,m\},\qquad \mathbb P(Z^\delta=0)\le\epsilon, \] computed from band spins, uniformly for sufficiently small mesh $\delta$. Assign to each nonexceptional state $i$ its deterministic signed regular barrier $\Gamma_i$. For every compatible full reveal transcript, adding its plus pins and then minus pins changes the target law by total variation errors summing to at most $\eta$, and gives the same target-side Gibbs law $Q_{i,\delta}$ for all transcripts in state $i$. Inward barriers can additionally be moved slightly farther while removing the old pins, with all target errors still summing to at most $\eta$ and a positive buffer around the final free component. For any fixed finite collection of bands, the descriptor joint laws converge in total variation when their bins are limiting continuity sets. State count, barriers and clearances depend on geometry and $\epsilon,\eta$, but not on $\delta$. A law whose band density is at most $K$ times the reference density has exceptional probability at most $K\epsilon$; the conclusion also applies to mixtures of such laws.

Outline of the argument

FK connections in the graph with pinned vertices removed bound likelihood ratios. Buffered crossing estimates make that bound small at separated scales; adaptive interface exploration and regular barriers then give a finite approximation uniform over bounded target observables.

Formal verification

For family 218, the formal scope is a finite-graph likelihood comparison through the zero-field FK connection probability after common pins are deleted. Stopping-band resolution and the universality companions are excluded. The listed Comparator files are BufferedIsing.lean. The inventory does not supply a named declaration for these Comparator entries. 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

Go to contribution →