TorchLean API

FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.Basic

Decimal interchange arithmetic and its numerical guarantees #

Exact rational intermediates implement addition, subtraction, multiplication, division, and fused multiply-add. An integer square root and exact squared midpoint comparisons implement square root.

The imported theorems establish destination validity, nearest and directed rounding bounds, exactness on every representable rational, signed-zero and preferred-cohort optimality for exact results, least-quantum cohorts for inexact results, and numerical inexactness. Quantize rounds directly to its requested quantum, with fixed-grid error and status proofs. For valid finite inputs in formats with nonnegative maximum quantum, integral rounding preserves max(Q(x), 0) and produces an integer. A custom format with negative maximum quantum returns invalid because it cannot store that preferred quantum. The two variants differ only in whether numerical inexactness raises a flag. Decimal tininess is tested before rounding, except that quantize never signals underflow. These guarantees cover the operations provided here; they are not a claim of complete IEEE 754 implementation or certification.

Inspection.Basic adds exact comparisons and their flags, numerical classification, total-order laws and tie rules, quantum queries, and bit-preserving sign operations.

Use DecimalInterchange.Basic separately for BID/DPD interchange codecs, or Arithmetic.Operations when only executable arithmetic is needed.