Physics Ising2 D

The two-dimensional Ising check

The two-dimensional Ising model is a lattice of tiny magnets, each pointing up or down, that was solved exactly by Lars Onsager in 1944. Near its critical temperature, where the material flips between ordered and disordered states, its behavior is described by a set of exponents: ν = 1, η = 1/4, β = 1/8, γ = 7/4, and δ = 15. These are exact rational numbers, not approximations, and they satisfy the four scaling relations of critical phenomena: Rushbrooke, Fisher, Widom, and hyperscaling.

In Recognition Science, the framework's core result forces three spatial dimensions as the unique physical dimension. Its leading-order prediction for the correlation length exponent is ν₀ = φ⁻¹ ≈ 0.618, where φ is the golden ratio. The two-dimensional Ising model provides a sharp test: the Onsager value is ν = 1, which is larger than 0.618 by more than 0.38, a 38 percent discrepancy. This is not a failure of the framework; it is a diagnostic. The framework derives D = 3, so its formulas are not expected to reproduce the D = 2 case.

The module ledger, a discrete record of events, verifies the Onsager exponents satisfy all four scaling relations, including the hyperscaling relation Dν = 2 − α, which holds only in two dimensions. It then proves the RS leading-order value falls below the Onsager value. The certificate bundles these results: the classical exponents are internally consistent, and the framework's prediction does not match them, exactly as expected for a theory that singles out three dimensions.

The practical lesson is that the framework's reach is dimension-specific. The golden-ratio formula works in three dimensions, where it was derived, and fails in two, where it was never claimed to apply. The module documents this boundary explicitly, turning a potential embarrassment into a precise statement about the framework's domain of validity.

def nu_onsager : ℝ := 1

def eta_onsager : ℝ := 1 / 4

def beta_onsager : ℝ := 1 / 8

def gamma_onsager : ℝ := 7 / 4

def delta_onsager : ℝ := 15

/-- Rushbrooke: α + 2β + γ = 0 + 2·(1/8) + 7/4 = 0 + 1/4 + 7/4 = 2. -/
theorem rushbrooke_onsager : alpha_onsager + 2 * beta_onsager + gamma_onsager = 2 := by
  unfold alpha_onsager beta_onsager gamma_onsager D2 nu_onsager; ring

/-- Fisher: γ = ν(2 − η) = 1·(2 − 1/4) = 7/4. -/
theorem fisher_onsager : gamma_onsager = nu_onsager * (2 - eta_onsager) := by
  unfold gamma_onsager nu_onsager eta_onsager; ring

/-- Widom: γ = β(δ − 1) = (1/8)·14 = 14/8 = 7/4. -/
theorem widom_onsager : gamma_onsager = beta_onsager * (delta_onsager - 1) := by
  unfold gamma_onsager beta_onsager delta_onsager; ring

/-- Hyperscaling (D = 2): Dν = 2 − α → 2·1 = 2 − 0 = 2. -/
theorem hyperscaling_onsager : D2 * nu_onsager = 2 - alpha_onsager := by
  simp only [D2, nu_onsager, alpha_onsager]; ring

/-- RS leading-order ν₀ = φ⁻¹ < 1 = ν_Onsager. -/
theorem rs_leading_order_below_onsager : 1 / phi < nu_onsager := by
  unfold nu_onsager
  have h := one_lt_phi
  have hp := phi_pos
  have : 1 / phi < 1 / 1 := by
    exact (one_div_lt_one_div phi_pos (by norm_num : (0:ℝ) < 1)).mpr h
  linarith

/-- The gap: ν_Onsager − ν₀ > 0.38 (a 38% discrepancy). -/
theorem onsager_rs_gap : (0.38 : ℝ) < nu_onsager - 1 / phi := by
  unfold nu_onsager
  have h_upper : 1 / phi < (0.619 : ℝ) :=
    calc 1 / phi < 1 / (1.618 : ℝ) :=
        (one_div_lt_one_div phi_pos (by norm_num : (0:ℝ) < 1.618)).mpr phi_gt_1618
      _ < (0.619 : ℝ) := by norm_num
  linarith

What this page does not claim

The RS framework predicts the Onsager exponents in two dimensions. The discrepancy between the RS value and the Onsager value is a contradiction of the framework. The Onsager solution itself is derived from the RS framework.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/Ising2D.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: