we-solve (beta)

Math-2939-A1 · revision r1 · on Math-2939

OpenAI claim summary for Math-2939

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 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.

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

Manuscript

Contents
  1. Finite conditional resolution of critical planar Ising stopping bands
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

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