EL_holds
plain-language theorem explainer
The lemma establishes that the J-cost function on the logarithmic axis is stationary at zero and globally minimal there. Researchers modeling equilibrium points in the Recognition Science cost framework would cite this to anchor the zero of the log axis. The proof is a direct term that pairs the stationarity theorem with the global minimality theorem from the Cost module.
Claim. $ (d/dt) J_{log}(0) = 0 $ and $ J_{log}(0) $ is the global minimum of $ J_{log} $ on the real line.
background
The module re-exposes stationarity and minimality of the cost function on the log axis from the central Cost module. EL_prop is the conjunction stating that the derivative of Jlog vanishes at zero and that Jlog attains its global minimum at zero. Upstream results supply the stationarity theorem obtained by direct simplification and the global minimality theorem that follows from non-negativity after using the Jlog_zero identity.
proof idea
The proof is a one-line term that constructs the required pair by applying the stationarity theorem EL_stationary_at_zero together with the global minimality theorem EL_global_min, both drawn from the Cost module.
why it matters
This lemma supplies the Prop witness used by the downstream lawful_normalizer_exists_unique to construct a trivial normalizer at lambda equals one. It confirms the equilibrium point on the log axis inside the URC adapter layer and anchors the J-uniqueness property at the fixed point consistent with forcing-chain step T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.