fisher_onsager
plain-language theorem explainer
Physicists studying critical phenomena cite the verification that the susceptibility exponent satisfies γ = ν(2 − η) for the exact Onsager values in the two-dimensional Ising model. The relation confirms consistency among the known rationals ν = 1, η = 1/4, γ = 7/4. The proof is a one-line term that unfolds the three constant definitions and normalizes the arithmetic identity via the ring tactic.
Claim. $γ = ν(2 − η)$
background
The module verifies scaling relations for the exact Onsager solution of the two-dimensional Ising model. The relevant exponents appear as simple constants: nu_onsager is defined to be 1, eta_onsager to be 1/4, and gamma_onsager to be 7/4. These values are known to obey the standard scaling identities of critical phenomena. The local theoretical setting is diagnostic: the Recognition Science leading-order formula ν₀ = φ⁻¹ does not reproduce the D = 2 value, consistent with the framework forcing D = 3 as the unique physical dimension from the T0–T8 chain.
proof idea
The term proof unfolds the definitions of gamma_onsager, nu_onsager, and eta_onsager, then applies the ring tactic to confirm the resulting numerical identity.
why it matters
The theorem is used inside the ising2DCert structure that bundles all verified Onsager scaling relations. It supports the module's check that the D = 2 solution obeys Fisher scaling while underscoring that Recognition Science phi-algebraic formulas are derived for three dimensions. The result therefore closes one consistency test before the framework asserts uniqueness of D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.