neg_hi
plain-language theorem explainer
Negation on a rational-endpoint interval I maps the high bound of -I exactly to the negation of I's low bound. Formal verification users of interval arithmetic cite this when composing sign-reversing operations. The proof is immediate reflexivity once the interval negation is defined by endpoint swap and negation.
Claim. For a closed interval $I$ with rational endpoints $a, b$ where $a ≤ b$, the upper endpoint of the negated interval satisfies $(-I).hi = -a$.
background
This module supplies verified interval arithmetic using rational endpoints to compute exact bounds on real functions. The Interval structure consists of lo and hi as rationals with the validity condition lo ≤ hi. This choice enables decidable equality and exact arithmetic in Lean.
proof idea
The proof applies reflexivity directly to the defining equation of interval negation, which sets (-I).hi to -I.lo by construction.
why it matters
It underpins the downstream result neg_contains_neg, which establishes that containment is preserved under negation. This supports the overall machinery for rigorous bounding in the Recognition Science numerics layer, ensuring sign changes do not introduce errors in certified computations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.