we-solve (beta)

Math-1736 · mathematics · Probability

Limit shape of first-passage percolation

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Fix $d\ge2$ and give $\mathbb Z^d$ its nearest-neighbor edges. Assign independent exponential passage times $\tau_e$ of mean one to all edges. For vertices $x,y$, define \[ T(x,y)=\inf_{\gamma:x\to y}\sum_{e\in\gamma}\tau_e, \] where the infimum ranges over finite nearest-neighbor paths. Let $B(t)=\{x:T(0,x)\le t\}$, and replace each of its vertices by the unit cube centered there to obtain a subset $\widetilde B(t)\subset\mathbb R^d$.

The shape theorem supplies a deterministic compact convex body $K_d$ with nonempty interior such that $t^{-1}\widetilde B(t)$ converges to $K_d$ almost surely in Hausdorff distance. Equivalently, $K_d=\{x:\mu_d(x)\le1\}$, where the directional time constant is $\mu_d(x)=\lim_{n\to\infty}T(0,nx)/n$ for lattice directions and is extended to a norm on $\mathbb R^d$.

Determine this body explicitly, or equivalently determine the directional dependence of $\mu_d$. If only the shape up to scale is sought, normalize $K_d$ to Euclidean diameter one. Merely expressing the answer through the same unknown passage-time limit does not identify the shape.

The equivalent discrete growth process begins with only $0$ black, chooses uniformly among edges with exactly one black endpoint, and turns that edge's white endpoint black. Exponential memorylessness makes this the embedded jump chain of the passage-time model. Uniform choice is among boundary edges, so a white vertex with several black neighbors is proportionally more likely to be chosen. This distinction fixes the precise random growth model in the original question.

Short English statement

What is the deterministic macroscopic shape of exponential first-passage growth on a Euclidean lattice?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-1736

The cited theorem gives strict convexity and C1 differentiability of the planar exponential shape, but our question asks its explicit directional norm in every d>=2; neither a formula nor the other dimensions is determined. This entry records partial support; complete coverage of the question is not established by this catalogue.

Limit shape of first-passage percolation

OpenAI's claim

OpenAI presents a mathematical result relevant to this question in the selected manuscript. The exponential planar first-passage shape is claimed to be strictly convex with a continuously differentiable boundary; Gamma laws are also claimed to give differentiable time constants.

Mathematical statement of the claimed result

Result 1.
For nearest-neighbor first-passage percolation on $\mathbb Z^2$ with independent exponential weights of fixed rate $\lambda>0$, let $\mu$ denote the time-constant norm and $\mathcal B=\{x:\mu(x)\le1\}$. The source claims differentiability of $\mu$ on $\mathbb R^2\setminus\{0\}$, a $C^1$ boundary of $\mathcal B$, and \[ x,y\in\partial\mathcal B,\ x\ne y,\ 0<t<1 \quad\Longrightarrow\quad\mu((1-t)x+ty)<1. \] Thus its unit ball is strictly convex and has one supporting line at each boundary point. This theorem is for exponential weights, not arbitrary passage laws.

Outline of the argument

The argument separates the removal of corners from the removal of flat faces. Busemann and geodesic comparisons establish differentiability for Gamma weights, while an additional exponential-law argument excludes linear boundary segments; the two conclusions are then combined.

Formal verification

For family 212, the documented entries give differentiability and continuously differentiable boundaries for planar Gamma shapes, including the exponential law. They do not supply strict convexity or the separate no-bigeodesic theorem. The listed Comparator files are GammaPassage.lean, PlanarFirstPassage.lean. Named declarations include OAI.PlanarFPP.manuscriptMain. 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 →