PRCRealCofinalToleranceScheduleTarget_proved
plain-language theorem explainer
A positive PRC-rational tolerance schedule τ(n)=1/(n+1) is cofinal: every positive ε is eventually strictly above τ(n). Completeness and tail-selection diagonal arguments cite this as the concrete schedule that drives the diagonal proof. The proof packages the unit-fraction sequence with its positivity and eventual-smallness lemmas in one refine.
Claim. There exists a sequence $\tau:\mathbb{N}\to\mathrm{PRCRat}$ of positive PRC-rationals such that for every positive $\varepsilon\in\mathrm{PRCRat}$ there is $N\in\mathbb{N}$ with $\tau(n)<\varepsilon$ whenever $n\ge N$.
background
Primitive Recognition Calculus (PRC) rebuilds ordered-field and completeness structure from recognition primitives rather than classical reals. Inside that development, PRC-rationals carry a positivity predicate and a strict order, both tied to an underlying rational embedding (toRat).
A cofinal tolerance schedule is a sequence of positive PRC-rationals that becomes arbitrarily small: for every positive tolerance ε there is a tail beyond which every schedule value is strictly less than ε. The module records this as the exact target needed by the tail-selection diagonal proof of real completeness.
The concrete schedule used here is the unit-fraction sequence τ(n)=1/(n+1), built as a PRC-rational from the distinction-natural denominator n+1. That sequence is verifier display machinery for the completeness argument, not a new PRC primitive. Upstream lemmas already show every unit fraction is positive and that the sequence is eventually smaller than any fixed positive PRC-rational.
proof idea
One short tactic proof. refine supplies the existential witness as the unit-fraction schedule, then discharges the two conjuncts: positivity of every term via the unit-fraction positivity lemma, and the cofinal eventual-smallness clause by applying the unit-fraction eventual-less-than lemma to the given positive ε. No further case analysis or classical real analysis is invoked.
why it matters
This closes the cofinal-schedule obligation required by the tail-selection diagonal route to PRC real completeness. Downstream it is consumed by the sharpened completeness certificate, which assembles raw Cauchy realization, quotient-point, and diagonal-selection targets into a single package.
In the Recognition foundation stack, completeness of the reconstructed reals is infrastructure rather than a forcing-chain landmark (T5–T8). Still, without a concrete positive schedule that is cofinal in the PRC order, the diagonal selection that turns raw Cauchy data into a completed real cannot be stated. The unit-fraction choice keeps the certificate elementary and fully constructive at the schedule layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.