jcost_successor_increment_tendsto

Recognition cost on a positive ratio is the standard RS functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). It is the unique solution of the Recognition Composition Law once reciprocal symmetry, normalization, and a unit calibration are imposed; the calibration condition is the continuous second-derivative constraint $G''(0)=1$ at the identity of the multiplicative group.

The present statement is the discrete counterpart of that calibration. One steps along the integer ladder by the successor ratio $(n+1)/n$ and multiplies the cost by $n^{2}$ so that the leading coefficient survives the continuum limit. The module develops native cost uniqueness for the Primitive Recognition Calculus: forcing $J$ from order/monotonicity hypotheses rather than analytic continuity.

An exact closed form $n^{2} J((n+1)/n)=n/(2(n+1))$ (valid for $n\ge 1$) is already available from the sibling identity used in the proof; the limit is then elementary real analysis.

First record the standard null sequences $1/(n+1)\to 0$ and $1/(2(n+1))\to 0$ (the latter by scaling the former by the constant $1/2$). Their difference from the constant $1/2$ therefore tends to $1/2$.

It remains only to identify the target sequence with that elementary expression eventually. Restrict to $n\ge 1$, invoke the closed-form identity jcost_successor_increment (which rewrites $n^{2} J((n+1)/n)$ as $n/(2(n+1))$), and finish by field simplification and ring to match $1/2-1/(2(n+1))$. Filter congruence then transfers the limit.

This is the canonical $c=1$ instance of the δ-act ladder calibration: the discrete per-step cost sees the invariant $c^{2}/2$ (here $1/2$) and nothing more, matching the continuous calibration $G''(0)=c^{2}$ without fixing absolute scale. In the forcing chain it supplies the concrete numerical content of unit calibration that T5's uniqueness of $J$ relies on when the analytic continuity hypothesis is dropped.

Downstream it is consumed by law_of_logic_forces_jcost_monotone, the headline capstone of the module: any reciprocal-symmetric, normalized, composition-law cost whose log-transform is monotone and which satisfies unit calibration equals $J$ on $\mathbb{R}_{>0}$. The present limit is the discrete witness that the calibration coefficient really is $1/2$, so the monotone forcing theorem can quote a completed real-analysis fact rather than an analytic second derivative.