we-solve (beta)

Math-2256-A1 · revision r1 · on Math-2256

OpenAI claim summary for Math-2256

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: 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 theorem proves critical nonpercolation for nearest-neighbor bond and site percolation on Z3 only. The problem statement quantifies every infinite vertex-transitive graph, which is a much larger class. The theorem covers infinite connected locally finite quasi-transitive graphs only when pc<1. The literal problem statement does not exclude pc=1 or non-locally-finite graphs; Z has pc=1 and percolates at pc. The finite critical L2 two-point norm on nonamenable locally finite quasi-transitive graphs implies critical nonpercolation in that class, but does not prove the problem statement assertion for all infinite transitive graphs, especially its unexcluded pc=1 case. 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. No critical infinite cluster on transitive graphs
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Result 2.
  6. Result 3.
  7. Outline of the argument
  8. Formal verification
  9. Status caveat
  10. Sources

No critical infinite cluster on transitive graphs

OpenAI's claim

The linked manuscripts present the following claims by OpenAI: Both bond and site percolation on $\mathbb Z^3$ are claimed to have only finite clusters at their respective critical probabilities; Critical bond percolation is claimed to have no infinite component on every infinite locally finite quasi-transitive graph with $p_c<1$; 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. Together they provide the following support within the scopes described below.

Mathematical statement of the claimed result

Result 1.
For independent nearest-neighbor bond percolation on $\mathbb Z^3$, write $p_c^{\mathrm{bond}}$ for the first parameter permitting an infinite cluster. The source asserts \[ \mathbb P_{p_c^{\mathrm{bond}}}(\exists\text{ infinite open cluster})=0. \] For independent nearest-neighbor site percolation, it separately claims \[ \mathbb P_{p_c^{\mathrm{site}}}(\exists\text{ infinite open cluster})=0. \] These are two cubic-lattice statements at their respective critical parameters.
Result 2.
Suppose $G$ is infinite, connected, locally finite, undirected, and has finitely many vertex orbits under automorphisms. For Bernoulli bond percolation, define $p_c(G)$ as the infimum of parameters with positive probability of an infinite cluster. The claimed implication is \[ p_c(G)<1\quad\Longrightarrow\quad \mathbb P_{p_c(G)}(\exists\text{ infinite open cluster})=0. \] Equivalently, every fixed vertex $x$ satisfies $\mathbb P_{p_c}(|C_x|=\infty)=0$. The hypothesis $p_c<1$ is essential to the stated scope.
Result 3.
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

Independent hyperedges provide a finite connection inequality that accommodates the two models. Finite-scale extension bounds allow an adaptive exploration to maintain successful connections; assuming critical percolation would make this construction survive below the threshold, a contradiction.

The proof separates growth regimes and uses finitary structural reduction in the polynomial-growth case. Two coordinate moves are glued through fresh corridors using a conditional connection inequality; adaptive exploration would then produce subcritical percolation if an infinite critical cluster existed.

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 213, the Lean scope covers cubic-lattice bond and site critical nonpercolation, and quasi-transitive bond graphs when $p_c<1$. The listed Comparator files are CriticalPercolation.lean, CriticalZ3.lean. Named declarations include OAI.CriticalZ3.critical_no_infinite. 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