Sums of numbers with digits zero and one

Each of finitely many numbers has, in base b, the digit one at the positions of a finite set and zero elsewhere. If, at every position, fewer than b of the numbers have the digit one, then adding any of them produces no carries: the sum has, at each position, the number of chosen summands with the digit one there. This is the arithmetic behind the digit construction reducing 3SAT to subset sum Sipser, Theorem 7.56.

Main results

• Nat.sum_range_mul_pow_inj: base-b digits below b are determined by the number.
• Nat.sum_range_mul_pow_lt: a number with N base-b digits is less than b ^ N.
• Cslib.Complexity.sum_sum_pow_eq_iff: without carries, a subfamily sums to the number with digits T exactly when, at each position, T of its members have the digit one there.

References

• M. Sipser, Introduction to the Theory of Computation

theorem Nat.sum_range_mul_pow_inj {b N : ℕ} {a c : ℕ → ℕ} (ha : ∀ p < N, a p < b) (hc : ∀ p < N, c p < b) : ∑ p ∈ Finset.range N, a p * b ^ p = ∑ p ∈ Finset.range N, c p * b ^ p ↔ ∀ p < N, a p = c p

Base-b digits that are less than b are determined by the number they represent.

theorem Nat.sum_range_mul_pow_lt {b N : ℕ} {a : ℕ → ℕ} (ha : ∀ p < N, a p < b) : ∑ p ∈ Finset.range N, a p * b ^ p < b ^ N

A number with base-b digits below b at the positions below N is less than b ^ N.

theorem Cslib.Complexity.sum_sum_pow_eq_iff {ι : Type u_1} {U F : Finset ι} (hF : F ⊆ U) {col : ι → Finset ℕ} {b N : ℕ} {T : ℕ → ℕ} (hcol : ∀ x ∈ U, col x ⊆ Finset.range N) (hU : ∀ p < N, {x ∈ U | p ∈ col x}.card < b) (hT : ∀ p < N, T p < b) : ∑ x ∈ F, ∑ p ∈ col x, b ^ p = ∑ p ∈ Finset.range N, T p * b ^ p ↔ ∀ p < N, {x ∈ F | p ∈ col x}.card = T p

No carries. Let each x ∈ U have base-b digit one exactly at the positions col x, all below N, with fewer than b members of U having digit one at each position. Then a subfamily F ⊆ U sums to the number with digits T < b exactly when, at each position p < N, exactly T p members of F have digit one at p.