JlogNonnegCert
plain-language theorem explainer
Audit certificate packaging the claim that the log-domain cost satisfies J_log(t) ≥ 0 for every real t. Verification and cost-function auditors cite it to lock the non-negativity half of the unique-minimizer story for the Recognition cost. The discharge theorem is a one-line wrapper around the existing Jlog_nonneg lemma.
Claim. There is a unit certificate type whose verification predicate is the proposition $\forall t \in \mathbb{R},\ J_{\log}(t) \geq 0$. Every inhabitant of the certificate type satisfies that predicate.
background
The log-domain cost is $J_{\log}(t) := J_{\mathrm{cost}}(e^t)$, equivalently $\cosh(t)-1$ in the closed form used elsewhere in Cost.Jlog. It is the pullback of the multiplicative J-cost along the exponential chart, so $t=0$ corresponds to the multiplicative identity $x=1$.
This module sits in the Verification layer and packages non-negativity as an audit certificate rather than a bare lemma. The module doc states the target identity $\forall t,\ J_{\log}(t)\geq 0$ and notes that, together with the companion zero certificate ($J_{\log}(t)=0$ iff $t=0$), one obtains that $t=0$ is the unique global minimizer with value 0.
Upstream, Jlog_nonneg already proves $0\leq J_{\log}(t)$ by reducing to non-negativity of $J_{\mathrm{cost}}$ on the positive reals via $e^t>0$. The algebraic picture in the module doc is $J_{\log}(t)=(e^t-1)^2/(2e^t)$: numerator nonnegative, denominator positive.
proof idea
The structure itself is an empty marker type (Repr only). The real content is the simp predicate verified, defined as $\forall t:\mathbb{R},\ 0\leq J_{\log}(t)$, and the theorem verified_any, which discharges it for every certificate inhabitant.
That theorem is a one-line wrapper: introduce $t$, then apply the upstream lemma Jlog_nonneg. No new analysis is done at the certificate layer.
why it matters
In the Recognition cost story, J is forced (T5) as $J(x)=(x+x^{-1})/2-1$, and the log chart is the natural additive coordinate. Non-negativity of $J_{\log}$ is the half of the unique-minimizer package that says the cost never goes below zero; the zero certificate supplies uniqueness of the root at $t=0$ (equivalently $x=1$).
The module doc is explicit: combined with JlogZeroCert, this proves $J_{\log}\geq 0$ everywhere and that $J_{\log}(0)=0$ is the global minimum. That underwrites every later argument that treats the Recognition cost as a genuine defect or distance-like functional (RCL identities, rung costs, Hamiltonian emergence).
No downstream consumers are wired in the graph yet (used_by is empty), so this is presently a leaf certificate in the audit chain rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.