Additional lemmas for natural number bit operations

This file contains general-purpose lemmas about Nat.testBit, Nat.bitIndices, and sums of powers of 2 that are used throughout the formalization.

Main results

• Nat.testBit_iff_mem_bitIndices: n.testBit i = true ↔ i ∈ n.bitIndices
• Nat.testBit_finset_sum_pow_two: For a finset s of natural numbers, (∑ i ∈ s, 2^i).testBit j ↔ j ∈ s
• Nat.testBit_sum_pow_two_fin: Same for Finset (Fin k)

These lemmas connect the bit representation of natural numbers with finset membership, which is fundamental for binary encoding arguments.

theorem Nat.testBit_iff_mem_bitIndices (n i : ℕ) : n.testBit i = true ↔ i ∈ n.bitIndices

n.testBit i = true if and only if i appears in n.bitIndices. This connects the pointwise bit test with the list of set bit positions.

theorem Nat.testBit_finset_sum_pow_two {s : Finset ℕ} {i : ℕ} : (∑ x ∈ s, 2 ^ x).testBit i = true ↔ i ∈ s

testBit of a sum of distinct powers of 2 equals membership in the index set. For a finset s of natural numbers, (∑ i ∈ s, 2^i).testBit j = true ↔ j ∈ s.

theorem Nat.testBit_sum_pow_two_fin {k : ℕ} {s : Finset (Fin k)} (j : Fin k) : (∑ i ∈ s, 2 ^ ↑i).testBit ↑j = true ↔ j ∈ s

testBit of a sum of 2^j over Finset (Fin k) equals membership. This is the Fin-indexed version of testBit_finset_sum_pow_two.