jfrustrationCert
plain-language theorem explainer
The definition packages the four classification and depth properties of J-frustration into a single certificate record. Complexity researchers assembling the master P versus NP certificate cite the record as the frustration component. It is formed by a direct structure construction that delegates each field to one of the four supporting lemmas on SAT classification and landscape depth.
Claim. The J-frustration certificate asserts that the frustration measure $J(f)$ equals zero on any satisfiable CNF formula $f$ and is at least one on any unsatisfiable $f$, while the landscape depth $D(f)$ is nonnegative for every formula and at least one when $f$ is unsatisfiable.
background
In the J-frustration module, frustration measures the topological depth of the J-cost landscape barrier around a formula's satisfying region. Landscape depth is defined as the average J-cost across all assignments. The module states that frustration is binary (zero for SAT, one for UNSAT) and supplies the four supporting lemmas that establish the concrete bounds.
proof idea
The definition is a direct record construction that supplies the four fields of the certificate structure from the four sibling theorems on frustration classification and landscape depth bounds.
why it matters
This definition supplies the frustration component required by the master P versus NP certificate. It completes the packaging of non-natural complexity measures needed for the lower-bound arguments. The module positions J-frustration as a non-natural property that separates satisfiable from unsatisfiable formulas via landscape depth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.