satJCost_zero_iff
plain-language theorem explainer
The equivalence states that J-cost vanishes precisely when an assignment satisfies every clause of a CNF formula. Researchers on recognition-based complexity models cite it to separate satisfiable instances (zero cost reachable) from unsatisfiable ones (positive cost obstruction). The proof unfolds the cost and satisfaction definitions then equates zero length of the unsatisfied-clause filter with universal satisfaction via list lemmas on nil and all-true predicates.
Claim. Let $f$ be a CNF formula over $n$ variables and let $a$ be an assignment. The J-cost of $f$ under $a$ equals zero if and only if $a$ satisfies every clause of $f$.
background
CNFFormula is the structure holding a list of clauses together with a variable count fixed at $n$. Assignment is the type Fin $n$ to Bool. satJCost counts the clauses that remain unsatisfied under a given assignment, returning a real that is exactly the length of the filtered list of unsatisfied clauses. The module sets the local setting as the R̂ encoding of SAT inside Recognition Science, where the operator supplies a non-natural polytime certifier that reaches zero J-cost for satisfiable instances in O(n) recognition steps while unsatisfiable instances encounter a topological obstruction. Upstream, the definition of satJCost records that J equals zero exactly when all clauses are satisfied and is nonnegative otherwise.
proof idea
The tactic proof first unfolds satJCost and the satisfiedBy predicate on the formula. It then applies constructor to split the biconditional. The forward direction extracts that the filtered list of unsatisfied clauses has length zero, converts to the empty list, and invokes List.all_eq_true to conclude every clause is satisfied. The reverse direction uses List.filter_eq_nil_iff together with the assumption that every clause satisfies the predicate to show the filtered list is empty, after which simp closes the equality to zero.
why it matters
This equivalence supplies the key link used by sat_reaches_zero to construct a zero-cost witness from the isSAT hypothesis and by unsat_positive_jcost to prove every assignment carries positive J-cost. It therefore completes the constructive half of the module claim that satisfiable k-CNF instances reach zero J-cost in O(n) recognition steps under R̂. The result sits inside the Recognition Science framework at the interface between the J-cost functional and the eight-tick octave structure, sharpening the distinction between recognition-time complexity and Turing-machine time without resolving the classical P versus NP question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.