satJCost_zero_iff
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove P ≠ NP for Turing machines.
- Does not apply outside CNF formulas.
- Does not supply explicit recognition-step bounds beyond the zero-cost equivalence.
- Does not address the Betti-number obstruction for unsatisfiable instances.
Lean usage
theorem use_site {n : ℕ} (f : CNFFormula n) (a : Assignment n) (h : f.satisfiedBy a = true) : satJCost f a = 0 := (satJCost_zero_iff f a).mp hformal statement (Lean)
90theorem satJCost_zero_iff {n : ℕ} (f : CNFFormula n) (a : Assignment n) :
91 satJCost f a = 0 ↔ f.satisfiedBy a = true := by
proof body
Tactic-mode proof.
92 unfold satJCost CNFFormula.satisfiedBy
93 constructor
94 · intro h
95 have hlen : (f.clauses.filter (fun c => !c.satisfiedBy a)).length = 0 := by exact_mod_cast h
96 have hfilt : (f.clauses.filter (fun c => !c.satisfiedBy a)) = [] :=
97 List.eq_nil_iff_length_eq_zero.mpr hlen
98 rw [List.all_eq_true]
99 intro c hc
100 by_contra hc2
101 push_neg at hc2
102 have hmem : c ∈ f.clauses.filter (fun c => !c.satisfiedBy a) := by
103 simp only [List.mem_filter]
104 exact ⟨hc, by simp [hc2]⟩
105 rw [hfilt] at hmem
106 simp at hmem
107 · intro h
108 rw [List.all_eq_true] at h
109 have hfilt : (f.clauses.filter (fun c => !c.satisfiedBy a)) = [] := by
110 rw [List.filter_eq_nil_iff]
111 intro c hc
112 have hsat := h c hc
113 simp [hsat]
114 simp [hfilt]
115
116/-! ## Part 1: Satisfiable → Zero Cost (O(n) recognition steps) -/
117
118/-- **THEOREM**: For a satisfiable formula, R̂ finds zero-cost assignment in O(n) steps.
119 The constructive proof: if f.isSAT, then there exists a in 2^n candidates
120 with satJCost f a = 0. R̂ evaluates this assignment directly.
121
122 Recognition time = n (one variable at a time, each step costs at most 1 tick). -/