Browse › Probability and statistical mechanics › 236 The exact factor-of-IID threshold for free Ising spins on trees
The sharp factor-of-IID threshold for the free Ising model on regular trees
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
For every integer d ≥ 3 and inverse temperature β ≥ 0, the free zero-field ferromagnetic Ising measure on the infinite d-regular tree is a factor of IID exactly when $\tanh\beta\le(d-1)^{-1/2}$. We prove the positive implication, including equality, resolving the conjecture of Nam, Sly and Zhang; the strict converse is known. The spin factor can be chosen to commute with every tree automorphism on every label input.
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, Lean scope note for family 236: The exact factor-of-IID threshold for free Ising spins on trees (lean/docs/236.md, 6 October 2026). The scope note says the formalized statement is the full threshold, including equality, with almost-sure equivariance for each fixed automorphism of a factor of uniform labels; finitary coding and coding-radius bounds are excluded. [family-level]
- OpenAI math release, lean/OAI/Probability/FreeIsing/Main.lean (openai/math, commit adc7f12, 2026). This file states
OAI.Problem367.free_ising_factor_iff_threshold(ford ≥ 3,beta ≥ 0: factor of IID ifftanh beta ≤ 1/sqrt(d-1)), the Lean counterpart of Theorem 1.1; the file has nosorry, but its supporting lemmas are imported from other modules.
Possibly relevant literature (found by the agent, not checked)
- Balázs Gerencsér and Viktor Harangi, Mutual information decay for factors of IID (arXiv:1703.04387, 2017). It proves sharp bounds of order (d−1)^(−k/2) on normalized mutual information between vertices at distance k for factor-of-IID processes on d-regular trees, which bears on the obstruction side of the threshold; the paper derives that side from the Backhausz–Szegedy–Virág correlation bound.
- Ágnes Backhausz and Bálint Virág, Spectral measures of factor of i.i.d. processes on vertex-transitive graphs (arXiv:1505.07412, 2015). It characterizes spectral measures of factor-of-IID processes on transitive graphs, a tool related to the spectral bound for equivariant observables used in the spatial-cancellation step (Section 6).
- Andrea Montanari, Sampling, Diffusions, and Stochastic Localization (arXiv:2305.10690, 2023). An exposition of stochastic-localization and diffusion processes with posterior drift, background to the Gaussian-observation framework (X_v(t)=tσ_v+B_v(t) and its innovations) on which the construction is built.
Digests and expositions
- Latent Seminar, The sharp IID-factor threshold for free tree Ising spins (6 October 2026). This exposition outlines the manuscript's innovations recovery, conditional-copy coupling, critical Osgood comparison, and everywhere-equivariant version, stating that it does not independently verify the complete proof. [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 236
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:The-sharp-factor-of-IID-threshold-for-the-free-Ising-model-on-regular-trees-September-26-2026,
author = {{OpenAI}},
title = {{The sharp factor-of-IID threshold for the free Ising model on regular trees}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/The-sharp-factor-of-IID-threshold-for-the-free-Ising-model-on-regular-trees-September-26-2026/article.pdf}{OAI:The-sharp-factor-of-IID-threshold-for-the-free-Ising-model-on-regular-trees-September-26-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/236.md. The Lean statements have not been checked by people against the paper's claims.
Family 236: The exact factor-of-IID threshold for free Ising spins on trees
Determines when the free zero-field ferromagnetic Ising state on the infinite d-regular tree is a factor of independent vertex labels: exactly when $\tanh\beta\le(d-1)^{-1/2}$, including equality, for d ≥ 3 and β ≥ 0. The construction uses no root and is almost surely equivariant for each fixed tree automorphism, resolving the ferromagnetic case of Lyons's question.
This is the only paper in this family.