JFrust
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.