unsat_cost_lower_bound
plain-language theorem explainer
For any unsatisfiable CNF formula the J-cost of every assignment is bounded below by 1. Researchers working on recognition models of complexity cite the result to separate the zero-cost landscape of satisfiable instances from the obstructed landscape of unsatisfiable ones. The proof applies the strict-positivity lemma for unsatisfiable formulas and lifts the real-valued inequality to the natural numbers via integer casting and the omega tactic.
Claim. Let $f$ be a CNF formula over $n$ variables that is unsatisfiable. Then for every assignment $a$, the J-cost of $f$ under $a$ satisfies $J(f,a) = |$unsatisfied clauses$| ≥ 1$.
background
A CNFFormula is a list of clauses over $n$ variables; an Assignment is a map Fin $n$ → Bool that evaluates literals and clauses in the usual way. The function satJCost returns the real number equal to the count of clauses left unsatisfied by a given assignment, serving as the J-cost in the Recognition Science encoding of SAT. The module shows that satisfiable instances reach zero J-cost in linear recognition steps while unsatisfiable instances carry a topological obstruction that keeps every J-cost positive. This theorem rests on the upstream lemma unsat_positive_jcost, which already establishes that every assignment yields strictly positive J-cost when the formula is unsatisfiable.
proof idea
The tactic proof introduces an arbitrary assignment $a$, invokes unsat_positive_jcost to obtain satJCost $f$ $a$ > 0, extracts the integer length of the filtered unsatisfied clauses, applies mod_cast to relate the real and natural values, and uses omega to conclude the length is at least 1 before casting back to the desired lower bound.
why it matters
The declaration supplies the concrete lower bound consumed by moat_width_unsat and landscapeDepth_unsat; it appears verbatim in the unsat_obstruction field of dissolution_holds and in the local_certifier_fails component of rsatSeparation. It therefore closes the UNSAT half of the recognition-time separation between SAT and its complement inside the R̂ model, without resolving classical P versus NP. The result aligns with the module's claim that recognition complexity differs from Turing time precisely because of this positive J-cost obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.