nu_monotone_ising_xy
plain-language theorem explainer
The correlation length exponent ν increases strictly from the Ising (N=1) to the XY (N=2) universality class in three dimensions. Researchers mapping O(N) critical phenomena to Q₃ automorphism subgroups would cite this monotonicity to check consistency with bootstrap references. The proof is a one-line wrapper that unfolds the two bootstrap definitions and confirms the numerical inequality via norm_num.
Claim. $0.629971 < 0.67169$, where the left value is the correlation length exponent for the O(1) Ising class and the right value is that for the O(2) XY class.
background
The module maps symmetry rank N to leading critical exponents through the automorphism structure of Q₃. A UniversalityClass is a triple holding the integer rank N, the correlation length exponent ν, and the anomalous dimension η. The satisfies_scaling predicate enforces the four thermodynamic relations (alpha + 2 beta + gamma = 2) for any such class in dimension D=3.
proof idea
The proof is a one-line wrapper. It unfolds the definitions of ising_bootstrap and xy_bootstrap, exposing their ν components as the literals 0.629971 and 0.67169, then applies norm_num to discharge the strict inequality.
why it matters
The declaration records the first step of the expected monotonic rise of ν with N inside the O(N) framework derived from Q₃ geometry. It directly supports the bootstrap reference values (Ising ν=0.62997, XY ν=0.67169, Heisenberg ν=0.71164, spherical ν=1.0) listed in the module documentation. No downstream theorems depend on it yet, but it supplies the base case for any later proof that ν(N) is increasing toward the spherical limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.