atmospheric_equilibrium
plain-language theorem explainer
The declaration establishes that the J-cost vanishes at the unit argument, supplying the equilibrium condition for atmospheric stability in the Recognition Science model. Researchers modeling convective layers or inversion layers cite it when setting J = 0 as the stable boundary. The proof reduces directly to the unit lemma for the J-cost function via a one-line application.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2 / (2x)$ is the J-cost.
background
In the Atmospheric Physics from RS module, atmospheric stability is identified with J-cost balance. Positive J-cost signals convective instability for a rising parcel, while J = 0 marks stable inversion layers. The module equates five canonical layers and five weather phenomena to configDim D = 5. The J-cost is defined as J(x) = (x-1)²/(2x) in the Cost module. This theorem supplies the equilibrium value at the unit scale. It rests on the lemma Jcost_unit0 which states Jcost 1 = 0 by simplification.
proof idea
One-line wrapper that applies the lemma Jcost_unit0 from the Cost module.
why it matters
This result supplies the equilibrium field inside the atmosphericPhysicsCert definition that bundles the five layers, five phenomena, and the zero-cost condition. It realizes the J-cost balance for stability described in the module documentation. Within the framework it fixes the zero point of the cost function, consistent with J-uniqueness at T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.