PRCJCostDistance_abs_diff_lt_of_lt_order_delta
plain-language theorem explainer
If the J-cost distance between two PRC rationals is below a positive threshold δ controlled by γ, their ordinary difference lies strictly in (−γ, γ). Order-congruence arguments for PRC Cauchy sequences cite this when converting small cost gaps into ordinary bounds. The proof sets η = γ², invokes the squared-difference modulus lemma, then applies the rational square-root bound.
Claim. Let $a,b,\gamma,\delta$ be PRC rationals with $\gamma>0$ and $\delta>0$. If $\delta \le \frac{\gamma^{4}}{4(1+\gamma^{2})}$ and the J-cost distance between $a$ and $b$ is strictly less than $\delta$, then $-\gamma < a-b < \gamma$ as ordinary rationals (via the canonical embedding into $\mathbb{Q}$).
background
This module builds real order congruence for the Primitive Recognition Calculus (PRC): the order on Cauchy sequences of PRC rationals must be invariant under null equivalence so that the induced order on PRC reals is well-defined.
PRC rationals (PRCRat) are quotient classes of ratio orbits with nonzero denominator, identified by cross-multiplication. They carry an internal strict order and a positive cone, with a forgetful map toRat into ordinary rationals that preserves multiplication. The J-cost distance between two such rationals is the Recognition cost gap used as a modulus of closeness; it is the local avatar of the T5 cost $J(x)=(x+x^{-1})/2-1$.
The sibling squared-difference lemma already converts a small J-cost gap into $(a-b)^{2}<\eta$ under a matching bound on $\delta$ in terms of $\eta$. The present result specialises that modulus to $\eta=\gamma^{2}$ and extracts the two-sided ordinary bound $|a-b|<\gamma$.
proof idea
Introduce $\eta:=\gamma\cdot\gamma$ as a PRC rational and check positivity from positivity of $\gamma$ via toRat and nlinarith. Record $\eta.\mathrm{toRat}=\gamma.\mathrm{toRat}^{2}$.
Feed $a,b,\eta,\delta$ into the sibling PRCJCostDistance_sq_diff_lt_of_lt_modulus, rewriting the given $\delta$-bound with the identity for $\eta.\mathrm{toRat}$. That yields $(a.\mathrm{toRat}-b.\mathrm{toRat})^{2}<\gamma.\mathrm{toRat}^{2}$.
Finish with rat_sq_lt_sq_bounds on the positive rational $\gamma.\mathrm{toRat}$: a square strictly below $\gamma^{2}$ forces the difference into $(-\gamma,\gamma)$.
why it matters
Downstream, PRCRawEventuallyLe_of_null_equiv uses this bound to show that eventual inequality of raw PRC Cauchy sequences is preserved when both sides are replaced by null-equivalent sequences. Without a cost-to-ordinary bridge of this shape, null pairs could drift by a fixed rational gap and break order descent.
That invariance is the content of the real-order-congruence certificate in the same module: the PRC real order is a congruence for the null equivalence relation. In the broader foundation stack this sits under the construction of arithmetic and analysis from recognition primitives, upstream of continuum-level forcing (T5 J-uniqueness and the RCL) rather than inside the T0–T8 chain itself. It closes a concrete gap between the J-cost modulus and the ordered field structure needed for later continuum arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.