 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
 193end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.