Real correctness of configured posit logarithms

Every supported carrier decodes to the same model operation. The finite-domain theorems state the exact real logarithm being rounded, including the unrounded addition in Plus1.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_log2 {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 (log2 value) = (toModel value).log2

Configured base-two logarithm refines the exact model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_log10 {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 (log10 value) = (toModel value).log10

Configured base-ten logarithm refines the exact model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_log2Plus1 {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 (log2Plus1 value) = (toModel value).log2Plus1

Configured base-two Plus1 refines the exact model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_log10Plus1 {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 (log10Plus1 value) = (toModel value).log10Plus1

Configured base-ten Plus1 refines the exact model operation.

theorem FloatLib.Floats.ExecFloat.Posit.log2_eq_real {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)) {q : ℚ} (hvalue : toRat? value = some q) (hq : 0 < q) : toModel (log2 value) = Formats.Posit.Model.RealRounding.round format (Real.logb 2 ↑q)

Configured base-two logarithm rounds the exact signed real logarithm.

theorem FloatLib.Floats.ExecFloat.Posit.log10_eq_real {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)) {q : ℚ} (hvalue : toRat? value = some q) (hq : 0 < q) : toModel (log10 value) = Formats.Posit.Model.RealRounding.round format (Real.logb 10 ↑q)

Configured base-ten logarithm rounds the exact signed real logarithm.

theorem FloatLib.Floats.ExecFloat.Posit.log2Plus1_eq_real {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)) {q : ℚ} (hvalue : toRat? value = some q) (hq : -1 < q) : toModel (log2Plus1 value) = Formats.Posit.Model.RealRounding.round format (Real.logb 2 (1 + ↑q))

Configured base-two Plus1 forms 1 + x exactly before rounding the logarithm.

theorem FloatLib.Floats.ExecFloat.Posit.log10Plus1_eq_real {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)) {q : ℚ} (hvalue : toRat? value = some q) (hq : -1 < q) : toModel (log10Plus1 value) = Formats.Posit.Model.RealRounding.round format (Real.logb 10 (1 + ↑q))

Configured base-ten Plus1 forms 1 + x exactly before rounding the logarithm.