pith. sign in
module module high

IndisputableMonolith.Complexity.JFrustration

show as:
view Lean formalization →

J-Frustration assigns zero to satisfiable CNF formulas and one to unsatisfiable ones via the J-cost landscape on the Boolean hypercube. Complexity researchers pursuing Recognition Science routes to circuit lower bounds and P versus NP would cite this module. It assembles the J-cost Laplacian and RSAT encoding into a binary classifier that supports topological obstruction arguments for unsatisfiability.

claimFor a CNF formula $φ$ on $n$ variables, the J-frustration $J(φ)$ equals 0 when $φ$ is satisfiable and equals 1 when $φ$ is unsatisfiable, where the value is extracted from the weighted graph on the Boolean hypercube whose edge weights are absolute differences of satJCost.

background

The module operates in the Complexity domain of Recognition Science and defines J-frustration as a binary classifier for CNF formulas. It imports the J-cost Laplacian, which places vertices at assignments in {0,1}^n and weights edges by |satJCost(φ,a) - satJCost(φ,a')| for Hamming-distance-1 pairs. The RSatEncoding upstream result supplies the core claim that satisfiable instances reach zero J-cost in linear recognition steps while unsatisfiable instances carry a non-contractible topological obstruction (positive Betti-1). Constants supplies the RS time quantum τ₀ = 1 tick as the underlying discrete unit.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

J-frustration supplies the central object for the P versus NP assembly: it feeds CircuitLowerBound by linking high frustration to super-polynomial circuit size, NonNaturalness by showing the property evades Razborov-Rudich natural-proof criteria, and PvsNPAssembly by enabling the conditional path that UNSAT formulas have frustration at least 1 while SAT formulas reach zero. The module thereby closes the first phase of the Recognition Science resolution structure for P ≠ NP.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (8)