unsat_positive_jcost
plain-language theorem explainer
An unsatisfiable CNF formula has strictly positive J-cost under every assignment, so the J-cost landscape contains no zero point. Researchers studying recognition-time complexity in the R̂ model cite this to separate satisfiable and unsatisfiable cases. The argument is a short contradiction that invokes unsatisfiability, nonnegativity of J-cost, and the zero-cost characterization lemma.
Claim. If a CNF formula $f$ is unsatisfiable, then for every assignment $a$ the number of unsatisfied clauses under $a$ is positive.
background
In the R̂ SAT Encoding module a CNF formula consists of a list of clauses over $n$ variables and an assignment is a map from the $n$ variables to Boolean values. The J-cost of an assignment counts the unsatisfied clauses and equals zero precisely when the assignment satisfies the formula. The module establishes that the Recognition Science operator R̂ acts as a non-natural polytime certifier: satisfiable instances reach zero J-cost in $O(n)$ steps while unsatisfiable instances exhibit a non-contractible topological obstruction (positive Betti-1) that prevents reaching zero. Upstream lemmas establish that J-cost is nonnegative and equals zero if and only if the assignment satisfies every clause.
proof idea
The proof introduces an arbitrary assignment $a$ and obtains from the unsatisfiability hypothesis that $a$ fails to satisfy the formula. It assumes for contradiction that J-cost is at most zero. The nonnegativity lemma then forces J-cost exactly zero. The zero-cost characterization lemma rewrites this equality into the claim that $a$ satisfies the formula, producing an absurdity.
why it matters
This theorem is invoked directly by the unsat_cost_lower_bound result, which strengthens the bound to a minimum of 1. It completes the clause 'Unsatisfiable instances → topological obstruction' in the core claim of the R̂ SAT Encoding module. The result supports the separation of recognition-time complexity from Turing-machine time for SAT while leaving open the informal connection to the natural proof barrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.