PRCRawNullEquivalent
plain-language theorem explainer
Null equivalence of two raw rational ledgers: pointwise J-cost distance eventually drops below every positive PRC rational. Analysts building the PRC real quotient cite it when stating well-definedness of arithmetic on Cauchy classes. The declaration is a pure Prop definition (no proof obligations).
Claim. Two raw completed-orbit rational ledgers $s,t:\mathbb{N}\to\mathbb{Q}_{\mathrm{PRC}}$ 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 $s(n)$ and $t(n)$ is strictly less than $\varepsilon$.
background
In the Primitive Recognition Calculus, rationals are quotient classes of ratio orbits (nonzero-denominator cross-multiplication). A raw rational ledger is simply a map $\mathbb{N}\to\mathbb{Q}_{\mathrm{PRC}}$, before any Cauchy certificate is attached.
Distance on those rationals is the J-cost distance already used for Cauchy sequences: a sequence is Cauchy when that distance between late terms falls below every positive PRC rational. Strict order on PRC rationals is positivity of the difference $b-a$.
Null equivalence is the same eventual-small-distance condition, but comparing two ledgers termwise rather than a ledger to itself. It is the raw-level relation that will identify Cauchy sequences that represent the same real.
proof idea
Definition only: the body is the standard $\varepsilon$-$N$ statement that $\mathrm{dist}_J(s_n,t_n)$ is eventually smaller than every positive PRC rational $\varepsilon$. No lemmas are applied; the Prop reuses the existing positivity, strict order, and J-cost distance on PRC rationals.
why it matters
This relation is the exact congruence predicate needed to descend addition, negation, and multiplication to the quotient of Cauchy sequences by null distance. Downstream blockers PRCRealAddCongruenceTarget, PRCRealNegCongruenceTarget, and PRCRealMulCongruenceTarget each demand that null-equivalent Cauchy inputs yield null-equivalent raw images under pointwise add, neg, and mul.
In the Recognition foundation stack this sits inside the construction of a complete ordered field from logic-native arithmetic, so that later forcing-chain geometry (J-uniqueness, $\varphi$, eight-tick structure) can be stated over a PRC-native continuum rather than an imported classical $\mathbb{R}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.