PRCRawCauchy
plain-language theorem explainer
A raw rational ledger (sequence of PRC rationals) is Cauchy when J-cost distances between late terms fall below every positive rational threshold. Anyone assembling PRC reals from Cauchy data, or proving field-operation closure on those sequences, cites this predicate. The body is a pure definition: the standard ε–N Cauchy condition with PRCJCostDistance in place of absolute difference.
Claim. A raw rational ledger $s:\mathbb{N}\to\mathbb{Q}_{\mathrm{PRC}}$ is Cauchy when, for every positive PRC-rational $\varepsilon$, there exists $N\in\mathbb{N}$ such that for all $m,n\ge N$, the J-cost distance between $s(m)$ and $s(n)$ is strictly less than $\varepsilon$.
background
In the Primitive Recognition Calculus (PRC) stack, rationals are quotient classes of ratio orbits (nonzero-denominator signed-orbit pairs identified by cross-multiplication). A raw completed-orbit rational ledger is simply a map $\mathbb{N}\to\mathbb{Q}_{\mathrm{PRC}}$: the sequence data before any Cauchy certificate is attached.
Distance on these rationals is not absolute difference. The J-cost distance first forms the positive ratio gap $1+(a-b)^2$, then applies the PRC rational J-cost. Strict order $a<b$ means the difference $b-a$ is positive in the PRC-native sense (nonnegative signed numerator, not balanced to zero).
This module sits in the RealCompleteOrderedField layer: it packages the raw sequence type and the Cauchy predicate that later closure and completeness targets quantify over, matching the distance already used by the packaged Cauchy-sequence surface.
proof idea
Definition only: no proof obligations. Unfolding yields the classical Cauchy quantifier pattern $\forall\varepsilon>0.,\exists N.,\forall m,n\ge N., d_J(s_m,s_n)<\varepsilon$, with positivity, strict order, and $d_J$ supplied by the PRC rational field and the J-cost distance on square gaps. No lemmas are applied.
why it matters
This predicate is the gate on every raw ledger that is allowed to become a real. Downstream completeness targets require it: packaging a raw ledger as a Cauchy sequence, sending it to a null-distance quotient point, and building diagonal or tail-selected limit ledgers all assume the raw sequence is Cauchy in this sense.
Field structure blockers also land here. Addition, multiplication, and negation closure are stated as: the pointwise raw combination of two Cauchy ledgers is again Cauchy under this predicate. Until those targets close, the PRC reals cannot inherit a complete ordered field structure from the rational ledger layer.
In the broader Recognition foundation, this is infrastructure beneath the forcing chain rather than a T0–T8 step itself: it fixes how completeness is phrased once J-cost is the native metric on recognition data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.