scaling_always_holds
plain-language theorem explainer
Physicists studying critical phenomena cite this to confirm that the thermodynamic scaling relation holds identically once alpha, beta, and gamma are expressed through nu and eta. The result applies to any universality class with its symmetry rank N and any real dimension D. The proof is a one-line algebraic identity check after unfolding the definitions.
Claim. For any universality class with symmetry rank $N$ and exponents $nu, eta$, and any real dimension $D$, the scaling relation $alpha + 2 beta + gamma = 2$ holds identically, where $alpha = 2 - D nu$, $beta = nu (D - 2 + eta)/2$, and $gamma = nu (2 - eta)$.
background
The module maps O(N) symmetry ranks to critical exponents through the automorphism structure of Q3. A universality class is the structure carrying a natural number N together with real exponents nu and eta. The predicate satisfies_scaling encodes the Rushbrooke scaling relation by substituting the standard expressions for alpha, beta, and gamma and requiring their linear combination to equal 2.
proof idea
The term proof unfolds satisfies_scaling to expose the explicit expressions for alpha, beta, and gamma, then applies the ring tactic to verify the polynomial identity.
why it matters
The declaration shows that the scaling relation is an algebraic tautology under the chosen exponent parametrization, supplying a consistency check for the O(N) classes derived from J-cost in CriticalPhenomenaFromJCost. It anchors the bootstrap targets listed in the module for D = 3 (Ising, XY, Heisenberg) by guaranteeing thermodynamic closure before numerical comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.