PRCJCostDistance
plain-language theorem explainer
J-cost distance on PRC rationals: feed additive separation through the positive gap 1+(a−b)², then apply the rational J-cost. Cited by anyone defining the first PRC Cauchy surface, proving eventual boundedness, or discharging the triangle-certificate step. One-line composition of the square gap with the lifted J-cost on the rational quotient.
Claim. For PRC rationals $a,b$, define the J-cost distance $d_J(a,b) := J_{\mathrm{PRC}}\bigl(1+(a-b)^2\bigr)$, where $J_{\mathrm{PRC}}$ is the Recognition J-cost lifted to the PRC rational quotient and $1+(a-b)^2$ is the positive square gap.
background
PRC rationals are the nonzero-denominator ratio-orbit quotient: classes identified by cross-multiplication of orbit-level numerators and denominators. They are the arithmetic carrier for the first Cauchy surface in Primitive Recognition Calculus.
The square gap sends a pair $(a,b)$ to the strictly positive rational $1+(a-b)^2$. Squaring removes any need for a rational absolute value in this pass, so comparison stays inside the ordered field of PRC rationals.
The PRC J-cost on rationals is the lift of the orbit-level cost $J$ (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$) to the quotient. Composing that lift with the square gap yields a nonnegative rational that vanishes exactly when $a=b$.
proof idea
Pure definitional composition: apply the square gap to $(a,b)$, then feed the result to the J-cost already lifted to PRC rationals. No lemmas, no tactics; the body is the two-name composition of those upstream defs.
why it matters
This is the distance that defines a PRC Cauchy sequence: a ledger whose pairwise J-cost distances eventually fall below every positive PRC rational tolerance. Downstream it appears in the self-zero and symmetry lemmas, in the display theorem that matches the ordinary rational formula, and in the conditional triangle certificate whose only remaining obligation is an explicit rational inequality.
It also drives the boundedness modulus: small J-cost distance below a fixed positive threshold forces the ordinary squared increment below one, which closes eventual containment in a symmetric rational interval and clears the multiplication blocker for real product continuity. In the Recognition forcing chain this sits under the foundation layer that builds completed reals before T5–T8 (J-uniqueness, phi, eight-tick, D=3) are applied to physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.