nu_leading

formal source

 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]
 124  exact thermal_eigenvalue_relevant
 125
 126/-! ## 5. Anomalous-Dimension Correction -/
 127
 128/-- The anomalous correction to ν on a D-dimensional lattice.
 129
 130    When the anomalous dimension η ≠ 0, the thermal direction couples to
 131    the D field modes at the Q₃ spectral gap (multiplicity D).
 132    The correction η/(D + η) is the unique simplest (Padé [0/1]) rational
 133    function satisfying:
 134    * f(0) = 0 (vanishes at leading order),
 135    * f'(0) = 1/D (rate set by the spectral-gap multiplicity).
 136
 137    On Q₃ with D = `Q3_degree` = 3, the spectral-gap multiplicity equals D,
 138    matching the denominator. -/
 139def anomalous_nu_correction (D η : ℝ) : ℝ := η / (D + η)
 140
 141theorem anomalous_nu_correction_zero (D : ℝ) :
 142    anomalous_nu_correction D 0 = 0 := by
 143  unfold anomalous_nu_correction; simp
 144