energy_nonneg
plain-language theorem explainer
Energy_RS(r) is non-negative for every positive real r. Workers on Noether symmetries and thermodynamic stability in Recognition Science invoke this when certifying ground-state energies. The proof reduces directly to the non-negativity of the J-cost function via a single lemma application.
Claim. For every real number $r > 0$, the recognition energy satisfies $0 ≤ E(r)$, where $E(r) := J(r)$ and $J$ denotes the J-cost function.
background
In the NoetherTheoremDeep module, energy arises from time-translation symmetry of the recognition action, with the explicit definition energy_RS(r) := Jcost(r). The J-cost function itself is given by J(x) = (x + 1/x)/2 - 1, which is known to be non-negative for x > 0 by the AM-GM inequality. Upstream results establish Jcost_nonneg in multiple modules, including Cost.JcostCore and Gravity.CoherenceCollapse, each proving 0 ≤ Jcost(x) for x > 0 via algebraic identities or positivity arguments.
proof idea
The proof is a one-line term that directly invokes the Jcost_nonneg lemma on the hypothesis hr : 0 < r. No further tactics or reductions are required.
why it matters
This theorem supplies the energy_nonneg field of the NoetherTheoremDeepCert structure, which assembles the four charges, non-negativity, and zero-at-equilibrium properties into a single certificate. It completes the energy_from_time_translation step in the module's list of proved results. The non-negativity anchors thermodynamic interpretations and stability arguments downstream in JCostThermoBridge and ILG.CPMInstance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.