nu_corrected_at_zero

formal source

 159def nu_corrected (D η : ℝ) : ℝ :=
 160  nu_leading + anomalous_nu_correction D η
 161
 162theorem nu_corrected_at_zero (D : ℝ) :
 163    nu_corrected D 0 = nu_leading := by
 164  unfold nu_corrected; rw [anomalous_nu_correction_zero]; ring
 165
 166/-- The Q₃ spectral-gap multiplicity equals the graph degree D = 3.
 167    This is the structural reason why D = 3 appears in the denominator
 168    of the anomalous correction. -/
 169theorem spectral_gap_multiplicity_eq_degree :
 170    Q3_multiplicities = [1, Q3_degree, Q3_degree, 1] := by
 171  unfold Q3_multiplicities Q3_degree; native_decide
 172
 173/-! ## 6. Summary Certificate -/
 174
 175structure ThermalFixedPointCert where
 176  char_poly_root : fibonacci_char_poly phi = 0
 177  uniqueness : ∀ r : ℝ, 0 < r → fibonacci_char_poly r = 0 → r = phi
 178  cascade : ∀ n : ℕ, phi ^ (n + 2) = phi ^ (n + 1) + phi ^ n
 179  eigenvalue : thermal_eigenvalue = phi
 180  nu : nu_leading = 1 / phi
 181
 182def thermalFixedPointCert : ThermalFixedPointCert where
 183  char_poly_root := fibonacci_char_poly_root
 184  uniqueness := fibonacci_char_poly_unique_pos_root
 185  cascade := fibonacci_recurrence
 186  eigenvalue := rfl
 187  nu := rfl
 188
 189end
 190
 191end ThermalFixedPoint
 192end Physics