JFrustrationCert
plain-language theorem explainer
JFrustrationCert packages four properties showing that J-frustration is zero exactly on satisfiable CNF formulas and at least one on unsatisfiable ones, while landscape depth remains nonnegative and reaches at least one for unsatisfiable instances. Researchers assembling the Recognition Science dissolution of P versus NP cite it as the phase-2 frustration certificate inside PneqNPConditional and PvsNPMasterCert. The structure is populated by direct application of the four supporting lemmas without further reasoning steps.
Claim. A certificate consists of the four assertions that, for every $n$ and every CNF formula $f$ on $n$ variables, unsatisfiability of $f$ implies $J(f)geq 1$, satisfiability of $f$ implies $J(f)=0$, the average J-cost of $f$ over all assignments is nonnegative, and unsatisfiability of $f$ implies that average is at least 1, where $J$ is the binary J-frustration function and the average is taken with respect to the uniform measure on the $2^n$ assignments.
background
In this module J-frustration of a CNF formula is the binary indicator that returns 0 when the formula is satisfiable and 1 otherwise. Landscape depth is defined as the average value of the satisfiability J-cost function across the full hypercube of Boolean assignments. The module states that J-frustration measures the topological depth of the J-cost landscape barrier around a formula's satisfying region. CNFFormula encodes a k-CNF formula as a list of clauses together with its declared variable count.
proof idea
The declaration is a structure definition that simply collects four independent lemmas into a single record. It is realized by the companion definition jfrustrationCert, which populates the four fields by direct invocation of jfrust_unsat_ge_one, jfrust_sat_eq_zero, landscapeDepth_nonneg, and landscapeDepth_unsat.
why it matters
This certificate supplies the phase-2 frustration component required by both PneqNPConditional and PvsNPMasterCert in the P versus NP assembly. It completes the topological obstruction argument by confirming that unsatisfiable formulas sit behind a J-cost barrier of height at least 1. The construction relies on the J-cost Laplacian and spectral gap certificates from the preceding phase of the Recognition Science complexity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.