JlogZeroCert
plain-language theorem explainer
Audit certificate packaging the unique-zero law for the log-domain cost: J_log(t)=0 if and only if t=0. Anyone checking that the origin is the sole critical point of the log-cost (hence x=1 is the sole minimum of J) would cite it. The verification theorem is a one-line wrapper of the existing Jlog_eq_zero_iff lemma.
Claim. There is a unit certificate type whose verification predicate asserts: for every real $t$, $J_{\log}(t)=0$ if and only if $t=0$. Every inhabitant of the certificate type satisfies that predicate.
background
In the Recognition cost layer, the multiplicative cost is $J(x)=\frac12(x+x^{-1})-1$ on $x>0$ (equivalently $\cosh(\log x)-1$). The log-domain cost is the pullback $J_{\log}(t):=J(e^t)$, which expands to $\cosh(t)-1$.
This module is a thin verification wrapper in the certificate chain. Its module doc states the target identity $J_{\log}(t)=0\iff t=0$, and notes that together with nonnegativity of $J_{\log}$ this makes $t=0$ the unique global minimum, corresponding to $x=1$ for $J$.
Upstream, Jlog is defined as $J\circ\exp$ (and also directly as $\frac12(e^t+e^{-t})-1$). The lemma Jlog_eq_zero_iff already proves the biconditional used here.
proof idea
The structure itself is empty data (a unit certificate). The predicate verified is definitionally $\forall t:\mathbb{R},, J_{\log}(t)=0\leftrightarrow t=0$.
The theorem that every certificate is verified is a one-line wrapper: introduce $t$ and apply Jlog_eq_zero_iff t. No new analysis is done at this layer; the work lives in the Cost module (via the squared representation of $J$ and positivity of $\exp$).
why it matters
Unique zero of $J_{\log}$ is the log-coordinate form of unique minimality of $J$ at $x=1$, which is the content of the T5 J-uniqueness landmark ($J(x)=\frac12(x+x^{-1})-1$). The certificate chain uses this to lock the cost geometry before building mass ladders, forcing steps, and continuum limits.
The module doc is explicit: combined with $J_{\log}\ge 0$, this proves $t=0$ is the unique global minimum, translating to $x=1$ for $J_{\mathrm{cost}}$. Downstream use count is currently zero in the graph, so this is a leaf audit artifact rather than a lemma other proofs import by name; its role is certification packaging, not new mathematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.