IndisputableMonolith.Physics.Ising2D

   1import IndisputableMonolith.Constants
   2
   3/-!
   4# D = 2 Ising Model: Onsager Exact Solution Diagnostic
   5
   6The 2D Ising model is exactly solvable (Onsager, 1944). Its critical exponents
   7are known exactly as rational numbers. This module verifies the Onsager values
   8satisfy the scaling relations and tests whether the RS φ-algebraic formulas
   9extend to D = 2.
  10
  11## Onsager exact exponents (D = 2):
  12  ν = 1, η = 1/4, β = 1/8, γ = 7/4, α = 0 (log divergence), δ = 15
  13
  14## Diagnostic result:
  15  The RS leading-order formula ν₀ = φ⁻¹ does NOT reproduce ν = 1 for D = 2.
  16  This is expected since RS derives D = 3 as the unique physical dimension.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Physics
  21namespace Ising2D
  22
  23open Constants
  24
  25noncomputable section
  26
  27private lemma phi_gt_1618 : (1.618 : ℝ) < phi := by
  28  simp only [phi]
  29  have h5 : (2.236 : ℝ) < Real.sqrt 5 := by
  30    have h : (2.236 : ℝ) ^ 2 < 5 := by norm_num
  31    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.236)]
  32    exact Real.sqrt_lt_sqrt (by norm_num) h
  33  linarith
  34
  35/-! ## Onsager Exact Values -/
  36
  37def D2 : ℝ := 2
  38def nu_onsager : ℝ := 1
  39def eta_onsager : ℝ := 1 / 4
  40def beta_onsager : ℝ := 1 / 8
  41def gamma_onsager : ℝ := 7 / 4
  42def delta_onsager : ℝ := 15
  43
  44/-! ## Scaling Relations for Onsager Values
  45
  46We verify all four scaling relations hold for the exact D = 2 exponents.
  47Note: α = 0 for D = 2 (logarithmic divergence), so we use α = 2 − Dν = 0.
  48-/
  49
  50/-- Onsager α = 2 − 2·1 = 0. -/
  51def alpha_onsager : ℝ := 2 - D2 * nu_onsager
  52
  53theorem alpha_onsager_eq : alpha_onsager = 0 := by
  54  unfold alpha_onsager D2 nu_onsager; ring
  55
  56/-- Rushbrooke: α + 2β + γ = 0 + 2·(1/8) + 7/4 = 0 + 1/4 + 7/4 = 2. -/
  57theorem rushbrooke_onsager : alpha_onsager + 2 * beta_onsager + gamma_onsager = 2 := by
  58  unfold alpha_onsager beta_onsager gamma_onsager D2 nu_onsager; ring
  59
  60/-- Fisher: γ = ν(2 − η) = 1·(2 − 1/4) = 7/4. -/
  61theorem fisher_onsager : gamma_onsager = nu_onsager * (2 - eta_onsager) := by
  62  unfold gamma_onsager nu_onsager eta_onsager; ring
  63
  64/-- Hyperscaling (D = 2): Dν = 2 − α → 2·1 = 2 − 0 = 2. -/
  65theorem hyperscaling_onsager : D2 * nu_onsager = 2 - alpha_onsager := by
  66  simp only [D2, nu_onsager, alpha_onsager]; ring
  67
  68/-- Widom: γ = β(δ − 1) = (1/8)·14 = 14/8 = 7/4. -/
  69theorem widom_onsager : gamma_onsager = beta_onsager * (delta_onsager - 1) := by
  70  unfold gamma_onsager beta_onsager delta_onsager; ring
  71
  72/-- β from scaling: β = ν(D − 2 + η)/2 = 1·(0 + 1/4)/2 = 1/8. -/
  73theorem beta_from_scaling : beta_onsager = nu_onsager * (D2 - 2 + eta_onsager) / 2 := by
  74  unfold beta_onsager nu_onsager D2 eta_onsager; ring
  75
  76/-- δ from scaling: δ = (D + 2 − η)/(D − 2 + η) = (4 − 1/4)/(0 + 1/4) = (15/4)/(1/4) = 15. -/
  77theorem delta_from_scaling : delta_onsager = (D2 + 2 - eta_onsager) / (D2 - 2 + eta_onsager) := by
  78  unfold delta_onsager D2 eta_onsager; norm_num
  79
  80/-! ## RS Leading-Order Fails for D = 2
  81
  82The RS leading-order ν₀ = φ⁻¹ ≈ 0.618 does not equal the Onsager ν = 1.
  83This is expected: RS derives D = 3 as the unique physical dimension.
  84The D = 2 result is a diagnostic, not a contradiction.
  85-/
  86
  87/-- RS leading-order ν₀ = φ⁻¹ < 1 = ν_Onsager. -/
  88theorem rs_leading_order_below_onsager : 1 / phi < nu_onsager := by
  89  unfold nu_onsager
  90  have h := one_lt_phi
  91  have hp := phi_pos
  92  have : 1 / phi < 1 / 1 := by
  93    exact (one_div_lt_one_div phi_pos (by norm_num : (0:ℝ) < 1)).mpr h
  94  linarith
  95
  96/-- The gap: ν_Onsager − ν₀ > 0.38 (a 38% discrepancy). -/
  97theorem onsager_rs_gap : (0.38 : ℝ) < nu_onsager - 1 / phi := by
  98  unfold nu_onsager
  99  have h_upper : 1 / phi < (0.619 : ℝ) :=
 100    calc 1 / phi < 1 / (1.618 : ℝ) :=
 101        (one_div_lt_one_div phi_pos (by norm_num : (0:ℝ) < 1.618)).mpr phi_gt_1618
 102      _ < (0.619 : ℝ) := by norm_num
 103  linarith
 104
 105/-! ## Certificate -/
 106
 107structure Ising2DCert where
 108  rushbrooke : alpha_onsager + 2 * beta_onsager + gamma_onsager = 2
 109  fisher : gamma_onsager = nu_onsager * (2 - eta_onsager)
 110  widom : gamma_onsager = beta_onsager * (delta_onsager - 1)
 111  hyperscaling : D2 * nu_onsager = 2 - alpha_onsager
 112  alpha_zero : alpha_onsager = 0
 113  rs_fails : 1 / phi < nu_onsager
 114
 115def ising2DCert : Ising2DCert where
 116  rushbrooke := rushbrooke_onsager
 117  fisher := fisher_onsager
 118  widom := widom_onsager
 119  hyperscaling := hyperscaling_onsager
 120  alpha_zero := alpha_onsager_eq
 121  rs_fails := rs_leading_order_below_onsager
 122
 123end
 124
 125end Ising2D
 126end Physics
 127end IndisputableMonolith
 128