PRCRealRawDiagonalLedgerTarget_proved
plain-language theorem explainer
Every representative-Cauchy family of PRC Cauchy sequences admits a raw rational ledger that is itself Cauchy and eventually close to each family member. Completeness workers cite this as the raw diagonal construction once quotient packaging is stripped away. The proof is a one-line wrapper: feed the proved tail-selection target into the tail-to-raw reduction.
Claim. For every sequence $U$ of PRC Cauchy sequences that is representative-Cauchy, there exists a raw rational ledger $s$ such that $s$ is Cauchy and, for every positive rational $\varepsilon$, there is $N$ so that for all $n \ge N$ the raw ledger of $U_n$ is eventually $\varepsilon$-close to $s$.
background
In the Primitive Recognition Calculus, reals are built from Cauchy sequences of rationals (ledgers). A PRC Cauchy sequence packages a raw rational ledger with a Cauchy witness; forgetting the witness yields the raw ledger via the raw projection. Completeness asks that Cauchy families of such sequences converge in the quotient.
The raw diagonal ledger target is the sharpened form of that demand: given a representative-Cauchy family $U$, produce an explicit raw rational ledger $s$ that is Cauchy and eventually close (in the raw sense) to each $(U_n).\mathrm{raw}$. The module isolates this as the mathematical core after quotient and packaging bookkeeping are removed.
Upstream, the tail-selection target supplies an explicit index function pick selecting terms along the family so the diagonal is Cauchy and limiting. The reduction theorem states that any such tail selection immediately yields a raw diagonal ledger by setting $s(n) = (U_n).\mathrm{term}(\mathrm{pick}, n)$.
proof idea
One-line term wrapper. Apply the reduction PRCRealRawDiagonalLedgerTarget_of_tail_selection to the already-proved PRCRealTailSelectionTarget_proved. The reduction unpacks the tail-selection witness (pick, hs_cauchy, hs_limit) and packages the diagonal ledger fun n => (U n).term (pick n) with those two properties, which is exactly the raw diagonal target.
why it matters
This closes the raw-diagonal blocker in the PRC real-completeness stack. Downstream, PRCRealDiagonalSelectionTarget_proved is the one-line packaging of this result into the quotient-level diagonal selection target ("a raw diagonal ledger packages immediately as the representative limit needed by the quotient-level diagonal selection target"). That selection target, together with raw Cauchy realization and quotient-point targets, assembles the sharpened completeness certificate prc_real_completeness_sharpened_certificate.
In the broader Recognition foundation, real completeness underwrites continuum structure used by later continuum bridges and geometric analysis. The declaration does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure ordered-field completeness infrastructure that those layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.