PRCJCostDistance_self_zero
plain-language theorem explainer
Equal PRC rationals have vanishing J-cost distance. Anyone assembling the first PRC Cauchy surface, constant ledgers, or the null-distance setoid for reals cites this reflexivity seed. The proof reduces through the injective rational display, rewrites the square-gap and on-rational J formulas, and simplifies to J(1)=0.
Claim. For every PRC rational $a$, the J-cost distance satisfies $d_J(a,a)=0$, where $d_J(a,b)$ is the PRC rational J-cost of the positive ratio $1+(a-b)^2$.
background
Primitive Recognition Calculus builds rationals as nonzero-denominator ratio-orbit quotients (PRCRat), with an injective display toRat into ordinary rationals. The local module constructs the first Cauchy surface for an internal real carrier from these rationals.
The J-cost on positive ratios is the forced cost from the Recognition Composition Law and T5 uniqueness: $J(x)=(x+x^{-1})/2-1$. The sibling distance sends additive separation through the always-positive gap $1+(a-b)^2$, then applies that J-cost on PRC rationals. The square-gap display identity states $(1+(a-b)^2)$ maps to $1+(a.toRat-b.toRat)^2$, and the on-rational J display recovers the classical formula.
This lemma is the diagonal vanishing fact needed before Cauchy sequences and null-equivalence can be stated with that distance.
proof idea
Apply injectivity of the rational display so it suffices to check equality after toRat. Unfold the distance definition, rewrite by the on-rational J display and the square-gap display identity, then simp. On the diagonal the gap becomes $1$, and $J(1)=(1+1^{-1})/2-1=0$.
why it matters
Reflexivity of J-cost distance is the first metric axiom on the PRC Cauchy surface. Downstream, constant rational ledgers use it to prove they are Cauchy; the intended null-distance relation between Cauchy ledgers uses it for reflexivity; and the Build Order step-8 certificate packages it explicitly as jcost_distance_self_zero beside constant embedding and null-relation reflexivity/symmetry.
In the broader framework this is the cost surface induced by T5's unique J, not an ad-hoc metric. It does not yet finish the real quotient (transitivity of null-equivalence remains the named target), but it closes the self-zero obligation on the path from rational ledgers to an internal real carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.