Exact semantics of configured powers and fused minus-one exponentials

The configured operations refine the model kernels for every lawful storage codec. Their real semantics hold under the same domain conditions, independently of storage width. These are correctness results for certified comparison and exact fallback, not bounds on execution cost.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_pow {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (base exponent : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (pow base exponent) = (toModel base).pow (toModel exponent)

Configured power preserves the exact model result.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_exp2 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (exp2 value) = (toModel value).exp2

Configured base-two exponential preserves the exact model result.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_exp10 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (exp10 value) = (toModel value).exp10

Configured base-ten exponential preserves the exact model result.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_exp2Minus1 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (exp2Minus1 value) = (toModel value).exp2Minus1

Configured base-two exponential minus one preserves the fused model result.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_exp10Minus1 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (exp10Minus1 value) = (toModel value).exp10Minus1

Configured base-ten exponential minus one preserves the fused model result.

theorem FloatLib.Floats.ExecFloat.Posit.pow_eq_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (base exponent : ExecFloat (Formats.Posit.Configured.Family format code plan)) {b e : ℚ} (hbase : toRat? base = some b) (hexponent : toRat? exponent = some e) (hb : 0 ≤ b) (hdomain : b ≠ 0 ∨ 0 < e) : toModel (pow base exponent) = Formats.Posit.Model.RealRounding.roundPositive format (↑b ^ ↑e)

Nonnegative configured bases in the real domain round the exact real power once.

theorem FloatLib.Floats.ExecFloat.Posit.pow_eq_roundRat_of_neg {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (base exponent : ExecFloat (Formats.Posit.Configured.Family format code plan)) {b e : ℚ} (hbase : toRat? base = some b) (hexponent : toRat? exponent = some e) (hb : b < 0) (hinteger : e.den = 1) : toModel (pow base exponent) = Formats.Posit.Model.roundRat format (b ^ e.num)

Negative configured bases with integral exponents round their exact rational power once.

theorem FloatLib.Floats.ExecFloat.Posit.pow_eq_nar_of_neg_nonintegral {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (base exponent : ExecFloat (Formats.Posit.Configured.Family format code plan)) {b e : ℚ} (hbase : toRat? base = some b) (hexponent : toRat? exponent = some e) (hb : b < 0) (hinteger : e.den ≠ 1) : toModel (pow base exponent) = Formats.Posit.Model.nar format

A negative configured base with nonintegral exponent produces NaR.

theorem FloatLib.Floats.ExecFloat.Posit.exp2_eq_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {e : ℚ} (hvalue : toRat? value = some e) : toModel (exp2 value) = Formats.Posit.Model.RealRounding.roundPositive format (2 ^ ↑e)

Every finite configured base-two exponential rounds the exact real power.

theorem FloatLib.Floats.ExecFloat.Posit.exp10_eq_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {e : ℚ} (hvalue : toRat? value = some e) : toModel (exp10 value) = Formats.Posit.Model.RealRounding.roundPositive format (10 ^ ↑e)

Every finite configured base-ten exponential rounds the exact real power.

theorem FloatLib.Floats.ExecFloat.Posit.exp2Minus1_eq_round {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {e : ℚ} (hvalue : toRat? value = some e) : toModel (exp2Minus1 value) = Formats.Posit.Model.RealRounding.round format (2 ^ ↑e - 1)

A finite configured base-two exponential minus one rounds the exact fused expression.

theorem FloatLib.Floats.ExecFloat.Posit.exp10Minus1_eq_round {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {e : ℚ} (hvalue : toRat? value = some e) : toModel (exp10Minus1 value) = Formats.Posit.Model.RealRounding.round format (10 ^ ↑e - 1)

A finite configured base-ten exponential minus one rounds the exact fused expression.