alpha_2D_Ising
plain-language theorem explainer
alpha_2D_Ising sets the specific-heat critical exponent for the two-dimensional Ising model to zero by treating its logarithmic divergence as an exponent of zero. Researchers checking scaling relations in two-dimensional critical phenomena cite this constant when confirming Rushbrooke and Josephson identities. The implementation is a direct one-line assignment of the numerical value 0.
Claim. For the two-dimensional Ising model the specific-heat critical exponent is defined by $α = 0$.
background
The module derives universal critical exponents from φ-scaling near phase transitions. Standard notation defines specific heat diverging as |t|^{-α}, order parameter as (-t)^β, susceptibility as |t|^{-γ}, and correlation length as |t|^{-ν}, with t the reduced temperature. Recognition Science obtains universality from J-cost fluctuations that are structured by the golden-ratio fixed point, independent of microscopic lattice details.
proof idea
The declaration is a direct definition that assigns the constant value 0. Downstream theorems such as rushbrooke_relation_2D and josephson_hyperscaling_2D unfold the identifier and reduce the resulting numerical identity with norm_num.
why it matters
This supplies the α value required by the Rushbrooke relation and Josephson hyperscaling theorems in two dimensions. It completes the 2D case of the THERMO-005 derivation of universal critical exponents from golden-ratio scaling. The assignment is consistent with the φ-scaling mechanism that constrains exponents by dimensionality and symmetry class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.