neg
plain-language theorem explainer
Negation of a Delta-real: each nested rational interval is reflected through zero by swapping and sign-flipping its endpoints. Anyone building the additive group of constructive reals in the recognition calculus cites this. The definition packages the interval map and discharges nestedness and the width bound by linear arithmetic on the source protocol's certificates.
Claim. Given a protocol $x$ (a nested family of closed rational intervals with width at most $1/(n+1)$ at stage $n$), its negation $-x$ is the protocol whose stage-$n$ interval is $\bigl[-(x_n)^{\mathrm{hi}},\, -(x_n)^{\mathrm{lo}}\bigr]$. Nestedness and the width bound are inherited from $x$.
background
A Protocol (Delta-real) is a nested family of closed rational intervals whose width at precision $n$ is at most $1/(n+1)$. The intended real is the unique point common to every interval. Each stage is a RatInterval: a pair of rationals $(\ell,h)$ with $\ell\le h$, and width $h-\ell$.
Negation on the underlying integers and rationals is already available from the logic-first arithmetic stack (swap of difference pairs on integers; induced map on rationals). This definition lifts that sign flip to the interval protocol: lower and upper endpoints exchange roles after negation, so the closed interval is reflected through the origin.
The local module builds a constructive real line suited to recognition calculus, before the usual Mathlib reals are treated as the completed object. Lower and upper endpoint projections (lo, hi) read the protocol as real-valued bounds once the rational endpoints are coerced.
proof idea
Definitional construction, not a deep theorem. The approximating map sends stage $n$ to the interval with endpoints $(-h_n,-\ell_n)$, where $(\ell_n,h_n)$ is the source interval; the endpoint order proof is linarith from $\ell_n\le h_n$.
Nestedness: subset of successive intervals swaps the two endpoint inequalities, so the source nestedness certificates are applied after simp and closed by linarith. Width bound: width is $h-\ell$, so the reflected width equals the original; unfold width, simp, and reuse the source bound via linarith.
why it matters
Delta-reals need additive inverses before subtraction, group laws, and signed costs can be stated inside the foundation. This is the protocol-level negation that feeds that structure.
Downstream, signed arithmetic on these objects appears across the algebra and constants layers: the $\varphi$-ring cost bridge $J(\varphi)=(\sqrt{5}-2)/2$ (coherence cost of self-similarity on the $\varphi$-ladder), integer pairs in $\mathbb{Z}[\varphi]$, logarithmic derivatives of $\alpha^{-1}$ with respect to the gap parameter, and cosmological sums that treat signed weights. Those uses sit on top of a real line that ultimately rests on protocol arithmetic of this kind.
In the forcing chain, signed quantities are routine once $J$ and $\varphi$ are fixed (T5–T6); the present definition is infrastructure, not a new physical claim. It closes the sign-flip gap in the constructive real API rather than an open scientific question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.