beta_onsager
plain-language theorem explainer
beta_onsager supplies the Onsager critical exponent β = 1/8 for the two-dimensional Ising model. Critical phenomena researchers cite this value when checking scaling relations such as Rushbrooke and Widom identities against exact solutions. The definition is a direct numerical assignment with no computational steps.
Claim. The magnetic critical exponent β of the two-dimensional Ising model is β = 1/8.
background
Module Physics.Ising2D verifies that the exact Onsager exponents for the D = 2 Ising model satisfy all scaling relations. The relevant definitions include beta_onsager as the magnetic exponent, alongside nu_onsager = 1, eta_onsager = 1/4, gamma_onsager = 7/4, alpha_onsager = 0, and delta_onsager = 15. The local theoretical setting is a diagnostic test of whether Recognition Science φ-algebraic formulas extend to D = 2, where the leading-order RS formula ν₀ = φ^{-1} fails to match the exact ν = 1.
proof idea
The declaration is a direct definition that assigns the rational value 1/8 to beta_onsager.
why it matters
This definition supplies the input constant for the structure Ising2DCert, which certifies that the Onsager exponents obey Rushbrooke, Fisher, Widom, and hyperscaling relations. It also supports the theorems beta_from_scaling, rushbrooke_onsager, and widom_onsager. The placement highlights the module's conclusion that RS derives D = 3 uniquely via the eight-tick octave, so the D = 2 exponents serve only as a diagnostic contrast.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.