15.3 Exact evaluation-span certificates
On this page · Permalink · Source line 206
For an integer \(d\ge0\), form the evaluation vector
and write \(U=f^{-1}(0)\).
Theorem 15.4: Dual certificate for failure of safe detection
For every positive input \(v\),
Proof
A degree-at-most-\(d\) polynomial is a coefficient covector on the evaluation space. It is safe exactly when it annihilates every negative evaluation vector, equivalently their span. Such a covector can equal one on \(v_d(v)\) exactly when \(v_d(v)\) lies outside that span. This is finite-dimensional linear duality over \({\mathbb F_2}\).
Corollary 15.5: Finite support of a dual witness
When the right side of (15.2) holds, there is \(W\subseteq U\) with
The cardinality \(|W|\) is odd.
Proof
Choose a basis of the span from negative evaluation vectors and express \(v_d(v)\) in that basis. Over \({\mathbb F_2}\), the nonzero coefficients select a subset \(W\) of size at most the ambient dimension. The constant-monomial coordinate of every evaluation vector is one; comparing it on both sides shows that \(|W|\) is odd.
Such a relation is replayable by exact linear arithmetic. It does not provide an efficient way to enumerate all negatives of an arbitrary SAT verifier. The theorem assumes that the negative vectors or their proved structure are available.