PRCJCostDistanceRatDisplay
plain-language theorem explainer
Explicit rational formula for the PRC J-cost square-gap distance between two rationals: J applied to 1+(x-y)^2. Downstream triangle certificates, the null-distance quotient, and the toRat display theorem all cite this display rather than the abstract PRC object. The body is a two-line closed form, not a proof.
Claim. For rationals $x,y\in\mathbb{Q}$, the verifier display of the J-cost square-gap distance is $D(x,y)=\frac{g+g^{-1}}{2}-1$, where $g=1+(x-y)^2$. Equivalently $D(x,y)=J\bigl(1+(x-y)^2\bigr)$ with the standard Recognition cost $J(t)=(t+t^{-1})/2-1$.
background
In Recognition Science the unique cost forced by the Recognition Composition Law is $J(t)=(t+t^{-1})/2-1$ (T5). The Primitive Recognition Calculus (PRC) lifts this cost to a quotient-level distance on positive ratios and on a rational carrier PRCRat.
The true PRC distance is an abstract object on that carrier. For verifier work (triangle inequalities, null-distance setoid, certificates) one needs a purely rational closed form. This definition supplies that form: first form the square gap $g=1+(x-y)^2$, then evaluate $J(g)$. The companion theorem PRCJCostDistance_toRat states that projecting the abstract PRC distance recovers exactly this display.
Upstream cost defs (observer forcing, multiplicative recognizer, recognizer bridge) all route through the same $J$; the display is the rational specialization used when the analytic estimate is stated only on conservative rational displays.
proof idea
Definition, not a theorem. Bind $g:=1+(x-y)^2$ in $\mathbb{Q}$, then return $(g+g^{-1})/2-1$. No lemmas are applied; the body is the closed-form expression that later unfold/rw steps match against PRCJCost.onPRCRat_toRat and PRCSquareGap_toRat.
why it matters
This display is the concrete formula every step-9a certificate talks about. PRCJCostDistance_toRat proves the abstract PRC distance projects to it. PRCJCostDistanceVerifierTriangleTarget states the remaining rational inequality purely in terms of this display (and a positive PRC rational delta). The conditional certificate structure packages the display equality plus that target as the only open mathematical obligation for the null-distance quotient.
Downstream, the increment form PRCJCostDistanceIncrementDisplay t := D(0,t) and the translation-invariance identity $D(x,y)=D(0,x-y)$ reduce triangle work to a one-variable rational function, later rewritten as $t^4/(2(1+t^2))$. That reduction sits on the J-uniqueness landmark (T5) and feeds the PRC null-distance setoid used in the foundation forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.