The cutwidth lower bound

This umbrella collects the (4 - ε) n lower bound for circuits over the full binary basis: rectangle-free functions, the cut-counting lemma for constraint networks, the wiring graph of a circuit, the derivation of the graph-ordering bound from the pathwidth hypothesis for cubic graphs, the final assembly, the transfer to nondeterministic circuits by forgetting witness ports, and the average-case bound for balanced functions through the direction of the wiring graph. Start from Algebraic.LowerBound.Cutwidth.FourN; the average case is Algebraic.LowerBound.Cutwidth.AverageCase.