PRCUnitFraction_eventually_lt
plain-language theorem explainer
Unit fractions 1/(n+1) in the PRC rational type eventually drop below any fixed positive rational tolerance. Completeness and cofinal-schedule arguments cite this Archimedean fact when building PRC reals. The proof embeds into ordinary Q, picks N larger than the reciprocal of the tolerance, and finishes by field arithmetic.
Claim. For every positive PRC rational $\varepsilon$, there exists a natural number $N$ such that for all $n \ge N$, the unit fraction $1/(n+1)$ (represented as a PRC rational) is strictly less than $\varepsilon$.
background
The Primitive Recognition Calculus rebuilds arithmetic from recognition primitives: signed orbits for integers, then PRC rationals as fractions of those. The RealCompleteness module constructs reals as Cauchy quotients over this base and needs a concrete positive sequence of tolerances that becomes arbitrarily fine.
The unit-fraction schedule sends each natural $n$ to the PRC rational $1/(n+1)$. Sibling material already records that this value is positive and that its ordinary-rational image under the toRat embedding is exactly $1/(n+1)$. The local setting is the Archimedean step: any positive PRC rational must dominate all sufficiently late unit fractions, so the schedule is cofinal in the positive cone.
Upstream order facts (transitivity of $\le$ and the internal strict order on signed orbits and PRC rationals) underwrite the comparison lemmas used after the embedding.
proof idea
Transport positivity of $\varepsilon$ across the toRat embedding to obtain $0 < \varepsilon.\mathrm{toRat}$ in $\mathbb{Q}$. Invoke the standard Archimedean fact that some natural $N$ exceeds $1/\varepsilon.\mathrm{toRat}$. For $n \ge N$, rewrite the PRC strict order as the corresponding $\mathbb{Q}$ inequality between $1/(n+1)$ and $\varepsilon.\mathrm{toRat}$. Chain $1/\varepsilon < N \le n < n+1$ to get $1/\varepsilon < n+1$, multiply on the left by the positive $\varepsilon$, clear the product identity $\varepsilon\cdot(1/\varepsilon)=1$, then finish with field simplification and linear arithmetic on the cleared inequality.
why it matters
This lemma is the existence half of the cofinal tolerance schedule: the unit-fraction sequence is positive and eventually below every positive $\varepsilon$. The schedule target is discharged by packaging the sequence with its positivity proof and this eventual-dominance fact.
Downstream, that schedule feeds real tail selection (choosing late indices inside Cauchy data) and the three-leg J-cost modulus arguments that control cost distances on the completed reals. In the Recognition Science foundation stack, PRC real completeness sits under the forcing chain that later forces $\varphi$, the eight-tick octave, and $D=3$; without an Archimedean unit-fraction ladder the Cauchy quotient would lack a concrete, fully internal modulus schedule for cost comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.