# Canonical $`O(3)`$ continuum limit and exact $`O(4)`$ mass asymptotics

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

- [Exponential decay in two-dimensional classical $O(n)$ models](../../preprints/Exponential-decay-in-two-dimensional-classical-On-models-September-23-2026/paper.pdf)

## Scope

The formalized result proves exponential decay of spin correlations for the two-dimensional classical $O(n)$ model at every temperature when $n\ge3$. For each interaction bound $\beta>0$, constants $A$ and $m>0$ work for every finite square-lattice subgraph with free boundary and nonnegative edge strengths at most $\beta$: the correlation between sites $x,y$ is at most $Ae^{-m|x-y|}$. The infinite-volume limit and the separate $O(4)$ spectral-gap claim are not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Exponential correlation decay for classical $O(n)$ models | [ClassicalON.lean](../ComparatorChallenges/ClassicalON.lean) |