PRCRowTailBound
plain-language theorem explainer
A candidate index N is deep enough for one Cauchy sequence at one rational tolerance when every pair of terms beyond N has J-cost distance strictly below that tolerance. Completeness and diagonal-selection arguments cite this predicate as the local row-tail constraint. The body is a direct unpacking of the Cauchy condition at fixed sequence, epsilon, and N.
Claim. For a PRC Cauchy sequence $u$, a rational tolerance $\varepsilon$, and $N \in \mathbb{N}$, the row-tail bound holds when $\forall m,n \geq N$, the J-cost distance between $u_m$ and $u_n$ is strictly less than $\varepsilon$.
background
In the Primitive Recognition Calculus, reals are built from Cauchy ledgers of PRC rationals. A PRC Cauchy sequence is an orbit-indexed map $\mathrm{Nat} \to \mathrm{PRCRat}$ whose J-cost distance eventually falls below every positive rational tolerance. The J-cost distance sends additive separation through the positive ratio $1+(a-b)^2$ and then applies the rational J-cost; strict order on rationals is positivity of the difference.
This module develops completeness of that Cauchy surface: diagonal and finite-row schedulers that pick indices deep enough for many sequences at once. The present definition freezes one sequence, one tolerance, and one candidate index, and records the pairwise tail condition that the Cauchy axiom already promises exists for each positive $\varepsilon$.
Upstream, the structure field cauchy on PRC Cauchy sequences is exactly the quantified form of this predicate: for every positive $\varepsilon$ there exists some $N$ such that the row-tail bound holds.
proof idea
Definitional, not a proved theorem. The body is the universal quantification over pairs of indices past $N$ of the strict J-cost inequality that appears inside the Cauchy axiom of a PRC Cauchy sequence. No lemmas are applied; it names that local tail condition so later existence and monotonicity results can quantify over it.
why it matters
Finite-row and diagonal completeness targets are stated in terms of this predicate. The existence theorem that, for any family of Cauchy sequences and any positive tolerance, every finite initial segment of rows admits a common deep enough index, uses it as the conclusion. The finite-row selection target asks for a pick function such that each diagonal rung $r$ satisfies the bound for all rows $i \leq r$ at unit-fraction tolerance $1/(r+1)$. The finite diagonal scheduler combines row-tail and representative-tail constraints at each tolerance rung; this is still finite-rung scheduling, not yet the completed global tail-selection theorem.
Monotonicity in the index (larger $N$ still works) is the immediate companion lemma. In the Recognition foundation stack this is bookkeeping for real completeness from the J-cost Cauchy surface, not a forcing-chain landmark (T5–T8) by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.