PRCRealFiniteRepresentativeTailSelectionTarget_proved
plain-language theorem explainer
Any representative-Cauchy sequence of PRC Cauchy sequences admits a finite scheduler: for each tolerance rung one outer index and one raw depth that witness all finite representative-tail comparisons at the unit-fraction scale. Completeness and diagonal-construction arguments in the Primitive Recognition Calculus cite this. The proof chooses the outer map from the representative-Cauchy hypothesis at unit fractions, then applies the finite-tail existence lemma rungwise.
Claim. For every sequence $U$ of PRC Cauchy sequences that is representative-Cauchy, there exist maps $\mathrm{outer},\mathrm{pick}:\mathbb{N}\to\mathbb{N}$ such that: (i) whenever $m,n\ge\mathrm{outer}(r)$, the raw sequences of $U_m$ and $U_n$ are eventually close at tolerance $1/(r+1)$; (ii) for each rung $r$, the finite representative-tail bound for $U$ at that unit-fraction tolerance, outer threshold, and comparison depth $r$ holds at raw depth $\mathrm{pick}(r)$.
background
This module builds a constructive real-completeness layer for the Primitive Recognition Calculus: Cauchy data are raw integer ledgers with rational tolerances, not classical $\varepsilon$-$N$ nets. Unit fractions $\mathrm{PRCUnitFraction},r$ (positive by a sibling lemma) supply the discrete tolerance schedule indexed by rung.
A sequence $U:\mathbb{N}\to\mathrm{PRCCauchySeq}$ is representative-Cauchy when, at every positive rational tolerance, some outer index forces raw eventual closeness of all later representatives. The target proposition packages the exact finite scheduler the diagonal argument needs: for each rung, an outer Cauchy-representative threshold together with a raw depth realizing all finite representative-tail comparisons up to that rung.
Upstream, PRCRepresentativeFiniteTailBound_exists already produces, for fixed outer threshold and tolerance, a single raw depth $N$ witnessing the finite representative-tail bound. The present theorem only has to thread that existence through the unit-fraction schedule.
proof idea
Tactic proof, two dependent choices then a pair constructor. Introduce $U$ and the representative-Cauchy hypothesis $hU$. For each rung $r$, instantiate $hU$ at the unit fraction $1/(r+1)$ (using positivity) to obtain an outer index and the corresponding raw-closeness witnesses; choose packages these into maps outer and houter.
Rungwise, feed $U$, the unit fraction, outer r, the comparison depth $r$, and houter r into PRCRepresentativeFiniteTailBound_exists to obtain a raw depth; a second choose yields pick and hpick. Close with the existential pair $\langle\mathrm{outer},\mathrm{pick}\rangle$ and the two witness families.
why it matters
This is the representative half of the finite diagonal scheduler. Downstream, PRCRealFiniteDiagonalScheduleTarget_proved combines it with the finite row-tail selector so one raw choice function meets both row-tail and representative-tail constraints at every tolerance rung. That finite schedule is still not the completed global tail-selection theorem; the module doc on the diagonal target stresses the distinction.
The sharpened completeness certificate prc_real_completeness_sharpened_certificate assembles raw Cauchy realization, quotient points, and diagonal selection; this lemma is on the path that discharges the representative-tail obligation inside that certificate. In the broader Recognition stack it supports constructive completeness of the PRC real line used by later forcing and measurement layers, without yet invoking the T5–T8 geometric forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.