PRCRawEventuallyClose
plain-language theorem explainer
Two raw rational ledgers are eventually close at a fixed PRC tolerance when, past some index, their pointwise J-cost distance stays strictly below that tolerance. Completeness and representative-Cauchy arguments cite this as the quantitative tail predicate. The body is a direct existential definition over natural indices, not a proved theorem.
Claim. For raw rational ledgers $s,t:\mathbb{N}\to\mathrm{PRCRat}$ and a tolerance $\varepsilon\in\mathrm{PRCRat}$, say $s$ and $t$ are eventually close at $\varepsilon$ when there exists $N\in\mathbb{N}$ such that for every $n\ge N$, the J-cost distance between $s(n)$ and $t(n)$ is strictly less than $\varepsilon$.
background
This module builds a PRC-native complete ordered field from raw rational ledgers before Cauchy data are attached. A raw ledger is simply a sequence $\mathbb{N}\to\mathrm{PRCRat}$ of PRC rationals (ratio-orbit quotient classes). The comparison tool is the J-cost distance already used for Cauchy sequences in the primitive recognition calculus: it measures separation of two rationals via the cost functional $J$, not via an external absolute value.
Strict order on PRC rationals is the internal order lifted from signed orbits (nonnegative nonzero difference). Positivity of a tolerance is the corresponding PRC-native positivity predicate on ratio orbits. The present definition packages the standard "tails agree within $\varepsilon$" pattern in those native terms, so later completeness statements never leave the Recognition stack for classical $\mathbb{R}$.
Upstream scaffolding supplies the order and distance primitives: LogicNat/SignedOrbit strict order, the PRCRat quotient, and PRCJCostDistance from the RealCauchy layer.
proof idea
Definitional, not a proof. The predicate is the existential $\exists N,\forall n\ge N$ of the strict inequality PRCRat.lt (PRCJCostDistance (s n) (t n)) eps. No lemmas are applied; sibling abbreviations supply the raw-ledger type and the J-cost distance comparison.
why it matters
This is the atomic closeness atom for the PRC real-completion path. Representative Cauchy for a sequence of Cauchy ledgers is defined by requiring that representative tails are eventually close at every positive PRC tolerance. Finite diagonal and representative-tail selection targets in RealCompleteness quantify over the same predicate at unit-fraction rungs, and the raw diagonal ledger target uses it to state limit closeness of the constructed ledger. The finite-tail bound existence theorem takes an outer threshold already guaranteeing eventual closeness and produces a uniform raw depth. In the broader RS foundation, this keeps completeness internal to the J-cost geometry that later feeds the forcing chain, rather than importing classical metric completeness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.