value_add
plain-language theorem explainer
Addition of two Delta-real protocols is compatible with ordinary real addition of their values. Anyone building certified analytic registries or proving that protocol arithmetic displays as a ring cites this. The proof identifies the sum of the two values as the unique real trapped in every nested interval of the sum protocol, via the lower/upper endpoint bounds at doubled precision.
Claim. If $x$ and $y$ are Delta-real protocols (nested rational interval families with width at most $1/(n+1)$), then the value of their interval-sum protocol equals the sum of their values: $\mathrm{value}(x+y)=\mathrm{value}(x)+\mathrm{value}(y)$.
background
A Protocol (Delta-real) is a nested family of rational intervals whose width at precision $n$ is at most $1/(n+1)$. The intended quantity is the unique real lying in every interval; that real is written $\mathrm{value}$. Lower and upper endpoints, cast to $\mathbb{R}$, are $\mathrm{lo},n$ and $\mathrm{hi},n$, and the sandwich $\mathrm{lo},n\le\mathrm{value}\le\mathrm{hi},n$ holds for every $n$.
Protocol addition is the pointwise Minkowski sum of the approximating intervals (with a precision reindexing that preserves the width bound). The uniqueness lemma for values says that any real trapped between every lower and upper endpoint of a protocol must equal that protocol's value. Upstream endpoint inequalities $\mathrm{lo}_\mathrm{le}_\mathrm{value}$ and $\mathrm{value}_\mathrm{le}_\mathrm{hi}$ supply the one-sided bounds used here.
proof idea
Symmetrize the goal and apply value uniqueness: it suffices to show that $x.\mathrm{value}+y.\mathrm{value}$ lies in every approximating interval of $\mathrm{add},x,y$. For the lower bound at precision $n$, unfold the sum's lower endpoint and invoke $\mathrm{lo}_\mathrm{le}_\mathrm{value}$ for $x$ and $y$ at index $2n+1$; after casting, $\mathrm{linarith}$ closes. The upper bound is symmetric, using $\mathrm{value}_\mathrm{le}_\mathrm{hi}$ at the same doubled index. No separate continuity or completeness argument is needed beyond uniqueness of the trapped real.
why it matters
This is the native addition law for Delta-reals. It is the lemma that CertifiedAnalyticProtocols.value_add and CertifiedAnalyticTransformers.value_add reduce to by simp, and it appears as a conjunct in both transcendental_protocol_closure and rich_transformer_closure (countable certified registries display addition as ordinary $+$). Downstream, display_real_forgetful lists it among the Phase 1 headline facts: protocol operations are interval rules whose values form a ring. value_sub is an immediate corollary via negation. In the Recognition foundation this keeps analytic content on countable protocol carriers rather than on the continuum as a primitive, while still recovering classical real arithmetic on display values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.