neg_lo
plain-language theorem explainer
The theorem states that negating a closed rational interval swaps its bounds with a sign change, so the new lower endpoint equals the negation of the original upper endpoint. Numerics researchers using verified bounds for real computations would cite this when simplifying expressions involving negated intervals. The proof is immediate reflexivity from the definition of interval negation.
Claim. For a closed interval $I$ with rational endpoints $lo_I$ and $hi_I$ satisfying $lo_I ≤ hi_I$, the lower endpoint of the negated interval satisfies $(-I).lo = -hi_I$.
background
The module supplies verified interval arithmetic with rational endpoints to bound real values exactly, per the module documentation on rigorous computation of transcendental functions. The Interval structure consists of rational lo and hi fields together with a proof that lo ≤ hi, and is used to represent closed intervals. This theorem depends on the local Interval definition and on the parallel real-endpoint Interval structure from Recognition.Certification.
proof idea
The proof is a one-line reflexivity (rfl) that holds directly by the definition of the negation operation on Interval, which constructs the new interval with lo set to the negation of the original hi.
why it matters
This lemma is invoked by neg_contains_neg to establish that containment is preserved under negation, supporting the full set of interval operations in the Numerics layer. It supplies a basic algebraic identity needed for bound propagation in Recognition Science computations, such as sign changes arising in phi-ladder evaluations or J-cost calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.