satJCost
plain-language theorem explainer
The declaration defines J-cost for a CNF formula under an assignment as the count of unsatisfied clauses. Researchers studying recognition-time complexity cite it to separate satisfiable instances (zero defect) from unsatisfiable ones (positive moat). The definition is obtained directly by filtering the clause list and taking its length.
Claim. Let $f$ be a CNF formula over $n$ variables and let $a$ be an assignment of truth values to those variables. The J-cost of $f$ under $a$ equals the number of clauses in $f$ that fail to be satisfied by $a$.
background
In this module a CNFFormula n is a structure holding a list of clauses together with a variable count fixed equal to n. An Assignment n is a function from the finite index set of size n to Boolean values; satisfaction of a literal or clause is defined by direct evaluation under this function. J-cost therefore records the defect size of any concrete assignment as the cardinality of the unsatisfied sublist.
proof idea
One-line definition that filters the clause list of f to retain only those clauses for which satisfiedBy a returns false, then returns the length of the resulting list.
why it matters
This supplies the basic defect measure used by CircuitSeparation and CircuitLedgerCert to prove that satisfiable formulas reach zero J-cost in at most n recognition steps while unsatisfiable formulas maintain a moat of width at least 1. It thereby supports the module's partial theorem that the Recognition operator R̂ separates recognition-time complexity of SAT from Turing-machine time. The construction is consistent with the broader Recognition Science claim that J-cost landscapes encode topological obstructions for unsatisfiable instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.