EulerLagrangeCert
plain-language theorem explainer
Packages the Euler-Lagrange conditions for the log-domain cost: stationarity of J_log at the origin and global minimality of that value. Variational and cost-minimization arguments in Recognition Science cite this certificate. Verification is a two-conjunct constructor that applies the Cost-layer stationarity and global-min lemmas.
Claim. An Euler-Lagrange certificate is a unit witness whose verification predicate holds iff $\frac{d}{dt}J_{\log}(t)\big|_{t=0}=0$ and $J_{\log}(0)\le J_{\log}(t)$ for every real $t$. That predicate is true for every such certificate.
background
The module audits the variational calculus of the log-domain cost used throughout Recognition Science. Write $J_{\log}(t):=J_{\mathrm{cost}}(e^{t})$, equivalently $J_{\log}(t)=\cosh t-1$. This is the pullback of the unique J-cost (T5) along the exponential chart, so critical-point statements at $t=0$ correspond to the multiplicative identity $x=1$.
Two Cost-layer facts feed the certificate. Stationarity: $\mathrm{deriv},J_{\log},0=0$ (the derivative is $\sinh$, and $\sinh 0=0$). Global minimum: $J_{\log}0\le J_{\log}t$ for all real $t$, obtained from nonnegativity of $J_{\log}$ together with $J_{\log}0=0$. The module frames these as the EL conditions needed for action-minimization language and for the bridge to uniqueness of the origin as minimizer once strict convexity is available.
proof idea
The structure itself is a bare unit type (only Repr). The content lives in the simp predicate verified, defined as the conjunction of the two EL statements, and in the theorem that every certificate satisfies it.
That theorem is a one-step constructor: the left conjunct is exactly EL_stationary_at_zero; the right conjunct is exactly EL_global_min. No further rewriting is required at this layer.
why it matters
This is a verification-layer packaging of the variational foundation of the RS cost, not a new analytic result. The module doc places it in the certificate chain: stationarity plus global minimum, and (with strict convexity, proved elsewhere) uniqueness of the origin as minimizer. That uniqueness link is the bridge toward T5 J-uniqueness, where $J(x)=(x+x^{-1})/2-1$ is forced as the unique admissible cost.
Physically it licenses the cost-minimization reading of recognition dynamics and the usual EL language for action principles. No downstream consumers are wired in the current graph; the declaration stands as an audit checkpoint rather than a lemma in a longer proof spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.