satJCost
plain-language theorem explainer
satJCost defines the J-cost of a CNF formula under an assignment as the count of unsatisfied clauses. Researchers on the R̂ model for recognition-time separation of SAT cite this definition when establishing zero-cost witnesses for satisfiable instances and positive lower bounds for unsatisfiable ones. The definition is realized by a direct filter-and-length computation on the clause list.
Claim. For a CNF formula $f$ over $n$ variables and an assignment $a : Fin n → Bool$, the J-cost equals the cardinality of the set of clauses in $f$ that are not satisfied by $a$.
background
CNFFormula n is a structure holding a list of clauses together with a var_count field fixed to n. Assignment n is the type Fin n → Bool. Clause.satisfiedBy checks whether at least one literal evaluates to true under the assignment via Literal.satisfiedBy. The module encodes SAT instances inside the Recognition Science framework so that the operator R̂ can be applied to the resulting J-cost landscape. Upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the general J-cost construction that this specialization instantiates for CNF formulas.
proof idea
One-line definition that applies List.filter to retain only those clauses for which satisfiedBy returns false, then takes the length of the resulting list.
why it matters
This definition supplies the concrete cost metric used by CircuitLedgerCert, CircuitSeparation, moat_width_unsat, moat_zero_sat, jcostEdgeWeight, and LandscapeDepth. It realizes the core claim in the module doc that satisfiable instances reach zero J-cost while unsatisfiable instances carry a positive defect. The construction sits inside the Recognition Science J-cost formalism (T5 J-uniqueness and the Recognition Composition Law) and feeds the separation between recognition steps and Turing time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.