UniversalityClass
plain-language theorem explainer
The UniversalityClass structure packages the O(N) symmetry rank together with the critical exponents nu and eta. Critical-phenomena researchers cite it when checking thermodynamic scaling or when instantiating bootstrap values for Ising, XY and Heisenberg classes. The declaration is a plain record definition with three fields and no proof obligations.
Claim. A universality class is a triple $(N, nu, eta)$ where $N$ is a natural number giving the O(N) symmetry rank and $nu, eta$ are real numbers giving the correlation-length and anomalous-dimension exponents.
background
The module maps subgroups of Aut(Q3) to O(N) universality classes in three spatial dimensions. An upstream inductive type in CriticalPhenomenaFromJCost enumerates the five concrete classes (Ising, XY, Heisenberg, mean-field, percolation). The present structure supplies the numerical data that those classes carry. Module documentation lists the D=3 reference values: Ising nu approximately 0.62997 eta 0.03630, XY nu 0.67169 eta 0.03810, Heisenberg nu 0.71164 eta 0.03784, and spherical nu 1 eta 0.
proof idea
Structure definition that introduces the three fields N, nu, eta.
why it matters
The record is the data type consumed by CriticalPhenomenaCert and by the bootstrap constants ising_bootstrap, heisenberg_bootstrap, xy_bootstrap and spherical_exact. It supplies the concrete exponents required by the O(N) framework that the module derives from Q3 automorphism structure. The declaration does not close any open question in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.