From the finite construction to the asymptotic upper bound

The integer root bound holds at every input length, including zero. For positive lengths it gives the usual real-exponent statement, with one constant for all symmetric functions at each fixed depth.

theorem Complexity.Shallow.symmetric_circuit_bound_nat (d : ℕ) (hd : 2 ≤ d) : ∃ (C : ℕ), ∀ (n : ℕ) (f : BitString n → Bool), Symmetric f → ∃ (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1), (c.Computes Basis.unboundedAndOr.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) ∧ c.depth ≤ d ∧ c.size ≤ 2 ^ (C * ((d - 1).nthRoot n + 1)) ∧ InputNegationsOnly c

theorem Complexity.Shallow.symmetric_circuit_bound_real (d : ℕ) (hd : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (f : BitString n → Bool), Symmetric f → ∃ (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1), (c.Computes Basis.unboundedAndOr.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) ∧ c.depth ≤ d ∧ ↑c.size ≤ 2 ^ (C * ↑n ^ (1 / ↑(d - 1))) ∧ InputNegationsOnly c