jCostLog_eq_cosh_sub_one
plain-language theorem explainer
J-cost in log coordinates equals cosh(t) − 1 for every real t. Anyone routing the Recognition cost into hyperbolic or Regge geometry cites this identity. The proof is a one-line reparametrization of the known G-form of Jcost under the exponential change of variables.
Claim. For every real number $t$, the J-cost evaluated at $e^{t}$ equals $\cosh t - 1$.
background
The ambient module targets a local nonlinear correspondence between the full Regge action and a J-cost action: near a flat configuration the Regge action equals its flat value plus the canonical J/Dirichlet quadratic term, with an explicitly bounded cubic Taylor remainder. It does not claim global equality of the two actions.
The J-cost is the unique continuous solution of the Recognition Composition Law fixed by T5: $J(x)=(x+x^{-1})/2-1$. The local definition jCostLog is simply that cost in log coordinates, $t\mapsto J(e^{t})$. Upstream, the functional-equation layer already records the same identity as $G(J)(t)=\cosh t-1$, where $G(F)(t):=F(e^{t})$ is the standard log reparametrization. The Gravity inflaton potential is defined by the same closed form $G(t)=\cosh t-1$.
proof idea
One-line wrapper. Unfold jCostLog (which is $J(e^{t})$) and the log reparametrization $G$, then apply the upstream lemma Jcost_G_eq_cosh_sub_one, which already proves $G(J)(t)=\cosh t-1$ by rewriting $J(e^{t})=(e^{t}+e^{-t})/2-1$ via the definition of cosh. simpa discharges the equality.
why it matters
This is the concrete T5 bridge into the nonlinear Regge surface. Downstream, t5_to_nonlinear_regge_jcost_bridge_holds in the Unified Forcing Chain routes J-uniqueness into the nonlinear Regge/J-cost correspondence precisely by making this log-coordinate form available. The sibling evenness lemma jCostLog_neg also depends on it: once the cosh identity is in hand, $J(e^{-t})=J(e^{t})$ is immediate from $\cosh(-t)=\cosh t$.
In the primer landmarks this is exactly T5's closed form $J(x)=\cosh(\log x)-1$, specialized to the edge-action variables used by the Regge correspondence. It lets the quadratic Dirichlet term and the cubic remainder estimates sit on a hyperbolic rather than algebraic footing without reopening uniqueness of $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.