we-solve (beta)

Math-2350 · mathematics · Probability

Transience Implies Ballisticity for Uniformly Elliptic RWRE

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
For a uniformly elliptic i.i.d. random walk in random environment in dimension $d\geq2$, does transience in a direction $\ell$ imply ballisticity in that direction?

Formulation references: [S1], [S2].

Short English statement

For a uniformly elliptic i.i.d. random walk in random environment in dimension $d\geq2$, does transience in a direction $\ell$ imply ballisticity in that direction?

Sources

Catalogue entry

Statement licence: CC-BY-SA-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2350

The main theorem treats every iid uniformly elliptic nearest-neighbor environment on Zd in every d>=2 and every deterministic direction with almost-sure directional transience, and gives a deterministic limiting velocity whose projection in that same direction is positive. This is exactly the transience-to-ballisticity implication in the problem statement. Within these assumptions, this is a claimed affirmative answer to the stated question.

Transience Implies Ballisticity for Uniformly Elliptic RWRE

OpenAI's claim

OpenAI presents a proof in the selected manuscript. Iid uniformly elliptic nearest-neighbor walks in dimensions $d\geq2$ are claimed to have positive directional speed whenever escape in that direction is almost sure.

Mathematical statement of the claimed result

Result 1.
On $\mathbb Z^d$, take iid nearest-neighbor transition rows with a deterministic lower bound $\kappa>0$ on every transition probability. Let $P_0$ be the environment-averaged walk law and $A_\ell=\{X_n\cdot\ell\to+\infty\}$. For $d\ge2$, the main claim is \[ P_0(A_\ell)=1\quad\Longrightarrow\quad \exists v\in\mathbb R^d\text{ deterministic}:\ v\cdot\ell>0,\quad P_0(X_n/n\to v)=1. \] For $d\ge3$, the corollary replaces the premise by $P_0(A_\ell)>0$. If any such direction exists, then for each fixed $u\in S^{d-1}$, \[ P_0(A_u)=1\ \Longleftrightarrow\ P_0(A_u)>0\ \Longleftrightarrow\ v\cdot u>0. \] It does not assert a simultaneous pathwise statement for uncountably many directions.

Outline of the argument

Regeneration is split into spatial-radius and temporal estimates. Controlling radii first yields quantitative crossing information without assuming nearby directional transience, and the resulting tail estimates make regeneration duration integrable, producing a deterministic positive speed.

Formal verification

For family 220, the documented iid results include strict-ellipticity directional zero--one laws, uniform-ellipticity ballisticity, and the positive-velocity hemisphere. The later finite-range-dependent environment theorem is not selected. The listed Comparator files are DirectionalBallisticity.lean, DirectionalWalk.lean, VelocityHemisphere.lean. Named declarations include OAI.DirectionalTransience.directional_transience_implies_ballisticity. 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 →