Exact configured posit integer functions

Every lawful storage codec transports the model's exact integer semantics. Floor, ceiling, and nearest-even results are exactly representable at the input posit width.

@[simp]

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

Configured floor refines model floor for every lawful storage codec.

@[simp]

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

Configured ceiling refines model ceiling for every lawful storage codec.

@[simp]

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

Configured nearest-integer rounding refines the nearest-even model operation.

theorem FloatLib.Floats.ExecFloat.Posit.toRat?_floor_of_finite {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) : toRat? (floor value) = some ↑q.floor

Finite configured floor denotes the exact mathematical floor.

theorem FloatLib.Floats.ExecFloat.Posit.toRat?_ceil_of_finite {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) : toRat? (ceil value) = some ↑q.ceil

Finite configured ceiling denotes the exact mathematical ceiling.

theorem FloatLib.Floats.ExecFloat.Posit.toRat?_nearestInt_of_finite {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) : toRat? (nearestInt value) = some ↑(Numerics.roundRatEven q)

Finite configured nearest-integer rounding denotes the exact nearest-even integer.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toRat?_floor {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)) : toRat? (floor value) = Option.map (fun (q : ℚ) => ↑q.floor) (toRat? value)

Configured floor has exact optional semantics, including NaR propagation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toRat?_ceil {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)) : toRat? (ceil value) = Option.map (fun (q : ℚ) => ↑q.ceil) (toRat? value)

Configured ceiling has exact optional semantics, including NaR propagation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toRat?_nearestInt {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)) : toRat? (nearestInt value) = Option.map (fun (q : ℚ) => ↑(Numerics.roundRatEven q)) (toRat? value)

Configured nearest-even rounding has exact optional semantics, including NaR.

theorem FloatLib.Floats.ExecFloat.Posit.floor_of_int {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)) {n : ℤ} (hvalue : toRat? value = some ↑n) : floor value = value

Configured floor fixes every integer-valued input.

theorem FloatLib.Floats.ExecFloat.Posit.ceil_of_int {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)) {n : ℤ} (hvalue : toRat? value = some ↑n) : ceil value = value

Configured ceiling fixes every integer-valued input.

theorem FloatLib.Floats.ExecFloat.Posit.nearestInt_of_int {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)) {n : ℤ} (hvalue : toRat? value = some ↑n) : nearestInt value = value

Configured nearest-integer rounding fixes every integer-valued input.

theorem FloatLib.Floats.ExecFloat.Posit.nearestInt_spec {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) : ∃ (n : ℤ), toRat? (nearestInt value) = some ↑n ∧ |↑n - q| ≤ 1 / 2 ∧ (∀ (z : ℤ), |↑n - q| ≤ |↑z - q|) ∧ (|↑n - q| = 1 / 2 → n % 2 = 0)

The configured result is a nearest integer, with half-unit error and even ties.