PRCRawAdd
plain-language theorem explainer
Pointwise addition on raw rational ledgers: sequences of rationals indexed by natural numbers are added termwise. Anyone building the real-field structure from Cauchy ledgers cites this as the underlying sum before Cauchy and null-equivalence conditions are imposed. The body is the obvious function definition, not a proof.
Claim. Given two raw rational ledgers $u,v:\mathbb{N}\to\mathrm{PRCRat}$, their sum is the ledger $n\mapsto u(n)+v(n)$.
background
In the Primitive Recognition Calculus construction of a complete ordered field, a raw rational ledger is simply a map $\mathbb{N}\to\mathrm{PRCRat}$: a completed-orbit sequence of rationals with no Cauchy certificate yet attached. Cauchy ledgers package such a sequence with a proof that it is Cauchy in the $J$-cost distance; the forgetful map raw extracts the underlying sequence.
Field operations on the eventual reals are defined first on these raw sequences, then lifted once closure and congruence targets are discharged. Pointwise addition is the additive half of that raw algebra; the same pattern appears for negation and multiplication among the module siblings.
proof idea
Pure definition: return the function $n\mapsto u(n)+v(n)$. No lemmas, tactics, or obligations. The type is an abbreviation for $\mathrm{Nat}\to\mathrm{PRCRat}$, so termwise rational addition is well-typed immediately.
why it matters
This is the raw carrier for addition in the PRC real construction. Downstream, PRCRealAddClosureTarget asks that pointwise sums of Cauchy ledgers remain Cauchy, and PRCRealAddCongruenceTarget asks that null-equivalent inputs yield null-equivalent sums; both are stated directly in terms of this operation on forgotten raw sequences. Until those blockers close, the additive structure on the quotient of Cauchy ledgers by null distance cannot be installed. The definition itself is scaffolding-free; it only supplies the algebraic skeleton those targets quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.