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

UniversalityClass

show as:
view Lean formalization →

UniversalityClass packages the O(N) symmetry rank together with the critical exponents nu and eta. Researchers mapping symmetry groups to scaling behavior in three dimensions cite it when labeling Ising, XY or Heisenberg classes. The entry is a bare structure definition with no computational content or proof obligations.

claimA 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 presents O(N) universality classes as subgroups of Aut(Q3). It supplies reference values for D=3: Ising (N=1) with nu approximately 0.630 and eta approximately 0.036, XY (N=2), Heisenberg (N=3) and the spherical limit (N infinite). Upstream the inductive UniversalityClass in CriticalPhenomenaFromJCost enumerates the five discrete classes Ising, Heisenberg, XY, meanField and percolation. The eta definitions supply the baryon-to-photon ratio from nucleosynthesis and the metric bilinear form.

proof idea

The declaration is a structure definition that introduces the three fields N, nu and eta with no further computation or proof obligations.

why it matters in Recognition Science

This structure carries the bootstrap values (ising_bootstrap, heisenberg_bootstrap) and supplies the input to satisfies_scaling, which checks the thermodynamic relations alpha + 2 beta + gamma = 2. It feeds CriticalPhenomenaCert asserting exactly five classes. In the Recognition framework it supplies the concrete exponents that connect J-cost geometry to observed critical phenomena in D=3.

scope and limits

formal statement (Lean)

  29structure UniversalityClass where
  30  N : ℕ
  31  nu : ℝ
  32  eta : ℝ
  33
  34/-- The four thermodynamic scaling relations constrain any universality class. -/

used by (9)

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

depends on (3)

Lean names referenced from this declaration's body.