Representation-independent numerical semantics

Numerical systems, exact dyadic and rational values, quantization contracts, reduction errors, and primitive representations used by the concrete formats.

At and AtFinite attach erased proofs to a system's runtime carrier. Optional capabilities state the order, radix, rounding, error, or block-scaling assumptions needed by a theorem.

Use these definitions when implementing a format or proving a result independent of its encoding. Application examples start with import FloatLib; concrete families are under FloatLib.Floats.Formats.