jfrust_sat_eq_zero
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not establish computational complexity of deciding or computing J-frustration.
- Does not apply to encodings other than CNF formulas.
- Does not connect J-frustration values to specific physical constants or spatial dimensions.
- Does not address average depth or landscape properties beyond the binary classification.
formal statement (Lean)
46theorem jfrust_sat_eq_zero {n : ℕ} (f : CNFFormula n) (h : f.isSAT) :
47 JFrust f = 0 := by
proof body
Term-mode proof.
48 unfold JFrust
49 haveI := Classical.propDecidable f.isSAT
50 simp [h]
51
52/-! ## Landscape Depth -/
53
54/-- The average J-cost across all assignments. -/