Inequality lower bounds from preimages #
If pulling a set problem back along a map gives the inequality problem, every AND/OR circuit constructing the original problem also constructs inequality after applying the preimage homomorphism. The existing inequality lower bound therefore applies without changing the circuit or its AND cost.
theorem
Algebraic.Fusion.Neq.and_lowerBound_of_preimage
{n : ℕ}
{Γ : Type u}
{source : SetProblem Γ}
(f : Ground (2 ^ n) → Γ)
(image : Problem.map source (AndOr.preimageHomomorphism f).map = problem (2 ^ n))
(circuit : Circuit AndOr.signature source.inputCount 1)
(constructs : Problem.Constructs source circuit (AndOr.setInterpretation Γ))
:
If the preimage of a set problem is the 2 ^ n-vertex inequality
problem, every circuit constructing the source problem uses at least n AND
gates, even when OR gates are free.