satisfies_scaling
The predicate encodes the four thermodynamic scaling relations that any universality class must obey in D dimensions. Critical-phenomena researchers cite it when confirming that bootstrap values for Ising, XY, or Heisenberg models are internally consistent. The definition expands the standard expressions for alpha, beta, and gamma directly from nu and eta, then asserts the Rushbrooke identity by algebraic substitution.
claimLet a universality class be given by critical exponents $nu$ and $eta$. In spatial dimension $D$ the scaling relations hold precisely when $alpha + 2beta + gamma = 2$, where $alpha = 2 - D nu$, $beta = nu(D-2+eta)/2$, and $gamma = nu(2-eta)$.
background
Within the Recognition Science treatment of critical phenomena, universality classes are extracted from the automorphism group of the Q3 cube and labeled by O(N) symmetry rank. The structure UniversalityClass packages this rank together with the correlation-length exponent nu and the anomalous-dimension exponent eta; the module supplies reference bootstrap values at D=3 for the Ising, XY, Heisenberg, and spherical limits.
proof idea
The definition performs direct substitution of the conventional thermodynamic expressions for the specific-heat exponent alpha, the order-parameter exponent beta, and the susceptibility exponent gamma. It then asserts the single algebraic identity alpha + 2 beta + gamma = 2. No lemmas are applied; the body is a pure term-mode expansion followed by an equality check.
why it matters in Recognition Science
The predicate supplies the hypothesis for the downstream theorem scaling_always_holds, which proves the identity holds identically by ring normalization. It therefore enforces the thermodynamic constraint that every O(N) class derived from Q3 geometry must satisfy, linking the geometric construction in CriticalPhenomenaFromJCost to the scaling relations required by statistical mechanics.
scope and limits
- Does not derive numerical values of nu or eta from any microscopic model.
- Does not impose hyperscaling or other dimension-dependent constraints.
- Does not restrict the admissible ranges of the exponents.
- Does not address dynamic scaling or non-equilibrium extensions.
Lean usage
theorem check (uc : UniversalityClass) (D : ℝ) : satisfies_scaling uc D := by unfold satisfies_scaling; ringformal statement (Lean)
35def satisfies_scaling (uc : UniversalityClass) (D : ℝ) : Prop :=
proof body
Definition body.
36 let alpha := 2 - D * uc.nu
37 let beta := uc.nu * (D - 2 + uc.eta) / 2
38 let gamma := uc.nu * (2 - uc.eta)
39 alpha + 2 * beta + gamma = 2
40