Circuits for existential convolution

Small translate covers yield small circuits for sumset membership. All input negations are computed once, after which translating a Boolean circuit by a fixed bit string only rewires its inputs. The finite disjunction then costs one gate per term and an initial constant.

Applying Ellenberg's sumset cover [Ellenberg2017Sumsets, Theorem 1] gives the exact nonuniform bound n + 3 M (max(C(f), C(g)) + 1) + 1 for existential XOR convolution, where M = ∑_{j ≤ ⌊n/3⌋} binom(n,j). No degree restriction is imposed on the input functions. Gate counts use the De Morgan basis, counting constants and negations as well as binary gates. The exact integer inequality for the cube of the circuit-size excess certifies the exponential base (27/4)^(1/3) = 2^(H₂(1/3)), approximately 1.88988, without rounding an exponent.

Main results

• Cslib.Circuits.Boolean.complexity_exists_translate_le: compile any finite disjunction of translated functions, sharing the input negations across all terms.
• Cslib.Circuits.Boolean.complexity_sumset_le_of_cover: compile any two-sided translate cover into a circuit for sumset membership.
• Cslib.Circuits.Boolean.complexity_orConvolution_le: the binomial-sum circuit bound for arbitrary Boolean functions.
• Cslib.Circuits.Boolean.exists_orConvolution_circuit: an exact circuit attaining that bound.
• Cslib.Circuits.Boolean.complexity_orConvolution_sub_pow_three_mul_four_pow_le: the exact exponential improvement, stated using integer powers.

References

• J. S. Ellenberg, Sumsets as unions of sumsets of subsets, arXiv:1612.01929v2, Theorem 1, pp. 1–2; the circuit compilation is a corollary proved here.

theorem Cslib.Circuits.Boolean.complexity_exists_translate_le {n : ℕ} {α : Type u_1} (s : Finset α) (f : α → BooleanFunction n) (shift : α → BitString n) : complexity interpretation (single fun (x : Fin n → Bool) => decide (∃ i ∈ s, f i (x + shift i) = true)) ≤ n + ∑ i ∈ s, (complexity interpretation (single (f i)) + 1) + 1

A finite disjunction of translated functions pays for the input negations only once. Each term uses a circuit for its function, with free rewiring of the translated inputs.

theorem Cslib.Circuits.Boolean.complexity_sumset_le_of_cover {n : ℕ} (A B A₀ B₀ : Finset (BitString n)) (hcover : A + B = A₀ + B ∪ (A + B₀)) : complexity interpretation (single fun (x : Fin n → Bool) => decide (x ∈ A + B)) ≤ n + A₀.card * (complexity interpretation (single fun (x : Fin n → Bool) => decide (x ∈ B)) + 1) + B₀.card * (complexity interpretation (single fun (x : Fin n → Bool) => decide (x ∈ A)) + 1) + 1

If every sum is covered by a translate whose left endpoint lies in A₀ or whose right endpoint lies in B₀, compile that cover. The sets and their cover may be selected nonuniformly; the conclusion concerns the size of an exact circuit.

theorem Cslib.Circuits.Boolean.complexity_orConvolution_le {n : ℕ} (f g : BooleanFunction n) : complexity interpretation (single (BitString.orConvolution f g)) ≤ n + (3 * ∑ j ∈ Finset.range (n / 3 + 1), n.choose j) * (max (complexity interpretation (single f)) (complexity interpretation (single g)) + 1) + 1

Nontrivial exact convolution circuits. For arbitrary Boolean functions f and g, their existential XOR convolution has a De Morgan circuit within the binomial-sum bound. The circuit and representative sets may depend on the full truth tables; this is a nonuniform size bound, not a uniform algorithm for constructing the circuit.

theorem Cslib.Circuits.Boolean.exists_orConvolution_circuit {n : ℕ} (f g : BooleanFunction n) : ∃ (c : Circuit signature n 1), c.Computes interpretation (single (BitString.orConvolution f g)) ∧ c.size ≤ n + (3 * ∑ j ∈ Finset.range (n / 3 + 1), n.choose j) * (max (complexity interpretation (single f)) (complexity interpretation (single g)) + 1) + 1

There is an actual fan-in-two circuit computing existential convolution within the binomial-sum bound. All gates, including constants and input negations, are counted.

theorem Cslib.Circuits.Boolean.complexity_orConvolution_sub_pow_three_mul_four_pow_le {n : ℕ} (f g : BooleanFunction n) : (complexity interpretation (single (BitString.orConvolution f g)) - (n + 1)) ^ 3 * 4 ^ n ≤ 27 ^ n * (3 * (max (complexity interpretation (single f)) (complexity interpretation (single g)) + 1)) ^ 3

The exponential base is below two. Cubing the circuit-size excess beyond n + 1 gives an exact integer bound with factor (27/4)^n. Thus the original excess is at most 3 (max(C(f), C(g)) + 1) (27/4)^(n/3) over the reals, whose exponential base is approximately 1.88988. The natural-number subtraction also covers circuits smaller than n + 1.