value_add
plain-language theorem explainer
Addition of rich certified-analytic expressions is faithful under the real-value display: the value of a sum expression equals the sum of the values. Anyone proving ring-homomorphism or closure properties for rich protocol registries cites this. The proof is a one-line simp wrapper through evaluation and the underlying Delta-real addition law.
Claim. For any rich registry $R$ and any two finite rich expressions $a,b$, the real display value of the sum expression equals the ordinary sum of the display values: $\mathrm{val}_R(a+b)=\mathrm{val}_R(a)+\mathrm{val}_R(b)$.
background
In the Primitive Recognition Calculus, a Delta-real protocol is a nested family of rational intervals whose widths shrink at least as $1/(n+1)$. Its intended quantity is the unique real common to all intervals; that real is the protocol's value. Protocol addition is defined by interval arithmetic and is already known to satisfy $(\mathrm{add},x,y).\mathrm{value}=x.\mathrm{value}+y.\mathrm{value}$.
A RichRegistry packages countably many certified constants together with unary and binary protocol transformers. RichExpr is the free finite expression language over that registry: rationals, named constants, negation, addition, subtraction, and applications of the unary/binary transformers. Evaluation eval interprets an expression as a protocol; value is evaluation followed by the real display map.
The thinner Registry/Expr layer already has the same addition law. This declaration lifts it to the richer language that admits binary transformers.
proof idea
One-line wrapper. Unfold value (display of eval) and the recursive clause of eval on the .add constructor, then apply Protocol.value_add, which states that protocol addition preserves real values. The simp call discharges the equality in a single step.
why it matters
This is one of the ring-homomorphism legs of rich certified-analytic closure. The parent theorem rich_transformer_closure packages countability of the value set, protocol witnessing of every value, rational embedding, addition fidelity, and negation fidelity; the addition conjunct is exactly this lemma.
Downstream it also feeds the thinner transcendental protocol closure and the Delta-real Phase-1 headline display_real_forgetful, which asserts that classical reals are the forgetful values of protocols and that protocol operations act as a ring on those values. In the Recognition foundation this supports the claim that analytic content lives on a countable certified protocol registry rather than on an uncountable continuum carrier: arithmetic on expressions remains ordinary real arithmetic after display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.