PRCRealDiagonalSelectionTarget_proved
plain-language theorem explainer
Every representative-Cauchy sequence of Cauchy ledgers admits a Cauchy ledger that is its representative limit. Completeness arguments in the Primitive Recognition Calculus cite this as the diagonal-selection step that closes the quotient-level completeness target. The proof is a one-line packaging of the already-proved raw diagonal ledger construction.
Claim. For every sequence $U$ of Cauchy ledgers that is representative-Cauchy, there exists a Cauchy ledger $L$ which is a representative limit of $U$.
background
In the Primitive Recognition Calculus, reals are built from Cauchy ledgers (Cauchy sequences of rationals with ledger structure) and then quotiented. Internal completeness asks that every Cauchy sequence of such reals again has a limit inside the same construction.
The diagonal selection target is the named blocker for that step: given a sequence $U$ of Cauchy ledgers that is representative-Cauchy, produce an actual Cauchy ledger $L$ realizing the representative limit. A sharper sibling target constructs the raw rational ledger underneath $L$ and proves both its Cauchy and limit properties; packaging that raw object yields the quotient-level statement.
Upstream, the raw diagonal ledger target is already proved (via tail selection), and a packaging lemma states that any such raw ledger "packages immediately as the representative limit needed by the quotient-level diagonal selection target."
proof idea
One-line term wrapper. Apply the packaging lemma that turns a raw diagonal ledger into a representative limit, feeding it the already-proved raw diagonal ledger target. No new analytic work occurs here: the raw construction and the packaging bookkeeping are both upstream.
why it matters
This discharges the diagonal-selection half of internal real completeness in PRC. Downstream, the full completeness target is obtained by feeding this result into the diagonal-to-completeness packaging lemma, and the sharpened completeness certificate records the same packaging arrow as its diagonal field.
In the Recognition foundation stack, internal completeness of the real ledger is prerequisite infrastructure before continuum limits, constants, and geometric forcing (T5–T8) can sit on a closed real base. The declaration itself is bookkeeping closure rather than a new forcing step: it converts the raw diagonal construction into the named Prop that the completeness certificate and the top-level completeness theorem both demand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.