PRCUnitFraction_toRat
plain-language theorem explainer
The PRC unit-fraction display at index n maps under the verifier rational embedding to the ordinary rational 1/(n+1). Completeness and cofinal-tolerance arguments cite this bridge when moving between PRC rationals and Mathlib ℚ. The proof unfolds the constructor and simplifies via the signed-orbit and distinction-nat transport lemmas.
Claim. For every natural number $n$, the verifier rational image of the PRC unit fraction with denominator $n+1$ equals $\frac{1}{n+1}$ in $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, rationals are quotient classes of ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator, identified by cross-multiplication (K4.7–K4.8). The display map toRat sends a ratio orbit to the ordinary rational (num.toInt)/(den.toNat); on the quotient it is the corresponding transport wrapper.
The unit-fraction schedule PRCUnitFraction n is not a new PRC primitive. It is verifier display machinery for the real-completeness argument: numerator is the signed unit orbit, denominator is the distinction-nat for $n+1$ (proved nonzero). This module builds the completeness side of PRC reals from ordered congruence and integer-rational layers.
Upstream, one_toInt records that the signed unit has integer image 1, and toNat_ofNat recovers the underlying natural from a distinction-nat built by ofNat. Together they pin the concrete rational value of the unit-fraction display.
proof idea
Term-mode proof by unfolding and simplification. Unfold the unit-fraction constructor to expose the ratio-orbit package (signed unit over distinction-nat $n+1$). Rewrite with the quotient display lemma toRat_mk, which reduces the PRC-rational display to the underlying ratio-orbit toRat. Unfold that definition and simp with one_toInt (numerator becomes 1) and toNat_ofNat (denominator becomes $n+1$), yielding $1/(n+1)$ in $\mathbb{Q}$.
why it matters
This identity is the bridge that lets positivity and cofinal-tolerance lemmas work in Mathlib $\mathbb{Q}$ while staying native on the PRC side. Downstream, PRCUnitFraction_positive rewrites positivity through this equality and closes by positivity. PRCUnitFraction_eventually_lt uses the same bridge to show that the unit-fraction schedule is eventually below any positive PRC rational, the exact cofinal tolerance schedule needed by tail-selection in the real-completeness construction.
In the broader foundation stack this is bookkeeping, not a forcing-chain step (T0–T8). It keeps the completeness proof honest: tolerances are PRC objects, yet their Archimedean decay is checked against ordinary rationals without smuggling extra structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.