value_add
plain-language theorem explainer
Addition of finite certified-analytic expressions is preserved by the real-valued display map: the value of an add-node equals the sum of the values of its children. Anyone proving ring-homomorphism or closure facts for countable protocol registries cites this. The proof is a one-line simplification through evaluation and the underlying Delta-real addition law.
Claim. For any countable registry $R$ of certified analytic protocols and any two finite expressions $a,b$ over $R$, the real display satisfies $\mathrm{value}_R(a+b)=\mathrm{value}_R(a)+\mathrm{value}_R(b)$.
background
In the Primitive Recognition Calculus, analytic content is carried by Delta-real protocols: nested families of rational intervals whose widths shrink as $1/(n+1)$, each protocol determining a unique real (its value). A Registry packages a countable supply of constant protocols and unary protocol transformers. Finite expressions over a registry are the native objects: rationals, registered constants, negation, addition, subtraction, and unary transforms. Evaluation walks the expression tree to a protocol; the display map then reads off that protocol's real value.
Binary analytic operations beyond the native additive structure are deliberately kept out of the registry; they can be encoded later as unary transforms on paired protocols. The underlying protocol layer already proves that protocol addition displays as ordinary real addition. The present lemma lifts that fact from protocols to expression trees.
proof idea
One-line simplification. Unfold the expression-level display map (evaluation followed by protocol value) and the recursive evaluator on an add-node; the goal reduces to the protocol-level identity that the value of a sum of protocols is the sum of the values, which is already available from DeltaReal.
why it matters
This is one of the four algebraic clauses packed into transcendental protocol closure: any countably indexed registry generates only countably many reals, every such real is protocol-witnessed, rationals embed, and addition and negation are preserved under display. The same pattern is mirrored for rich registries with binary transformers. Downstream, the forgetful Phase-1 headline that the classical real line is the value of Delta-real protocols relies on the protocol-level addition law; the expression-level version keeps the countable syntactic carrier honest as a ring homomorphism into $\mathbb{R}$. In the Recognition foundation this supports the claim that the continuum is not the carrier of analytic content: a certified countable protocol registry is.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.