widom_relation_2D
plain-language theorem explainer
The declaration verifies that the Widom scaling relation holds exactly for the two-dimensional Ising model using its known critical exponents. Researchers in statistical mechanics or critical phenomena would cite it to confirm consistency of the 2D values with scaling hypotheses. The proof is a one-line wrapper that substitutes the explicit definitions and normalizes the resulting arithmetic identity.
Claim. In the two-dimensional Ising model the critical exponents satisfy the Widom relation $γ = β(δ - 1)$, where $β = 1/8$, $γ = 7/4$ and $δ = 15$.
background
The module THERMO-005 derives universal critical exponents from Recognition Science φ-scaling near phase transitions. Quantities diverge as power laws in the reduced temperature t: specific heat ~ |t|^{-α}, order parameter ~ (-t)^β, susceptibility ~ |t|^{-γ}, and correlation length ~ |t|^{-ν}. The 2D Ising model is exactly solvable with the explicit values α = 0 (logarithmic), β = 1/8, γ = 7/4, ν = 1, η = 1/4, δ = 15. The upstream definitions supply these constants directly: beta_2D_Ising := 1/8, gamma_2D_Ising := 7/4, delta_2D_Ising := 15.
proof idea
The proof is a one-line wrapper that unfolds the three definitions of the 2D Ising exponents and applies norm_num to confirm the arithmetic identity 7/4 = (1/8) * (15 - 1).
why it matters
This declaration confirms that the exact 2D Ising exponents satisfy the Widom relation, a standard consequence of scaling hypotheses in critical phenomena. It supports the module's aim of linking exponents to φ-scaling by first establishing consistency with classical results. In the Recognition Science framework it aligns with universality from φ-structured fluctuations near criticality, as stated in the module doc-comment on THERMO-005. No open questions are addressed here because the 2D case is fully settled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.