jcost_logCurvature_one
plain-language theorem explainer
The recognition cost J in log coordinates has unit curvature at the identity: the second derivative of t ↦ J(e^t) at t=0 equals 1. Cite this when fixing the δ-cost gauge that feeds the RS forcing chain. The proof identifies J(e^t) with cosh(t)−1, applies the general log-curvature formula for the cosh family, and evaluates c² at c=1.
Claim. Let $J(x)=\frac{x+x^{-1}}{2}-1$. Then $\frac{d^2}{dt^2}\big|_{t=0} J(e^t)=1$. Equivalently, $J$ satisfies the calibration normalization that the log-coordinate second derivative at the unit equals one.
background
Recognition Science forces a unique cost on positive ratios. The native cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. In log coordinates one studies $G(t)=J(e^t)$. The Calibration axiom (CostAxioms) demands $G''(0)=1$, which kills the residual gauge in the $\delta$-forced family and singles out one member rather than a scale orbit.
Upstream, jcost_log_eq_clog_one already shows $J(e^t)=\cosh(1\cdot t)-1$, so $J$ is the $c=1$ member of that family. Separately, logCurvature computes the second derivative of $t\mapsto\cosh(c,t)-1$ at zero and obtains $c^2$. The present result simply specializes that residual gauge parameter to the calibrated value.
The local module welds the primitive recognition calculus to the RS forcing chain: the cost entry must be this calibrated $J$, and later rungs ($\varphi$, eight-tick, $D=3$) must land in the countable minimal field.
proof idea
Pointwise rewrite the composite via the sibling identity $J(e^t)=\cosh(1\cdot t)-1$, then extensionality to equate the two functions. Substitute into the goal and apply the general log-curvature theorem at $c=1$, which yields $1^2$. Finish by norm_num. No differentiation is redone here; the work is the identification plus the $c=1$ specialization.
why it matters
This is the calibration half of the Item-3 weld. Downstream, delta_cost_feeds_rs_chain packages exactly this identity with $\varphi\in$ the countable RS field, proving the forcing chain is fed by the calibrated $\delta$ cost and already runs on a countable carrier at the $J$ and $\varphi$ rungs. The sharpened sibling rs_chain_all_rungs_in_field extends the same package through T7 (eight-tick $8=2^3$) and T8 ($D=3$), so every named chain output lives in the countable field.
In the primer landmarks this discharges the gauge-fix step that turns T5's $J$-uniqueness into the concrete unit-curvature $J$ used by the rest of the chain. Without $G''(0)=1$, the cost would remain a one-parameter family; with it, the RS chain has a unique cost entry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.