PRCJCostDistanceVerifierTriangleTarget_proved
plain-language theorem explainer
The verifier-rational three-endpoint triangle inequality for PRC J-cost distance displays is closed. Anyone assembling the null-distance quotient on rational displays cites this. The argument is a one-line application of the increment-to-verifier implication to the already proved increment triangle target.
Claim. For every positive PRC-rational $\varepsilon$ there exists a positive PRC-rational $\delta$ such that for all ordinary rationals $x,y,z$, if the rational J-cost distance displays of $(x,y)$ and of $(y,z)$ are both strictly less than $\delta$, then the display of $(x,z)$ is strictly less than $\varepsilon$.
background
Primitive Recognition Calculus (PRC) builds logic-native integers and rationals (Grothendieck completion of logic naturals, then field of fractions) and measures separation by a J-cost distance. The classical J-cost is $J(x)=(x+x^{-1})/2-1$; here one works with conservative rational displays of that cost rather than a completed real metric.
The verifier triangle target asks for a uniform positive PRC-rational modulus $\delta(\varepsilon)$ controlling three ordinary-rational endpoints on those displays. It is the exact inequality still needed for the null-distance quotient. An upstream increment-only target is stronger in form: it estimates successive increments and already has a full proof in this module.
A bridge lemma states that any proof of the increment triangle target yields the verifier-rational three-endpoint target. Logic-native setoids on integer and rational carriers sit underneath the PRC rational type used in the quantifiers.
proof idea
Pure term-mode one-line wrapper. Apply the bridge lemma that the increment-only triangle target implies the verifier-rational three-endpoint target, feeding it the already established proof of the increment triangle target. No new $\varepsilon$-$\delta$ arithmetic is performed here; all constructive content lives in the increment proof and the bridge.
why it matters
This is the final closure step for the rational increment modulus on the verifier side. Downstream, the triangle-modulus target is obtained from this theorem by another one-line of_verifier wrapper, and both facts are packed into the increment-triangle certificate whose doc-comment states that the explicit rational increment estimate closes the whole J-cost null-distance setoid chain.
In the Recognition foundation this discharges the last rational-display triangle obligation before null-distance can be shown transitive and promoted to a setoid. That setoid is the discrete skeleton on which later forcing-chain geometry (J-uniqueness, the $\phi$ fixed point, eight-tick structure) can sit without an analytic metric completion. No open scaffold remains on this edge once the certificate is assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.