The quasi-isometry classification, embeddability, and automorphism-matching theorems are formally verified in Lean, using AI-assisted formalisation workflows.
Abstract
We classify, up to quasi-isometry, the large-scale geometry of Galton–Watson trees for every finitely supported offspring distribution. Apart from the trivial finite diameter regimes, we condition on infinite diameter. We find that the remaining classes are the ray class, the full tree class (which includes the binary tree), one chain class $(\mathrm{C}_Λ)$ for every possible branching semigroup $Λ$, and the bushy class. Two independent trees almost surely admit a root-preserving quasi-isometry when their offspring distributions belong to the same class and are almost surely not quasi-isometric when they belong to different classes. Any two survival-conditioned supercritical realisations with finitely supported offspring laws nevertheless a.s. admit quasi-isometric embeddings in both directions. We prove that the class of a realisation depends only on the support of the offspring distribution, not its specific distribution. For offspring distributions supported on $\{1,2\}$, we additionally obtain an explicit exponential tail bound for the probability of non-existence of a root-preserving $D$-quasi-isometry. The classification also implies that the corresponding random Cantor boundaries are almost surely quasisymmetrically equivalent. Conditioned on nonextinction, this applies to strongly separated fractal percolation, even when the underlying self-similar iterated function systems and retention parameters differ. We also classify two families of trees with continuous random branching times. Our proofs use new automorphism-matching theorems for random graph labellings of trees, based on contraction estimates for mismatch potentials. These matching results for Markov labellings on the binary tree may be of independent interest. The quasi-isometry classification, embeddability, and matching theorems are formally verified in Lean.
Problem
The paper classifies the large-scale geometry, up to quasi-isometry, of Galton–Watson trees with finitely supported offspring distributions, conditioned on infinite diameter.
Approach
Each realisation is reduced to a branching skeleton with local pieces, encoded as quantised random labels on a binary tree. New automorphism-matching theorems for independent and Markov random labellings, proved via contraction estimates for mismatch potentials, produce root-preserving quasi-isometries. The main theorems were formalised in Lean with AI assistance (Claude, ChatGPT/Codex, and the vibefeld workflow).
Results
The infinite regimes split into a ray class, a full tree class, one chain class for each branching semigroup, and a bushy class. Independent trees in the same class are almost surely quasi-isometric, and trees in different classes almost surely are not. The class depends only on the support of the offspring distribution, and the result implies quasisymmetric equivalence of random Cantor boundaries, including those from fractal percolation.
Figure 1. Finite truncations illustrating the three non-ray infinite regimes, embedded in the Poincaré disc. Regime (R) is omitted. The top row shows regime (F), with support \{2,3,4\} , and regime (B), with support \{0,1,2,3\} . The middle row shows regime (B), with support \{0,1,2,3,4\} , and (\mathrm{C}_{\langle 1\rangle}) , with support \{1,2\} . The bottom row shows (\mathrm{C}_{\langle 2\ran