PRCJCostDistanceIncrementDisplay
plain-language theorem explainer
One-increment specialization of the rational J-cost square-gap display: evaluate the two-point formula from the origin to a rational endpoint t. Triangle, modulus, and verifier certificates cite it as the translation-invariant core of the displayed distance. The body is a one-line specialization of the two-argument rational display at first argument zero.
Claim. For $t\in\mathbb{Q}$, the one-increment J-cost display is the rational obtained by evaluating the two-point square-gap display between $0$ and $t$. Explicitly, if $g=1+t^2$ and $J(u)=(u+u^{-1})/2-1$, the value is $J(g)$, equivalently $t^4/(2(1+t^2))$.
background
In the primitive recognition calculus, the verifier display of J-cost distance is not the internal PRC metric itself; it is the rational formula exported by the to-rational bridge. For endpoints $x,y\in\mathbb{Q}$ one sets $g=1+(x-y)^2$ and returns $J(g)=(g+g^{-1})/2-1$. That expression is the classical RS cost $J$, forced unique by the Recognition Composition Law and the T5 uniqueness step in the forcing chain.
The two-argument display depends on the pair only through the difference $x-y$. Fixing the first endpoint at zero therefore loses no information: the full display is recovered by feeding the increment alone. This module sits in the Foundation layer that builds exact rational certificates for triangle-type inequalities on that display, feeding later null-distance and setoid targets.
proof idea
Definitional one-liner. Unfold to the two-argument rational display with first argument $0$ and second argument $t$. No tactics, no lemmas: the meaning is entirely inherited from the upstream square-gap formula $g=1+(0-t)^2=1+t^2$, then $J(g)$. Downstream algebra rewrites this to the closed form $t^4/(2(1+t^2))$ by clearing the inverse of $g$.
why it matters
This is the translation-invariant core used throughout the increment-triangle and verifier-triangle stack. The identity that the two-point display equals the one-increment display of $x-y$ is proved by simp and ring. The closed-form formula theorem, the small-display-implies-small-square comparison, and its converse all rewrite through this name.
The increment-triangle target (an additive two-leg modulus for rational increments) is stated directly in terms of this display; it is the mathematical core behind the three-endpoint verifier triangle. The Build Order step 9c closure certificate packages the formula identity together with that target. In the broader RS picture this keeps the J-cost geometry on $\mathbb{Q}$ under exact rational control before any real completion or physical units are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.