PRCJCostDistanceVerifierTriangleTarget
plain-language theorem explainer
Verifier-rational triangle target for the J-cost square-gap distance: every positive PRC-rational ε admits a positive PRC-rational δ so that if the rational displays of (x,y) and (y,z) both lie below δ, the display of (x,z) lies below ε. Cited by anyone closing the PRC triangle-modulus or null-distance setoid. Bare Prop definition of the residual analytic obligation; no proof body.
Claim. For every positive PRC rational $\varepsilon$ there exists a positive PRC rational $\delta$ such that, for all rationals $x,y,z$, if the J-cost square-gap display of $(x,y)$ is less than the rational image of $\delta$ and the display of $(y,z)$ is likewise less than that of $\delta$, then the display of $(x,z)$ is less than the rational image of $\varepsilon$.
background
In Primitive Recognition Calculus, pairwise cost is measured by the J-functional forced at T5: $J(t)=(t+t^{-1})/2-1$. The verifier display on ordinary rationals is the square-gap specialization $\mathrm{display}(x,y)=J\bigl(1+(x-y)^2\bigr)$, written explicitly as $(g+g^{-1})/2-1$ with $g=1+(x-y)^2$. This is not the internal PRC distance; it is the conservative rational formula exposed by the display theorem.
PRC rationals are ratio-orbit quotient classes (cross-multiplication setoid on nonzero-denominator pairs), with a transport map into $\mathbb{Q}$. Positive elements are those in the positive cone of that field.
The module sits in foundation build-order step 9: conditional certificates reduce the triangle-modulus target and the null-distance setoid target to an explicit uniform estimate on these rational displays. The estimate is the constructive stand-in for transitivity of zero cost.
proof idea
No proof work: the declaration is a Prop-valued definition whose body is exactly the quantified inequality (universal over positive PRC-rational $\varepsilon$, existential over positive $\delta$, then universal over rational triples under two strict display bounds). Downstream lemmas take inhabitation of this Prop as a hypothesis and push it across display equalities to obtain the PRC-level triangle-modulus and null-distance setoid targets.
why it matters
Names the residual obligation of the step-9a conditional certificate: "the only remaining mathematical problem is now the explicit rational inequality" in this target. Inhabitation feeds PRCJCostDistanceTriangleModulusTarget_of_verifier by display transport, and thence PRCNullDistanceSetoidTarget_of_verifier_triangle, which closes transitivity of zero J-cost for the recognition quotient. Parallel step-9b/9c paths reduce the same Prop to a translation-invariant increment formula on a single rational and discharge it in PRCJCostDistanceVerifierTriangleTarget_proved. Framework landmark: the underlying cost is the T5-unique $J$ from the Recognition Composition Law; controlling its square-gap display on $\mathbb{Q}$ is what makes the null-distance setoid well-defined before completeness and later forcing (eight-tick, $D=3$) are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.