PRCRealFiniteRowTailBound_exists
plain-language theorem explainer
For any countable family of PRC Cauchy sequences and any fixed positive rational tolerance, every finite initial segment of rows admits a single common tail index deep enough for all of them. Completeness and diagonal-selection arguments cite this as the finite-row scheduler. The proof is induction on the row bound, taking maxima of the individual Cauchy moduli and using monotonicity of the tail-bound predicate.
Claim. Let $U$ be a sequence of PRC Cauchy sequences and let $\varepsilon$ be a positive PRC rational. Then for every natural number $r$ there exists $N\in\mathbb{N}$ such that for all $i\le r$, the pair of terms of $U_i$ beyond $N$ has $J$-cost distance strictly less than $\varepsilon$ (i.e., $N$ is a common row-tail bound for the finite initial segment of rows $0,\ldots,r$).
background
This module builds PRC reals by completing PRC rationals along Cauchy ledgers. A PRC Cauchy sequence is a sequence of PRC rationals whose $J$-cost pairwise distances become arbitrarily small in the tail. The predicate PRCRowTailBound packages one modulus step: index $N$ is deep enough for ledger $u$ at tolerance $\varepsilon$ when every pair of terms past $N$ has $J$-cost distance strictly below $\varepsilon$.
PRC rationals are ratio-orbit quotient classes (nonzero-denominator cross-multiplication identification). Positivity is the PRC-native signed-numerator condition on the orbit display. The ambient setting is the Primitive Recognition Calculus real-completeness layer, which imports the real-order congruence development and works entirely with these native types rather than classical $\mathbb{R}$.
The theorem is the finite-uniformization step before diagonal selection: one fixed $\varepsilon$ and one finite window of rows, not yet a cofinal schedule over all rows and shrinking tolerances.
proof idea
Induction on the finite row bound $r$.
Base $r=0$: apply the Cauchy modulus of $U_0$ at $\varepsilon$ to obtain $N$, then the only index $i\le 0$ is $i=0$, so the bound holds.
Successor: invoke the inductive hypothesis for $r$ to get $N_{\mathrm{prev}}$ working for rows $0,\ldots,r$, and the Cauchy modulus of $U_{r+1}$ to get $N_{\mathrm{last}}$. Take $N=\max(N_{\mathrm{prev}},N_{\mathrm{last}})$. For $i\le r$, monotonicity of the tail-bound predicate under larger indices (from $N_{\mathrm{prev}}\le N$) reuses the inductive bounds; for $i=r+1$, the same monotonicity lifts $N_{\mathrm{last}}$. Case split on $i\le r$ versus the last row closes the successor step.
why it matters
Diagonal completeness arguments need one raw index that simultaneously controls every row already opened. This lemma is exactly that finite-row scheduler at fixed tolerance. Downstream, PRCRealFiniteRowTailSelectionTarget_proved chooses, for each diagonal row $r$, a common bound for rows $0,\ldots,r$ at unit-fraction tolerance $1/(r+1)$, by specializing this existence result and packaging the choice function.
In the Recognition stack this sits inside the foundation path that constructs the continuum from recognition ledgers before analysis and physics constants are interpreted. It does not itself invoke the forcing chain (T5 $J$-uniqueness, T6 $\phi$, T7 eight-tick, T8 $D=3$), but it is infrastructure those later layers rely on once reals exist as Cauchy quotients. Closing finite-row control is a standard completeness bottleneck; here it is discharged with no sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.