PRCRealDiagonalSelectionTarget_of_raw_diagonal_ledger
plain-language theorem explainer
If the raw diagonal ledger target holds, the packaged diagonal selection target follows at once. Anyone proving internal completeness of the PRC reals cites this to discharge the quotient-level diagonal blocker from the sharper raw construction. The proof is a five-line packaging step: extract the raw Cauchy ledger, wrap it as a PRCCauchySeq, and rewrite the limit predicate.
Claim. Assume that for every sequence $U$ of PRC Cauchy ledgers that is representative-Cauchy, there exists a raw rational ledger $s$ that is Cauchy and eventually close (in the raw sense) to $(U_n)^{\mathrm{raw}}$ for every positive PRC-rational tolerance. Then for every such $U$ there exists a PRC Cauchy ledger $L$ that is a representative limit of $U$.
background
In the Primitive Recognition Calculus, a PRC Cauchy sequence is an orbit-indexed rational ledger whose J-cost distance eventually falls below every positive PRC-rational tolerance. Completeness of the PRC reals is organized as a stack of named blockers rather than a single classical completeness axiom.
The diagonal selection target asks: given a representative-Cauchy sequence $U$ of such Cauchy ledgers, produce an actual Cauchy ledger $L$ that is a representative limit of $U$. A representative limit means that for every positive tolerance $\varepsilon$, the raw ledger of $U_n$ is eventually close to the raw ledger of $L$.
The raw diagonal ledger target is the sharper sibling: it demands an explicit raw rational ledger $s$ that is itself Cauchy and satisfies the same eventual-closeness condition against $(U_n)^{\mathrm{raw}}$. As its doc-comment states, this is "the mathematical work left after the quotient and packaging bookkeeping is removed." The present theorem is exactly that packaging bridge.
proof idea
Term-style packaging, not a construction of the diagonal. Introduce the sequence $U$ and the representative-Cauchy hypothesis. Apply the raw-target hypothesis to obtain a raw ledger $s$ together with its Cauchy certificate and its limit certificate. Package $s$ into a PRCCauchySeq by setting term := s and reusing the Cauchy proof. The remaining goal is the representative-limit predicate; a simpa against the definitions of representative limit and of the raw projection of a Cauchy sequence discharges it from the raw limit certificate.
why it matters
This is the bookkeeping hinge between the hard analytic diagonal work and the named completeness certificate. Downstream, PRCRealDiagonalSelectionTarget_proved is the one-line application of this theorem to the proved raw target, and prc_real_completeness_sharpened_certificate records the implication as the field diagonal_selection_from_raw_diagonal.
In the Recognition foundation stack, internal completeness of the PRC ordered field is a prerequisite for treating continuum limits (mass ladder, continuum fields, operator spectra) without smuggling classical reals. The theorem does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only closes the packaging gap so those later steps can quote a complete PRC continuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.