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. An operation returns none if decoding fails, an outward bound is unavailable, or a divisor interval contains zero. Binary, decimal, and posit adapters instantiate the scalar field with exact rationals.

This implements the outward enclosure construction in Rump's Verification methods, §5.3, equations (5.14)–(5.15). OutwardRounding requires containment, so an adapter may return wider bounds than the tight directed rounding used there.

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.