ising_bootstrap
plain-language theorem explainer
The ising_bootstrap definition records the conformal bootstrap reference values for the O(1) Ising universality class in three dimensions. It fixes symmetry rank N=1 together with nu=0.629971 and eta=0.0362978. Researchers comparing RS-derived critical exponents to known D=3 results cite these numbers as targets. The entry is a direct structure constructor with no further computation.
Claim. The O(1) Ising universality class is the structure with symmetry rank $N=1$, correlation-length exponent $nu=0.629971$, and anomalous dimension $eta=0.0362978$.
background
UniversalityClass is the structure that stores symmetry rank N along with the two critical exponents nu and eta. The module maps O(N) symmetry groups to these exponents via the automorphism structure of the cube Q3. An upstream inductive type in CriticalPhenomenaFromJCost enumerates the classes Ising, XY, Heisenberg, mean-field, and percolation. The present definition supplies the high-precision D=3 bootstrap numbers listed in the module header as reference targets.
proof idea
This is a one-line definition that applies the UniversalityClass constructor to the triple (1, 0.629971, 0.0362978).
why it matters
The definition supplies the numerical targets used by the downstream theorems ising_eta_in_band and nu_monotone_ising_xy. It occupies the bootstrap reference slot inside the O(N) universality classes framework, allowing direct comparison with RS derivations of exponents at D=3. The surrounding module situates these values within the Q3 geometry and the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.