PRCRepresentativeFiniteTailBound_exists
plain-language theorem explainer
Given a family of Cauchy sequences pairwise eventually close past an outer index at tolerance ε, a single raw depth N makes every eligible row i (outer ≤ i ≤ r) J-cost-close to the target row r past N. Completeness and diagonal-selection arguments cite this as the finite representative-tail scheduler. The proof strengthens to all intermediate row bounds and inducts, taking maxima of pairwise eventual-closeness witnesses.
Claim. Let $U$ be an $\mathbb{N}$-indexed family of Cauchy sequences and $\varepsilon$ a rational tolerance. Suppose an outer index is given so that for all $m,n$ at least that outer index, the raw sequences of $U_m$ and $U_n$ are eventually $\varepsilon$-close. Then for any finite row bound $r$ there exists a raw depth $N$ such that whenever $\mathrm{outer}\le i\le r$ and $k\ge N$, the $J$-cost distance between the $k$-th terms of $U_i$ and $U_r$ is strictly less than $\varepsilon$.
background
In the Primitive Recognition Calculus real-completeness development, candidate reals are Cauchy sequences of rationals, with closeness measured by $J$-cost distance (the Recognition cost $J(x)=(x+x^{-1})/2-1$ used as a metric on positive quantities). Two raw sequences are eventually $\varepsilon$-close when past some depth their pairwise $J$-cost stays below $\varepsilon$.
The finite representative-tail bound asserts that one raw depth $N$ simultaneously witnesses $\varepsilon$-closeness of every eligible representative row $i$ (outer $\le i\le r$) to the fixed target row $r$. The outer threshold is the point past which the family $U$ is assumed pairwise eventually close at $\varepsilon$: the Cauchy condition on the sequence of representatives in the quotient.
This module assembles completeness of the PRC reals from raw Cauchy data, quotient points, and diagonal or tail selection schedules that turn a Cauchy net of reals into one realizing Cauchy sequence.
proof idea
Strengthen the goal: for every intermediate bound $\ell\le r$ there is an $N$ that works for all rows $i$ with outer $\le i\le\ell$. The stated claim is the case $\ell=r$.
Induct on $\ell$. At zero: if outer $>0$ the row range is empty and $N=0$ works vacuously; if outer $\le 0$, apply the outer pairwise hypothesis between rows $0$ and $r$, then substitute $i=0$.
At successor: the inductive hypothesis yields $N_{\mathrm{prev}}$. If outer exceeds the successor, the new row is ineligible and $N_{\mathrm{prev}}$ still works. Otherwise call the outer hypothesis between the successor row and $r$ to get $N_{\mathrm{last}}$, and take $\max(N_{\mathrm{prev}},N_{\mathrm{last}})$. Split on whether $i\le\ell$ or $i$ equals the successor, routing each case to the matching witness. Arithmetic comparisons are discharged by omega and le_trans.
why it matters
Directly feeds the proved finite-representative-tail selection target in the same module. That target packages, for each tolerance rung, an outer Cauchy-representative threshold together with a raw depth realizing all finite representative-tail comparisons up to that rung; the downstream proof chooses the outer map from the Cauchy hypothesis on unit-fraction tolerances, then chooses the depth map by applying this existence result.
The selection target is the exact finite scheduler needed by the diagonal construction that builds one Cauchy sequence from a Cauchy net of PRC reals. Without a uniform finite-tail depth, $J$-cost Cauchy convergence of the selected representatives cannot be forced. The result is infrastructural foundation work for completeness of the PRC reals (and any later analytic use of those reals as a complete ordered field). It does not invoke forcing-chain landmarks T5--T8 directly; the link is through the real-number substrate of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.