EL_global_min
plain-language theorem explainer
EL_global_min asserts that the log-domain cost Jlog attains its global minimum at argument zero. Researchers establishing the EL properties in the URC adapters cite it to confirm nonnegativity after the exponential change of variables. The proof is a one-line term wrapper that applies Jlog_nonneg and rewrites the left side via Jlog_zero.
Claim. $Jlog(0) ≤ Jlog(t)$ for all real $t$, where $Jlog(t) := Jcost(e^t)$ and $Jcost$ satisfies $Jcost(x) ≥ 0$ for $x > 0$.
background
The Cost module works in the log-domain by defining Jlog t as the composition Jcost (exp t). Jcost itself is the base cost obeying the Recognition Composition Law and the AM-GM lower bound of zero for positive arguments. Upstream lemmas establish Jlog_nonneg by transporting Jcost_nonneg across the positive exponential, and Jlog_zero by direct simplification showing the value at zero is exactly zero. The module imports Mathlib and supplies the cost axioms used in the forcing-chain derivations.
proof idea
The term proof applies the lemma Jlog_nonneg to the argument t, then uses simpa with the Jlog_zero lemma to replace the left-hand side Jlog 0 by zero, yielding the desired inequality in one step.
why it matters
This supplies the global-minimum half of the pair used by EL_holds in URCAdapters.ELProp to build EL_prop as the conjunction of stationarity at zero and this result. It thereby supports the J-uniqueness step (T5) in the UnifiedForcingChain by confirming the cost minimum after the exponential map, consistent with the eight-tick octave and D=3 landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.