PRCJCostDistance_symmetric
plain-language theorem explainer
The J-cost distance on PRC rationals is symmetric: d_J(a,b) equals d_J(b,a). Anyone building the PRC Cauchy surface or the null-equivalence relation on ledgers cites this. The proof pushes both sides through the injective toRat display, expands the square-gap and J-cost layers, and finishes by ring.
Claim. For all PRC rationals $a$ and $b$, the J-cost distance satisfies $d_J(a,b)=d_J(b,a)$, where $d_J$ is the composition of the positive square-gap map $(a,b)\mapsto 1+(a-b)^2$ with the PRC rational J-cost.
background
Primitive Recognition Calculus (PRC) builds a real line from orbit-indexed rational ledgers before ordinary analysis is available. PRC rationals are nonzero-denominator ratio-orbit quotient classes (K4.8), displayed injectively into ordinary rationals by toRat.
The local distance is not absolute difference. PRCJCostDistance first forms the positive square gap $1+(a-b)^2$, then applies the PRC rational J-cost (the same cost family forced by the Recognition Composition Law and T5 uniqueness of $J(x)=(x+x^{-1})/2-1$). That yields a nonnegative, self-zero cost suitable for Cauchy tolerances.
This module sits after the rational field and trace-closure layers and before the Cauchy-ledger quotient. Symmetry of the distance is the elementary metric axiom needed so that null-equivalence of two sequences is well-defined independently of order.
proof idea
Term-mode proof by transport along the injective display toRat. Apply injectivity of toRat on PRC rationals, unfold the distance definition, rewrite both sides with the commuting diagrams PRCJCost.onPRCRat_toRat and PRCSquareGap_toRat, then close the resulting rational identity by ring (the square gap is even in $a-b$, so the two compositions agree).
why it matters
Feeds PRCNullEquivalent, the intended null-distance relation on PRC Cauchy sequences: two ledgers are null-equivalent when their pairwise J-cost distance eventually falls below every positive PRC rational tolerance. Downstream doc states this relation "should become the final real quotient once transitivity is proved from the J-cost distance surface."
Without symmetry, that relation would not even be reflexive in both argument orders, blocking the real completion. In the broader RS chain this is scaffolding for the analytic layer under the forcing tower (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick), not a new physical claim: it makes the cost geometry of recognition ledgers into a genuine pseudometric seed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.