value_neg
plain-language theorem explainer
Native negation of a finite expression over a certified analytic registry displays as ordinary real negation of that expression's value. Anyone assembling ring laws for registry-generated reals, or closing the transcendental-protocol package, cites this. The proof is a one-line simp that unfolds value and eval and applies the underlying Protocol negation lemma.
Claim. For any registry $R$ of certified analytic protocol ingredients and any finite expression $a$ over $R$, the displayed real value of the negated expression equals the ordinary real negation of the value of $a$: $\mathrm{value}_R(\neg a) = -\mathrm{value}_R(a)$.
background
In the certified-analytic protocols layer, a Registry is a countable catalogue of constant protocols and unary protocol transformers. Finite expressions over a registry (Expr) are the native objects: rationals, registered constants, native additive constructors (neg, add, sub), and registered unary transforms. Evaluation of an expression returns a Delta-real Protocol, never an uncountable graph; value is evaluation followed by the protocol's real display.
Delta-real protocols already carry a native negation whose display is ordinary real negation (Protocol.value_neg in DeltaReal). The present lemma lifts that fact from protocols to the expression tree: the expression constructor .neg is interpreted by protocol negation, so the displayed value commutes with negation. The same pattern appears for the richer transformer registry.
Local setting: keep analytic content countable and protocol-witnessed, with the classical real line recovered only as a forgetful display.
proof idea
One-line wrapper. Unfold value (display of eval) and eval on the .neg constructor, then apply Protocol.value_neg, which states that protocol negation displays as real negation. No induction on the expression tree is needed; the constructor case reduces directly.
why it matters
This is one of the ring-law legs packaged by transcendental_protocol_closure: that theorem asserts countability of registry values, protocol witnessing of every value, rational embedding, additivity, and this negation identity. The same identity is re-proved for rich expressions and feeds rich_transformer_closure.
Downstream, DeltaReal.value_sub builds subtraction as add-of-neg and rewrites with this (or the protocol-level) negation law; value_surjective and the Phase-1 headline display_real_forgetful list native negation among the forgetful ring operations that make the classical line the display of protocols. In the Recognition foundation, the point is structural: analytic content lives in countable certified protocols; continuum arithmetic is recovered only after display. Negation commuting with display is a minimal faithfulness check for that story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.