Real-containment contracts for expression backends

The elementary-function proofs hold for every real member of the input interval. Outward rounding preserves those bounds when they are stored in another endpoint format. The integer backend uses the direct binary-grid arithmetic theorems for its algebraic operations.

theorem FloatLib.Numerics.Interval.Backend.containsReal_elementaryBounds? (config : Config) {op : UnaryOp} {I J : Interval ℚ} (h : elementaryBounds? config op I = some J) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some J (op.eval x)

Successful elementary enclosures contain the function value at every real input member.

theorem FloatLib.Numerics.Interval.Backend.ofRounding_sound {α : Type u_1} (R : OutwardRounding α ℚ) (config : Config := { }) : (ofRounding R config).Sound

Any sound rational outward rounder supplies a sound expression backend.

theorem FloatLib.Numerics.Interval.Backend.rational_sound (config : Config := { }) : (rational config).Sound

Exact rational endpoints satisfy the common real-containment contract.

theorem FloatLib.Numerics.Interval.Backend.binaryGrid_sound (config : Config := { }) : (binaryGrid config).Sound

Direct integer arithmetic and rounded elementary bounds give a sound binary-grid backend.