PRCRealRawDiagonalLedgerTarget
plain-language theorem explainer
Every representative Cauchy sequence of PRC reals admits a single raw rational Cauchy ledger that is eventually close, at every positive rational tolerance, to the raw ledgers of the terms. Completeness arguments cite this as the residual analytic content once quotient packaging is stripped away. The declaration is a pure Prop definition; existence is discharged later by tail selection.
Claim. For every sequence $U$ of Cauchy sequences of rationals that is a representative Cauchy sequence of PRC reals, there exists a raw rational ledger $s$ that is itself Cauchy, and such that for every positive rational $\varepsilon$ there is an index $N$ with the property that for all $n \ge N$ the raw ledger of $U_n$ is eventually $\varepsilon$-close to $s$.
background
In the Primitive Recognition Calculus, rationals (PRCRat) are ratio-orbit quotient classes, and reals are built from Cauchy sequences of those rationals. A raw rational ledger is the underlying sequence data before quotient packaging; PRCRawCauchy is the Cauchy predicate at that raw level, and PRCRawEventuallyClose compares two raw ledgers within a positive rational tolerance.
The module develops completeness of the PRC reals. After representative Cauchy sequences and quotient bookkeeping are set up, the remaining analytic obligation is a diagonal construction: extract one raw Cauchy ledger that tracks the raw parts of the input sequence of Cauchy sequences. The doc-comment frames this Prop as the "sharper diagonal blocker": construct that ledger and prove both its Cauchy property and its limit property.
Upstream, the rational field and Cauchy-sequence layers supply the types and predicates quantified here; the RS-native unit gauge and cost functional equation sit further back in the foundation stack and are not used directly in this statement.
proof idea
No proof: this is a def equating a name to a quantified Prop. The body is the universal-existential statement itself (representative Cauchy input sequence $U$, existence of raw ledger $s$, Cauchy of $s$, and the eventual-closeness limit clause in every positive rational $\varepsilon$).
Discharge happens elsewhere. PRCRealRawDiagonalLedgerTarget_of_tail_selection builds a witness by reading off actual terms via an explicit tail-selection map. PRCRealRawDiagonalLedgerTarget_proved is the one-line composition of that implication with the proved tail-selection target.
why it matters
This Prop is the raw-level diagonal obligation inside PRC real completeness. Downstream, PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger packages a raw diagonal ledger into the representative limit demanded by the quotient-level diagonal selection target. PRCRealRawDiagonalLedgerTarget_of_tail_selection and PRCRealRawDiagonalLedgerTarget_proved close the existence claim from an explicit tail pick.
The sharpened completeness certificate (PRCRealCompletenessSharpenedCertificate) records the implication from this raw diagonal target to diagonal selection as one of its fields, alongside raw Cauchy realization and null-closed representative completeness. In the Recognition foundation stack this is bookkeeping for the real completion of the primitive calculus, not a forcing-chain landmark (T5–T8), but it is required infrastructure before continuum-level statements can sit on PRC reals rather than on classical ℝ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.