Browse › Probability and statistical mechanics › 231 The free uniform spanning forest is a factor of IID
The free uniform spanning forest is a factor of IID
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 free uniform spanning forest is a factor of IID on every infinite connected locally finite simple unweighted graph. One Borel rule works for all such graphs and uses no root, answering affirmatively the general factor question for unimodular random graphs. We also show that every translation-invariant strongly Rayleigh process indexed by a countable group is a factor of IID, including invariant determinantal processes with Hermitian positive-contraction kernels. This group-action conclusion requires no amenability.
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 math release / mathcommunity, Lean scope notes for family 231 (lean/docs/231.md, 6 October 2026). The release's scope note says the formalization covers the universal root-independent FUSF factor theorem and supplements on strongly Rayleigh and determinantal laws on countable groups, with links to the comparator statements
FreeUniformSpanningForest.leanandStronglyRayleighDPP.lean. - OpenAI, SpanningForest/Factor.lean (openai/math, commit adc7f12). States
fusf_is_factor_iid(a single Borel equivariant factor rule on every graph code) andfusf_factor_for_every_unimodular_law, corresponding to Theorem 1.1 and Corollary 1.2 of the paper. - OpenAI, StrongRayleigh/Main.lean (openai/math, commit adc7f12). States
strongly_rayleigh_group_factorandinvariant_positive_contraction_dpp_factor, among other results, corresponding to the paper's strongly Rayleigh group theorem and determinantal corollary.
Possibly relevant literature (found by the agent, not checked)
- Lyons and Peres, Probability on Trees and Networks (Cambridge University Press, 2016; online corrected edition). A standard monograph on uniform spanning forests and Wilson's algorithm rooted at infinity, background for the paper's discussion of the free and wired forests; it is not in the paper's bibliography.
- Hutchcroft and Pete, Kazhdan groups have cost 1 (arXiv:1810.11015, Invent. Math. 2020). Timár cites it right after stating that the general FUSF factor question is open, in a discussion of fixed price; it may bear on the cost motivation of Lyons's 2013 question, which the paper cites.
- Chen and Eldan, Localization Schemes: A Framework for Proving Mixing Bounds for Markov Chains (arXiv:2203.04163, 2022). A general stochastic-localization framework related to the observation and posterior-drift mechanism that the paper adapts from Eldan, El Alaoui–Montanari and Nam–Sly–Zhang.
Digests and expositions
- Latent Seminar, Sampling the free uniform spanning forest from IID labels (6 October 2026). This exposition outlines the covariance response bound, Brownian innovations, deterministic inverse and equivariant allocation of edge noise, explicitly without independently verifying the complete proof.
- Open Mathematics Courses, The free uniform spanning forest (undated). Four lessons develop weighted trees, the free limit, tilted laws and the drift equation toward the manuscript's construction, but explicitly do not yet include the factor-of-IID theorem. [AI-generated per source]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 231
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026,
author = {{OpenAI}},
title = {{The free uniform spanning forest is a factor of IID}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/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}{OAI:The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/231.md. The Lean statements have not been checked by people against the paper's claims.
Family 231: The free uniform spanning forest is a factor of IID
On every infinite connected locally finite simple unweighted graph, the free uniform spanning forest is a factor of independent vertex labels, by one isomorphism-equivariant rule using no root. Translation-invariant strongly Rayleigh binary processes on every countable group, including invariant determinantal processes with Hermitian positive-contraction kernels, are also factors of IID.
This is the only paper in this family.