PRCRealTailSelectionTarget_proved

This module builds real completeness inside Primitive Recognition Calculus: reals arise as Cauchy ledgers of rationals under a J-cost distance, not as a Dedekind cut package. A raw rational ledger is a sequence of rationals; a Cauchy sequence packages such a ledger with a modulus. The J-cost distance measures separation of terms via the Recognition cost $J$, so Cauchy and closeness statements are cost-metric rather than absolute-value statements.

The target is the tail-selection form of the raw diagonal theorem: given a family $U$ of Cauchy sequences that is representative-Cauchy (pairwise raw ledgers become arbitrarily close in the J-cost sense), one must choose, for each index $n$, a deep enough term of $U(n)$ so the diagonal of those chosen terms is itself raw-Cauchy and tracks every late $U(n)$.

Upstream ingredients include a finite diagonal schedule (rowwise Cauchy control plus a pick map), the three-leg modulus for J-cost distance (a triangle-type bound on four points), and the fact that unit fractions $1/(m+1)$ eventually fall below any positive rational tolerance.

Tactic proof. From the finite diagonal schedule on $U$, obtain a pick map and rowwise closeness. The two goals are: the diagonal $s(n)=U(n)_{\mathrm{pick}(n)}$ is raw-Cauchy, and each late $U(n)$ is eventually close to $s$.

For the Cauchy goal, fix positive $\varepsilon$. The three-leg modulus supplies a positive $\delta$ controlling a three-edge J-cost path. Representative-Cauchy of $U$ and eventual smallness of unit fractions give thresholds $N_{\mathrm{rep}},N_{\tau}$. For $m,n$ past $\max(N_{\mathrm{rep}},N_{\tau})$, take a common deep index $K\ge\max(\mathrm{pick}(m),\mathrm{pick}(n),N_{\mathrm{pair}})$. Bound the three legs $U(m)_{\mathrm{pick}(m)}\to U(m)_K\to U(n)K\to U(n){\mathrm{pick}(n)}$ each by $\delta$ (row schedule plus unit-fraction vs $\delta$, and the pairwise representative modulus), then apply the three-leg lemma.

The eventually-close goal is the same pattern with one free index $n$ and a late comparison index $l$, again routing through a deep $K$ and the three-leg modulus.

Tail selection is the constructive heart of the raw diagonal: the diagonal ledger is assembled from genuine terms of the input Cauchy ledgers, not from abstract equivalence-class data. Downstream, PRCRealRawDiagonalLedgerTarget_proved is exactly the packaging PRCRealRawDiagonalLedgerTarget_of_tail_selection applied to this theorem; that raw diagonal then feeds representative-limit constructions.

It also sits under prc_real_completeness_sharpened_certificate, which bundles raw Cauchy realization, quotient-point existence, and diagonal selection into the sharpened real-completeness certificate for PRC. In the Recognition foundation this is the step that turns a Cauchy net of rationals into a single raw Cauchy ledger usable as a real, before quotienting by eventual closeness.

Relative to the forcing chain, this is infrastructure rather than a T5–T8 landmark: it makes the real line available so later cost, mass, and continuum arguments can quantify over completed scalars. No open scaffold remains here; the claim is fully proved.