PRCRealAddClosureTarget_proved
plain-language theorem explainer
Pointwise sums of two PRC Cauchy ledgers remain Cauchy in the J-cost distance. Anyone building the real carrier from Cauchy ledgers cites this as the addition-closure blocker. The argument picks a common tail via the triangle modulus, then reduces pairwise distances by left/right translation invariance of the J-cost metric.
Claim. For any two Cauchy ledgers $u$ and $v$ (sequences of PRC rationals that are Cauchy in the $J$-cost distance), the pointwise sum ledger $n \mapsto u_n + v_n$ is again Cauchy: for every $\varepsilon > 0$ there exists $N$ such that for all $m,n \ge N$, the $J$-cost distance between $u_m+v_m$ and $u_n+v_n$ is less than $\varepsilon$.
background
In the Primitive Recognition Calculus, candidate reals are Cauchy ledgers: sequences of PRC rationals that are Cauchy for the $J$-cost distance. The $J$-cost is the Recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), and the associated distance on positive ratios is the metric used to define Cauchy tails.
Addition on ledgers is defined pointwise (PRCRawAdd). For the quotient by null distance to carry a well-defined addition, the raw sum of two Cauchy ledgers must itself be Cauchy. That exact blocker is the proposition PRCRealAddClosureTarget.
Two upstream facts drive the estimate. First, $J$-cost distance is invariant under simultaneous left or right translation by a fixed rational (PRCJCostDistance_add_left, PRCJCostDistance_add_right). Second, the triangle modulus for $J$-cost distance is closed (PRCJCostDistanceTriangleModulusTarget_proved): given $\varepsilon>0$ one obtains a positive $\delta$ controlling a three-point chain.
proof idea
Fix Cauchy ledgers $u,v$ and $\varepsilon>0$. Apply the proved triangle-modulus target to obtain $\delta>0$ such that any three-point chain with consecutive $J$-distances $<\delta$ has endpoints within $\varepsilon$.
Extract Cauchy tails $N_u,N_v$ for $u$ and $v$ at scale $\delta$. Set $N=\max(N_u,N_v)$. For $m,n\ge N$, compare the three points $u_m+v_m$, $u_n+v_m$, $u_n+v_n$. Right-translation invariance reduces the first hop to $d_J(u_m,u_n)<\delta$; left-translation invariance reduces the second hop to $d_J(v_m,v_n)<\delta$. The modulus then yields $d_J(u_m+v_m,u_n+v_n)<\varepsilon$.
why it matters
This discharges the addition-closure target in the PRC real construction. Downstream, prc_real_complete_ordered_field_conditional_certificate packages it as add_closure in Order step 10 ("quotient algebra is reduced to exact closure and congruence targets"), and the promoted certificate prc_real_complete_ordered_field_promoted_certificate installs the same proof as a permanent field of the promoted real certificate.
Without add-closure, the Cauchy-ledger quotient cannot inherit addition, so the ordered-field carrier for Recognition reals stays blocked. The result is pure foundation scaffolding toward a complete ordered field; it does not yet touch the forcing chain T0–T8, the Recognition Composition Law, or physical constants, but it is a necessary algebraic step before those layers can sit on a PRC real base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.