# The geometric phase diagram, diffusion, and spectra of random planar maps

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

- [Brownian continuum random tree limits of finite Fortuin–Kasteleyn maps above four](../../preprints/Brownian-continuum-random-tree-limits-of-finite-Fortuin-Kasteleyn-maps-above-four-September-24-2026/main.pdf)

## Scope

For every fixed $q>4$, the formalization proves the Brownian continuum-random-tree limit for critical finite Fortuin–Kasteleyn planar maps. After rescaling graph distances in an $n$-edge map by a constant depending on $q$ times $n^{-1/2}$ and using normalized degree measure, the metric-measure space converges in distribution to the Brownian continuum random tree in the Gromov–Hausdorff–Prokhorov topology. The convergence holds through all positive integer sizes.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Brownian continuum-random-tree limit for finite FK maps | [FKCRT.lean](../ComparatorChallenges/FKCRT.lean) |