jfrust_unsat_ge_one
plain-language theorem explainer
The declaration shows that J-frustration of any unsatisfiable CNF formula is at least 1. Complexity researchers in Recognition Science cite it when establishing lower bounds on landscape depth for unsatisfiable instances. The proof unfolds the binary definition of JFrust and applies classical decidability plus a direct contradiction to reach the inequality via simplification.
Claim. Let $f$ be a CNF formula over $n$ variables. If $f$ is unsatisfiable then its J-frustration satisfies $J(f) = 1$, where $J(f)$ equals 0 precisely when $f$ is satisfiable and equals 1 otherwise.
background
J-frustration is introduced as a binary measure of the topological depth of the J-cost landscape barrier around a formula's satisfying assignments. The definition sets JFrust(f) to 0 for satisfiable formulas and to 1 for unsatisfiable ones, using classical decidability on the isSAT predicate. The module sits inside the Complexity domain and lists this classification alongside landscapeDepth results. It depends on the CNFFormula structure, which packages a list of clauses together with a variable count.
proof idea
The tactic proof first unfolds the JFrust definition. It obtains classical decidability for isSAT, derives a contradiction from the assumption of satisfiability under the given unsatisfiability hypothesis, and finishes with a simplification step that yields the required inequality.
why it matters
This result supplies the unsat_ge_one component of the JFrustrationCert record, which aggregates the core classification properties. It completes the basic SAT/UNSAT dichotomy inside the J-frustration module and supports downstream landscape-depth theorems for unsatisfiable formulas. The placement aligns with Recognition Science's use of J-cost to derive complexity bounds without reference to external axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.