IndisputableMonolith.Verification.JlogAMGMCert
Verification module packaging a machine-checkable certificate that the Recognition J-cost, written in logarithmic coordinates, is exactly the normalized AM–GM gap. Analysts of the cost layer and the forcing chain cite it when they need a Lean-facing witness that J(e^t)=cosh(t)-1 is nonnegative with unique zero at the identity. The argument is a short algebraic identity plus Mathlib’s hyperbolic/AM–GM facts, imported through the Cost module.
claimCertificate that the logarithmic form of the Recognition cost satisfies $J(e^{t})=\cosh(t)-1\ge 0$ for all real $t$, with equality if and only if $t=0$ (equivalently $J(x)\ge 0$ for $x>0$ with equality only at $x=1$), i.e. that $J$ is the normalized AM–GM defect on the pair $(x,x^{-1})$.
background
Recognition Science takes the cost functional $J$ as the unique continuous solution (up to scaling) of the Recognition Composition Law, forced in the T5 step of the unified forcing chain to be $J(x)=(x+x^{-1})/2-1$. In logarithmic coordinates $x=e^{t}$ this is identical to $\cosh(t)-1$.
Nonnegativity of $J$ with a unique zero at the identity is precisely the AM–GM inequality on the pair $(x,x^{-1})$, rewritten as a defect. The Cost module supplies the native definitions of $J$ and its log form; this verification module sits one layer above and packages those facts as an explicit certificate object usable by downstream checkers.
The local setting is pure real analysis: no discrete eight-tick or dimensional hypotheses are required here. Only positivity of the argument of $J$ and the standard hyperbolic identities are used.
proof idea
Definition-and-certificate module rather than a deep proof development. It introduces a certificate structure (or theorem bundle) whose fields record: (i) the identity $J(e^{t})=\cosh(t)-1$, (ii) nonnegativity via Mathlib’s $\cosh$ or AM–GM lemmas, and (iii) the equality case $t=0\Leftrightarrow x=1$. The body is a thin wrapper over lemmas already proved in IndisputableMonolith.Cost, re-exported in a shape convenient for verification consumers. No new analytic work is performed inside the module.
why it matters in Recognition Science
Gives the verification layer a named, importable witness that the T5 J-cost is a genuine nonnegative defect. Downstream checkers and any audit of the forcing chain can point at this certificate instead of re-deriving AM–GM in log coordinates. It does not itself appear in the T0–T8 forcing proofs, but it closes a common trust gap: that the analytic $J$ used in mass ladders, the alpha band, and the composition law is the same object whose nonnegativity is classical. With no recorded used_by edges yet, its role is infrastructural: a stable interface between Cost and higher Verification modules.
scope and limits
- Does not re-prove uniqueness of J under the Recognition Composition Law (that is T5).
- Does not address discrete eight-tick, D=3, or phi-ladder mass formulae.
- Does not supply numerical bounds on alpha or dimensionful constants.
- Does not claim anything for x≤0; the domain is strictly positive reals.
- Does not introduce new axioms; it only repackages Cost and Mathlib facts.