PRCRepresentativeFiniteTailBound
plain-language theorem explainer
Defines the finite representative-tail predicate: a raw depth N forces every eligible row i (outer ≤ i ≤ r) to sit within J-cost distance eps of the target row r at all later indices. Completeness and diagonal-schedule arguments cite it as the local comparison obligation. The body is a pure universal Prop over row and depth indices; no proof work lives here.
Claim. Fix a family $U:\mathbb{N}\to\mathrm{CauchySeq}$ of PRC Cauchy sequences, a positive rational tolerance $\varepsilon$, and naturals $\mathrm{outer}$, $r$, $N$. The predicate holds when for every row $i$ with $\mathrm{outer}\le i\le r$ and every depth $k\ge N$, the $J$-cost distance between the $k$-th terms of $U_i$ and $U_r$ is strictly less than $\varepsilon$.
background
Primitive Recognition Calculus builds reals from Cauchy sequences valued in PRC rationals (quotient classes of ratio orbits). Distance is measured by the $J$-cost metric on those rationals: $\mathrm{PRCJCostDistance}$ is the native gap used in place of absolute value. Strict order on PRC rationals is the positive-gap predicate: $a<b$ means $b-a$ has a positive ratio-orbit representative.
The ambient module develops completeness of this PRC real line. A family $U$ of Cauchy sequences is treated as a sequence of candidate representatives; an outer threshold marks when those representatives have already become mutually close at tolerance $\varepsilon$. The present predicate packages the remaining finite-row obligation: once past that outer threshold, a single raw depth $N$ must make every eligible row $i\le r$ stay $\varepsilon$-close to the target row $r$ at all later terms.
Upstream scaffolding supplies the Cauchy sequence type, the $J$-cost distance, and the PRC rational order. Downstream existence and monotonicity lemmas turn this Prop into a usable scheduler atom.
proof idea
Definition only: the body is the universal statement $\forall i,k,;\mathrm{outer}\le i\le r\land N\le k\implies d_J((U_i)_k,(U_r)_k)<\varepsilon$ with $d_J$ the PRC $J$-cost distance and $<$ the PRC rational order. No tactics or lemmas are invoked; later theorems prove existence of such an $N$ from mutual eventual closeness of the raw sequences past $\mathrm{outer}$, and prove that larger depths inherit the bound.
why it matters
This is the atomic comparison obligation inside the finite representative-tail scheduler. Existence (PRCRepresentativeFiniteTailBound_exists) and monotonicity (PRCRepresentativeFiniteTailBound_mono) discharge and enlarge the bound; both feed PRCRealFiniteRepresentativeTailSelectionTarget and the combined finite diagonal scheduler PRCRealFiniteDiagonalScheduleTarget.
Those targets are the finite-rung stepping stones toward a completed global tail-selection theorem for PRC reals. In the Recognition framework they sit in the foundation layer that reconstructs analysis from recognition primitives (Cauchy data, $J$-cost geometry, phi-native units), rather than importing classical completeness. The definition itself closes no open question; it names the finite comparison that the diagonal proof must schedule at each tolerance rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.