nu_monotone_heisenberg_spherical
plain-language theorem explainer
The theorem establishes that the correlation length exponent for the O(3) Heisenberg universality class is strictly smaller than the exact value for the spherical model. Researchers in critical phenomena would cite it to confirm the ordering of exponents across O(N) classes in three dimensions. The proof is a one-line term wrapper that unfolds the two numerical definitions and applies norm_num to verify the inequality.
Claim. In the O(N) universality classes from Q₃ geometry, the correlation length exponent for the Heisenberg class satisfies $0.71164 < 1$, where the spherical model has exact value $1$.
background
The module maps O(N) universality classes to subgroups of Aut(Q₃) and supplies bootstrap reference values in D=3: Ising (O(1)) has ν ≈ 0.62997, XY (O(2)) has ν ≈ 0.67169, Heisenberg (O(3)) has ν = 0.71164, and the spherical model (O(∞)) has ν = 1 exactly. The Heisenberg bootstrap is the structure carrying symmetry rank 3 together with those exponents; the spherical exact structure carries rank 0 and the exact infinite-N values. The RS conjecture states that leading-order ν₀(N) is fixed by the Q₃ automorphism structure.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the Heisenberg bootstrap and spherical exact definitions, then invokes norm_num to confirm the numerical comparison.
why it matters
The result verifies monotonic growth of ν with symmetry rank N from O(3) to O(∞), consistent with the RS framework for D=3. It supplies one concrete link in the ordering of universality classes required by the Q₃ geometry. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.