rushbrooke_onsager
plain-language theorem explainer
The Rushbrooke scaling relation holds exactly for the Onsager critical exponents of the two-dimensional Ising model. Researchers auditing scaling relations in exactly solvable lattice models would cite this verification. The proof substitutes the explicit values for alpha, beta and gamma then simplifies the arithmetic identity.
Claim. $α + 2β + γ = 2$ where $α = 0$, $β = 1/8$, $γ = 7/4$ are the Onsager critical exponents for the two-dimensional Ising model.
background
The module records the Onsager 1944 solution for the D=2 Ising model and lists its exact rational exponents: ν=1, η=1/4, β=1/8, γ=7/4, α=0 (log divergence), δ=15. Alpha_onsager is defined as 2 − D2 · nu_onsager with D2=2 and nu_onsager=1, so alpha_onsager evaluates to zero. Beta_onsager and gamma_onsager are the fixed constants 1/8 and 7/4. The local setting is a diagnostic check whether RS φ-algebraic formulas reproduce these D=2 values; the module states that the leading-order RS formula ν₀ = φ⁻¹ does not match ν=1, as expected since RS derives D=3 uniquely.
proof idea
The proof unfolds the definitions of alpha_onsager, beta_onsager, gamma_onsager, D2 and nu_onsager, then applies the ring tactic to reduce the resulting arithmetic expression to the identity 2=2.
why it matters
The theorem supplies the Rushbrooke component to the ising2DCert certificate that bundles all Onsager scaling relations. It confirms the standard hyperscaling identity holds exactly in D=2, furnishing a baseline against which the Recognition Science derivation of D=3 from the eight-tick octave (T7–T8) can be contrasted. The module explicitly notes that the RS φ-ladder formulas are not expected to reproduce the D=2 exponents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.