OAI.PlanarFPP.manuscriptMain

The theorem states that, for any probability space (Ω, P) carrying an edge-weight family τ indexed by the edges of the nearest-neighbour lattice ℤ², where each vertex p has an east edge (p,false) and a north edge (p,true), such that the τ(e) are measurable, mutually independent, and each has the exponential distribution with rate 1 (the ExponentialEnvironment hypothesis), there exists a function μ on the plane ℝ² with the following properties. First, μ is a norm: nonnegative, zero only at the origin, subadditive, and satisfying μ(av)=|a|μ(v) for all real a. Second, μ is the time constant: for every v in ℝ², almost surely the first-passage time from (0,0) to the lattice point (⌊tv₀⌋,⌊tv₁⌋), defined as the infimum of path costs over nearest-neighbour step sequences (east, west, north, south) that sum the edge weights along the path, divided by t, converges to μ(v) as t→∞. Third, μ is Fréchet differentiable at every nonzero point. Fourth, at every point v with μ(v)=1 there is exactly one linear functional ℓ with ℓ(v)=1 and ℓ(w)≤μ(w) for all w. Fifth, the unit sphere of μ is a C¹ curve in the sense that near each point v with μ(v)=1 there is an open neighbourhood U and a C¹ function g on U whose zero set in U is exactly the set where μ=1, with g having a nonzero Fréchet derivative at each of those zeros. Sixth, for each boundary point v of the unit ball {μ≤1}, there is a unique line L that is the level set {z : g(z)=g(v)} of some nonzero continuous linear functional g that attains its maximum over the unit ball at v, so each boundary point has a unique supporting line. Seventh, every boundary point v of the unit ball has a C¹ curve chart: an open neighbourhood U of v and a C¹ map γ:ℝ→ℝ² with nowhere vanishing derivative, together with a function θ continuous on U, such that γ takes values in the boundary within U, θ(γ(t))=t for all t, and γ(θ(z))=z for each boundary point z in U.