PRCJCostDistanceIncrementDisplay_formula
plain-language theorem explainer
Closed rational form for the one-step J-cost distance display: the verifier distance from 0 to t equals t^4 / (2(1+t^2)). Anyone proving small-increment or modulus estimates for the PRC J-cost null-distance setoid cites this identity. The proof unfolds the two display defs, clears the positive denominator 1+t^2, and finishes by ring.
Claim. For every rational $t$, the one-increment J-cost distance display equals $\frac{(t\cdot t)\cdot(t\cdot t)}{2(1+t\cdot t)}$. Equivalently, if $D(0,t)$ is the rational verifier formula $(g+g^{-1})/2-1$ with $g=1+t^2$, then $D(0,t)=t^4/(2(1+t^2))$.
background
Primitive Recognition Calculus works with a rational verifier display of the J-cost square-gap distance, not the abstract PRC metric itself. The display is
$$D(x,y)=\frac{g+g^{-1}}{2}-1,\qquad g=1+(x-y)^2,$$
which is the standard J-cost $J(g)=(g+g^{-1})/2-1$ evaluated at that gap. Upstream, PRCJCostDistanceRatDisplay packages exactly this formula; the one-increment display is the specialization $D(0,t)$.
The local module builds the increment-triangle certificate for that display: translation invariance, triangle inequalities, and modulus estimates that later feed real boundedness and product continuity. The identity here is the algebraic engine those estimates rewrite against.
proof idea
Unfold the increment display to $D(0,t)$ and then to the rational J-cost formula with $g=1+t^2$. Prove $1+t^2>0$ by nlinarith from nonnegativity of $t^2$, hence the denominator is nonzero. field_simp clears the inverse; ring reduces both sides to the same polynomial, yielding $t^4/(2(1+t^2))$.
why it matters
This identity is the rewrite target for every quantitative increment lemma in the module: increment_display_lt_of_sq_lt and sq_lt_of_display_lt_delta (and their RealProductContinuity twins) open by rewriting with it. It is also a field of the package certificate prc_jcost_distance_increment_triangle_certificate, whose doc states that "the explicit rational increment estimate closes the whole J-cost null-distance setoid chain."
In the broader RS foundation, J-uniqueness (forcing step T5) fixes $J(x)=(x+x^{-1})/2-1$. The display is that cost on the square gap; simplifying the one-step case to a rational monomial over a quadratic is what makes modulus and continuity arguments purely algebraic on $\mathbb{Q}$ before lifting to $\mathbb{R}$. Without the closed form, the null-distance setoid and real product continuity packages cannot discharge their small-increment hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.