JlogAMGMCert
plain-language theorem explainer
Empty certificate carrier whose verification predicate asserts that the log-coordinate cost Jlog is nonnegative on all reals and vanishes only at zero. Anyone checking elementary nonnegativity of the RS cost (AM-GM route, no calculus) cites this package. The top-level check is a two-line constructor that hands off to the existing Jlog nonnegativity and zero-set lemmas.
Claim. A certificate object whose verification predicate is the conjunction: for every real $t$, $\mathrm{Jlog}(t)\ge 0$, and $\mathrm{Jlog}(t)=0$ if and only if $t=0$. Here $\mathrm{Jlog}(t)=J(e^{t})=\cosh t-1$ is the cost in additive (log) coordinates.
background
In Recognition Science the unique cost satisfying the composition law is $J(x)=(x+x^{-1})/2-1$ on $x>0$ (T5 J-uniqueness). Passing to log coordinates via $x=e^{t}$ yields $\mathrm{Jlog}(t)=J(e^{t})=((e^{t}+e^{-t})/2)-1$, equivalently $\cosh t-1$.
The module packages an elementary nonnegativity certificate for this function. Module doc: AM-GM gives $x+1/x\ge 2$ for $x>0$, hence $J(x)\ge 0$ with equality iff $x=1$; transporting by $x=e^{t}>0$ yields $\mathrm{Jlog}(t)\ge 0$ with equality iff $t=0$. This route avoids convexity or derivatives.
Upstream, Jlog is defined as $J(\exp t)$ (and equivalently via the cosh form). The lemmas Jlog_nonneg and Jlog_eq_zero_iff already record the two conjuncts; the certificate merely names them as a single verification predicate.
proof idea
The structure itself is an empty carrier (only Repr). The predicate verified is definitional: the pair of universal statements "nonnegative" and "zero iff argument zero".
The companion theorem that every such certificate verifies is a one-line constructor: first conjunct by Jlog_nonneg (which reduces to nonnegativity of $J$ at the positive point $e^{t}$), second conjunct by Jlog_eq_zero_iff. No new arithmetic is done at this layer.
why it matters
Nonnegativity of the cost with a unique zero is the analytic backbone of the forcing chain: it makes $J$ a genuine defect measure and pins the fixed point of self-similarity (T5–T6). Packaging the AM-GM proof as a named certificate gives the verification layer an elementary, calculus-free witness that the log-cost is a proper distance-like functional on $\mathbb{R}$.
Downstream use count is presently zero in the graph; the object sits in the Verification domain as a reusable check that other certificates or reports can import when they need to assert cost positivity without reopening the Cost module. It complements any convexity-based proofs of the same facts by supplying the purely algebraic AM-GM path highlighted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.