EL_prop
plain-language theorem explainer
The declaration defines the EL property as the conjunction of stationarity (derivative of the log-domain cost vanishes at zero) and global minimality (zero is the least value). Researchers establishing lawful normalizers cite it to confirm the exponential-log transform preserves the origin minimum. The definition is a direct conjunction drawn from the central cost definitions without additional lemmas.
Claim. The property that the derivative of the log-domain cost function at zero equals zero and that this value is a global minimum: $J'_{log}(0)=0$ and $J_{log}(0)≤J_{log}(t)$ for all real $t$, where $J_{log}(t)=((e^t+e^{-t})/2)-1$.
background
The URCAdapters module extracts the EL stationarity and minimality on the log axis. It re-exposes the minimal Prop using the central Cost module. Jlog is the log-domain cost obtained by composing the recognition cost J with the exponential map. Upstream definitions give Jlog(t) explicitly as ((exp t + exp(-t))/2)-1 and as Jcost composed with exp, with Cost itself an abbreviation for Quantity CostUnit.
proof idea
This is a definition that directly states the conjunction of the derivative condition at zero and the inequality for all t. It packages the two properties extracted from the Cost module as a single Prop without invoking further lemmas or tactics.
why it matters
This definition supplies the EL property required by the LawfulNormalizer structure and is asserted by the lemma EL_holds. It supports the stationarity condition at the self-similar fixed point, consistent with J-uniqueness in the forcing chain. It leaves open full integration with the phi-ladder mass formulas and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.