satJCost_zero_iff
plain-language theorem explainer
J-cost of a CNF formula under an assignment equals zero precisely when that assignment satisfies every clause. Researchers on recognition-time complexity for SAT cite the equivalence to separate satisfiable instances under the R̂ operator. The tactic proof unfolds the cost as the length of the unsatisfied-clause filter and applies list lemmas to both directions of the biconditional.
Claim. Let $f$ be a CNF formula over $n$ variables and let $a$ be an assignment. Then the J-cost of $f$ under $a$ equals zero if and only if $a$ satisfies every clause of $f$.
background
In the R̂ SAT Encoding module a CNFFormula is a list of clauses over $n$ variables and an Assignment is a map from Fin $n$ to Bool. The function satJCost returns the length of the sublist of clauses that fail the satisfiedBy predicate, hence zero exactly when no defects remain. The module setting states that R̂ supplies a non-natural polytime certifier for SAT: satisfiable instances reach zero J-cost in O($n$) recognition steps while unsatisfiable instances encounter a topological obstruction.
proof idea
The tactic proof unfolds satJCost and CNFFormula.satisfiedBy, then applies constructor. The forward direction casts the zero cost to a zero-length filter, obtains the empty list via eq_nil_iff_length_eq_zero, and uses all_eq_true plus a contradiction on membership in the filter. The reverse direction rewrites the all_eq_true hypothesis into filter_eq_nil_iff and concludes the length is zero by simp.
why it matters
The equivalence is invoked directly by sat_reaches_zero to extract a zero-cost witness from the isSAT hypothesis and by unsat_positive_jcost to obtain the strict inequality for every assignment when isUNSAT holds. It supplies the constructive half of the module claim that R̂ certifies satisfiability in linear recognition steps. The result sits inside the Recognition Science separation of recognition-time complexity from Turing time and supports the J-cost landscape distinction between satisfiable and unsatisfiable formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.