raw
plain-language theorem explainer
Projects a PRC Cauchy sequence to its underlying Nat-indexed rational ledger, discarding the J-cost Cauchy certificate. Completion, ledger algebra, and constant-derivation code cite this forgetful map whenever only the raw orbit terms are needed. The body is the structure-field projection onto `term`.
Claim. Given a completed-orbit Cauchy ledger $u$ (a map $\mathbb{N}\to\mathrm{PRCRat}$ together with a certificate that J-cost distances eventually fall below every positive PRC-rational tolerance), return the underlying raw ledger $\mathbb{N}\to\mathrm{PRCRat}$ by forgetting the certificate.
background
In the Primitive Recognition Calculus, real numbers are built from completed-orbit rational ledgers. A raw ledger is simply a sequence $\mathbb{N}\to\mathrm{PRCRat}$. A PRC Cauchy sequence packages such a ledger with a certificate: for every positive PRC-rational $\varepsilon$ there exists $N$ so that for all $m,n\ge N$, the J-cost distance between the $m$-th and $n$-th terms is strictly less than $\varepsilon$.
The J-cost distance is the same defect metric used throughout the forcing chain (the cost $J$ forced at T5). This module sits in the real-completion layer: it separates the raw sequence data from the Cauchy proof so that algebraic operations can be defined on bare ledgers before re-attaching certificates.
Upstream, PRCCauchySeq supplies the bundled structure; PRCRawRatLedger is the bare type alias $\mathrm{Nat}\to\mathrm{PRCRat}$.
proof idea
One-line definitional projection: return the term field of the Cauchy-sequence structure. No tactic proof, no lemmas applied; the type of term is already PRCRawRatLedger.
why it matters
This forgetful map is the bridge between certified Cauchy ledgers and the raw ledger algebra used across the monolith. Downstream CostAlgebra results on the unnormalized RCL star operation (commutativity, associator defect $2(a-c)$, flexibility) and the global failure of a quasi-triangle inequality for defect distance work with raw real data obtained after projection. Constants modules (coherence, frequency, and $\hbar$ quanta in RS-native units; cube edge counts in the $\Lambda_{\mathrm{rec}}$ derivation) likewise consume raw numeric ledgers.
In the Recognition framework it keeps the T5 J-cost Cauchy data detachable from the sequence payload, so completion quotients and cost-composition identities can be stated on bare orbits without carrying certificates through every algebraic step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.