PRCRealDiagonalSelectionTarget
plain-language theorem explainer
Named completeness obligation: every representative-Cauchy sequence of PRC Cauchy ledgers admits a Cauchy ledger that is its representative limit. Completeness and certificate authors cite it as the quotient-level diagonal selection blocker. It is a pure Prop definition (no proof body); discharge goes through the raw-diagonal packaging theorems.
Claim. For every sequence $(U_n)_{n\in\mathbb{N}}$ of PRC Cauchy ledgers that is Cauchy as a sequence of null-quotient representatives, there exists a PRC Cauchy ledger $L$ that is a representative limit of $(U_n)$.
background
In the Primitive Recognition Calculus, a PRC Cauchy sequence is an orbit-indexed rational ledger whose pairwise J-cost distances eventually fall below every positive PRC rational tolerance. The real-number layer works with null-quotient representatives of such ledgers rather than classical Dedekind or Cauchy reals.
A sequence $U$ of Cauchy ledgers is representative-Cauchy when, for every positive PRC tolerance, the raw tails of $U_m$ and $U_n$ are eventually close once $m,n$ are large enough. A ledger $L$ is a representative limit of $U$ when the same eventual-closeness relation holds between $L$ and the terms of $U$.
This module packages internal completeness of the PRC reals as a chain of named Prop targets. The present definition is the diagonal-selection blocker at the representative (quotient) level: it asks only for existence of a Cauchy ledger limit, not yet for a raw rational diagonal construction.
proof idea
Definitional Prop with no proof obligations. The body is the universal-existential statement above: quantify over sequences of Cauchy ledgers, assume representative-Cauchy, demand a Cauchy ledger that is a representative limit. Discharge is external, via packaging theorems that build the limit from a raw diagonal ledger.
why it matters
This is the sharpened completeness target at the representative level. Downstream, PRCRealCompletenessTarget_of_diagonal_selection identifies it with the main completeness target (one-line identity). The packaging theorem from a raw diagonal ledger turns a constructed rational diagonal into this Prop, and PRCRealDiagonalSelectionTarget_proved closes it once the raw diagonal is available.
It sits inside the Step 10e sharpened certificate, which records raw-Cauchy realization, quotient-point facts, and the implication from raw diagonal ledger to this diagonal selection target. In the Recognition foundation stack it is bookkeeping that isolates the real mathematical work (building the diagonal ledger) from quotient packaging, so completeness of the PRC ordered field can be cited cleanly by later forcing and continuum constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.