Natural-number bit lemmas

Small format-independent facts about viewing natural numbers as bit strings. Floating-point and posit proofs share these results without depending on one another's representation layers.

theorem Nat.lt_two_pow_of_lt_two_pow_of_le {value smallWidth largeWidth : ℕ} (hvalue : value < 2 ^ smallWidth) (hwidth : smallWidth ≤ largeWidth) : value < 2 ^ largeWidth

A value that fits in a given bit width also fits in every larger bit width.

theorem Nat.testBit_eq_true_iff_two_pow_le_of_lt {value width : ℕ} (hvalue : value < 2 ^ (width + 1)) : value.testBit width = true ↔ 2 ^ width ≤ value

For a value that fits in width + 1 bits, bit width is set exactly when the value reaches 2 ^ width.

theorem Nat.log2_shiftLeft_of_ne_zero (value shift : ℕ) (hvalue : value ≠ 0) : (value <<< shift).log2 = value.log2 + shift

Left shifting a nonzero natural increases its binary logarithm by the shift distance.