PRCJCostDistanceTriangleModulusTarget_of_verifier
plain-language theorem explainer
The verifier-rational triangle inequality for PRC J-cost distance transports, by display maps, to the native triangle-modulus target on PRC rationals. Cite this when closing the null-distance setoid or the Build Order 9a conditional certificate. The argument is pure transport: rewrite the three inequalities through the to-rational comparison and the distance display theorem, then apply the rational estimate.
Claim. Assume that for every positive PRC rational $\varepsilon$ there exists a positive PRC rational $\delta$ such that, for all ordinary rationals $x,y,z$, if the displayed J-cost distances satisfy $d_{\mathrm{disp}}(x,y)<\delta^{\mathbb{Q}}$ and $d_{\mathrm{disp}}(y,z)<\delta^{\mathbb{Q}}$, then $d_{\mathrm{disp}}(x,z)<\varepsilon^{\mathbb{Q}}$. Then the PRC triangle-modulus target holds: the same modulus statement with the native PRC J-cost distance on PRC rationals in place of the rational displays.
background
Primitive Recognition Calculus (PRC) builds rationals as ratio-orbit quotients (PRCRat), with a verifier display toRat sending each class to an ordinary rational by cross-multiplication of numerator and denominator. The PRC J-cost distance is the native cost gap on those classes; its display theorem states that the displayed distance of two PRC rationals equals the rational-display distance of their toRat images.
The verifier-triangle target is the analytic estimate still needed for the null-distance quotient: it supplies a PRC-rational modulus $\delta$, but the inequality itself is stated only on conservative rational displays. The triangle-modulus target is the same modulus statement lifted to native PRC distances on PRCRat.
Local setting is the Foundation layer that turns J-cost (the unique cost from the Recognition Composition Law / T5) into a distance suitable for a null-setoid quotient on reals built from PRC data.
proof idea
Term-mode transport, not an analytic estimate. Fix positive $\varepsilon$ and unpack the verifier hypothesis to obtain positive $\delta$ and the rational triple inequality. Re-export that same $\delta$. For native PRC rationals $a,b,c$ with $d(a,b)<\delta$ and $d(b,c)<\delta$, rewrite both hypotheses and the goal via the comparison lemma that reduces PRC-rational order to ordinary rational order on displays, then rewrite the three distances via the display theorem equating native distance to PRCJCostDistanceRatDisplay of the toRat images. The verifier estimate on $a.toRat$, $b.toRat$, $c.toRat$ finishes the goal.
why it matters
This is the display-transport half of Build Order step 9a: once the rational inequality is available, the native triangle-modulus target is free. Downstream, PRCJCostDistanceTriangleModulusTarget_proved closes the modulus by feeding in the proved verifier target; PRCNullDistanceSetoidTarget_of_verifier_triangle then obtains the null-distance setoid target (transitivity of zero J-cost distance) by composing with the modulus-to-setoid bridge; and the conditional certificate packages display, verifier target, this transport, and the setoid bridge as a single Build Order artifact.
In the broader RS chain, J-cost is the T5 unique cost $J(x)=(x+x^{-1})/2-1$. A working triangle inequality on that cost is what lets null pairs form a setoid, so later real and continuum constructions can quotient by recognition-indistinguishability rather than by an external metric axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.