EL_prop
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish that the derivative condition holds.
- Does not derive the explicit expression for the log-domain cost.
- Does not extend to non-log domains or other cost functions.
- Does not reference the forcing chain steps or spatial dimension claims.
formal statement (Lean)
12def EL_prop : Prop :=
proof body
Definition body.
13 (deriv Cost.Jlog 0 = 0) ∧ (∀ t : ℝ, Cost.Jlog 0 ≤ Cost.Jlog t)
14