Exact fixed-point conversion proofs

The conversion contract exposes nearest-even coefficient selection, its half-unit error bound, and the parity of a tie. The complete code and status remain uniquely determined.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.Conversion.run_finite {radix : Numerics.Radix} {fractionalDigits : ℕ} (exact : ℚ) : run () (Numerics.NumericalValue.finite exact) = have rounded := roundRat exact; ConversionOutcome.success rounded { inexact := rounded.toRat != exact }

Finite rationals are rounded once to the destination's fixed grid.

theorem FloatLib.Floats.ExecFloat.FixedPoint.Conversion.implements_run {radix : Numerics.Radix} {fractionalDigits : ℕ} : spec.Implements run

Integer rounding supplies the coefficient bound and tie rule in the conversion contract.

theorem FloatLib.Floats.ExecFloat.FixedPoint.Conversion.spec_iff_eq_run {radix : Numerics.Radix} {fractionalDigits : ℕ} (context : Unit) (input : Numerics.NumericalValue ℚ) (outcome : ConversionOutcome (FixedPoint radix fractionalDigits)) : spec context input outcome ↔ outcome = run context input

The coefficient and status clauses determine the original complete conversion outcome.

theorem FloatLib.Floats.ExecFloat.FixedPoint.Conversion.coefficient_nearest_of_spec {radix : Numerics.Radix} {fractionalDigits : ℕ} (exact : ℚ) (rounded : FixedPoint radix fractionalDigits) (indicators : ConversionStatus) (h : spec () (Numerics.NumericalValue.finite exact) (ConversionOutcome.success rounded indicators)) (candidate : ℤ) : |↑rounded.coefficient - exact * ↑(scale radix fractionalDigits)| ≤ |↑candidate - exact * ↑(scale radix fractionalDigits)|

Every admitted finite result is at least as close as every competing grid coefficient.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.Conversion.exactDecoder_run {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : FixedPoint radix fractionalDigits) : ExactDecoder.run value = Numerics.NumericalValue.finite value.toRat

The installed decoder exposes the exact stored rational.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.Conversion.run_infinity {radix : Numerics.Radix} {fractionalDigits : ℕ} (negative : Bool) : run () (Numerics.NumericalValue.infinity negative) = ConversionOutcome.failure (ConversionFailure.infinity InputPosition.source negative)

Infinity is rejected because an exact fixed-point grid has no infinite code.

@[simp]

theorem FloatLib.Floats.ExecFloat.FixedPoint.Conversion.run_exceptional {radix : Numerics.Radix} {fractionalDigits : ℕ} (exceptional : Numerics.ExceptionalValue) : run () (Numerics.NumericalValue.exceptional exceptional) = ConversionOutcome.failure (ConversionFailure.exceptional InputPosition.source exceptional)

Exceptional observations are rejected because exact fixed point has no reserved code.