Partial interval arithmetic on arbitrary endpoint carriers

Exact endpoint calculations take place in an ordered field. A supplied OutwardRounding encodes the lower and upper results; failure is explicit rather than silently saturating an invalid enclosure. Binary, decimal, and posit adapters can instantiate the scalar field with exact rationals. No IEEE-specific exceptional values enter this layer.

def FloatLib.Numerics.OutwardRounding.checkedCandidates? {α : Type u_1} {β : Type u_2} [LinearOrder β] (decode : α → Option β) (candidate : β → Interval α) (x : β) : Option (Interval α)

Check candidate encodings against the exact scalar before accepting an enclosure.

def FloatLib.Numerics.OutwardRounding.ofCandidates {α : Type u_1} {β : Type u_2} [LinearOrder β] (decode : α → Option β) (candidate : β → Interval α) : OutwardRounding α β

Build a sound partial rounder from candidate endpoints and their exact decoder.

The check also rejects overflowed, saturated-on-the-wrong-side, and exceptional results. Candidate generation may use a fast untrusted search; successful results carry checked bounds.

def FloatLib.Numerics.Interval.encloseInterval? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) (I : Interval β) : Option (Interval α)

Round the lower bound downward and the upper bound upward, with explicit failure.

def FloatLib.Numerics.Interval.liftUnary? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) (f : Interval β → Interval β) (I : Interval α) : Option (Interval α)

Decode, apply an exact endpoint enclosure, and round outward.

def FloatLib.Numerics.Interval.liftBinary? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) (f : Interval β → Interval β → Interval β) (I J : Interval α) : Option (Interval α)

Decode two intervals, apply an exact endpoint enclosure, and round outward.

def FloatLib.Numerics.Interval.neg? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I : Interval α) : Option (Interval α)

Outward-rounded negation, exchanging the endpoints.

def FloatLib.Numerics.Interval.add? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I J : Interval α) : Option (Interval α)

Outward-rounded addition; missing finite interpretations and overflow return none.

def FloatLib.Numerics.Interval.sub? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I J : Interval α) : Option (Interval α)

Outward-rounded subtraction.

def FloatLib.Numerics.Interval.mul? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I J : Interval α) : Option (Interval α)

Outward-rounded four-corner multiplication.

def FloatLib.Numerics.Interval.div? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) (I J : Interval α) : Option (Interval α)

Outward-rounded four-corner division, defined only away from a zero-crossing denominator.

The generic endpoint carrier need not represent unbounded intervals, so a denominator that does not lie strictly on one side of zero returns none.