value_neg
plain-language theorem explainer
Negation of a Delta-real protocol displays as ordinary real negation: the unique real common to the negated nested intervals is minus the original value. Anyone building ring operations or certified-analytic registries on protocols cites this. The proof identifies −x.value as the unique real trapped in every interval of neg x, via the uniqueness lemma and endpoint swap.
Claim. For every Delta-real protocol $x$ (a nested family of rational intervals of width at most $1/(n+1)$), the unique real value of the negated protocol equals the ordinary real negation of the value of $x$: $\mathrm{value}(\mathrm{neg}\, x) = -\mathrm{value}(x)$.
background
A Protocol (Delta-real) is a nested sequence of rational intervals whose width at precision $n$ is at most $1/(n+1)$. The intended quantity is the unique real lying in every interval; that real is value. Lower and upper endpoints are exposed as real sequences lo and hi, with the sandwich lo n ≤ value ≤ hi n for all $n$.
Negation on protocols swaps endpoints: the $n$th interval of neg x is $[-\mathrm{hi}_n(x), -\mathrm{lo}_n(x)]$. The same construction appears upstream for logic integers as pair swap $(a,b)\mapsto(b,a)$. Uniqueness of the trapped real (value_unique) is the main prior: any real that sits in every approximating interval must equal value.
This module builds the forgetful display of classical reals from protocol data, so arithmetic operations must commute with that display before higher certified-analytic layers can treat negation as native.
proof idea
Term-mode proof. Symmetry reduces the goal to showing that $-x.\mathrm{value}$ equals $(\mathrm{neg}, x).\mathrm{value}$. Apply value_unique to $\mathrm{neg}, x$: it suffices that $-x.\mathrm{value}$ lies in every approximating interval of $\mathrm{neg}, x$.
For each $n$, the lower bound $(\mathrm{neg}, x).\mathrm{lo}, n \le -x.\mathrm{value}$ unfolds to $-x.\mathrm{hi}, n \le -x.\mathrm{value}$, which is the existing upper sandwich $x.\mathrm{value} \le x.\mathrm{hi}, n$ after casting and linarith. The upper bound $-x.\mathrm{value} \le (\mathrm{neg}, x).\mathrm{hi}, n$ likewise unfolds to the existing lower sandwich $x.\mathrm{lo}, n \le x.\mathrm{value}$. No new analysis is needed beyond endpoint swap and the two sandwich lemmas.
why it matters
This is the unary half of the ring-display laws for Delta-reals. Downstream, value_sub is literally value_add plus this lemma plus ring. The Phase-1 headline display_real_forgetful packages surjectivity, rational embedding, observational faithfulness, and the full ring laws; its negation clause is exactly this theorem.
Certified-analytic layers lift it by simp: both CertifiedAnalyticProtocols.value_neg and the rich-transformer analogue reduce native expression negation to Protocol.value_neg. Those feed the closure theorems (transcendental_protocol_closure, rich_transformer_closure), which assert that countable registries of certified constants and transformers produce only countably many protocol-witnessed reals, with negation commuting with display. In the Recognition foundation this keeps analytic content on countable protocol carriers rather than on the continuum as a primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.