Exact encoding of external P3109 results

Report precision rounding and saturation produce representable dyadics. The binary encoder therefore preserves every finite projected value, including a significand carry. The executable result decodes to that exact rational, with no second rounding. Exceptional results use the specified signed infinity or canonical quiet NaN; zero is encoded with positive sign.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.encode_finite (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (value : Numerics.Dyadic) (hgrid : FitsGrid format value) (hbound : |value.toReal| ≤ (BinaryInterchange.Model.posMaxFinite format).toReal) : (encode format (Numerics.NumericalValue.finite value)).isFinite = true ∧ (encode format (Numerics.NumericalValue.finite value)).toReal = value.toReal

A grid value in the external finite range is encoded exactly, including a binade carry.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.project_finite (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (input : Numerics.NumericalValue ℚ) (result : Numerics.Dyadic) (hresult : projectValue format policy input = Numerics.NumericalValue.finite result) : (project format hformat policy input).isFinite = true ∧ (project format hformat policy input).toReal = result.toReal

Every finite projected result is encoded with its exact real value.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.decode_eq_finite_of_isFinite (format : BinaryInterchange.FloatFormat) (word : BinaryInterchange.Model format) (value : Numerics.Dyadic) (hfinite : word.isFinite = true) (hreal : word.toReal = value.toReal) : decode word = Numerics.NumericalValue.finite value.toRat

The exact external decoder agrees with the real interpretation on every finite word.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.decode_project_finite (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (input : Numerics.NumericalValue ℚ) (result : Numerics.Dyadic) (hresult : projectValue format policy input = Numerics.NumericalValue.finite result) : decode (project format hformat policy input) = Numerics.NumericalValue.finite result.toRat

Finite external results refine the exact report projection through the executable decoder.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.project_infinity (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (input : Numerics.NumericalValue ℚ) (negative : Bool) (hresult : projectValue format policy input = Numerics.NumericalValue.infinity negative) : project format hformat policy input = if negative = true then BinaryInterchange.Model.negInf format else BinaryInterchange.Model.posInf format

A projected infinity retains its sign in the external encoding.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.project_nan (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (input : Numerics.NumericalValue ℚ) (exception : Numerics.ExceptionalValue) (hresult : projectValue format policy input = Numerics.NumericalValue.exceptional exception) : project format hformat policy input = BinaryInterchange.Model.canonicalNaN format

A projected NaN becomes the canonical quiet external NaN.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.project_zero (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (input : Numerics.NumericalValue ℚ) (result : Numerics.Dyadic) (hresult : projectValue format policy input = Numerics.NumericalValue.finite result) (hzero : result.significand = 0) : project format hformat policy input = BinaryInterchange.Model.zero format false

Every projected zero uses the external positive-zero encoding.

def FloatLib.Floats.Formats.P3109.Arithmetic.External.Encodes {format : BinaryInterchange.FloatFormat} (word : BinaryInterchange.Model format) : Numerics.NumericalValue Numerics.Dyadic → Prop

Exact finite decoding, with the report's prescribed external exceptional encodings.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.project_refines (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (input : Numerics.NumericalValue ℚ) : Encodes (project format hformat policy input) (projectValue format policy input)

External projection refines its rounded and saturated datum on every input class.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.configuredDestination_toModel (format : BinaryInterchange.FloatFormat) (plan : BinaryInterchange.Configured.StoragePlan format) (code : Type) [ExecFloat.ModelCodec plan (BinaryInterchange.Model format) code] (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (input : Numerics.NumericalValue ℚ) : ExecFloat.Binary.toModel ((configuredDestination format plan code hformat).project policy input) = project format hformat policy input

A configured carrier preserves every bit of the external report projection.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.mixed_binary_refines {Left LeftExact Right RightExact : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Left) (right : Right) : Encodes (Mixed.binary (destination format hformat) policy operation left right) (projectValue format policy (operation (Mixed.decode left) (Mixed.decode right)))

External mixed binary arithmetic has the same total refinement as direct projection.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.mixed_ternary_refines {Left LeftExact Right RightExact Third ThirdExact : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] [ExecFloat.ExactDecoder Third ThirdExact] [ExecFloat.ExactMap ThirdExact ℚ] (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Left) (right : Right) (third : Third) : Encodes (Mixed.ternary (destination format hformat) policy operation left right third) (projectValue format policy (operation (Mixed.decode left) (Mixed.decode right) (Mixed.decode third)))

External fused arithmetic preserves the complete ternary expression through encoding.