PRCRawCauchyRealizationTarget
plain-language theorem explainer
Every raw orbit-indexed rational ledger that is Cauchy in J-cost distance can be packaged as a full PRC Cauchy sequence whose underlying terms recover that ledger. Completeness and certificate authors cite this packaging target when closing the raw-to-structured passage. The declaration is the Prop itself: a universal quantification standing as a named realization goal.
Claim. For every raw completed-orbit rational ledger $s:\mathbb{N}\to\mathrm{PRCRat}$, if $s$ is Cauchy under $J$-cost distance (for every positive PRC rational tolerance $\varepsilon$ there is $N$ such that $m,n\ge N$ implies the $J$-cost distance of $s(m)$ and $s(n)$ is $<\varepsilon$), then there exists a PRC Cauchy sequence $u$ with underlying raw ledger equal to $s$.
background
In the Primitive Recognition Calculus real layer, a raw completed-orbit rational ledger is simply a map $\mathbb{N}\to\mathrm{PRCRat}$: the sequence of terms before any Cauchy witness is attached. The raw Cauchy predicate asserts that $J$-cost distances between late terms fall below every positive PRC rational tolerance, matching the Cauchy field of the structured sequence type.
A PRC Cauchy sequence packages that data: a term map together with a proof that the $J$-cost distance eventually drops below every positive tolerance. The forgetful map raw projects a structured sequence back to its term ledger. The local module builds completeness infrastructure for the PRC reals from these raw and structured ledgers.
Upstream, the structured Cauchy type is defined so that its Cauchy field uses the same $J$-cost distance predicate as the raw Cauchy predicate, making packaging a pure data-and-witness assembly step rather than a new analytic claim.
proof idea
No proof body: this is a bare Prop definition. It names the universal statement that every raw Cauchy ledger $s$ admits some structured Cauchy sequence $u$ with $u$'s underlying terms equal to $s$. The companion theorem discharges it by packaging $s$ with its raw Cauchy hypothesis as the structured Cauchy field and discharging equality of raw projections by reflexivity.
why it matters
This target is the first closed fact recorded on the Step 10e sharpened completeness certificate: that certificate requires the raw-ledger realization fact, the quotient-point target, and the diagonal/tail-selection chain for representative completeness of the null-closed PRC reals. The immediate parent theorem proves the Prop by the packaging construction above.
In the Recognition foundation stack, completeness of the PRC ordered field is the analytic substrate on which later forcing and measurement constructions sit. Naming the raw-to-structured realization as an explicit Prop keeps the certificate modular: later steps can assume packaging without reopening the Cauchy predicate match. It does not itself invoke T5–T8 or the Recognition Composition Law; it is pure real-construction scaffolding inside the PRC calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.