we-solve (beta)

Math-1722 · mathematics · Probability

Cheeger constant and the percolation nonuniqueness phase

Status Partially solved · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Let $G$ be an infinite connected locally finite vertex-transitive graph. For each $p\in[0,1]$, perform Bernoulli bond percolation by retaining edges independently with probability $p$, and let $N_\infty(p)$ be the number of infinite open components. Define \[ p_c(G)=\inf\{p:\mathbb P_p(N_\infty(p)\ge1)>0\}, \qquad p_u(G)=\inf\{p:\mathbb P_p(N_\infty(p)=1)=1\}. \] For finite nonempty $A\subset V(G)$, write $\partial_G A$ for the external vertex boundary, and set $h(G)=\inf_A|\partial_G A|/|A|$.

Prove the equivalence \[ p_c(G)<p_u(G)\quad\Longleftrightarrow\quad h(G)>0. \] In particular, the difficult direction asks whether every nonamenable transitive graph has a nonempty interval of parameters on which there are infinitely many infinite open clusters almost surely. The constants and the length of this interval may depend on the graph.

Local finiteness and transitivity imply a common finite degree. No restriction to Cayley graphs, unimodular graphs, planar graphs, or hyperbolic graphs is part of the assertion. The definition of $p_u$ specifies uniqueness with probability one, rather than uniqueness conditional on a selected root being in an infinite cluster. The target makes no separate assertion about what happens at either endpoint $p_c$ or $p_u$. It compares the existence of an intermediate percolation phase with expansion measured by all finite vertex sets in the underlying graph.

Short English statement

Does every nonamenable transitive graph have a percolation phase with infinitely many infinite clusters, and only such graphs?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-1722

The cited theorem proves pc<p2to2<=pu for every nonamenable locally finite quasi-transitive graph, hence the nonamenable direction for all vertex-transitive graphs in our equivalence; the reverse is the established uniqueness theorem for amenable transitive Bernoulli percolation. The claimed conclusion supplies the requested case and extends it in the directions just specified.

Cheeger constant and the percolation nonuniqueness phase

OpenAI's claim

OpenAI presents a proof 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

Go to contribution →