P3109 conversion proofs

These theorems expose the executable equations, connect conversion output to the proved round-then-saturate projection semantics, and discharge the declared quantizer contract.

@[simp]

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.run_eq_success {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) : run policy input = ConversionOutcome.success (projectRat policy input) (status format policy input)

Every P3109 conversion is the policy-selected projection with its computed status.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.run_finite {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (exact : ℚ) : run policy (Numerics.NumericalValue.finite exact) = ConversionOutcome.success (ofRat policy exact) (status format policy (Numerics.NumericalValue.finite exact))

Finite conversion uses the exact rational projection path directly.

@[simp]

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.run_infinity {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (negative : Bool) : run policy (Numerics.NumericalValue.infinity negative) = ConversionOutcome.success (projectRat policy (Numerics.NumericalValue.infinity negative)) (status format policy (Numerics.NumericalValue.infinity negative))

Infinity conversion is controlled entirely by the named P3109 projection policy.

@[simp]

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.run_exceptional {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (exceptional : Numerics.ExceptionalValue) : run policy (Numerics.NumericalValue.exceptional exceptional) = ConversionOutcome.success (projectRat policy (Numerics.NumericalValue.exceptional exceptional)) (status format policy (Numerics.NumericalValue.exceptional exceptional))

Exceptional conversion is controlled entirely by the named P3109 projection policy.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.sameDatum_decode_run_value {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) : Formats.P3109.Format.SameDatum (projectRat policy input).decode (format.projectRatValue policy input)

Decoding a conversion result yields the proved P3109 round-then-saturate datum.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.implements_run {format : Formats.P3109.Format} : spec.Implements run

The codec bridge supplies the semantic clause as well as the complete word and status.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.spec_iff_eq_run {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) (outcome : ConversionOutcome (P3109 format)) : spec policy input outcome ↔ outcome = run policy input

The semantic contract retains the converter's complete outcome, including its status.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.sameDatum_of_spec {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) (value : P3109 format) (indicators : ConversionStatus) (h : spec policy input (ConversionOutcome.success value indicators)) : Formats.P3109.Format.SameDatum value.decode (format.projectRatValue policy input)

Any successful outcome admitted by the contract denotes the policy-selected datum.

@[simp]

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.exactDecoder_run {format : Formats.P3109.Format} (value : P3109 format) : ExactDecoder.run value = decodeRat value

The installed P3109 exact decoder exposes exact rational denotations.