PRCRawRatLedger
plain-language theorem explainer
A raw completed-orbit rational ledger is simply a sequence of PRC rationals indexed by natural numbers, with no Cauchy condition yet. Anyone building the PRC real line from orbit-level rationals cites this as the carrier type before packaging or quotienting. The declaration is a one-line type synonym for Nat → PRCRat.
Claim. A raw completed-orbit rational ledger is a function $\mathbb{N} \to R$, where $R$ denotes the PRC rationals (nonzero-denominator ratio-orbit quotient classes identified by cross-multiplication).
background
In the Primitive Recognition Calculus, rationals are not classical $\mathbb{Q}$. They are PRCRat: quotient classes of ratio orbits under the cross-multiplication setoid (K4.8). Sequences of such rationals are the raw material for constructing reals via a J-cost Cauchy condition.
A full PRC Cauchy sequence packages a term map Nat → PRCRat together with the predicate that J-cost distance eventually falls below every positive PRC rational tolerance. The raw ledger is that term map alone, before the Cauchy proof is attached. The forgetful map raw sends a packaged Cauchy sequence to this underlying ledger.
The local module builds the complete ordered field structure on PRC reals. Raw ledgers are the intermediate objects on which pointwise arithmetic, eventual order, null equivalence, and the Cauchy predicate are defined before quotienting by null distance.
proof idea
One-line type abbreviation: the raw ledger type is defined to be exactly Nat → PRCRat. No proof obligations; no lemmas applied.
why it matters
This carrier type is the common substrate for the completeness targets and the ordered-field operations on raw sequences. Downstream, PRCRawCauchy states the J-cost Cauchy predicate on raw ledgers; PRCRawAdd, PRCRawNeg, and PRCRawMul give pointwise arithmetic; PRCRawEventuallyLe and null equivalence prepare the quotient.
Completeness scaffolding uses it directly: every raw Cauchy ledger should package as a PRCCauchySeq (PRCRawCauchyRealizationTarget), determine a null-quotient point (PRCRawCauchyQuotientPointTarget), and appear as the diagonal ledger in the representative-Cauchy limit construction (PRCRealRawDiagonalLedgerTarget, PRCRealTailSelectionTarget). Those targets isolate the remaining mathematical work after bookkeeping is stripped away.
In the Recognition forcing chain this sits under the foundation layer that eventually supports the real calculus used by cost, mass, and continuum constructions; it does not itself invoke T5–T8 or the RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.