PRCRealFiniteRowTailSelectionTarget_proved
plain-language theorem explainer
For any countable family of PRC Cauchy sequences, a single pick map sends each diagonal row r to a raw index deep enough that every earlier row i ≤ r meets the tail bound at tolerance 1/(r+1). Diagonal-schedule and sharpened real-completeness certificates cite it. The proof is classical choice on the per-row existence lemma with unit-fraction tolerances.
Claim. For every family $U:\mathbb{N}\to\mathrm{PRCCauchySeq}$ there exists $\mathrm{pick}:\mathbb{N}\to\mathbb{N}$ such that whenever $i\le r$, the $i$-th sequence satisfies the row-tail bound at tolerance $1/(r+1)$ from index $\mathrm{pick}(r)$ onward.
background
This module builds a sharpened completeness certificate for the Primitive Recognition Calculus (PRC) model of the reals: Cauchy sequences of rationals, quotiented by a null-tail relation, with explicit diagonal schedulers that keep all constructions finitary and choice-explicit.
A unit fraction here is the positive rational tolerance $1/(r+1)$ attached to diagonal row $r$. The row-tail bound asserts that from a raw index $N$ onward, consecutive terms of a fixed Cauchy sequence stay within a given positive rational $\varepsilon$. The sibling existence theorem states that, for fixed $U$, $\varepsilon>0$, and row $r$, a single $N$ works simultaneously for every row $i\le r$.
The target proposition packages that existence into one pick function of $r$ alone, which is exactly the finite-row scheduler the diagonal tail-selection argument needs.
proof idea
Term-mode proof by choice. Introduce the family $U$. For each row $r$, instantiate the upstream existence lemma at tolerance equal to the $r$-th unit fraction (using positivity of that fraction) to obtain some raw index that works for all $i\le r$. The choose tactic turns that $r$-indexed family of existence proofs into a single function pick together with the universal bound. Package the pair as the required witness.
why it matters
This is the exact finite-row scheduler named in the target's doc-comment: one raw index per diagonal row $r$ deep enough for all eligible representative rows $i\le r$ at tolerance $1/(r+1)$. Downstream, the finite diagonal schedule proof cases on this result first, then pairs it with a representative-tail selector. That schedule in turn feeds the sharpened PRC real-completeness certificate, which assembles raw Cauchy realization, quotient points, and diagonal selection into one certificate object.
In the broader Recognition foundation this is bookkeeping for constructing $\mathbb{R}$ inside PRC without hidden analytic completeness axioms: every $\varepsilon$-$N$ choice is named and finite-row. It does not itself touch the forcing chain (T5–T8) or the mass ladder; it sits under the analytic substrate those later layers assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.