jcost_successor_increment
plain-language theorem explainer
The recognition cost of the successor ratio (n+1)/n equals exactly 1/(2n(n+1)) for every positive real n. Anyone working the δ-act ladder or the discrete calibration of J cites this closed form. The proof is a three-step algebraic identity: unfold the J-cost definition, clear denominators, and ring-normalize.
Claim. For every real $n > 0$, the recognition cost of the successor ratio satisfies $$J\!\left(\frac{n+1}{n}\right) = \frac{1}{2n(n+1)},$$ where $J(x) = \frac{x + x^{-1}}{2} - 1$.
background
In Recognition Science the native cost of a positive ratio is the J-cost $J(x) = (x + x^{-1})/2 - 1$, equivalently $\cosh(\log x) - 1$. It is the unique continuous solution (up to a positive scale) of the Recognition Composition Law, forced at T5 of the Unified Forcing Chain.
The present module develops the Primitive Recognition Calculus (PRC) native-cost uniqueness story. The most elementary discrete act along the integer ladder is the step from orbit $n$ to orbit $n+1$, carried by the ratio $(n+1)/n$. The doc-comment names this the literal "cost of one δ-act" (Move 1 of the δ publication program).
Upstream, Cost.Jcost is the shared definition used across cosmology and foundation modules. No deep uniqueness theorem is needed here: the identity is pure algebra on that definition.
proof idea
Three tactics. First record $n \neq 0$ and $n+1 \neq 0$ from positivity. Unfold Cost.Jcost to expose $(x + x^{-1})/2 - 1$ at $x = (n+1)/n$. Then field_simp clears the denominators $n$ and $n+1$, and ring finishes the polynomial identity equating the result to $1/(2n(n+1))$. No external lemmas beyond positivity and field arithmetic.
why it matters
This is the exact closed form that feeds jcost_successor_increment_tendsto, which recovers the calibration coefficient $1/2$ as the leading per-step coefficient $n^2 \cdot J((n+1)/n) \to 1/2$. That limit is the canonical $c=1$ instance of the family pattern $n^2 \cdot \mathrm{costLambda},c,((n+1)/n) \to c^2/2$.
Two structural facts fall out immediately. Partial-fraction decomposition gives $1/(2n(n+1)) = \tfrac12(1/n - 1/(n+1))$, so ladder costs telescope and the total cost of building the integer ladder from the unit orbit is exactly $1/2$. The same identity shows that calibration is a discrete leading coefficient of an exact rational ladder, not an analytic posit: the residual freedom is one positive scale (faithfulness of the costLambda family).
In the broader framework this sits under T5 J-uniqueness and the RCL, supplying the elementary δ-act brick used by native-cost uniqueness arguments in PRC.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.