PRCNullEquivalent
plain-language theorem explainer
Two PRC Cauchy sequences are null-equivalent when their termwise J-cost distance eventually falls below every positive rational tolerance. Builders of the internal real quotient from recognition ledgers cite this as the intended setoid kernel. The definition is the standard Cauchy-null predicate; reflexivity and symmetry follow at once from self-zero and symmetry of J-cost distance.
Claim. Two Cauchy sequences $u$ and $v$ of PRC rationals are null-equivalent when, for every positive PRC rational $\varepsilon$, there exists $N\in\mathbb{N}$ such that for all $n\ge N$ the J-cost distance between the $n$th terms satisfies $d_J(u_n,v_n)<\varepsilon$.
background
In Primitive Recognition Calculus, reals are built internally from Cauchy ledgers rather than imported from classical analysis. A PRC Cauchy sequence is an orbit-indexed sequence of PRC rationals whose pairwise J-cost distance eventually falls below every positive rational tolerance.
J-cost distance is the recognition-theoretic surface induced by the unique cost $J(x)=(x+x^{-1})/2-1$ forced at T5 (equivalently $\cosh(\log x)-1$). Sibling facts record that this distance vanishes on the diagonal and is symmetric. The local module carries Order step 8 of the foundation chain: internal Cauchy ledgers plus a named null-distance quotient target, without classical real aliases.
proof idea
The body is a definition, not a derived theorem: null-equivalence is the standard eventual-closeness predicate under J-cost distance. The accompanying reflexivity proof is a one-line wrapper: take $N=0$, rewrite by the self-zero lemma for J-cost distance, and use positivity of the tolerance. Symmetry is likewise a wrapper: reuse the same witness $N$ after rewriting by the symmetry lemma for J-cost distance.
why it matters
This relation is the intended kernel of the internal real setoid. Downstream, the null-distance setoid target packages full equivalence (reflexivity and symmetry already proved here; triangle-style transitivity is the live blocker). The first-pass real Cauchy certificate records reflexivity and symmetry of the null relation and names the setoid obligation explicitly. Additive, multiplicative, and negation congruence targets in the complete ordered-field module all quantify over this relation, so field operations on the quotient wait on its properties. Closing J-cost triangle inequality is the exact mathematical step before the internal real quotient can form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.