alpha_onsager_eq
plain-language theorem explainer
The declaration establishes that the Onsager critical exponent alpha equals zero for the two-dimensional Ising model. Researchers verifying scaling relations or testing dimension-specific formulas in critical phenomena would cite this result. The proof is a one-line wrapper that unfolds the definition of alpha_onsager in terms of D2 and nu_onsager then simplifies the arithmetic via the ring tactic.
Claim. The Onsager specific-heat exponent satisfies $alpha = 2 - D nu = 0$, where $D = 2$ and $nu = 1$.
background
The module examines the exactly solvable two-dimensional Ising model whose Onsager exponents are nu = 1, eta = 1/4, beta = 1/8, gamma = 7/4, alpha = 0, and delta = 15. It defines D2 as the spatial dimension equal to 2 and nu_onsager as the correlation-length exponent equal to 1. The quantity alpha_onsager is introduced by the relation alpha_onsager := 2 - D2 * nu_onsager, which encodes the standard hyperscaling identity for the specific-heat exponent in this setting.
proof idea
The proof is a one-line wrapper that unfolds the definitions of alpha_onsager, D2, and nu_onsager, then applies the ring tactic to reduce the expression 2 - 2 * 1 to zero.
why it matters
The result supplies the alpha_zero field inside the ising2DCert structure that assembles the verified Onsager scaling relations. It reinforces the module's diagnostic that the Recognition Science phi-algebraic formulas, which derive D = 3 via the eight-tick octave and the self-similar fixed point, do not reproduce the D = 2 exponents, as expected from the framework's uniqueness claim for three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.