neg
plain-language theorem explainer
The neg definition equips closed rational intervals with negation by swapping and negating the endpoints. Numerics code that propagates bounds through sign changes in Recognition computations cites it when evaluating expressions involving negative values. The definition is a direct record constructor that reuses the input validity proof via neg_le_neg.
Claim. For a closed interval $I=[a,b]$ with rational endpoints satisfying $a≤b$, the negation is defined by $-I:=[-b,-a]$.
background
The Interval structure is a closed interval with rational endpoints lo and hi obeying lo ≤ hi. The module supplies verified interval arithmetic that uses exact rational endpoints to bound real values, particularly for transcendental functions. Upstream negations in logic-derived integers and rationals swap components or negate numerators, while the elliptic-curve version negates the y-coordinate; the present definition follows the same pattern of endpoint reversal.
proof idea
The definition builds a fresh Interval record by setting the new lower bound to the negation of the input upper bound and the new upper bound to the negation of the input lower bound. The validity field is discharged by a direct application of the lemma neg_le_neg to the original valid proof.
why it matters
Negation is a prerequisite for the ring and group structures that appear in PhiRing (J_at_phi, PhiInt) and RecognitionCategory (PhiRingHom, canonicalPhiRingObj). It supplies the basic sign-flip operation required by the numerics layer that supports exact bound tracking for the phi-ladder and the alpha band. No open scaffolding questions are addressed here; the definition simply closes a missing primitive used by forty downstream declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.