hyperscaling_onsager
plain-language theorem explainer
The hyperscaling relation holds exactly for the two-dimensional Ising model using Onsager exponents, confirming that twice the correlation-length exponent equals two minus the specific-heat exponent. Researchers auditing scaling relations in exactly solvable critical models or checking consistency with dimension-specific predictions would cite this verification. The proof substitutes the explicit numerical values for dimension, correlation length exponent, and specific-heat exponent then reduces the arithmetic identity by ring simplification.
Claim. In two spatial dimensions the hyperscaling relation reads $2ν = 2 - α$, where $ν = 1$ and $α = 0$ are the exact Onsager critical exponents for the Ising model.
background
The module examines the two-dimensional Ising model whose critical exponents are known exactly from Onsager's 1944 solution. These include the correlation-length exponent $ν = 1$, the specific-heat exponent $α = 0$ (logarithmic divergence), and the spatial dimension fixed at two. The upstream definition of the specific-heat exponent is given directly by $α = 2 - 2ν$, which is the algebraic rearrangement of the hyperscaling relation itself.
proof idea
The proof is a one-line wrapper that substitutes the definitions of the spatial dimension, the correlation-length exponent, and the specific-heat exponent, then invokes the ring tactic to verify the arithmetic identity.
why it matters
This result is assembled into the composite certificate ising2DCert that collects all Onsager scaling relations. It fills the hyperscaling slot in the diagnostic that contrasts the exact D = 2 solution against the Recognition Science derivation of D = 3 as the unique physical dimension. The module notes that the RS φ-algebraic formula for ν is not expected to reproduce the two-dimensional value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.