A cyclic fusion lower bound for inequality graphs

The canonical semi-ultrafilter coding bound for the inequality graph applies unchanged to least-fixed-point cyclic AND/OR circuits. Thus cycles do not reduce the n-AND cost of constructing inequality on 2 ^ n vertices.

theorem Algebraic.Fusion.Neq.cyclic_and_lowerBound {n g : ℕ} (circuit : CyclicCircuit AndOr.signature (2 ^ n + 2 ^ n) g) (constructs : circuit.Constructs (AndOr.setInterpretation (Ground (2 ^ n)))) : n ≤ circuit.cost AndOr.andCost

Every least-fixed-point cyclic row/column construction of inequality on 2 ^ n vertices uses at least n AND equations, even with free OR equations.