PRCRealTailSelectionTarget
plain-language theorem explainer
Any representative-Cauchy family of PRC Cauchy sequences admits an explicit index-picking map whose diagonal of chosen terms is itself a raw Cauchy ledger and is eventually close to each input row. Completeness arguments in the Primitive Recognition Calculus cite this as the constructive diagonal step before quotienting to reals. The declaration is a pure proposition interface; a companion theorem discharges it from a finite diagonal schedule.
Claim. For every family $U$ of PRC Cauchy sequences indexed by $\mathbb{N}$, if $U$ is representative-Cauchy, then there exists a selection map $\mathrm{pick}:\mathbb{N}\to\mathbb{N}$ such that the diagonal raw ledger $s(n)=U(n)_{\mathrm{pick}(n)}$ is raw-Cauchy, and for every positive PRC rational $\varepsilon$ there exists $N$ so that for all $n\ge N$ the raw sequence of $U(n)$ is eventually $\varepsilon$-close to $s$.
background
In the Primitive Recognition Calculus, continuum reals are obtained by completing Cauchy ledgers valued in PRC rationals (ratio-orbit quotient classes identified by cross-multiplication). A PRC Cauchy sequence packages a raw rational ledger with Cauchy control; a family $U$ is representative-Cauchy when the rows themselves form a Cauchy pattern at the representative level, which is the hypothesis needed before a diagonal limit can be formed.
The tail-selection target is the constructive form of the classical diagonal argument. Instead of an abstract limit ledger, one must exhibit, for each row $n$, a deep enough raw index so that the chosen terms assemble one raw Cauchy ledger that is eventually close to every input row under every positive rational tolerance. Upstream PRC rationals, raw-Cauchy predicates, and eventual-closeness supply the arithmetic language. The module sits in the real-completeness layer of the foundation stack, imported over the real-order congruence development.
proof idea
This declaration is a proposition definition, not a proved theorem. The body is a universal quantifier over families $U$ of Cauchy sequences, gated by the representative-Cauchy hypothesis, asserting existence of a pick map $\mathbb{N}\to\mathbb{N}$. The diagonal ledger is defined pointwise by reading the chosen term of row $n$. Two conjuncts are required: that diagonal is raw-Cauchy, and that for every positive PRC rational tolerance there is a tail beyond which each input row is eventually close to the diagonal.
The companion proved theorem discharges the target by invoking the finite diagonal schedule result, extracting its pick map, and refining the two conjuncts from the schedule's row and Cauchy controls. A one-line downstream wrapper then unpacks the same pick into the raw-diagonal-ledger target.
why it matters
This target is the constructive spine of the raw diagonal step in PRC real completeness. Downstream, the implication from tail selection to the raw diagonal ledger target is a direct unpacking of the pick map into a ledger witness. The sharpened completeness certificate (Step 10e) records the closed raw-ledger realization fact, the tail-selection diagonal, and representative-completeness for null-closed PRC reals.
Within Recognition Science, completing the PRC reals is display and verifier machinery for continuum-level statements built on the discrete foundation (eight-tick octave, phi-ladder, J-cost uniqueness). The doc-comment stresses that the construction uses actual terms of the input Cauchy ledgers, not an external choice principle. The target itself introduces no new physical primitive; it packages the diagonal obligation that the completeness certificate must close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.