constant
plain-language theorem explainer
Every constant sequence of PRC rationals is a PRC Cauchy sequence under J-cost distance. Anyone embedding fixed ledgers into the completed real line, or building constant paths in the action calculus, cites this constructor. The Cauchy witness is immediate: pairwise J-distance is identically zero, hence below every positive tolerance from index 0.
Claim. For every PRC rational $q$, the sequence $n \mapsto q$ is a PRC Cauchy sequence: for every positive PRC rational tolerance $\varepsilon$, there exists $N$ (namely $N=0$) 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 reals from orbit-indexed rational ledgers. A PRC rational is a ratio-orbit quotient class (nonzero-denominator cross-multiplication identification). The ambient metric on those rationals is J-cost distance: the cost gap induced by the unique J-functional $J(x)=(x+x^{-1})/2-1$ forced at T5 of the unified chain.
A PRC Cauchy sequence is a map $\mathbb{N}\to\mathrm{PRCRat}$ whose J-cost distance eventually falls below every positive PRC rational tolerance. Completing under that Cauchy filter yields the PRC reals used downstream in ordered-field and continuity modules.
The local module supplies the distance lemmas needed here: self-distance vanishes, and positivity of a tolerance implies the zero element is strictly below it.
proof idea
The term field is the constant function $n\mapsto q$. For the Cauchy field, fix any positive tolerance $\varepsilon$. Take $N=0$. For all $m,n\ge 0$, rewrite the pairwise J-cost distance via the self-zero lemma, obtaining $0$. The positivity-to-strict-order lemma then gives $0<\varepsilon$, which is exactly the required strict inequality.
why it matters
Constant ledgers are the base points of the PRC real completion and the trivial geodesics of the Recognition action calculus. Downstream, the Action layer uses constant paths heavily: the constant-1 path is a geodesic of the Hessian metric; the cost-rate Euler–Lagrange equation reduces to $J'(q)=0$ and is satisfied precisely at the constant path $\gamma\equiv 1$; the converse rigidity theorem says admissible EL paths are constantly one. Hamiltonian total energy and energy conservation along Newtonian trajectories likewise evaluate constant backgrounds. In the forcing chain this sits under T5 J-uniqueness: the same J that defines the Cauchy filter is the cost whose critical point is the constant ledger at the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.