ofRat

In the Primitive Recognition Calculus, reals are not postulated. One builds Cauchy sequences of PRC rationals (ratio-orbit quotient classes with nonzero denominators), then quotients by null distance. The carrier PRCRealNull is that quotient, but only after a transitivity target for null distance is in hand: it is defined as the quotient by the setoid induced from that target.

Constant sequences of a fixed rational are Cauchy (the upstream constant-ledger constructor). Null distance identifies sequences that become arbitrarily close in the recognition metric; the setoid package packages reflexivity, symmetry, and the supplied transitivity into a Lean setoid so that Quot can form classes.

The local module therefore separates the analytic obligation (transitivity / triangle modulus) from the pure type construction of the real carrier and its rational embedding.

One-line definitional wrapper. Form the constant Cauchy sequence at the given PRC rational via the upstream constant-ledger constructor, then apply Quot.mk with the setoid induced by the supplied null-distance transitivity target. No further arithmetic or Cauchy estimates appear here.

This is the rational spine of the conditional PRC real line. Downstream closed carriers re-export it once transitivity is proved, and Delta-real / protocol layers use rational embeddings as the base case of evaluation and of the forgetful map to classical $\mathbb{R}$. The continuum capstone that forces $J(x)=(x+1/x)/2-1$ on the completion (T5 J-uniqueness on $R_\delta$) needs a real carrier with a faithful rational embedding; this constructor is that embedding at the null-setoid stage. It does not itself force $J$, but without it the completion has no canonical $\mathbb{Q}$-points.