we-solve (beta)

Math-1723-A1 · revision r1 · on Math-1723

OpenAI claim summary for Math-1723

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 at unsolvedmath.com: partially solved. 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 cited theorem, with amenable transitive uniqueness and rough-isometry invariance of nonamenability, establishes threshold-separation invariance when both graphs are quasi-transitive; our statement allows arbitrary bounded-degree graphs without any transitivity. 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. Rough-isometry invariance of percolation nonuniqueness
  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

Rough-isometry invariance of percolation nonuniqueness

OpenAI's claim

OpenAI presents a mathematical result relevant to this question in the selected manuscript. Every nonamenable locally finite quasi-transitive graph is claimed to satisfy $p_c<p_{2\to2}\leq p_u$, yielding a nonempty phase with infinitely many infinite clusters.

Mathematical statement of the claimed result

Result 1.
Let $G=(V,E)$ have infinitely many vertices, finite degrees, connectedness and quasi-transitivity, with positive vertex Cheeger constant \[ h_V(G)=\inf_{0<|A|<\infty}|\partial_VA|/|A|>0. \] For independent bond percolation, let $T_p(x,y)=\mathbb P_p(x\leftrightarrow y)$, acting on $\ell^2(V)$ with counting measure, and $p_2=\sup\{p:\|T_p\|_{2\to2}<\infty\}$. With $p_c$ and $p_u$ the appearance and uniqueness thresholds, the source claims \[ \sup_{p<p_c}\|T_p\|_{2\to2}=\|T_{p_c}\|_{2\to2}<\infty, \qquad p_c<p_2\le p_u. \] It further supplies $p_c<p_1<p_2'<1$ such that the uniform-edge-label coupling almost surely has infinitely many infinite clusters simultaneously at every $p\in[p_1,p_2']$.

Outline of the argument

For the new unimodular case, local endpoint maps control moments of finite critical clusters. A deformation lowers susceptibility while retaining a large connectivity-operator norm, thereby proving the strict operator-threshold separation; the nonunimodular case uses the established operator result.

Formal verification

For family 214, the documented statements include the strict operator-threshold separation, the nonunique percolation interval, and selected critical moment and tail bounds, with a Cayley-graph specialization. The listed Comparator files are BenjaminiSchramm.lean, CayleyPercolation.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