Binary-interchange conversion proofs

Every configured and static-byte carrier adapter shares these conversion equations and numerical contract. For default IEEE finite rounding, the nearest-value clause follows from the real rounding bridge and the generic nearest-point theorem. Complete outcome equality retains all word, status, and policy guarantees.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.value_addExact (context : Context) (left right : Numerics.SignedRat) : (addExact context left right).value = left.value + right.value

The context changes only a possible zero sign, never the exact rational sum.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.value_subExact (context : Context) (left right : Numerics.SignedRat) : (subExact context left right).value = left.value - right.value

The context changes only a possible zero sign, never the exact rational difference.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.addExact_default (left right : Numerics.SignedRat) : addExact Context.default left right = left + right

The default context uses the ordinary nearest-even sign rule of SignedRat.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.subExact_default (left right : Numerics.SignedRat) : subExact Context.default left right = left - right

Default-context subtraction retains the ordinary SignedRat semantics.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.negative_addExact_downward_of_eq_zero {left right : Numerics.SignedRat} (hsum : left.value + right.value = 0) : (addExact (Context.withRounding Numerics.RoundingMode.towardNegative) left right).negative = (left.negative || right.negative)

Downward exact cancellation uses the disjunction of the operand signs.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.runWith_finite {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (context : Context) (exact : Numerics.SignedRat) : runWith pack context (Numerics.NumericalValue.finite exact) = quantizeFiniteWith pack context exact

Finite observations use the exact rational binary quantizer.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.runWith_infinity {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (context : Context) (negative : Bool) : runWith pack context (Numerics.NumericalValue.infinity negative) = quantizeInfinityWith pack context negative

Infinity observations are governed only by the explicit infinity policy.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.runWith_exceptional {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (context : Context) (exceptional : Numerics.ExceptionalValue) : runWith pack context (Numerics.NumericalValue.exceptional exceptional) = quantizeExceptionalWith pack context exceptional

Exceptional observations are governed only by the explicit exceptional policy.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.nearestFinite_roundRat (format : Formats.BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (exact : Numerics.SignedRat) : NearestFinite exact.value (Formats.BinaryInterchange.Model.roundRat format exact.negative exact.value.num.natAbs exact.value.den)

The canonical IEEE rational rounder selects a nearest finite value whenever its result is finite.

This includes signed zero. The independent real grid has no infinity, so nonfinite results are covered by the complete outcome clause of specWith.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.implements_runWith {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) : (specWith pack).Implements (runWith pack)

Descriptor rounding semantics establish the nearest clause for every carrier adapter.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.specWith_iff_eq_runWith {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (context : Context) (input : Numerics.NumericalValue Numerics.SignedRat) (outcome : ConversionOutcome Destination) : specWith pack context input outcome ↔ outcome = runWith pack context input

The additional semantic clause preserves exactly the original complete conversion outcomes.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.runWith_infinity_reject {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (negative : Bool) : runWith pack { infinity := InfinityPolicy.reject } (Numerics.NumericalValue.infinity negative) = ConversionOutcome.failure (ConversionFailure.infinity InputPosition.source negative)

Rejecting infinity produces the corresponding explicit failure for every carrier.

theorem FloatLib.Floats.ExecFloat.Binary.Conversion.runWith_exceptional_reject {format : Formats.BinaryInterchange.FloatFormat} {Destination : Type u} (pack : Formats.BinaryInterchange.Model format → Destination) (exceptional : Numerics.ExceptionalValue) : runWith pack { exceptional := ExceptionalPolicy.reject } (Numerics.NumericalValue.exceptional exceptional) = ConversionOutcome.failure (ConversionFailure.exceptional InputPosition.source exceptional)

Rejecting an exceptional observation preserves its complete common classification.