Shannon's lower bound for De Morgan circuits

This is the De Morgan specialization of Cslib.Circuits.Shannon.exists_hard_function. Together with Lupanov's construction, it gives the asymptotically sharp gate count 2ⁿ/n.

theorem Cslib.Circuits.Boolean.Shannon.exists_hard_function : ∃ (N : ℕ), ∀ n ≥ N, ∃ (f : BooleanFunction n), ∀ (c : Circuit signature n 1), c.Computes interpretation (single f) → 2 ^ n / ↑n < ↑c.size

For all sufficiently large n, some Boolean function on n inputs requires more than 2ⁿ/n De Morgan gates, counting constants and negations.