energy_balance
plain-language theorem explainer
The theorem states that the J-cost function evaluates to zero at argument one, encoding the energy balance condition for climate equilibrium in Recognition Science. Climate physicists would cite it to anchor the zero-imbalance state in planetary energy budgets. The proof applies the unit lemma Jcost_unit0 by direct reference.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2 / (2x)$ is the J-cost function.
background
The Climate Physics from RS module derives climate properties from the Recognition Science framework, with climate equilibrium defined by J = 0 in the energy budget and forcing by J > 0. The J-cost is expressed as the squared ratio J(x) = (x-1)^2 / (2x), per the upstream lemma in the Cost module. This theorem specializes the general unit result to the point x = 1.
proof idea
The proof is a direct reference to the lemma Jcost_unit0 from the Cost module, which simplifies Jcost 1 using the definition of Jcost.
why it matters
This theorem supplies the balance field in the climatePhysicsCert definition, which pairs it with the count of five feedbacks. It realizes the module claim that climate equilibrium equals J = 0, linking to the RS treatment of energy balance within the five-feedback configuration. No open questions attach to this specific instantiation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.