JFrust
JFrust assigns the real value 0 to any satisfiable CNF formula and 1 to any unsatisfiable one. Researchers analyzing J-cost landscape barriers within Recognition Science cite this indicator when separating feasible from infeasible instances. The definition performs a case split on the classically decidable isSAT predicate.
claimLet $f$ be a CNF formula on $n$ variables. Define the J-frustration $J(f)$ by $J(f) = 0$ if $f$ is satisfiable and $J(f) = 1$ otherwise.
background
The J-Frustration module treats J-frustration as a measure of the topological depth of the J-cost landscape barrier around a formula's satisfying region. CNFFormula is the upstream structure encoding a k-CNF formula as a list of clauses together with a variable count; an assignment is a Boolean function on those variables. The module states that JFrust serves as the binary classifier separating SAT from UNSAT instances, with LandscapeDepth providing the average J-cost across all assignments.
proof idea
The definition obtains a classical decidability instance for the isSAT predicate. It then branches via if-then-else: the satisfiable case returns 0 and the unsatisfiable case returns 1.
why it matters in Recognition Science
JFrust supplies the indicator used by JFrustrationCert to certify that unsatisfiable formulas satisfy JFrust ≥ 1 and satisfiable formulas satisfy JFrust = 0. It directly supports the module's landscapeDepth_unsat result and the classification theorems jfrust_sat_eq_zero and jfrust_unsat_ge_one. The construction aligns with the Recognition Science treatment of J-cost as a frustration measure on the phi-ladder, though it remains a discrete proxy rather than a continuous depth function.
scope and limits
- Does not compute explicit J-cost values for individual assignments.
- Does not apply to formulas outside the CNF fragment.
- Does not incorporate the continuous J-function or phi-ladder rung structure.
- Does not yield quantitative bounds on landscape depth beyond the binary threshold.
Lean usage
theorem jfrust_sat_eq_zero {n : ℕ} (f : CNFFormula n) (h : f.isSAT) : JFrust f = 0 := by unfold JFrust; simp [h]formal statement (Lean)
34def JFrust {n : ℕ} (f : CNFFormula n) : ℝ :=
proof body
Definition body.
35 haveI := Classical.propDecidable f.isSAT
36 if f.isSAT then 0 else 1
37