heisenberg_bootstrap
plain-language theorem explainer
The Heisenberg bootstrap supplies the O(3) reference values nu = 0.71164 and eta = 0.03784 for three-dimensional systems with vector order parameter. Physicists modeling magnetic phase transitions cite these numbers when comparing renormalization-group flows to measured critical exponents. The definition is a direct record constructor that populates the UniversalityClass structure with the bootstrap numbers stated in the module documentation.
Claim. The Heisenberg universality class is the structure with symmetry rank $N=3$, correlation-length exponent $nu=0.71164$, and anomalous-dimension exponent $eta=0.03784$.
background
The module maps O(N) symmetry ranks to critical exponents via subgroups of Aut(Q₃). UniversalityClass is the structure whose fields are the natural number N together with the real numbers nu and eta; any such triple must satisfy the four thermodynamic scaling relations. The Heisenberg entry corresponds to the O(3) case in three dimensions, with the listed numerical values taken from the bootstrap reference table in the module documentation.
proof idea
One-line definition that applies the UniversalityClass constructor to the triple (3, 0.71164, 0.03784).
why it matters
This definition supplies the concrete values consumed by heisenberg_eta_in_band, nu_monotone_heisenberg_spherical, and nu_monotone_xy_heisenberg. It completes the O(3) row of the bootstrap table for D=3 systems, allowing direct numerical checks that the exponents lie inside the stable eta band and increase monotonically with N.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.