# Directional zero–one laws beyond iid environments and iid ballisticity

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

- [A directional zero–one law under strict ellipticity](../../preprints/A-directional-zero-one-law-under-strict-ellipticity-September-23-2026/paper.pdf)
- [Directional transience implies ballisticity](../../preprints/Directional-transience-implies-ballisticity-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/DirectionalWalk.lean) |
| Directional transience implies ballisticity | [DirectionalBallisticity.lean](../ComparatorChallenges/DirectionalBallisticity.lean) |
| Positive-probability transience and the velocity hemisphere | [VelocityHemisphere.lean](../ComparatorChallenges/VelocityHemisphere.lean) |