jfrust_sat_eq_zero
plain-language theorem explainer
If a CNF formula is satisfiable then its J-frustration equals zero. Researchers modeling complexity via J-cost landscapes would cite this classification result as the SAT half of the binary frustration measure. The proof is a one-line wrapper that unfolds the definition of JFrust and simplifies under the satisfiability hypothesis.
Claim. If a CNF formula $f$ over $n$ variables is satisfiable, then its J-frustration $J(f)$ equals zero.
background
J-frustration is defined on a CNF formula as the binary indicator that equals zero precisely when the formula is satisfiable and one otherwise. A CNF formula is a list of clauses together with a declared variable count. The module treats J-frustration as a non-natural complexity property that records the topological depth of the J-cost landscape barrier around any satisfying region.
proof idea
The proof unfolds the definition of JFrust, installs classical decidability for the isSAT predicate, and applies simp with the satisfiability hypothesis to obtain the zero value directly.
why it matters
The result supplies the SAT case for the JFrustrationCert certificate that aggregates the four basic properties of the measure. It anchors the claim that satisfiable formulas sit at zero depth in the J-cost landscape, consistent with the Recognition Composition Law and the cost functions derived from multiplicative recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.