value_neg
plain-language theorem explainer
Negation of a finite rich expression evaluates to the ordinary real negation of its value. Anyone citing rich certified-analytic closure or the forgetful real-line presentation needs this identity. The proof is a one-line simp wrapper through eval and the underlying protocol negation law.
Claim. For any rich registry $R$ and any finite rich expression $a$, the displayed real value of the native negation of $a$ equals the ordinary real negation of the displayed value of $a$: $\mathrm{val}_R(\neg a) = -\mathrm{val}_R(a)$.
background
The module builds a richer countable registry of certified analytic content: constants, unary protocol transformers, and binary protocol transformers. Finite expressions over that registry (rationals, constants, negation, addition, subtraction, unary and binary applications) are evaluated to Delta-real protocols and then displayed as classical reals.
The display map value is evaluation followed by the protocol's real value. Upstream, the plain (non-rich) registry already has the same law: native negation remains negation under the value display. At the protocol layer, Delta-real negation is the interval rule whose value is ordinary real negation.
Locally this lemma is the rich-expression counterpart of that protocol identity, needed so arithmetic on expressions matches arithmetic on displayed reals.
proof idea
One-line wrapper. Unfold the rich value (eval then protocol value) and the recursive eval clause for the negation constructor, then apply the upstream protocol lemma that (neg p).value = -p.value. No induction or case split is required beyond what simp discharges.
why it matters
Feeds the rich certified-analytic closure theorem, which packages countability of the value set, protocol witnessing of every value, rational embedding, and the ring laws for addition and negation on rich expressions. The same identity appears in the plain transcendental protocol closure and in the Phase 1 headline that the classical real line is the forgetful value of a Delta-real protocol (native operations remain ring operations under display).
In the Recognition foundation this is bookkeeping, not a forcing step: it keeps the countable certified carrier closed under negation so analytic content stays protocol-witnessed rather than continuum-native. It supports later surjectivity and subtraction lemmas that build on the same display faithfulness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.