The depth induction for symmetric circuits

The finite construction, prime-power moduli, and elementary size bounds give an integer-scale version of Theorem 1 of Lecomte and Ramakrishnan: at depth d+2, all symmetric functions on at most k^(d+1) inputs have size at most 2^(C_d*k), where C_d is independent of k and of the function.

theorem Complexity.Shallow.exists_symmetric_layers (d : ℕ) : ∃ (C : ℕ), ∀ (n k : ℕ), 1 ≤ k → n ≤ k ^ (d + 1) → ∀ (a : ℕ → Bool) (op : AndOrOp), ∃ (f : Layer n (d + 2)), f.size ≤ 2 ^ (C * k) ∧ ∀ (x : BitString n), Layer.eval op f x = a (weight x)