Browse › Probability and statistical mechanics › 212 Planar first-passage geometry and the absence of bigeodesics
Strict convexity and differentiability of the planar exponential first-passage limit shape
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove that the limit shape of undirected nearest-neighbor first-passage percolation on ℤ2 with independent exponential edge weights is strictly convex and has a C1 boundary. This resolves the strict convexity and differentiability conjectures for the planar exponential model. More generally, we prove differentiability of the time-constant norm for every Gamma edge-weight law with positive shape and rate.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI, Planar first-passage geometry and the absence of bigeodesics: Lean scope note (lean/docs/212.md, 2026). Reports formalization of differentiability of the time-constant norm and a $C^1$ limit-shape boundary for positive Gamma laws, including exponential weights; it explicitly excludes exponential strict convexity from its selected statements. [family-level]
Possibly relevant literature (found by the agent, not checked)
- Yuri Bakhtin, Douglas Dow, Differentiability of limit shapes in continuous first passage percolation models (arXiv:2406.09652, 2024). Gives conditions for limit-shape differentiability in an abstract class of continuous first- and last-passage models, relevant to the differentiability part (Theorems 1.1–1.2); the paper does not cite it.
- Malte Hassler, Classification of the limit shape for 1+1-dimensional FPP (arXiv:2411.13030, 2024; rev. 2025). In a planar model with deterministic vertical weights, shows a vertical flat edge occurs exactly when the horizontal law has an atom at its infimum, bearing on the paper's discussion of flat faces versus atoms (Marchand; Auffinger–Damron).
- Michael Damron, Michael Hochman, Examples of nonpolygonal limit shapes in i.i.d. first-passage percolation and infinite coexistence in spatial growth models (Ann. Appl. Probab. 23 (2013), 1074–1085). Constructs i.i.d. laws with nonpolygonal limit shapes, relevant to the paper's remark that differentiability for Gamma laws gives infinitely many extreme points.
Digests and expositions
- Orply / Perplexity, Exponential First-Passage Limit Shapes Have No Corners or Flat Sides (Orply, 2026-10-11). Outlines the separate arguments for Gamma differentiability and exponential strict convexity, including the change-of-measure estimate and iterative improvement of local paths. [AI-generated per source]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 212
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026,
author = {{OpenAI}},
title = {{Strict convexity and differentiability of the planar exponential first-passage limit shape}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026/main.pdf}{OAI:Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/212.md. The Lean statements have not been checked by people against the paper's claims.
Family 212: Planar first-passage geometry and the absence of bigeodesics
Proves that planar first-passage percolation has no doubly infinite geodesic for iid nonnegative nonatomic edge weights when the minimum of four weights has finite second moment. For exponential weights, the limit shape is strictly convex with C1 boundary. Differentiability also holds for every Gamma law with positive shape and rate.
Other papers in this family:
- No bigeodesics in planar first-passage percolation · September 24, 2026