xy_bootstrap
plain-language theorem explainer
The definition supplies the O(2) XY universality class with symmetry rank 2, correlation-length exponent 0.67169 and anomalous-dimension exponent 0.03810. Researchers studying critical phenomena cite it when establishing monotonic increase of the correlation-length exponent across O(N) classes or when verifying that the anomalous dimension lies inside the stable band. It is realized by a direct constructor that injects the bootstrap reference values listed in the module documentation.
Claim. The XY universality class is the structure with symmetry rank $N=2$, correlation-length exponent $nu=0.67169$ and anomalous-dimension exponent $eta=0.03810$.
background
A universality class is a structure consisting of an O(N) symmetry rank together with the critical exponents nu and eta. The module maps these classes to subgroups of the automorphism group of the cube Q₃ and supplies bootstrap reference values for D=3. The XY class corresponds to N=2 with the listed exponents. Upstream work defines an inductive enumeration of the same classes for decidability.
proof idea
The definition is a direct constructor application of the UniversalityClass structure with the numerical values 2, 0.67169 and 0.03810.
why it matters
This definition is referenced by the theorems establishing monotonicity of nu between the Ising and XY classes and between the XY and Heisenberg classes, as well as the theorem placing the XY anomalous dimension inside the stable band. It supplies the O(2) entry in the bootstrap reference table and supports the framework claim that D=3 geometry determines the sequence of universality classes via the Q₃ automorphism structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.