we-solve (beta)

Math-2869 · mathematics · Probability

Strict convexity and differentiability of the exponential planar passage shape

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For nearest-neighbor first-passage percolation on $Z^2$ with independent mean-one exponential edge weights, is the asymptotic unit ball strictly convex with a continuously differentiable boundary? Equivalently ask for differentiability of the time constant at every nonzero direction and no line segment in its unit sphere.

Short English statement

For nearest-neighbor first-passage percolation on $Z^2$ with independent mean-one exponential edge weights, is the asymptotic unit ball strictly convex with a continuously differentiable boundary? Equivalently ask for differentiability of the time constant at every nonzero direction and no line segment in its unit sphere.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2869

The source gives strict convexity and a continuously differentiable passage-shape boundary for exponential edge weights of every positive rate. Rate one is the model requested here, so that specialization proves the target.

Strict convexity and differentiability of the exponential planar passage shape

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 →