TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Flocq.Theory.Arithmetic

Refinement contracts for exact integer-mantissa arithmetic #

The exact operations in Calculation.Operations refine real arithmetic through the shared numerical-system contracts. Negation and multiplication require only integer arithmetic on the stored mantissas and exponents.

The real-valued decoder is proof-facing and erased from compiled kernels.

source
theorem FloatLib.Floats.Formats.Flocq.FloatRep.negExact_refines (β : Numerics.Radix) :
Numerics.Operation.Finite1 (numericalSystem β) (numericalSystem β) negExact fun (value : ℝ) => -value

Executable mantissa negation exactly refines real negation.

source
theorem FloatLib.Floats.Formats.Flocq.FloatRep.mulExact_refines (β : Numerics.Radix) :
Numerics.Operation.Finite2 (numericalSystem β) (numericalSystem β) (numericalSystem β) mulExact fun (left right : ℝ) => left * right

Executable mantissa/exponent multiplication exactly refines real multiplication.