PRCRealAddCongruenceTarget_proved
plain-language theorem explainer
Addition of PRC Cauchy sequences respects null equivalence under J-cost distance: if u ~ u' and v ~ v', then the pointwise sums are null-equivalent. Cited by anyone assembling the real quotient so addition descends to null classes. Proof feeds a triangle-modulus delta into both null witnesses, takes max index, and reduces the two legs by left/right translation invariance of J-cost distance.
Claim. If $u\sim u'$ and $v\sim v'$ are null-equivalent PRC Cauchy sequences, then $u+v\sim u'+v'$ under raw null equivalence: for every $\varepsilon>0$ there is $N$ such that for all $n\ge N$, the J-cost distance between $u_n+v_n$ and $u'_n+v'_n$ is less than $\varepsilon$.
background
Primitive Recognition Calculus builds candidate reals as Cauchy sequences of rationals measured by J-cost distance, not ordinary absolute value. Null equivalence collapses pairs whose J-cost distance tends to zero; the intended reals are the quotient by that relation.
The target proved here is the exact blocker for additive quotient well-definedness under null distance: pointwise addition of representatives must send null pairs to null pairs. Two upstream facts make the argument possible. J-cost distance is invariant under translating both endpoints on the left and on the right. Separately, the triangle-modulus target (now closed by an explicit rational increment estimate) supplies, for each $\varepsilon>0$, a $\delta>0$ controlling the outer leg of any three-point path.
The ambient module packages these congruence and closure targets into certificates for a complete ordered field.
proof idea
Intro the four sequences, the two null hypotheses, and $\varepsilon>0$. From the proved triangle-modulus target obtain $\delta>0$ such that any three-point path with consecutive J-cost legs $<\delta$ has outer leg $<\varepsilon$. Apply the two null witnesses at that $\delta$ to get indices $N_u,N_v$; set $N=\max(N_u,N_v)$.
For $n\ge N$, run the modulus on the path $u_n+v_n$, $u'_n+v_n$, $u'_n+v'_n$. Right-translation invariance rewrites the first leg as $d(u_n,u'_n)$; left-translation rewrites the second as $d(v_n,v'_n)$. Both are $<\delta$ by choice of indices, so the outer distance is $<\varepsilon$.
why it matters
Discharges the additive congruence obligation needed before addition can live on null classes. Downstream it is installed as add_congruence in the promoted real complete ordered field certificate, and it appears among the targets of the conditional Order-step-10 certificate, whose doc states that quotient algebra is reduced to exact closure and congruence targets.
Without this fact the PRC real carrier cannot carry a well-defined sum, so the foundation layer that later supports the forcing chain (T0–T8) and the recognition composition law would stall at the field axioms. It closes one concrete blocker; multiplicative and order congruences remain separate targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.