CVP is PTIME-hard

The reduction, and the hardness it discharges. Three steps:

• the certificate, on the source side: a Horn instance fails to be a yes-instance exactly when it is not Horn or some goal clause has all its negative literals forced (DescriptiveComplexity.CvpVal.not_hornSatisfiable_iff_glVal), which is DescriptiveComplexity.exists_goalClause in one direction and DescriptiveComplexity.forced_subset_model in the other;
• the circuit, on the target side: the drawn circuit accepts exactly when the value of its output gate – the top of the goal chain – holds, which is the two halves of DescriptiveComplexity.Problems.Cvp.Hardness.Value put together;
• the complement, on the class side: what the reduction gives is hardness of CVP for HORNSATᶜ, and polynomial time is closed under complement (DescriptiveComplexity.SigmaSOHornDefinable.compl), so complementing the Horn discharge turns that into hardness for every problem of the class.

Reducing from the complement is what keeps the circuit monotone: a circuit reporting satisfiability would have to negate the propagation, while one reporting failure only has to detect a falsified goal clause.

The certificate on the source side

theorem DescriptiveComplexity.CvpVal.not_hornSatisfiable_iff_glVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {M : A} (hM : ∀ (a : A), a ≤ M) : ¬HornSatisfiable A ↔ GlVal M

A Horn instance fails exactly when the goal chain fires: either it is not Horn, or some goal clause has all its negative literals forced.

What the drawn circuit accepts

The reduction and the completeness theorem

theorem DescriptiveComplexity.cvp_PTIME_hard : PTIME.Hard CVP

CVP is PTIME-hard: every SO-Horn definable problem reduces to it. The route is the Horn discharge applied to the complement of the problem, complemented back – which is available because polynomial time is closed under complement.