PRCRepresentativeFiniteTailBound_mono
plain-language theorem explainer
If a representative finite-tail bound holds from index N, it holds from every larger index M. Anyone assembling diagonal schedules for PRC real completeness cites this when relaxing a tail threshold. The proof is a one-line ≤-transitivity argument on the term index.
Claim. Let $U:\mathbb{N}\to\mathrm{PRCCauchySeq}$ and $\varepsilon$ a PRC rational. Fix outer threshold, target row $r$, and indices $N\le M$. If for every $i$ with $\mathrm{outer}\le i\le r$ and every $k\ge N$ the J-cost distance between $(U_i)_k$ and $(U_r)_k$ is strictly below $\varepsilon$, then the same holds with $N$ replaced by $M$.
background
Primitive Recognition Calculus builds reals from Cauchy sequences of PRC rationals. A PRC Cauchy sequence is an orbit-indexed rational ledger whose J-cost distance eventually drops below every positive PRC rational tolerance. J-cost distance is the recognition metric induced by the unique cost $J$ forced at T5.
The representative finite-tail bound says a raw index $N$ is deep enough that, once the outer representative threshold is crossed, every eligible row $i\le r$ stays within tolerance $\varepsilon$ of the target row $r$ at all later terms. It is a uniform tail-control predicate on a finite block of rows of a family $U$.
This module sits in the real-completeness layer of PRC: after integer and rational order, one constructs reals by Cauchy completion and needs finite diagonal schedules that pick cofinal tails row by row.
proof idea
Term-mode proof. Unfold the target bound (a universal quantifier over rows $i$ and term indices $k$). The hypotheses $\mathrm{outer}\le i$, $i\le r$, and $M\le k$ are given; compose $N\le M$ with $M\le k$ via $\mathrm{le_trans}$ to obtain $N\le k$, then apply the assumed bound at $N$. No arithmetic on rationals or J-cost identities is required.
why it matters
Feeds the proved finite diagonal schedule target in the same module (PRCRealFiniteDiagonalScheduleTarget_proved), which packages row-tail and representative-tail selection into a single schedule for a family of Cauchy sequences. Without monotonicity of the tail index, one could not freely enlarge a selected $N$ when synchronizing several rows under a common cofinal tolerance.
In the broader RS stack this is bookkeeping inside the PRC real-completeness path, not a forcing-chain landmark (T5–T8). It keeps the Cauchy-completion ledger coherent so later continuum and measure constructions rest on a fully constructive real type rather than a classical axiom of completeness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.