Exact rational arithmetic for P3109

The closed operations in Arithmetic evaluate finite operands in Rat, retaining infinities and the report's single NaN. In particular, division by zero returns NaN, including infinity divided by zero. FMA and fused add-add form the complete exact expression before projection.

The ExecFloat.P3109.*To operations accept independent source and destination descriptors and an explicit projection policy. Same-format operations use FloatLib's nearest-even, no-saturation policy by default. No IEEE exception flags or floating-point environment are used.

Exact rational intermediates can require large integers when the descriptor has a wide exponent range. This implementation does not promise a fixed workspace bound for arbitrary descriptors.

Reference

IEEE Working Group P3109, Interim Report on Arithmetic Formats for Machine Learning, version 4.0.3 (1 September 2026), §§4.10.1–4.10.8, revision 34f5964. This is an unapproved working-group report, not an approved IEEE standard. https://github.com/P3109/Public/tree/34f5964d9bb2382b2665d15467fc3517b990b308.

def FloatLib.Floats.Formats.P3109.Arithmetic.nan : Numerics.NumericalValue ℚ

The report's single exceptional datum.

def FloatLib.Floats.Formats.P3109.Arithmetic.toRat : Numerics.NumericalValue Numerics.Dyadic → Numerics.NumericalValue ℚ

Exact rational observation of a decoded binary datum.

def FloatLib.Floats.Formats.P3109.Arithmetic.neg : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Negation in the report's closed extended domain.

def FloatLib.Floats.Formats.P3109.Arithmetic.abs : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Absolute value in the report's closed extended domain.

def FloatLib.Floats.Formats.P3109.Arithmetic.copySign (value sign : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Copying a sign treats zero as nonnegative and propagates either NaN operand.

def FloatLib.Floats.Formats.P3109.Arithmetic.add : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact addition; opposite infinities have the indeterminate result NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.sub (left right : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Exact subtraction, with no projection of the negated operand.

def FloatLib.Floats.Formats.P3109.Arithmetic.mul : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact multiplication; zero times infinity is NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.div : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Exact division; every zero denominator and infinity divided by infinity yield NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.recip (value : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Exact reciprocal, before the sole destination projection.

def FloatLib.Floats.Formats.P3109.Arithmetic.fma (left right addend : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Exact fused multiply-add, with no intermediate rounding or saturation.

def FloatLib.Floats.Formats.P3109.Arithmetic.faa (left middle right : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Exact fused add-add, with no intermediate rounding or saturation.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.toClosedRat {source : Formats.P3109.Format} (value : P3109 source) : Numerics.NumericalValue ℚ

Exact closed rational value of a P3109 operand.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.unaryTo {source : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (value : P3109 source) : P3109 destination

Project an exact unary closed operation into an independently chosen destination.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.binaryTo {leftFormat rightFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : P3109 leftFormat) (right : P3109 rightFormat) : P3109 destination

Project an exact binary closed operation once, after evaluating both operands.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.ternaryTo {leftFormat rightFormat thirdFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : P3109 leftFormat) (right : P3109 rightFormat) (third : P3109 thirdFormat) : P3109 destination

Project an exact ternary closed operation once, after the complete expression.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.negTo {source : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 source → P3109 destination

Negate and project into the requested destination.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.absTo {source : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 source → P3109 destination

Take absolute value and project into the requested destination.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.copySignTo {leftFormat rightFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 leftFormat → P3109 rightFormat → P3109 destination

Copy the sign, propagating either NaN, and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.addTo {leftFormat rightFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 leftFormat → P3109 rightFormat → P3109 destination

Add exact decoded operands and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.subTo {leftFormat rightFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 leftFormat → P3109 rightFormat → P3109 destination

Subtract exact decoded operands and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.mulTo {leftFormat rightFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 leftFormat → P3109 rightFormat → P3109 destination

Multiply exact decoded operands and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.divTo {leftFormat rightFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 leftFormat → P3109 rightFormat → P3109 destination

Divide exact decoded operands, returning NaN for a zero denominator, and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.recipTo {source : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 source → P3109 destination

Take the exact reciprocal and project once.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.fmaTo {leftFormat rightFormat thirdFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 leftFormat → P3109 rightFormat → P3109 thirdFormat → P3109 destination

Fused multiply-add across independently chosen source and destination formats.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.faaTo {leftFormat rightFormat thirdFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) : P3109 leftFormat → P3109 rightFormat → P3109 thirdFormat → P3109 destination

Fused add-add across independently chosen source and destination formats.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.neg {format : Formats.P3109.Format} (value : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format negation followed by the supplied projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.abs {format : Formats.P3109.Format} (value : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format absolute value followed by the supplied projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.copySign {format : Formats.P3109.Format} (value sign : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format sign copying followed by the supplied projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.add {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format addition with one final projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.sub {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format subtraction with one final projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.mul {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format multiplication with one final projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.div {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format division with one final projection; a zero denominator yields NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.recip {format : Formats.P3109.Format} (value : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format reciprocal with one final projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.fma {format : Formats.P3109.Format} (left right addend : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format fused multiply-add with one final projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.faa {format : Formats.P3109.Format} (left middle right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Same-format fused add-add with one final projection.