PRCJCostDistance_add_left
plain-language theorem explainer
Left translation leaves J-cost distance unchanged on PRC rationals: d(c+a,c+b)=d(a,b). Anyone building addition of PRC reals from Cauchy ledgers cites this for closure and congruence. The proof injects into ordinary rationals and simplifies the square-gap display, which depends only on a−b.
Claim. For PRC rationals $a,b,c$, the J-cost distance satisfies $d_J(c+a,\,c+b)=d_J(a,b)$. Equivalently, left translation by any fixed rational is an isometry of the J-cost metric on the PRC rational line.
background
Primitive Recognition Calculus builds rationals as quotient classes of ratio orbits (nonzero-denominator pairs identified by cross-multiplication). The J-cost on positive ratios is the unique cost forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$. On the rational line the verifier display of J-cost distance is $d_J(x,y)=J\bigl(1+(x-y)^2\bigr)$, i.e. $\frac{g+g^{-1}}{2}-1$ with $g=1+(x-y)^2$.
The module constructs a complete ordered field of PRC reals as Cauchy ledgers modulo null equivalence, with the J-cost distance supplying the Cauchy modulus. Upstream, PRCJCostDistance_toRat identifies the abstract distance with that rational display, and injectivity of the rational display map lets equalities on $\mathbb{Q}$ lift back to PRC rationals.
proof idea
Apply injectivity of the PRC-to-ordinary rational display. Rewrite both sides via the display theorem so the goal is equality of two instances of the square-gap formula. Simplify: the formula depends only on the difference of the endpoints, and $(c+a)-(c+b)=a-b$, so both sides reduce to the same rational.
why it matters
Left-invariance of $d_J$ is the metric ingredient that makes pointwise addition well-defined on Cauchy ledgers. Downstream it feeds the proved add-closure target (pointwise sums of Cauchy ledgers remain Cauchy) and the proved add-congruence target (addition respects null equivalence). Together those discharge the algebraic half of the PRC real complete ordered field construction. In the broader forcing chain this sits under the foundation layer that eventually supports T5 J-uniqueness and the RCL-derived cost, not a physics constant claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.