pith. machine review for the scientific record. sign in
def definition def or abbrev high

ising_bootstrap

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  51def ising_bootstrap : UniversalityClass := ⟨1, 0.629971, 0.0362978⟩

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.