PRCRealRawDiagonalLedgerTarget_of_tail_selection
plain-language theorem explainer
An explicit tail-selection hypothesis yields the raw diagonal ledger target: from a Cauchy sequence of representatives one obtains a single raw rational ledger that is Cauchy and eventually close to each input. Completeness auditors cite this when reducing the diagonal construction to a pick-function. The proof is a short unpacking that builds the ledger from the selected terms and reuses the Cauchy and limit witnesses.
Claim. Assume that for every sequence $U$ of Cauchy representatives there is a pick map $n \mapsto k_n$ such that the diagonal ledger $s(n) = (U_n)_{k_n}$ is a raw rational Cauchy ledger and is eventually close to each $(U_n)^{\mathrm{raw}}$ at every positive rational tolerance. Then for every such $U$ there exists some raw rational ledger $s$ that is Cauchy and eventually close to each input representative (the pick map need not appear in the conclusion).
background
This module develops real completeness inside the Primitive Recognition Calculus: reals are packaged from Cauchy sequences of rational ledgers, and completeness is reduced to constructing a diagonal limit ledger under the raw (pre-quotient) data.
The raw diagonal ledger target asks, for any sequence $U$ of Cauchy representatives that is itself Cauchy in the representative sense, for a single raw rational ledger $s$ that is Cauchy and, at every positive rational $\varepsilon$, eventually $\varepsilon$-close to each input raw ledger $(U_n)^{\mathrm{raw}}$. The tail-selection target is the same statement with an explicit pick $n \mapsto k_n$ so that $s(n)$ is literally a term of $U_n$, not an abstract existence.
The local setting is the sharpened completeness certificate path: after quotient and packaging bookkeeping are stripped, the remaining mathematical work is this raw diagonal construction.
proof idea
Term-mode unpacking of the hypothesis. Fix a sequence $U$ of Cauchy representatives. Apply the tail-selection hypothesis to obtain a pick map together with Cauchy and limit witnesses for the diagonal $s(n) = (U_n).\mathrm{term}(\mathrm{pick}, n)$. Package that same $s$ with those witnesses as the existential data required by the raw diagonal ledger target. No new Cauchy or closeness argument is proved here.
why it matters
This is the reduction step from the constructive pick-function form of the diagonal to the existential raw-ledger form used by the completeness certificate. Downstream, PRCRealRawDiagonalLedgerTarget_proved discharges the raw diagonal target by feeding in the already-proved tail-selection theorem, and the sharpened completeness certificate packages that proved target with the raw Cauchy realization and quotient-point targets. In the Recognition foundation stack this closes the raw half of real completeness before order-congruence and quotient packaging; it is pure analysis bookkeeping, not a forcing-chain (T0–T8) step, but it is required for a complete real line on which later RS constructions sit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.