Small Nat lemmas for the IEEE32Exec float kernel

The executable IEEE-754 kernel (NN/Floats/IEEEExec/Exec32.lean) defines a handful of low-level Nat helpers such as:

• pow2 k = 2^k (as a Nat), implemented via Nat.shiftLeft.

The IEEEExec bridge and soundness proofs use the same facts about these helpers, so the shared lemmas live here.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.pow2_eq_two_pow (k : ℕ) : pow2 k = 2 ^ k

pow2 k is just 2^k.

Informal: pow2 is defined as Nat.shiftLeft 1 k, i.e. shifting the bit 1 left by k places, which equals the power of two 2^k.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.pow2_pos (k : ℕ) : 0 < pow2 k

pow2 k is strictly positive.

Informal: 2^k > 0 for all k, hence the same holds for pow2 k.