Explicit bounds for the shallow-circuit recurrence

These elementary natural-number inequalities keep the size proof separate from the circuit construction. All constants are independent of the input length and the integer root scale.

Main results

• Cslib.Circuits.Boolean.ShallowSymmetric.construction_size_bound: the size of the construction.

References

• V. Lecomte, P. Ramakrishnan, Optimal Shallow Circuits for Majority

theorem Cslib.Circuits.Boolean.ShallowSymmetric.mul_le_two_pow_add_mul {k a b x y : ℕ} (hx : x ≤ 2 ^ (a * k)) (hy : y ≤ 2 ^ (b * k)) : x * y ≤ 2 ^ ((a + b) * k)

Products of numbers below 2 ^ (a k) and 2 ^ (b k) are below 2 ^ ((a + b) k).

theorem Cslib.Circuits.Boolean.ShallowSymmetric.add_le_two_pow_add_add_one_mul {k a b x y : ℕ} (hk : 1 ≤ k) (hx : x ≤ 2 ^ (a * k)) (hy : y ≤ 2 ^ (b * k)) : x + y ≤ 2 ^ ((a + b + 1) * k)

Sums of numbers below 2 ^ (a k) and 2 ^ (b k) are below 2 ^ ((a + b + 1) k).

theorem Cslib.Circuits.Boolean.ShallowSymmetric.le_two_pow_mul (c k : ℕ) (hk : 1 ≤ k) : c ≤ 2 ^ (c * k)

A constant c is below 2 ^ (c k) for k ≥ 1.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.construction_size_bound {k n U V B N A D E : ℕ} (hk : 1 ≤ k) (hn : n ≤ 2 ^ (N * k)) (hu : U ≤ A * k) (hv : V ≤ 2 ^ (D * k)) (hb : B ≤ 2 ^ (E * k)) : 1 + (n + 1) * (1 + 3 ^ U * (n + 1) * (2 + V * (B + 2))) ≤ 2 ^ ((2 * A + 2 * N + D + E + 8) * k)

A bound for the entire finite construction, with only its three summary parameters: input count, sum of moduli, and sum of squared moduli.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.sum_sq_moduli_bound {r C k : ℕ} (hk : 1 ≤ k) (m : Fin r → ℕ) (hm : ∀ (i : Fin r), m i ≤ C * k) : ∑ i : Fin r, m i ^ 2 ≤ 2 ^ ((r + 2 * C + 2) * k)

Polynomial factors in the moduli fit into the exponential envelope.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.pair_size_bound {n d k m : ℕ} (hk : 1 ≤ k) (hn : n ≤ k ^ (d + 2)) (hm : k ≤ m) : 2 * (n / m + 1) ≤ (4 * k) ^ (d + 1)

Two blocks fit into the smaller instance used by the depth induction.