H_Jcost_eq_cosh
plain-language theorem explainer
The log-coordinate transform of the recognition cost equals hyperbolic cosine: H_J(t)=cosh(t) for all real t. Anyone invoking the d'Alembert form of the Recognition Composition Law, or the completeness-free monotone forcing theorems, cites this identification. The proof is a short term rewrite: unfold H, apply G_J(t)=cosh(t)-1, then ring.
Claim. For every real $t$, the log-coordinate transform $H_J(t):=G_J(t)+1$ of the recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$ equals $\cosh t$. Equivalently, $H_J(t)=(\cosh t-1)+1=\cosh t$.
background
The recognition cost on positive ratios is $J(x)=\frac{x+x^{-1}}{2}-1$. In log coordinates one works with the reparametrizations $G_J(t)=J(e^t)$ and $H_J(t)=G_J(t)+1$. The algebraic shift $H=J+1$ converts the Recognition Composition Law into the classical d'Alembert equation $H(xy)+H(x/y)=2,H(x)H(y)$.
An upstream identity already records the explicit form of $G$: $G_J(t)=\cosh t-1$, obtained by writing $J(e^t)=\frac{e^t+e^{-t}}{2}-1$ and matching the definition of $\cosh$. The present result is the one-step lift of that identity to $H$.
The surrounding module develops native-cost uniqueness for the Primitive Recognition Calculus: forcing the discrete cost ladder to the unique continuous $J$ (and its scale family) under completeness-free regularity hypotheses.
proof idea
Term-mode, three steps. Unfold the definition $H_F(t)=G_F(t)+1$. Rewrite the $G$ factor by the upstream lemma $G_J(t)=\cosh t-1$. The remaining algebraic identity $(\cosh t-1)+1=\cosh t$ is discharged by ring. No case splits or analytic estimates.
why it matters
This is the concrete bridge from the closed-form $J$ of T5 (J-uniqueness: $J(x)=\cosh(\log x)-1$) to the d'Alembert generator $H=\cosh$ used throughout the forcing chain. Downstream, H_Jcost_monotoneOn quotes it twice to conclude that $H_J$ is monotone on $[0,\infty)$ because $\cosh$ is strictly monotone there; that monotonicity is exactly the completeness-free regularity hypothesis fed to the monotone forcing theorems.
It also sits under costLambda_successor_increment_tendsto, which shows that the discrete $\delta$-act cost ladder recovers the calibration invariant $c^2$ and nothing more (Move 1 of native-cost uniqueness). Without $H_J=\cosh$, the regularity side of those uniqueness arguments has no closed form to cite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.