def definition def or abbrev

`thermalFixedPointCert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 182def thermalFixedPointCert : ThermalFixedPointCert where
 183  char_poly_root := fibonacci_char_poly_root

proof body

Definition body.

 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

depends on (6)

Lean names referenced from this declaration's body.

fibonacci_recurrence in IndisputableMonolith.Information.LocalCache decl_use
fibonacci_recurrence in IndisputableMonolith.Physics.EightTickPeriodicityFromD decl_use
fibonacci_char_poly_root in IndisputableMonolith.Physics.ThermalFixedPoint decl_use
fibonacci_char_poly_unique_pos_root in IndisputableMonolith.Physics.ThermalFixedPoint decl_use
fibonacci_recurrence in IndisputableMonolith.Physics.ThermalFixedPoint decl_use
ThermalFixedPointCert in IndisputableMonolith.Physics.ThermalFixedPoint decl_use