# The free uniform spanning forest is a factor of IID

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

- [The free uniform spanning forest is a factor of IID](../../preprints/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026.pdf)

## Scope

The formalization proves that the free uniform spanning forest is a factor of independent identically distributed vertex labels on every infinite connected locally finite simple unweighted graph. One Borel equivariant rule works for all such graphs and uses no distinguished root.

The linked supplements also give equivariant IID sampling for invariant strongly Rayleigh laws on countable groups and existence, uniqueness, and IID-factor results for determinantal laws with Hermitian positive-contraction kernels on countable index sets. These group results require neither amenability nor finite generation, and the kernels need not be trace class.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Strongly Rayleigh and determinantal-process IID factors | [StronglyRayleighDPP.lean](../ComparatorChallenges/StronglyRayleighDPP.lean) |
| A universal IID factor for the free uniform spanning forest | [FreeUniformSpanningForest.lean](../ComparatorChallenges/FreeUniformSpanningForest.lean) |