jcost_energy_nonneg
plain-language theorem explainer
J-cost energy, defined as the product of the positive coherence quantum E_coh and the J-cost function J(x) for ratio x, is non-negative for every x > 0. Engineers deriving storage density limits in the Recognition Science phi-ladder model cite this to guarantee no negative energies enter the hierarchy. The proof is a direct term reduction that multiplies the positivity of E_coh by the non-negativity of J(x).
Claim. For every real number $x > 0$, $0 ≤ E_{coh} · J(x)$, where $E_{coh} = φ^{-5}$ eV is the coherence quantum and $J(x) = ½(x + x^{-1}) - 1$.
background
In the EN-004 module, energy stored per recognition event equals J(x) times the coherence quantum E_coh = φ^{-5} eV. The J-cost satisfies J(1) = 0 with J(x) diverging as x approaches 0 or infinity. Upstream Jcost_nonneg states that J(x) ≥ 0 for x > 0 by the AM-GM inequality or direct squaring, while E_coh_storage_pos establishes that the coherence energy itself is positive.
proof idea
Unfolds the definition of jcost_energy to the product E_coh_storage * Jcost x. Applies the multiplication non-negativity lemma to E_coh_storage_pos.le together with Jcost_nonneg hx.
why it matters
This result secures non-negativity of stored energy inside the EN-004 energy storage density derivation and feeds directly into the en004_certificate that marks the full hierarchy as derived. It closes the step required before minimum-energy and ratio theorems can be stated, consistent with the J-uniqueness fixed point and the phi-ladder structure that separates chemical, nuclear, and mass-energy regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.