pith. machine review for the scientific record. sign in
def definition def or abbrev high

satJCost

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  81noncomputable def satJCost {n : ℕ} (f : CNFFormula n) (a : Assignment n) : ℝ :=

proof body

Definition body.

  82  (f.clauses.filter (fun c => !c.satisfiedBy a)).length
  83
  84/-- J-cost is nonneg (number of unsatisfied clauses ≥ 0). -/

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.