beta_from_scaling
plain-language theorem explainer
The scaling relation for the magnetic exponent beta holds exactly for the Onsager solution of the two-dimensional Ising model. Researchers verifying hyperscaling or critical-exponent identities in statistical mechanics would cite this algebraic check. The proof substitutes the four rational Onsager constants and reduces the expression by ring arithmetic.
Claim. $beta = nu (D-2+eta)/2$ holds for the Onsager values $D=2$, $nu=1$, $eta=1/4$, recovering $beta=1/8$.
background
The module records the exact Onsager exponents for the two-dimensional Ising model and tests their consistency with scaling relations. D2 is defined as the spatial dimension 2; nu_onsager, eta_onsager and beta_onsager are the corresponding rational constants 1, 1/4 and 1/8. The surrounding context is a diagnostic that contrasts these values with the Recognition Science phi-ladder predictions, which are derived only for D=3.
proof idea
The term proof unfolds the four definitions beta_onsager, nu_onsager, D2 and eta_onsager, then applies the ring tactic to obtain the algebraic identity.
why it matters
The declaration verifies one of the standard scaling relations inside the Onsager-exponent suite that also contains rushbrooke_onsager and hyperscaling_onsager. It underscores the module's diagnostic conclusion that the Recognition Science leading-order formula for nu does not reproduce the D=2 value, consistent with the framework's derivation of D=3 as the unique physical dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.