PRCJCostDistance_sq_diff_lt_of_lt_modulus
plain-language theorem explainer
If the J-cost distance between two PRC rationals is smaller than a positive threshold δ controlled by η, then the squared ordinary difference of their rational displays is strictly less than η. Real-order congruence arguments for the PRC completion cite this bound when passing from cost-smallness to ordinary closeness. The proof transports the internal distance inequality to the verifier display and applies a squared-difference comparison on rationals.
Claim. Let $a,b,\eta,\delta$ be PRC rationals with $\eta>0$ and $\delta>0$. Suppose $\delta\le \eta^{2}/(4(1+\eta))$ in the verifier rationals, and that the J-cost distance between $a$ and $b$ is strictly less than $\delta$. Then $(a_{\mathbb{Q}}-b_{\mathbb{Q}})^{2}<\eta$, where $(\cdot)_{\mathbb{Q}}$ denotes the ordinary rational display.
background
PRC rationals are the Recognition-native rationals: quotient classes of ratio orbits under cross-multiplication, with an internal strict order given by nonnegative unbalanced difference. The map toRat is only a verifier display into ordinary $\mathbb{Q}$; internal comparisons are transported by the corresponding lt_iff lemmas.
The J-cost distance on these rationals is the Recognition cost gap between two displays. In this module it is compared to ordinary squared differences via an increment display: the cost of a difference $t$ is rewritten as a rational increment functional, so small cost forces small $|t|$ once a modulus bound on the threshold is in force.
The local setting is real-order congruence for the primitive recognition calculus: one must show that cost-small pairs remain order-close after passage to the real completion. The squared-difference form is the intermediate step before absolute-value bounds.
proof idea
First convert internal positivity of $\eta$ and $\delta$ to ordinary positivity of their rational displays via the positivity transport lemma.
Next rewrite the hypothesis that the J-cost distance is $<\delta$: pass through the internal-to-display order equivalence, replace the cost by its rational display, and identify that display with the increment functional of $a_{\mathbb{Q}}-b_{\mathbb{Q}}$. This yields that the increment display of the ordinary difference is $<\delta_{\mathbb{Q}}$.
Finally apply the pure rational comparison lemma that, under the stated bound $\delta\le\eta^{2}/(4(1+\eta))$, an increment display smaller than $\delta$ forces the squared difference below $\eta$. The whole argument is a short transport-plus-apply tactic proof.
why it matters
This lemma is the squared-difference bridge inside real-order congruence. Its sole recorded consumer is the absolute-difference form: once $(a-b)^{2}<\eta$ is available, one obtains $|a-b|$ controlled by an order-delta threshold, which is what the congruence certificate needs.
In the broader foundation stack, order congruence for the real completion is part of making the Recognition cost geometry compatible with classical real order. That compatibility underwrites later forcing steps that identify continuum structure (spatial dimension, octave timing) with the unique J-cost fixed by the Recognition Composition Law. Without a clean cost-to-ordinary modulus, the real completion would not inherit the internal order in a usable way.
The result is fully proved; it closes a concrete inequality step rather than leaving a scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.