pith. machine review for the scientific record. sign in
def definition def or abbrev high

neg

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  66def neg (I : Interval) : Interval where
  67  lo := -I.hi

proof body

Definition body.

  68  hi := -I.lo
  69  valid := neg_le_neg I.valid
  70
  71instance : Neg Interval where
  72  neg := neg
  73

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.