Representation-independent error contracts

An error theorem should describe a particular executable kernel, exact interpretation, error measure, and bound. The universal numerical system therefore carries no mandatory norm or field structure. This proof-only capability accepts all four as parameters and works for absolute, relative, ulp, interval, vector, or family-specific measures.

class FloatLib.Numerics.HasErrorBound {Input : Type u} {Bound : Type v} [LE Bound] (system : NumericalSystem) (run : Input → system.Code) (exact : Input → system.Scalar) (measure : system.Scalar → system.Scalar → Bound) (bound : Input → Bound) : Prop

A code-producing kernel represents some finite result whose measured error satisfies bound.

The class lives in Prop, so the capability adds no runtime data to the kernel.

• error_le (input : Input) : ∃ (actual : system.Scalar), system.Represents (run input) actual ∧ measure actual (exact input) ≤ bound input

  Every kernel result has a finite denotation within its declared error bound.

@[inline]

def FloatLib.Numerics.absoluteError {α : Type} [AddCommGroup α] [LinearOrder α] (actual exact : α) : α

Absolute difference |actual - exact| in an additive commutative group with a linear order. The definition does not require the order to be compatible with addition.

theorem FloatLib.Numerics.HasErrorBound.exists_represents {Input : Type u} {Bound : Type v} [LE Bound] {system : NumericalSystem} {run : Input → system.Code} {exact : Input → system.Scalar} {measure : system.Scalar → system.Scalar → Bound} {bound : Input → Bound} [HasErrorBound system run exact measure bound] (input : Input) : ∃ (actual : system.Scalar), system.Represents (run input) actual

Extract the represented finite result guaranteed by an error-bound capability.