raw_apply
plain-language theorem explainer
The forgetful map from a PRC Cauchy sequence to its raw rational ledger is pointwise the sequence of terms: at every index the two agree. Anyone rewriting expressions that mix Cauchy ledgers with raw ledgers will fire this as a simp rule. The proof is pure definitional equality (rfl).
Claim. For every PRC Cauchy sequence $u$ and every $n \in \mathbb{N}$, the $n$-th entry of the raw rational ledger of $u$ equals the $n$-th term of $u$.
background
In the Primitive Recognition Calculus (PRC) development of a complete ordered field, a PRC Cauchy sequence is a completed orbit-indexed rational ledger whose J-cost distance eventually falls below every positive PRC rational tolerance. Concretely it packages a map term : Nat → PRCRat together with the Cauchy condition on the PRC J-cost distance between terms.
The raw projection forgets the Cauchy certificate and retains only the underlying rational ledger. By definition that projection is exactly the term map, so evaluating it at an index is the same as reading the term. This module sits in the foundation layer that builds reals from PRC rational ledgers and the J-cost metric, importing the Cauchy structure and the J-cost distance/triangle infrastructure.
proof idea
One-line term proof by rfl. The raw projection is defined as u.term, so u.raw n and u.term n are definitionally equal; no lemmas are applied.
why it matters
This is a simp lemma that keeps the forgetful interface between Cauchy ledgers and raw rational ledgers transparent. It supports the algebraic layer on raw ledgers (pointwise add, neg, mul, eventual order) that underpins the PRC construction of a complete ordered field from recognition cost geometry. No downstream theorems currently depend on it by name, but the @[simp] tag makes it ambient infrastructure for any later rewriting that mixes raw with term access. It does not itself touch forcing-chain landmarks (T5–T8) or the RCL; it is pure bookkeeping inside the real-completion stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.