alpha_onsager
plain-language theorem explainer
The declaration supplies the Onsager value of the specific heat exponent α for the two-dimensional Ising model by direct substitution into the hyperscaling relation. Physicists verifying scaling laws in exactly solvable models cite this constant when checking consistency with Rushbrooke or hyperscaling identities. The definition performs a one-line arithmetic evaluation using the fixed Onsager inputs D = 2 and ν = 1.
Claim. The Onsager specific-heat exponent is given by $α = 2 - Dν$ evaluated at the two-dimensional values $D = 2$ and $ν = 1$, yielding $α = 0$.
background
In the module on the two-dimensional Ising model, the Onsager exact solution provides rational critical exponents including the correlation-length exponent ν = 1. The spatial dimension is fixed at D = 2. These constants enter the standard scaling relation α = 2 − Dν that holds for the specific-heat singularity. The module tests whether Recognition Science φ-algebraic expressions reproduce these values and finds a discrepancy, as expected since the framework selects D = 3 as the unique physical dimension.
proof idea
The definition is a direct one-line substitution that evaluates 2 minus the product of the dimension constant D2 and the exponent nu_onsager.
why it matters
This supplies the α = 0 input required by the Rushbrooke identity theorem and the hyperscaling relation theorem in the same module. It also appears in the Ising2DCert structure that certifies the full set of Onsager scaling relations. The value highlights the gap between the Recognition Science leading-order formula for ν and the exact Onsager result, reinforcing that the framework targets three-dimensional physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.