PRCJCostDistance_neg_neg
plain-language theorem explainer
J-cost distance on PRC rationals is unchanged when both arguments are negated. Anyone building the ordered-field structure on PRC reals cites this when showing that pointwise negation preserves Cauchy ledgers and null equivalence. The proof reduces via the injective rational display to an algebraic identity on the square-gap formula, finished by ring normalization.
Claim. For PRC rationals $a,b$, the J-cost distance satisfies $d_J(-a,-b)=d_J(a,b)$, where $d_J$ is the distance obtained by sending the additive gap through the positive ratio $1+(a-b)^2$ and then applying the rational J-cost $J(x)=(x+x^{-1})/2-1$.
background
Primitive Recognition Calculus builds rationals as ratio-orbit quotient classes (PRCRat), with an injective display toRat into ordinary rationals. The first Cauchy surface uses a J-cost distance: additive separation is mapped to the positive ratio $1+(a-b)^2$, then the PRC rational J-cost is applied. Explicitly, the verifier display is $g=1+(x-y)^2$ followed by $(g+g^{-1})/2-1$, which is the standard RS cost $J$ of T5.
This module assembles a complete ordered field on the resulting real completion. Negation of ledgers is part of that field structure, so the distance must be compatible with sign flip. Upstream, the display theorem equates the abstract distance on PRCRat with the rational formula above, and injectivity of toRat lets equalities be checked after display.
proof idea
Apply injectivity of the rational display on PRCRat. Rewrite both sides with the display theorem so the goal becomes equality of the rational J-cost displays of $(-a,-b)$ and $(a,b)$. Unfold the display formula; the only nontrivial ingredient is $((-x)-(-y))^2=(x-y)^2$. simp plus ring_nf close the algebraic identity.
why it matters
Negation must preserve the Cauchy predicate and null equivalence before the PRC real quotient can carry a well-defined additive inverse. Downstream, the closure target uses this identity to replace $d_J(-(u_m),-(u_n))$ by $d_J(u_m,u_n)$ inside the Cauchy witness, and the congruence target does the same for null pairs. That pair of results is the exact blocker for additive inverses on the completed field.
In the broader RS chain this is infrastructure rather than a forcing step: it keeps the J-cost geometry (T5) intact under the field operations needed for the real completion that later hosts the eight-tick and dimension arguments. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.