Checked integer quantization

Acceptance is equivalent to representability of the rounded integer, rather than representability of the rational input. The same characterization covers arbitrary inclusive intervals and either word signedness.

theorem FloatLib.Numerics.IntegerRange.round?_eq_some_iff (range : IntegerRange) (round : ℚ → ℤ) (value : ℚ) (integer : ℤ) : range.round? round value = some integer ↔ round value = integer ∧ range.Contains integer

Acceptance preserves the chosen rounded integer and certifies its range. The rational input itself need not lie in the destination interval.

theorem FloatLib.Numerics.IntegerRange.round?_eq_none_iff (range : IntegerRange) (round : ℚ → ℤ) (value : ℚ) : range.round? round value = none ↔ ¬range.Contains (round value)

Rejection depends only on the rounded integer lying outside the inclusive range. An empty range therefore rejects every input, independently of the rounding rule.

theorem FloatLib.Numerics.IntegerFormat.zero_inRange (destination : IntegerFormat) : destination.InRange 0

Zero is representable in every signed or unsigned word format, including width zero.

theorem FloatLib.Numerics.IntegerFormat.toNat_inRange {width : ℕ} (word : BitVec width) : (unsigned width).InRange ↑word.toNat

An unsigned word's natural-number interpretation lies in its numerical range.

theorem FloatLib.Numerics.IntegerFormat.toNat_ofNat_of_inRange {width : ℕ} {value : ℤ} (hr : (unsigned width).InRange value) : ↑(BitVec.ofNat width value.toNat).toNat = value

Checked unsigned packing is exact, including width zero.

theorem FloatLib.Numerics.IntegerFormat.signed_succ_inRange_of_unsigned {width : ℕ} {value : ℤ} (hr : (unsigned width).InRange value) : (signed (width + 1)).InRange value

One additional signed bit contains the whole unsigned numerical range.