thermal_eigenvalue_relevant

formal source

 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]
 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,