PRCJCostDistanceTriangleModulusTarget_proved
plain-language theorem explainer
The J-cost rational distance admits a local triangle modulus: every positive tolerance has a smaller positive tolerance so that two short legs force the composed leg below the original. This closes the analytic blocker for the null-distance quotient on PRC rationals. Null-distance transitivity, three-leg modulus, and real addition closure/congruence all cite it. Proof is a one-line transport from the already-proved verifier-rational triangle inequality.
Claim. For every positive rational tolerance $\varepsilon$ there exists a positive rational $\delta$ such that, for all rationals $a,b,c$, if the J-cost distance from $a$ to $b$ is less than $\delta$ and the J-cost distance from $b$ to $c$ is less than $\delta$, then the J-cost distance from $a$ to $c$ is less than $\varepsilon$.
background
Primitive Recognition Calculus builds a real carrier from Cauchy ledgers of rationals, quotiented by a null-distance relation induced by a J-cost distance. The J-cost is the Recognition Science cost $J(x)=(x+x^{-1})/2-1$; on positive rationals it yields a symmetric nonnegative distance display used to decide when two ledgers are identified.
The triangle-modulus target is the exact analytic blocker for that quotient: for each positive rational tolerance there must exist a strictly smaller positive tolerance so that two legs below the smaller force the composed leg below the original. Without it, null distance need not be transitive and the quotient fails to be a setoid.
Upstream, the verifier-rational triangle inequality is already closed by an explicit rational increment estimate. A display-transport lemma then lifts any such verifier triangle witness to the modulus target itself.
proof idea
One-line term wrapper. Apply the display-transport lemma that turns a verifier-rational triangle witness into a triangle-modulus witness, feeding it the already-proved verifier triangle target (itself obtained from the explicit rational increment estimate). No new arithmetic is performed at this step.
why it matters
This declaration discharges the triangle-modulus blocker that the null-distance setoid depends on. Downstream it is the hypothesis for null-distance transitivity, and it is packaged into the increment-triangle certificate that records the whole J-cost null-distance chain as closed.
It is also the quantitative engine for completeness and ordered-field structure: the three-leg modulus is obtained by applying the two-leg modulus twice, and both addition-closure (pointwise sums of Cauchy ledgers remain Cauchy) and addition-congruence (addition respects null equivalence) open by invoking this modulus to choose a common $\delta$. In the Recognition foundation this is the step that lets the J-cost geometry support a real carrier rather than a mere premetric display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.