PRCRowTailBound_mono
plain-language theorem explainer
If index N is deep enough that a PRC Cauchy ledger stays within tolerance eps on its N-tail, then every larger index M is also deep enough. Anyone building finite diagonal schedules or uniform row-tail selections for PRC reals will cite this. The proof is a two-line tail inclusion via Nat.le_trans.
Claim. Let $u$ be a PRC Cauchy sequence and $\varepsilon$ a PRC rational. If $N \le M$ and the $J$-cost distance between any two terms of $u$ with indices at least $N$ is strictly less than $\varepsilon$, then the same holds for all pairs of indices at least $M$.
background
In the Primitive Recognition Calculus, reals are assembled from Cauchy ledgers of PRC rationals. A PRCCauchySeq is an orbit-indexed map Nat → PRCRat whose $J$-cost pairwise distances eventually fall below every positive rational tolerance. The predicate PRCRowTailBound u eps N packages one such witness: every pair of terms with indices $\ge N$ has $J$-cost distance strictly below eps.
PRC rationals themselves are quotient classes of ratio orbits (nonzero-denominator cross-multiplication). The $J$-cost distance is the recognition metric used throughout the forcing chain; here it only needs to be a strict order relation on rationals so that tail bounds are well-formed propositions.
The local module develops completeness of this construction: finite families of Cauchy rows, diagonal selection, and cofinal tolerance schedules. Monotonicity of the row-tail predicate is the elementary order fact those finite-selection arguments rely on.
proof idea
Unfold the target bound and take arbitrary indices $m,n \ge M$. From $N \le M$ and $M \le m$ (resp. $n$), two applications of le_trans give $N \le m$ and $N \le n$. Feed those into the hypothesis bound at $N$ to obtain the required strict $J$-cost inequality. No Cauchy property of $u$ is used; only the universal quantifiers in the bound and Nat-order transitivity.
why it matters
This lemma is the monotone-tail step inside PRCRealFiniteRowTailBound_exists, which produces a single index deep enough for the first $r+1$ rows of a finite family of Cauchy sequences at a fixed positive tolerance. That existence result is then consumed by PRCRealFiniteDiagonalScheduleTarget_proved, the finite diagonal schedule that underwrites completeness of the PRC real construction.
In the broader Recognition stack this sits in the arithmetic foundation beneath the forcing chain (T0–T8): before $J$-uniqueness, $\varphi$, the eight-tick octave, or $D=3$ can be stated over completed scalars, the real ledger must be closed under Cauchy limits. The mono fact is small but load-bearing for every finite uniform-tail argument in that closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.