PRCRealCofinalToleranceScheduleTarget
plain-language theorem explainer
Packages the exact cofinal tolerance-schedule obligation used by the PRC real tail-selection diagonal: a sequence of positive internal rationals that eventually falls below every positive epsilon. Completeness and diagonal-selection arguments cite this Prop as the schedule target. The body is a pure existence statement over the PRC rational order; discharge is separate.
Claim. There exists a sequence $\tau:\mathbb{N}\to\mathbb{Q}_{\mathrm{PRC}}$ of positive PRC-rationals such that for every positive $\varepsilon\in\mathbb{Q}_{\mathrm{PRC}}$ there is $N\in\mathbb{N}$ with $\tau(n)<\varepsilon$ whenever $n\ge N$.
background
In the Primitive Recognition Calculus, reals are built from Cauchy data over an internal rational type PRCRat: ratio-orbit quotient classes identified by cross-multiplication. Positivity of a ratio orbit means a nonnegative signed numerator that is not balanced with zero. The strict order on these rationals is the positive-gap relation: $a<b$ means $b-a$ is positive.
This module develops completeness infrastructure for those PRC reals (raw Cauchy realization, quotient points, diagonal and tail selection). A cofinal positive schedule is the standard device that turns "arbitrarily small positive tolerance" into a concrete sequence usable inside diagonal arguments.
The local target isolates exactly that schedule property, with no completeness claim attached yet. Upstream order and positivity lemmas supply the language; the schedule itself is only named here.
proof idea
Definitional Prop, not a proved theorem. The body is a single existential: a map from naturals into PRC-rationals that is pointwise positive and cofinal at zero under the PRC strict order (for every positive epsilon, a tail lies strictly below it). No tactics or lemmas fire at this declaration; the constructive witness appears only in the companion proved theorem, which instantiates the sequence by unit fractions.
why it matters
Names the exact schedule hypothesis required by the tail-selection diagonal proof in the PRC real-completeness stack. The companion theorem discharges it by taking the unit-fraction sequence and applying the eventual-below-epsilon lemma. Downstream, the sharpened completeness certificate records raw Cauchy realization, quotient-point formation, and the chain from tail selection through raw diagonal ledger to diagonal selection; this target is the schedule node that chain depends on. Within Recognition foundation work it is bookkeeping for constructive completeness of the PRC real type, not a physics forcing step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.