jcost_energy_min_at_ground
plain-language theorem explainer
Recognition Science expresses stored energy as E_coh times J(x), where J attains its global minimum of zero at the ground state x=1. The theorem asserts that this ground-state value is minimal for every positive real x and is cited by the EN-004 certificate and the phi-coherent minimization result. The term-mode proof unfolds the energy definition, reduces via Jcost_unit0, and closes with the product of two non-negative quantities.
Claim. $E_coh J(1) ≤ E_coh J(x)$ for all $x > 0$, where $J(x) = ½(x + x^{-1}) - 1$ and $E_coh = φ^{-5}$ eV.
background
The EN-004 module derives energy storage limits from the Recognition Science J-cost structure. Energy takes the form E = J(x) · E_coh with E_coh = φ^{-5} eV; the function J(x) = ½(x + x^{-1}) - 1 reaches its absolute minimum J(1) = 0 at the ground state and diverges at both zero and infinity. The upstream lemma Jcost_nonneg states that J(x) ≥ 0 for x > 0 by the AM-GM inequality, while Jcost_unit0 records the explicit value J(1) = 0.
proof idea
The term proof unfolds jcost_energy, simplifies with Jcost_unit0 to obtain a product E_coh · J(x), applies mul_nonneg using the positivity lemma E_coh_storage_pos.le, and finishes with the exact application of Jcost_nonneg hx.
why it matters
The result anchors the EN-004 energy-storage hierarchy by confirming the ground-state minimum. It is invoked directly by phi_coherent_minimizes_jcost_per_energy and appears in the en004_certificate. Within the Recognition framework it corroborates that optimal storage efficiency occurs at the φ-rung x = 1, consistent with the phi-ladder minimum and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.