raw_cauchy
plain-language theorem explainer
For any PRC Cauchy sequence, the underlying raw rational ledger remains Cauchy under J-cost distance. Builders of the real completion from orbit-indexed rational ledgers cite this when stripping structure. The proof is a one-line projection of the sequence's built-in Cauchy witness onto the raw predicate.
Claim. If $u$ is a PRC Cauchy sequence, then the raw rational ledger obtained by forgetting $u$'s Cauchy packaging satisfies the raw Cauchy predicate: 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 the $m$-th and $n$-th terms is strictly less than $\varepsilon$.
background
Primitive Recognition Calculus builds a real-like ordered field from rational ledgers indexed by natural numbers (orbit ticks), with closeness measured by J-cost distance rather than absolute value. The J-cost is the unique cost forced by the Recognition Composition Law; distances are formed from it on PRC rationals.
A PRC Cauchy sequence packages a term map $\mathbb{N}\to\mathrm{PRCRat}$ together with a witness that J-cost distance eventually drops below every positive PRC rational tolerance. The raw forgetful map discards that witness and retains only the term map as a bare rational ledger.
The raw Cauchy predicate is definitionally the same $\varepsilon$-$N$ statement, stated on bare ledgers. This module sits in the foundation layer that completes those ledgers toward an ordered field.
proof idea
One-line wrapper: the goal PRCRawCauchy u.raw is definitionally identical to the Cauchy field already stored on u, because raw is just the term projection and PRCRawCauchy copies the same quantifiers and J-cost comparison as the structure field. The proof therefore returns u.cauchy directly.
why it matters
In the Recognition foundation stack, reals are not imported as a black box; they are completed from rational ledgers under J-cost. This lemma licenses treating a structured Cauchy sequence as a raw Cauchy ledger, which is the type on which null-equivalence, addition, negation, and multiplication of raw classes are defined in the same module.
No downstream consumers are wired yet in the graph, so the lemma is presently a local bridge inside the complete ordered field construction. It aligns with the broader forcing chain only indirectly: J-cost uniqueness (T5) fixes the metric that makes the Cauchy condition meaningful, and the eight-tick and dimension steps sit further downstream once the field exists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.