theorem
proved
climateFeedbackCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ClimatePhysicsFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | waterVapor | iceAlbedo | planck | lapseRate | cloud
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem climateFeedbackCount : Fintype.card ClimateFeedback = 5 := by decide
29
30/-- Energy balance: J = 0. -/
31theorem energy_balance : Jcost 1 = 0 := Jcost_unit0
32
33structure ClimatePhysicsCert where
34 five_feedbacks : Fintype.card ClimateFeedback = 5
35 balance : Jcost 1 = 0
36
37def climatePhysicsCert : ClimatePhysicsCert where
38 five_feedbacks := climateFeedbackCount
39 balance := energy_balance
40
41end IndisputableMonolith.Physics.ClimatePhysicsFromRS