Explicit lower bound of 4.5n - o(n) for Boolean circuits

We prove a lower bound of 4.5n - o(n) for the circuit complexity of an explicit Boolean function (that is, a function constructible in deterministic polynomial time), over the basis U₂. That is, we obtain a lower bound of 4.5n - o(n) for the number of {and, or} gates needed to compute a certain Boolean function, over the basis {and, or, not} (where the not gates are not counted). Our proof is based on a new combinatorial property of Boolean functions, called Strongly-Two-Dependence, a notion that may be interesting in its own right. Our lower bound applies to any Strongly-Two-Dependent Boolean function.