nu_onsager
plain-language theorem explainer
The declaration supplies the exact Onsager correlation-length exponent for the two-dimensional Ising model. Critical-phenomena researchers and Recognition Science testers comparing dimension-specific predictions cite this constant when verifying scaling relations. It enters as a direct numerical assignment that subsequent algebraic identities then unfold.
Claim. The correlation-length exponent of the two-dimensional Ising model is given by $nu = 1$.
background
The module records the exact Onsager solution for the D = 2 Ising model and checks that its critical exponents satisfy the standard scaling relations while exposing the mismatch with Recognition Science formulas. Onsager exponents are stated as rational numbers: nu = 1, eta = 1/4, beta = 1/8, gamma = 7/4, alpha = 0 (log divergence), delta = 15. These satisfy Rushbrooke, Fisher, Widom, and hyperscaling identities in two dimensions. The local setting tests whether the RS leading-order formula nu_0 = phi^{-1} reproduces the D = 2 value; the module records that it does not, consistent with the framework's derivation of D = 3 as the unique physical dimension.
proof idea
The definition is a direct constant assignment of the real number 1. No lemmas or tactics are applied; the value is supplied for immediate use in the surrounding algebraic verifications of scaling laws.
why it matters
This constant anchors the Onsager exponent suite that populates the Ising2DCert structure, which certifies that Rushbrooke, Fisher, Widom, and hyperscaling relations hold exactly for D = 2. It feeds alpha_onsager, beta_from_scaling, fisher_onsager, and hyperscaling_onsager, all of which unfold it to confirm alpha = 0 and D nu = 2 - alpha. The declaration thereby quantifies the gap between the exact value 1 and the RS leading-order prediction 1/phi, reinforcing the framework's T8 result that D = 3 is forced by the eight-tick octave and J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.