satJCost_nonneg
J-cost counts unsatisfied clauses in a CNF formula under any assignment and is always nonnegative. Researchers analyzing recognition-time complexity for SAT cite this to bound J-cost landscapes from below. The proof is a one-line term wrapper that unfolds the definition and casts the natural-number nonnegativity lemma.
claimFor every natural number $n$, every CNF formula $f$ over $n$ variables, and every assignment $a$ of Boolean values to the variables, $0$ is less than or equal to the number of clauses in $f$ that fail to be satisfied by $a$.
background
The R̂ SAT Encoding module represents SAT instances as CNF formulas whose clauses are lists of literals over $n$ variables. An assignment maps each variable index to a Boolean; a clause is satisfied if at least one literal matches the assignment. J-cost is the real number equal to the count of unsatisfied clauses under that assignment, hence zero exactly on satisfying assignments.
proof idea
The proof is a term-mode one-liner. It unfolds satJCost to the length of the filtered list of unsatisfied clauses and applies Nat.zero_le, using exact_mod_cast to obtain the real-valued inequality.
why it matters in Recognition Science
This result is invoked by landscapeDepth_nonneg to establish nonnegativity of summed J-costs and by unsat_positive_jcost to show that unsatisfiable formulas have strictly positive J-cost everywhere. It supplies the elementary nonnegativity needed for the module's core claim that satisfiable instances reach zero J-cost while unsatisfiable ones encounter a topological obstruction. Within Recognition Science it supports the J-cost measure used to separate recognition steps from Turing time.
scope and limits
- Does not address Turing-machine runtime for SAT.
- Does not prove P versus NP separation.
- Applies only to the J-cost definition given in this module.
- Holds only for finite CNF formulas with finitely many variables.
formal statement (Lean)
85theorem satJCost_nonneg {n : ℕ} (f : CNFFormula n) (a : Assignment n) :
86 0 ≤ satJCost f a := by
proof body
Term-mode proof.
87 unfold satJCost; exact_mod_cast Nat.zero_le _
88
89/-- J-cost = 0 iff the assignment satisfies all clauses. -/