PRCJCostDistanceVerifierTriangleTarget_of_increment
plain-language theorem explainer
The additive two-leg modulus on rational J-cost increments implies the three-endpoint verifier triangle inequality on rational displays. Anyone closing the PRC null-distance setoid cites this reduction. The proof rewrites endpoint distances as pure increments by translation invariance, applies the two-leg estimate, and cancels the intermediate point by ring arithmetic.
Claim. If the rational J-cost distance obeys an additive two-leg modulus on increments (for every positive $\varepsilon$ there is positive $\delta$ such that $d_{\mathrm{inc}}(p)<\delta$ and $d_{\mathrm{inc}}(q)<\delta$ imply $d_{\mathrm{inc}}(p+q)<\varepsilon$), then the three-endpoint verifier target holds: for every positive $\varepsilon$ there is positive $\delta$ such that $d(x,y)<\delta$ and $d(y,z)<\delta$ imply $d(x,z)<\varepsilon$ on the rational displays.
background
In the Primitive Recognition Calculus, the verifier display of J-cost square-gap distance between rationals $x,y$ is $$d(x,y)=\frac{g+g^{-1}}{2}-1,\quad g=1+(x-y)^2,$$ i.e. the standard cost $J(g)$ with $J(u)=(u+u^{-1})/2-1$. The one-increment display is $d_{\mathrm{inc}}(t):=d(0,t)$. Translation invariance records that $d(x,y)=d_{\mathrm{inc}}(x-y)$.
The increment triangle target is the sharper exact blocker: an additive two-leg modulus purely on rational increments. The verifier triangle target is the three-endpoint form still needed for the null-distance quotient; it supplies a PRC-rational modulus $\delta$ but states the estimate only on conservative rational displays.
This module reduces the three-point verifier inequality to that one-dimensional additive estimate.
proof idea
Assume the increment triangle target. Fix positive $\varepsilon$ and obtain positive $\delta$ from that hypothesis. For rationals $x,y,z$ with $d(x,y)<\delta$ and $d(y,z)<\delta$, rewrite both bounds via the translation-invariance identity as $d_{\mathrm{inc}}(x-y)<\delta$ and $d_{\mathrm{inc}}(y-z)<\delta$. The additive two-leg estimate then yields $d_{\mathrm{inc}}((x-y)+(y-z))<\varepsilon$. Congruence plus ring shows $(x-y)+(y-z)=x-z$, so $d(x,z)=d_{\mathrm{inc}}(x-z)$, and rewriting finishes.
why it matters
This is the bridge from the one-dimensional increment modulus to the three-endpoint verifier triangle required for the PRC null-distance setoid. Downstream, the proved increment target is fed through this lemma to close the verifier triangle outright; the same reduction chains into the null-distance setoid target; and the Build Order step 9b conditional certificate packages the reduction as the verifier-from-increment field. In Recognition Science the cost $J$ is the unique T5 solution of the Recognition Composition Law, so controlling its rational-display triangle inequality is part of making null distance a setoid on the calculus side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.