PRCCauchySeq
plain-language theorem explainer
Defines a Cauchy sequence of PRC rationals: an orbit-indexed ledger whose J-cost pairwise distances eventually drop below every positive rational tolerance. Anyone building the PRC real completion or the null-distance quotient cites this carrier. It is a pure structure declaration (term map plus the Cauchy predicate), not a proved theorem.
Claim. A PRC Cauchy sequence is a pair $(t, C)$ where $t:\mathbb{N}\to\mathrm{PRCRat}$ is an orbit-indexed rational ledger and $C$ asserts: for every positive PRC rational $\varepsilon>0$ there exists $N\in\mathbb{N}$ such that for all $m,n\ge N$, the J-cost distance $d_J(t(m),t(n))$ is strictly less than $\varepsilon$.
background
This module sits in the Primitive Recognition Calculus real-construction layer: rationals are already built as nonzero-denominator ratio-orbit quotient classes (PRCRat), with a native strict order $a<b$ meaning the gap $b-a$ has a positive ratio-orbit representative, and a native positivity predicate on ratio orbits (nonnegative nonzero signed numerator).
The metric used here is not absolute difference. J-cost distance first sends additive separation through the positive ratio $1+(a-b)^2$ (the square-gap map), then applies the PRC rational J-cost. That is the distance surface against which the Cauchy condition is stated: eventually all pairwise ledger terms lie inside every positive J-cost ball.
Upstream order and arithmetic come from the logic-native naturals and signed-orbit integers; the rational field layer supplies positivity and field operations used in the gap and cost maps.
proof idea
No proof body: this is a structure definition. It packages a term map Nat → PRCRat with a single field asserting the standard $\varepsilon$-$N$ Cauchy condition measured in J-cost distance and ordered by the PRC-native strict order on rationals. Downstream constructors (constant ledgers) discharge the Cauchy field by picking $N=0$ and using self-distance zero of the J-cost.
why it matters
This is the carrier type for the first PRC Cauchy surface toward reals. Constant rational ledgers inhabit it; ofRat embeds a rational as the constant Cauchy ledger inside the eventual real quotient. The intended null-distance relation between two such sequences (eventual J-cost closeness of corresponding terms) is defined on this type and is meant to become the real equivalence once triangle-style transitivity is proved.
Downstream, PRCNullDistanceTransitiveTarget is exactly the open blocker: prove that null-equivalence is transitive on these Cauchy ledgers. Until that closes, the real quotient remains certificate-gated. In the broader Recognition stack this is foundation plumbing for completing the rational ledger before continuum-level forcing (J-uniqueness, $\varphi$, eight-tick structure) is interpreted on completed quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.