PRCJCostDistance_add_right
plain-language theorem explainer
J-cost distance on PRC rationals is invariant under a common additive shift of both endpoints. Builders of the real completion from Cauchy ledgers cite it when proving that pointwise sums stay Cauchy and that addition respects null equivalence. The proof pushes both sides through the injective rational display and simplifies the square-gap formula.
Claim. For all PRC rationals $a,b,c$, the J-cost distance satisfies $d_J(a+c,\,b+c)=d_J(a,b)$.
background
Primitive Recognition Calculus (PRC) builds rationals as nonzero-denominator ratio-orbit quotient classes (PRCRat), then equips them with a J-cost distance before completing to reals via Cauchy ledgers.
The J-cost is the Recognition Science cost $J(x)=(x+x^{-1})/2-1$. On rationals the distance is displayed by the square-gap formula: with $g=1+(x-y)^2$, one sets $d_J(x,y)=(g+g^{-1})/2-1$. The theorem PRCJCostDistance_toRat identifies the abstract PRC distance with this display, and toRat is injective on the quotient.
The local module constructs the complete ordered field structure on PRC reals; translation invariance of $d_J$ is the elementary algebraic fact needed before Cauchy closure and congruence of addition can be stated.
proof idea
One short tactic proof. Apply injectivity of the rational display map toRat so equality of distances reduces to equality of displayed rationals. Rewrite both sides with PRCJCostDistance_toRat, then simp against the square-gap display PRCJCostDistanceRatDisplay. The displayed formula depends only on the difference $x-y$, which is unchanged by adding the same $c$ to both arguments, so the two sides match.
why it matters
Feeds the two addition targets on PRC reals in the same module: PRCRealAddClosureTarget_proved (pointwise sums of Cauchy ledgers remain Cauchy) and PRCRealAddCongruenceTarget_proved (addition respects null equivalence). Both proofs reduce additive estimates to the unshifted distance via this invariance (and its left twin).
In the Recognition framework this is foundation plumbing under the J-cost forced at T5 of the forcing chain: before one can form a complete ordered field of recognition reals, the cost metric must be translation-invariant so addition descends to the Cauchy quotient. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.