# The exact factor-of-IID threshold for free Ising spins on trees

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

- [The sharp factor-of-IID threshold for the free Ising model on regular trees](../../preprints/The-sharp-factor-of-IID-threshold-for-the-free-Ising-model-on-regular-trees-September-26-2026/article.pdf)

## Scope

The formalized result determines the factor-of-IID threshold for the free zero-field Ising law on the infinite $d$-regular tree. For every $d\ge3$ and $\beta\ge0$, the law is a factor of IID exactly when $\tanh\beta\le1/\sqrt{d-1}$, including equality. The factor uses independent uniform vertex labels and is almost surely equivariant for each fixed tree automorphism. Finitary coding and coding-radius bounds are not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Factor-of-IID threshold for the free Ising model | [FreeIsing.lean](../ComparatorChallenges/FreeIsing.lean) |