PRCJCostDistanceRatDisplay_as_increment
plain-language theorem explainer
The rational J-cost distance display between endpoints x and y equals the one-increment display of their difference x−y. Anyone proving translation invariance of the PRC verifier distance, or reducing three-endpoint triangle estimates to additive increments, cites this identity. The proof is a two-step term proof: unfold both displays and normalize by ring.
Claim. For all rationals $x,y\in\mathbb{Q}$, the verifier display of the J-cost square-gap distance satisfies $d_{\mathrm{disp}}(x,y)=d_{\mathrm{inc}}(x-y)$, where $d_{\mathrm{disp}}(x,y)=\frac{g+g^{-1}}{2}-1$ with $g=1+(x-y)^2$, and $d_{\mathrm{inc}}(t):=d_{\mathrm{disp}}(0,t)$. Equivalently, the displayed distance is translation-invariant and depends only on the increment between the endpoints.
background
In the Primitive Recognition Calculus, the J-cost is the unique cost forced by the Recognition Composition Law: $J(z)=(z+z^{-1})/2-1$. The verifier display of the rational J-cost square-gap distance is not the internal PRC definition; it is the explicit rational formula obtained after transporting the distance to $\mathbb{Q}$. Concretely, one sets $g=1+(x-y)^2$ and evaluates $J(g)$.
The one-increment display is the specialization of that formula to a basepoint at zero: it records distance from $0$ to an increment $t$. The local module builds the three-endpoint verifier triangle target by first reducing geometry to additive increments on $\mathbb{Q}$. Translation invariance of the display is the algebraic hinge of that reduction.
Upstream, the two-argument display is defined in the triangle module as the rational formula shown by the display theorem for the PRC J-cost distance. The increment display is the sibling abbreviation used throughout the verifier-triangle development.
proof idea
Term-mode proof in two tactics. First simp unfolds the increment display (by definition equal to the two-argument display at $(0,t)$) and the two-argument display itself, exposing the formula in $g=1+(x-y)^2$ on the left and $g'=1+t^2$ with $t=x-y$ on the right. Then ring_nf normalizes the rational expressions and closes the equality. No external lemmas are required beyond the two definitions.
why it matters
This identity is the translation-invariance field of the Build Order step 9b conditional certificate: that certificate packages it with the increment-triangle target and the implication from increment triangle to full three-endpoint verifier triangle. Downstream, the increment form is what lets the verifier-triangle target be deduced from a one-dimensional additive estimate, and it is rewritten into square-gap comparisons in the real boundedness modulus and real order-congruence modules (small J-cost distance forces $(a-b)^2<1$ or a modulus-controlled square bound). Product-continuity targets also rewrite through this identity.
In the broader Recognition framework the display is the rational shadow of the T5 J-cost $J(z)=\cosh(\log z)-1$. Establishing that the verifier metric sees only increments is the first algebraic step toward a null-distance setoid and a genuine distance on recognition ratios, before any continuum or physical constants enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.