jCostLog_neg
plain-language theorem explainer
The log-coordinate J-cost is even: flipping the sign of the real argument leaves the value unchanged. Anyone building sign-flip invariance for nonlinear edge actions on a triangulation cites this. The proof is a two-line rewrite through the identity with cosh minus one, then evenness of cosh.
Claim. For every real number $t$, $J_{\log}(-t)=J_{\log}(t)$, where $J_{\log}(t):=\cosh(t)-1$ is the canonical J-cost written in additive (log-ratio) coordinates.
background
The module targets a local nonlinear bridge between the Regge action and a summed J-cost action on a 3D triangulation. It does not claim global exact equality; near a flat configuration the nonlinear Regge action equals its flat value plus the canonical J/Dirichlet quadratic term, with an explicitly bounded cubic Taylor remainder.
The Recognition cost $J$ is the unique solution forced by the Recognition Composition Law (T5): $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$ on positive ratios. In additive coordinates one works with the pullback $J_{\log}(t)=\cosh(t)-1$, which is the natural edge cost when vertex potentials supply signed log-ratios.
Sibling identity jCostLog_eq_cosh_sub_one records that equality. Upstream cost constructions (observer forcing, multiplicative recognizers, rung coarsening) all route through the same non-negative J-cost on ratios; the present lemma is the elementary parity fact needed once those costs are written in log coordinates.
proof idea
Term-style rewrite proof. Apply the sibling identity $J_{\log}(u)=\cosh(u)-1$ on both sides (argument $-t$ and argument $t$). The goal reduces to $\cosh(-t)-1=\cosh(t)-1$, which is immediate from the standard real-analysis fact that cosh is even (Real.cosh_neg). No case splits or positivity hypotheses are required.
why it matters
Feeds the parent theorem weightedJCostAction_neg: the full weighted J-cost edge action built from canonical incidence weights is invariant under global sign flip of the vertex potential. That evenness is the first structural property of the nonlinear J-cost action before the module splits off the quadratic jet and bounds the cubic remainder.
In the Recognition Gravity program this sits one step past the weak-field quadratic bridge closed in the first paper. The forcing chain landmark is T5 (J-uniqueness); the even log form is exactly $\cosh(\log x)-1$ evaluated on reciprocal ratios, so reciprocal edges contribute identically. Without this parity fact the nonlinear correspondence target cannot treat oppositely oriented potentials as the same action value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.