Sparse binary words

Sums of distinct powers of two have exactly their specified set bits. Thus an injective placement of Boolean coefficients cannot generate binary carries. The statements concern natural-number arithmetic, independently of a machine word width or execution cost.

Main results

• testBit_sum_two_pow: the set bits of a sum of distinct powers of two.
• testBit_sum_injective: injectively placed Boolean coefficients are recovered exactly.
• and_sum_two_pow: masking by sparse positions is their Boolean-weighted sum.

References

These extend Mathlib's finite-set/binary-digit correspondence.

theorem Cslib.BitString.testBit_sum_two_pow (s : Finset ℕ) (k : ℕ) : (∑ i ∈ s, 2 ^ i).testBit k = true ↔ k ∈ s

A sum of distinct powers of two has exactly the specified set bits.

theorem Cslib.BitString.testBit_sum_injective {α : Type u_1} (s : Finset α) (f : α → ℕ) (hf : Set.InjOn f ↑s) (c : α → Bool) (k : ℕ) : (∑ i ∈ s, (c i).toNat * 2 ^ f i).testBit k = true ↔ ∃ i ∈ s, c i = true ∧ f i = k

Boolean coefficients placed at distinct bit positions do not carry into one another.

theorem Cslib.BitString.and_sum_two_pow {α : Type u_1} [Fintype α] (f : α → ℕ) (hf : Function.Injective f) (x : ℕ) : x &&& ∑ i : α, 2 ^ f i = ∑ i : α, (x.testBit (f i)).toNat * 2 ^ f i

Masking by sparse positions selects their original coefficients.

theorem Cslib.BitString.sum_injective_lt_two_pow {α : Type u_1} (s : Finset α) (f : α → ℕ) (hf : Set.InjOn f ↑s) (c : α → Bool) {L : ℕ} (hL : ∀ i ∈ s, f i < L) : ∑ i ∈ s, (c i).toNat * 2 ^ f i < 2 ^ L

A Boolean-weighted sparse word fits below any width containing all its positions.

theorem Cslib.BitString.sum_strictMono_lt_iff {α : Type u_1} [Fintype α] [LinearOrder α] (f g : α → ℕ) (hf : StrictMono f) (hg : StrictMono g) (c d : α → Bool) : ∑ i : α, (c i).toNat * 2 ^ f i < ∑ i : α, (d i).toNat * 2 ^ f i ↔ ∑ i : α, (c i).toNat * 2 ^ g i < ∑ i : α, (d i).toNat * 2 ^ g i

Increasing placements of the same Boolean coefficients give the same comparisons. Gaps between bits do not affect numeric order.