Exact integer-valued posit functions

Integer rounding does not introduce a second numerical rounding error. An integral input is already representable. For a nonintegral input, the tapered fraction budget suffices to encode both neighboring integers, including a ceiling at the next power of two. The argument uses field-layout semantics and applies to every descriptor width.

theorem FloatLib.Floats.Formats.Posit.Model.exists_toRat?_integer_neighbor {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (n : ℤ) (hlower : q.floor ≤ n) (hupper : n ≤ q.ceil) : ∃ (result : Model format), result.toRat? = some ↑n

Every integer between the exact floor and ceiling of a finite posit is representable. This includes both endpoints and has no precision or magnitude precondition.

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_floor_of_finite {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.floor.toRat? = some ↑q.floor

Posit floor returns the exact mathematical floor, without a further rounding error.

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_ceil_of_finite {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.ceil.toRat? = some ↑q.ceil

Posit ceiling returns the exact mathematical ceiling, without a further rounding error.

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_nearestInt_of_finite {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.nearestInt.toRat? = some ↑(Numerics.roundRatEven q)

Nearest-integer posit rounding returns the shared exact nearest-even integer.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_floor {format : Format} (value : Model format) : value.floor.toRat? = Option.map (fun (q : ℚ) => ↑q.floor) value.toRat?

Exact floor semantics also accounts for the NaR input.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_ceil {format : Format} (value : Model format) : value.ceil.toRat? = Option.map (fun (q : ℚ) => ↑q.ceil) value.toRat?

Exact ceiling semantics also accounts for the NaR input.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_nearestInt {format : Format} (value : Model format) : value.nearestInt.toRat? = Option.map (fun (q : ℚ) => ↑(Numerics.roundRatEven q)) value.toRat?

Exact nearest-even semantics also accounts for the NaR input.

theorem FloatLib.Floats.Formats.Posit.Model.floor_of_int {format : Format} (value : Model format) {n : ℤ} (hvalue : value.toRat? = some ↑n) : value.floor = value

Floor fixes every posit that already denotes an integer.

theorem FloatLib.Floats.Formats.Posit.Model.ceil_of_int {format : Format} (value : Model format) {n : ℤ} (hvalue : value.toRat? = some ↑n) : value.ceil = value

Ceiling fixes every posit that already denotes an integer.

theorem FloatLib.Floats.Formats.Posit.Model.nearestInt_of_int {format : Format} (value : Model format) {n : ℤ} (hvalue : value.toRat? = some ↑n) : value.nearestInt = value

Nearest-integer rounding fixes every posit that already denotes an integer.

theorem FloatLib.Floats.Formats.Posit.Model.nearestInt_spec {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : ∃ (n : ℤ), value.nearestInt.toRat? = some ↑n ∧ |↑n - q| ≤ 1 / 2 ∧ (∀ (z : ℤ), |↑n - q| ≤ |↑z - q|) ∧ (|↑n - q| = 1 / 2 → n % 2 = 0)

The returned integer minimizes distance among all integers, lies within half a unit, and is even whenever that bound is attained. These properties describe the delivered posit.