climateFeedbackCount
plain-language theorem explainer
Exactly five climate feedback mechanisms are counted in the Recognition Science climate model. Physicists working on energy balance would cite this to match the feedback enumeration to the configuration dimension. The proof uses a decision procedure on the derived Fintype instance.
Claim. The cardinality of the type of climate feedback mechanisms is five: $|$water vapor, ice-albedo, Planck, lapse rate, cloud$| = 5$.
background
In the Climate Physics from RS module, climate equilibrium corresponds to vanishing J-cost in the energy balance. The five canonical mechanisms (water vapor, ice-albedo, Planck, lapse rate, cloud) are formalized as an inductive type deriving Fintype, DecidableEq, and related instances. Upstream, Energy is an abbreviation for the reals in RS-native units, and the inductive definition of ClimateFeedback supplies the finite type structure.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance derived from the inductive ClimateFeedback definition.
why it matters
This theorem supplies the five_feedbacks field inside the climatePhysicsCert definition that certifies the climate model. It realizes the module documentation claim of five feedbacks with zero sorrys. In the Recognition Science setting it ties the J = 0 equilibrium condition to the listed feedbacks while remaining separate from the spatial dimension D = 3 in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.