Fixed-width binary roundtrips

Nat.fromBits_toBits (in Encoding.lean) inverts one way; here we prove the other direction — Nat.toBits recovers any bit list of the right width from its value — and the resulting injectivity of Nat.fromBits on fixed-width lists. The universal machine compares state fields symbol-wise while the abstract table lookup compares their decoded numbers; these lemmas make the two agree.

theorem Complexity.Nat.toBits_add_pow_mul (w val c : ℕ) : w.toBits (val + c * 2 ^ w) = w.toBits val

Adding multiples of 2^w does not change the low w bits.

theorem Complexity.Nat.toBits_fromBits (l : List Bool) : l.length.toBits (Nat.fromBits l) = l

Nat.toBits is a left inverse of Nat.fromBits at the list's width.

theorem Complexity.Nat.fromBits_inj_of_length_eq {a b : List Bool} (hlen : a.length = b.length) (h : Nat.fromBits a = Nat.fromBits b) : a = b

Nat.fromBits is injective on lists of equal width.