pith. sign in
module module high

IndisputableMonolith.Complexity.RSatEncoding

show as:
view Lean formalization →

The RSatEncoding module supplies a simplified 3-SAT encoding that maps CNF formulas to J-cost functions on the Boolean hypercube. Complexity researchers tracing the P vs NP path in Recognition Science cite it when reducing satisfiability to J-frustration and circuit-size lower bounds. The module consists of core type definitions together with elementary lemmas on non-negativity and zero-cost assignments.

claimA clause is a list of at most three literal indices (positive for a variable, negative for its negation). A CNF formula is a list of such clauses. For an assignment $a : [n] → {0,1}$, the function satJCost($φ$, $a$) returns the total J-cost of unsatisfied clauses under $a$.

background

The module sits inside the Complexity domain and imports LedgerForcing (which shows J-symmetry forces double-entry structure) and Constants (where the RS time quantum $τ_0 = 1$ tick). It defines the basic objects Clause, CNFFormula and Assignment that later modules use to place SAT instances on the J-cost landscape. The encoding is deliberately restricted to 3-SAT so that the resulting J-cost function can be lifted to the hypercube graph studied in JCostLaplacian.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

RSatEncoding supplies the concrete SAT-to-J-cost translation required by CircuitLedger, CircuitLowerBound, JFrustration and PvsNPAssembly. Those modules in turn feed the three-phase argument that high J-frustration implies super-polynomial circuit size and that J-frustration is non-natural, thereby bypassing the Razborov-Rudich barrier.

scope and limits

used by (8)

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 (14)