jCostLog
plain-language theorem explainer
J-cost pulled back to additive log coordinates: evaluate the recognition cost at e^t for real t. Anyone building the nonlinear Regge–J edge action or the T5 uniqueness bridge cites this change of variables. The body is a one-line composition of the standard J-cost with the real exponential.
Claim. For $t \in \mathbb{R}$, set $J_{\log}(t) := J(e^{t})$, where $J(x) = \frac{x + x^{-1}}{2} - 1$ is the recognition cost on positive reals.
background
The recognition cost on ratios is $J(x) = \frac{x + x^{-1}}{2} - 1$ for $x > 0$. It is the unique reciprocal cost forced by the Recognition Composition Law (T5 in the forcing chain), equivalently $J(x) = \cosh(\log x) - 1$. Several modules re-export the same formula under the name J-cost.
This module targets a local nonlinear Regge/J-cost correspondence: near a flat configuration the full nonlinear 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 exact equality of the full Regge action with a summed J-cost action.
Working with edge potentials $\xi$ on a triangulation, differences $\xi_i - \xi_j$ are additive. Pulling $J$ back through the exponential converts multiplicative ratio cost into a function of those additive gaps, which is the natural input for a weighted edge action.
proof idea
Pure definition: apply the standard cost $J$ to $\mathrm{exp}(t)$. No lemmas, no tactics. Downstream identities (equality with $\cosh t - 1$, evenness under $t \mapsto -t$) are proved separately by rewriting through the functional-equation package.
why it matters
This is the coordinate change that lets the nonlinear J-cost edge action be written as a sum over vertex-potential differences. It is the building block of the weighted J-cost action on a 3D triangulation (canonical dual weights times $J_{\log}(\xi_i - \xi_j)$), and of the evenness lemmas for that action under $\xi \mapsto -\xi$.
In the forcing chain it feeds the T5-to-nonlinear-Regge bridge certificate: uniqueness of $J$ is packaged as the starting hypothesis for the local Regge/J correspondence. The companion identity $J_{\log}(t) = \cosh t - 1$ makes the quadratic jet of the edge action match the Dirichlet energy that appears in the weak-field quadratic bridge already closed by the first Recognition Gravity paper.
Framework landmarks: T5 J-uniqueness and the RCL fix the shape of $J$; the present def only changes coordinates so that shape can sit on Regge edge data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.