PRCRealAddClosureTarget
plain-language theorem explainer
Packages the exact additive-closure obligation for the PRC real completion: pointwise sums of J-cost Cauchy rational ledgers must again be Cauchy. Anyone assembling the null-quotient ordered field cites this Prop as the named blocker before promoting addition on equivalence classes. The body is a pure universal statement over Cauchy sequences; no proof lives here.
Claim. For all Cauchy sequences $u,v$ of PRC rationals (Cauchy with respect to J-cost distance), the pointwise sum ledger $n\mapsto u_n+v_n$ is itself Cauchy under the same J-cost distance.
background
In the Primitive Recognition Calculus, reals are built from orbit-indexed rational ledgers that are Cauchy for the J-cost distance: for every positive PRC rational tolerance $\varepsilon$ there is $N$ so that $m,n\ge N$ forces $\mathrm{dist}_J(s_m,s_n)<\varepsilon$. A PRCCauchySeq packages such a ledger with its Cauchy witness; forgetting the witness yields a raw ledger.
Pointwise addition on raw ledgers is the termwise sum $n\mapsto u_n+v_n$. The raw Cauchy predicate is identical in shape to the structured one, so the natural closure question is whether the sum of two Cauchy ledgers remains Cauchy. That obligation is isolated here as a named Prop before any quotient or field structure is installed.
The surrounding module is the first complete-ordered-field surface for PRC: carrier and rational embedding are closed, while algebra, order, and completeness are reduced to a bundle of exact targets of which this is the additive-closure entry.
proof idea
Definition only: the body is the universal Prop that every pair of Cauchy sequences has Cauchy pointwise sum under the raw J-cost Cauchy predicate. No tactics or lemmas are applied at this site. The discharging proof lives in the sibling theorem that introduces a modulus from the J-cost triangle inequality, pulls Cauchy tails for each summand at that modulus, and recombines them.
why it matters
This is the exact blocker for additive quotient well-definedness under null distance. It is the add_closure field of the targets bundle that feeds the conditional complete-ordered-field certificate, and it reappears as a required hypothesis of the promoted Step 10 certificate (closed operations on the internal null quotient, with Mathlib typeclass packaging deferred).
The sibling proved theorem discharges it by triangle-modulus control of J-cost distance, so the definition is the contract that theorem fulfills. Without this named Prop, addition cannot be lifted from raw ledgers to the null quotient, and the PRC real carrier cannot carry a field operation. It sits upstream of congruence, negation, and multiplication targets in the same bundle; those are separate blockers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.