Algebraic rounding contracts for configured binary values

The lossless codec preserves the full model result, including NaN payloads and signed zeros. For conventional IEEE descriptors, finite results also satisfy the model's nearest-even real rounding contracts. These statements do not depend on a particular carrier or width.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_rsqrt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (rsqrt value).toModel = (toModel value).rsqrt

Decoding reciprocal square root recovers the complete model result.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_hypot {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (hypot left right).toModel = (toModel left).hypot (toModel right)

Decoding the norm recovers the complete model result.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_powInt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (exponent : ℤ) : (powInt value exponent).toModel = (toModel value).powInt exponent

Decoding integer power recovers the complete model result.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_rootN {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (degree : ℤ) : (rootN value degree).toModel = (toModel value).rootN degree

Decoding integer root recovers the complete model result.

theorem FloatLib.Floats.ExecFloat.Binary.toReal_rsqrt_eq_roundAt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (hfmt : format.isIEEE = true) (hvalue : isFinite value = true) (hzero : isZero value = false) (hsign : signBit value = false) (hfinite : (rsqrt value).isFinite = true) : (rsqrt value).toModel.toReal = Formats.BinaryInterchange.Model.roundAt format (√(toModel value).toReal)⁻¹

A finite reciprocal square root rounds the exact real expression once.

theorem FloatLib.Floats.ExecFloat.Binary.toReal_hypot_eq_roundAt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (hfmt : format.isIEEE = true) (hleft : isFinite left = true) (hright : isFinite right = true) (hfinite : (hypot left right).isFinite = true) : (hypot left right).toModel.toReal = Formats.BinaryInterchange.Model.roundAt format √((toModel left).toReal ^ 2 + (toModel right).toReal ^ 2)

A finite norm rounds the exact sum of squares and square root once.

theorem FloatLib.Floats.ExecFloat.Binary.toReal_powInt_eq_roundAt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (exponent : ℤ) (hfmt : format.isIEEE = true) (hvalue : isFinite value = true) (hzero : isZero value = false) (hfinite : (powInt value exponent).isFinite = true) : (powInt value exponent).toModel.toReal = Formats.BinaryInterchange.Model.roundAt format ((toModel value).toReal ^ exponent)

A finite integer power of a finite nonzero base rounds the exact real power once.

theorem FloatLib.Floats.ExecFloat.Binary.toReal_rootN_eq_roundAt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (degree : ℤ) (hfmt : format.isIEEE = true) (hvalue : isFinite value = true) (hzero : isZero value = false) (hdegree : degree ≠ 0) (hdomain : signBit value = false ∨ degree % 2 ≠ 0) (hfinite : (rootN value degree).isFinite = true) : (rootN value degree).toModel.toReal = Formats.BinaryInterchange.Model.roundAt format (if signBit value = true then -|(toModel value).toReal| ^ (↑degree)⁻¹ else |(toModel value).toReal| ^ (↑degree)⁻¹)

A finite integer root rounds the chosen signed real branch once.