thermal_eigenvalue_eq_phi

formal source

  90       nothing else. -/
  91def thermal_eigenvalue : ℝ := phi
  92
  93theorem thermal_eigenvalue_eq_phi : thermal_eigenvalue = phi := rfl
  94
  95/-- No other positive real can serve as the thermal eigenvalue. -/
  96theorem thermal_eigenvalue_uniqueness (r : ℝ) (hr : 0 < r)
  97    (h : fibonacci_char_poly r = 0) : r = thermal_eigenvalue :=
  98  fibonacci_char_poly_unique_pos_root r hr h
  99
 100/-- The thermal eigenvalue satisfies the golden equation y² = y + 1. -/
 101theorem thermal_eigenvalue_golden :
 102    thermal_eigenvalue ^ 2 = thermal_eigenvalue + 1 := phi_sq_eq
 103
 104theorem thermal_eigenvalue_pos : 0 < thermal_eigenvalue := phi_pos
 105
 106/-- y_t > 1: the thermal direction is relevant (not marginal). -/
 107theorem thermal_eigenvalue_relevant : 1 < thermal_eigenvalue := one_lt_phi
 108
 109/-! ## 4. The Forced Leading-Order ν -/
 110
 111/-- Leading-order correlation-length exponent: ν₀ = 1/y_t.
 112    This is the standard RG relationship between the thermal eigenvalue
 113    and the divergence of the correlation length at the critical point. -/
 114def nu_leading : ℝ := 1 / thermal_eigenvalue
 115
 116theorem nu_leading_eq : nu_leading = 1 / phi := rfl
 117
 118theorem nu_leading_pos : 0 < nu_leading :=
 119  div_pos one_pos thermal_eigenvalue_pos
 120
 121/-- ν₀ < 1 (sub-mean-field, as expected for D = 3). -/
 122theorem nu_leading_lt_one : nu_leading < 1 := by
 123  rw [nu_leading, div_lt_one thermal_eigenvalue_pos]