add
plain-language theorem explainer
Addition of two Delta-reals (protocols): nested rational-interval approximations with width ≤ 1/(n+1) at stage n. At precision n the sum reads both operands at stage 2n+1, so summed widths again meet the bound. Anyone assembling arithmetic on recognition-native reals cites this. The body is a structure instance: nestedness from endpoint mono/antitone, width from a rational half-precision identity.
Claim. Given protocols $x$ and $y$ (nested families of closed rational intervals with width at most $1/(n+1)$ at stage $n$), their sum is the protocol whose stage-$n$ interval is the Minkowski sum of the stage-$(2n+1)$ intervals of $x$ and of $y$. The resulting family is nested and obeys the same width bound.
background
A protocol (Delta-real) is a map from natural precision $n$ to a closed rational interval, required to be nested under refinement and to satisfy $\mathrm{width}(\mathrm{approx}, n)\le 1/(n+1)$. The intended real is the unique point in the intersection of all stages.
Lower endpoints, viewed as reals, are monotone in $n$; upper endpoints are antitone. Both facts are immediate from the nestedness field of the structure. Rational intervals carry an explicit $lo\le hi$ witness used when forming sums.
The local module builds a constructive real layer on top of logic-derived arithmetic: intervals and protocols are the carriers on which addition, and later the rest of the field operations, are defined without classical completeness axioms.
proof idea
Structure instance with three fields. approx n sets $k=2n+1$ and returns the interval with endpoints $x.approx,k.lo+y.approx,k.lo$ and likewise for $hi$, discharging $lo\le hi$ by linarith on the two operand inequalities.
nested splits into lower and upper inclusions. Each side compares stages $2n+1$ and $2(n+1)+1$ via omega, applies lo_mono (resp. hi_anti) of each operand, then linarith on the summed endpoints.
width_bound pulls the operand bounds at stage $2n+1$, rewrites the summed width as the sum of widths (ring), and uses the identity $1/(2n+2)+1/(2n+2)=1/(n+1)$ (field_simp) to close the $\le 1/(n+1)$ goal.
why it matters
This is the first binary arithmetic operation on Delta-reals in the Primitive Recognition Calculus layer. It shows that the width budget $1/(n+1)$ is stable under addition once operands are read one bit finer ($2n+1$), so the protocol carrier is closed under sums without enlarging the modulus.
No downstream consumers are wired yet in the graph; the natural parents are the remaining field operations and the embedding of these protocols into the classical reals (or into whatever real interface the forcing chain later demands). In the broader Recognition stack this sits under Foundation arithmetic-from-logic work that must eventually support the constants and ladder constructions (phi-ladder masses, J-cost calculus) without smuggling classical analysis.
It does not itself touch T5–T8 or the RCL; it only supplies a constructive addition primitive those layers can later quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.