OpenAI claim summary for Math-2881

The exact IID-factor threshold for free Ising laws on regular trees

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The free Ising law on a $d$-regular tree is claimed to be a factor of iid exactly for $\tanh\beta\leq(d-1)^{-1/2}$, including equality.

Mathematical statement of the claimed result

Result 1.

On the $d$-regular tree, $d\ge3$, the free zero-field Ising law has edge correlation $\theta=\tanh\beta$. A factor of iid is a measurable map of independent uniform vertex labels to spins commuting with automorphisms. The claimed threshold is \[ \mu_{d,\beta}\text{ factor of iid}\quad\Longleftrightarrow\quad \tanh\beta\le(d-1)^{-1/2}\qquad(\beta\ge0). \] In that range the map can be Borel and equivariant on every label input. Finitary dependence or a coding-radius estimate is not asserted.

Outline of the argument

Posterior branch messages control how binary information combines and how intact side branches attenuate responses. Time-integrable response rows make an infinite Brownian innovation equation invertible; the resulting label-to-spin rule respects every tree automorphism even at criticality.

Formal verification

For family 236, the documented theorem gives the free-Ising iid-factor equivalence including the boundary value, with equivariance for each fixed automorphism. It does not claim finitary coding or a radius bound. The listed Comparator files are FreeIsing.lean. Named declarations include OAI.Problem367.free_ising_factor_iff_threshold. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

• OpenAI, The sharp factor-of-IID threshold for the free Ising model on regular trees, 2026-09-26; citation key OAI:The-sharp-factor-of-IID-threshold-for-the-free-Ising-model-on-regular-trees-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 236: Lean scope.
• Comparator FreeIsing.json.
• Comparator FreeIsing.lean.
• OpenAI catalogue entry.