Probability and statistical mechanics · Result 220

Directional zero–one laws beyond iid environments and iid ballisticity

3 papersLean

On ℤ^d, d ≥ 3, directional escape has probability zero or one for iid strictly elliptic nearest-neighbor environments, and for stationary ergodic finite-range-dependent environments under uniform ellipticity. In iid uniformly elliptic environments with d ≥ 2, almost-sure directional transience implies a deterministic limiting velocity with positive projection in that direction, resolving the ballisticity conjecture.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 3

A directional zero–one law for finite-range-dependent random environments

OpenAI · October 5, 2026

We prove a directional zero–one law for uniformly elliptic nearest-neighbor random walks in stationary, ergodic, finite-range-dependent environments on ℤ^d, d ≥ 3. For every fixed nonzero real direction, the probability of escape in that direction, averaged over the environment, is either zero or one. Finite-range dependence is imposed on the full transition rows: collections of rows at distance greater than a fixed range are independent, including collections indexed by infinite deterministic sets.

Read PDF Download Source

Cite

@misc{OAI:A-directional-zero-one-law-for-finite-range-dependent-random-environments-October-5-2026,
  author = {{OpenAI}},
  title = {{A directional zero--one law for finite-range-dependent random environments}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-directional-zero-one-law-for-finite-range-dependent-random-environments-October-5-2026/directional-zero-one-finite-range.pdf}{OAI:A-directional-zero-one-law-for-finite-range-dependent-random-environments-October-5-2026}},
  year = {2026}
}

A directional zero–one law under strict ellipticity

OpenAI · September 23, 2026

We prove the directional zero–one conjecture for nearest-neighbor random walks in independent and identically distributed strictly elliptic environments on ℤ^d, d ≥ 3: the probability of escape in each fixed nonzero real direction is zero or one. Only strict positivity of the transition probabilities is required; no uniform lower bound or moment assumption is imposed.

Read PDF Download Source

Cite

@misc{OAI:A-directional-zero-one-law-under-strict-ellipticity-September-23-2026,
  author = {{OpenAI}},
  title = {{A directional zero--one law under strict ellipticity}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-directional-zero-one-law-under-strict-ellipticity-September-23-2026/paper.pdf}{OAI:A-directional-zero-one-law-under-strict-ellipticity-September-23-2026}},
  year = {2026}
}

Directional transience implies ballisticity

OpenAI · September 23, 2026

We prove that almost-sure transience in a fixed direction implies a deterministic limiting velocity with positive projection in that direction for nearest-neighbor random walks in independent and identically distributed uniformly elliptic environments on ℤ^d, d ≥ 2. This resolves the ballisticity conjecture positively.

Read PDF Download Source

Cite

@misc{OAI:Directional-transience-implies-ballisticity-September-23-2026,
  author = {{OpenAI}},
  title = {{Directional transience implies ballisticity}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Directional-transience-implies-ballisticity-September-23-2026/paper.pdf}{OAI:Directional-transience-implies-ballisticity-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The directional zero–one conjecture asks whether a random walk's probability of escape in a fixed direction must be zero or one. The formalization proves this for nearest-neighbor walks in independent identically distributed strictly elliptic environments on \(\mathbb Z^d\), for every \(d\ge3\) and every nonzero real direction. Strict ellipticity means that every allowed transition probability is positive almost surely; no uniform positive lower bound or moment condition is assumed. The probability is the annealed law from the origin.

For an i.i.d. uniformly elliptic nearest-neighbor random environment on \(\mathbb Z^d\), the formalization proves that almost-sure directional transience implies convergence of \(X_n/n\) to a deterministic velocity with positive projection in that direction for every \(d\ge2\).

For \(d\ge3\), positive probability of transience in any nonzero direction already suffices. The limiting velocity is unique, and the unit directions with positive transience probability are exactly the open hemisphere having positive inner product with that velocity; transience has probability one on that hemisphere and zero on its complement. The environment is sampled once and retained along the walk, and the probabilities use the annealed law from the origin.

Comparator links

Result	Comparator statement
Directional zero–one law under strict ellipticity	DirectionalWalk.lean
Directional transience implies ballisticity	DirectionalBallisticity.lean
Positive-probability transience and the velocity hemisphere	VelocityHemisphere.lean

Scope note on GitHub →