PRCJCostDistanceTriangleModulusTarget
plain-language theorem explainer
The J-cost rational distance admits a local triangle modulus: every positive tolerance ε has a positive δ so that two legs shorter than δ force the third below ε. Builders of the null-distance setoid on PRC reals cite this Prop as the exact analytic blocker for the quotient. It is a pure definition packaging that quantified statement; proofs live downstream via the increment-triangle verifier.
Claim. For every positive PRC-rational $\varepsilon$ there exists a positive PRC-rational $\delta$ such that for all PRC-rationals $a,b,c$, if the J-cost distance $d_J(a,b)<\delta$ and $d_J(b,c)<\delta$, then $d_J(a,c)<\varepsilon$.
background
In the Primitive Recognition Calculus, rationals are ratio-orbit quotient classes (nonzero-denominator pairs identified by cross-multiplication). From those, a J-cost-derived distance $d_J$ is formed; J itself is the unique cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law and T5 uniqueness.
The ambient module builds a null-distance setoid on PRC reals: two Cauchy data are identified when their $d_J$-separation can be driven below every positive rational tolerance. Transitivity of that null relation is not free; it needs a uniform local triangle control on the rational distance.
Upstream order and positivity on PRC rationals supply the strict inequalities and the positive cone used in the quantifiers. The Kronecker and modular-arithmetic imports are ambient scaffolding, not ingredients of this Prop.
proof idea
No proof: the declaration is a def of a Prop. Its body is exactly the $\varepsilon$–$\delta$ triangle-modulus statement over PRC rationals and $d_J$. Downstream, the target is discharged by transporting an explicit rational verifier inequality (increment-triangle formula) through display equalities, then feeding the resulting hypothesis into null-distance transitivity and setoid constructors.
why it matters
This is the exact analytic blocker for the null-distance quotient on PRC reals. Downstream, the triangle-modulus hypothesis implies null-distance transitivity by completed-orbit index bookkeeping, and that yields the full null-distance setoid target. Conditional and proved certificates in the J-cost triangle and increment-triangle modules name this Prop as the remaining (then closed) obligation: the increment formula $t\mapsto t^4/(2(1+t^2))$ supplies the explicit rational estimate that proves the modulus.
In the broader Recognition chain, a well-behaved null setoid is prerequisite to treating PRC reals as a metric completion carrier on which later forcing steps (eight-tick register, spatial dimension, mass ladder) can sit. Closing the modulus removes the last analytic gap before the setoid certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.