PRCRealFiniteRowTailSelectionTarget
plain-language theorem explainer
For any countable family of PRC Cauchy sequences, a single pick map sends each diagonal row r to an index deep enough that every earlier row i ≤ r is already Cauchy below the unit-fraction tolerance 1/(r+1). Completeness and diagonal-selection arguments cite this as the finite-row scheduler. The declaration is the Prop target itself; the companion theorem discharges it by choosing per-row witnesses.
Claim. For every family $U:\mathbb{N}\to\mathrm{PRCCauchySeq}$ there exists a selection $p:\mathbb{N}\to\mathbb{N}$ such that for all rows $r$ and all $i\le r$, the index $p(r)$ is a tail bound for $U(i)$ at tolerance $1/(r+1)$: whenever $m,n\ge p(r)$, the $J$-cost distance between the $m$-th and $n$-th terms of $U(i)$ is strictly less than $1/(r+1)$.
background
Primitive Recognition Calculus builds reals from rational ledgers whose pairwise $J$-cost distances form Cauchy data. A PRCCauchySeq is an orbit-indexed sequence of PRC rationals such that for every positive PRC rational $\varepsilon$ there is an $N$ beyond which all pairs of terms have $J$-cost distance $<\varepsilon$.
PRCRowTailBound u $\varepsilon$ $N$ asserts that a single candidate index $N$ is already deep enough for one fixed Cauchy ledger $u$ at one fixed tolerance $\varepsilon$. The unit-fraction schedule PRCUnitFraction r supplies the concrete tolerances $1/(r+1)$ used as verifier display machinery in the completeness argument; it is not a new PRC primitive.
The local module develops the completeness side of the PRC ordered field. Finite-row tail selection is the scheduler that, given a whole diagonal of raw Cauchy ledgers, produces one index per row that simultaneously controls all earlier rows at that row's unit-fraction tolerance.
proof idea
This declaration is a bare Prop abbreviation: it packages the universal quantifier over families $U$, the existential pick map, and the finite-row bound condition. There is no proof body beyond the defining formula.
The companion theorem PRCRealFiniteRowTailSelectionTarget_proved discharges it in one choose step: for each row $r$ it invokes the existence lemma that a finite initial segment of Cauchy sequences admits a common tail bound at the positive tolerance $1/(r+1)$, then assembles those witnesses into the pick function.
why it matters
Diagonal completeness for PRC reals needs a uniform way to advance every earlier row when the diagonal index moves. This target is exactly that finite-row scheduler. Downstream, PRCRealFiniteRowTailSelectionTarget_proved closes the Prop, and PRCRealCompletenessSharpenedCertificate (Step 10e) records the closed raw-ledger realization, the tail-selection diagonal, and representative completeness for PRCRealNullClosed, with a field that routes raw-diagonal data through tail selection into diagonal selection.
In the broader Recognition stack this sits inside the foundation layer that reconstructs a complete ordered field from $J$-cost Cauchy data, upstream of continuum-level physics. It does not itself invoke the forcing chain T0–T8, but it is part of the analytic substrate those landmarks presuppose once reals are in play.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.