Strict majority is not in AC0 -- proof internals

A polynomial-size, depth-c family has at most C * n ^ K internal gates at every large length n. The top-down Karchmer–Wigderson bound Circuit.majority_superpolynomial_gates says that every depth-c circuit for strict majority eventually needs more than C * n ^ K + C internal gates, so the two bounds clash at one large length.

theorem Complexity.majority_not_mem_AC0_internal : (fun (x : ℕ) => majority) ∉ AC0