ofRat
plain-language theorem explainer
Embeds a PRC rational as the equivalence class of its constant Cauchy ledger inside the internal PRC real carrier. Anyone building the rational spine of the completion, Delta-real protocols, or the forced-J capstone cites this map. The body is a one-line quotient constructor: mark the constant Cauchy sequence under the same-term setoid.
Claim. For every PRC rational $q$, write $\iota(q)$ for the class in the PRC real carrier of the constant Cauchy sequence with every term equal to $q$. Thus $\iota$ embeds the PRC rationals into the Cauchy-ledger quotient that serves as the internal real line.
background
The module builds an internal real carrier from PRC data alone, without Lean's classical $\mathbb{R}$. A PRC rational is a ratio-orbit quotient class (nonzero-denominator pairs identified by cross-multiplication). A PRC Cauchy sequence is an orbit-indexed rational ledger whose J-cost distance eventually falls below every positive PRC rational tolerance.
Constant ledgers are Cauchy: the sequence with every term equal to a fixed rational $q$ has vanishing pairwise J-cost distance, so it is a valid Cauchy sequence. The first internal real carrier is the quotient of such Cauchy sequences by the same-term setoid (later refined toward a null-distance setoid target).
This embedding is the PRC-native analogue of $\mathbb{Q}\hookrightarrow\mathbb{R}$ via constant sequences. Parallel ofRat maps appear on Delta-real protocols and on the null-closed quotient carrier.
proof idea
Definitional one-liner. Apply the constant-Cauchy constructor to $q$, obtaining a PRC Cauchy sequence whose every term is $q$. Pass that sequence to the quotient constructor for the same-term setoid; the resulting class is the embedded real. No further proof obligations: constancy already discharges the Cauchy witness.
why it matters
This is the rational spine of the internal completion. Downstream, Delta-real ofRat, value_ofRat, and value_surjective use the same pattern so that classical reals arise as forgetful values of protocols with $\mathrm{value}(\mathrm{ofRat}, q)=q$. Certified analytic evaluators route rational literals through the analogous protocol embedding.
The continuum capstone forced_J_on_completion needs rationals inside the completed carrier so that reciprocal-symmetric RCL plus normalization and one calibration datum force $J(x)=(x+x^{-1})/2-1$ (T5 J-uniqueness) on the completion. Without a faithful rational embedding, the forcing chain cannot anchor calibration points or compare costs on dense data.
It also feeds the null-closed ofRat used in order-step closure certificates, tying the Cauchy ledger story to the null-distance quotient target recorded on the real carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.