pith. sign in
module module high

IndisputableMonolith.Complexity.RSatEncoding

show as:
view Lean formalization →

The module supplies the encoding of 3-SAT problems into the J-cost framework of Recognition Science. It defines clauses as short lists of literal indices and formulas as collections of clauses, together with the J-cost of an assignment. Complexity theorists studying the P versus NP gap in this framework cite the encoding to link Boolean satisfiability to recognition costs. The module contains only definitions.

claimDefines a clause as a list of at most three literals with indices in $Z$, a formula $phi$ as a list of clauses, an assignment $a$ as a map from variable indices to $B$, and the function $satJCost(phi,a)$ as the J-cost incurred by $a$ on $phi$.

background

The module operates in the Complexity subdomain and rests on the RS time quantum $tau_0 = 1$ tick together with the double-entry ledger structure forced by J-symmetry. It introduces the objects needed to represent SAT instances: a Clause as a list of at most three signed variable indices, a CNFFormula as a list of clauses, an Assignment as a function from Fin n to Bool, and the sat J-cost that sums the penalties from unsatisfied clauses. This encoding prepares the ground for measuring J-frustration on the Boolean hypercube.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions feed directly into the circuit ledger construction that models Boolean circuits as sub-ledgers, the J-frustration analysis that separates SAT from UNSAT, the non-naturalness argument, and the assembly of P versus NP resolution paths. It supplies the concrete link between SAT and the J-cost landscape used in the Recognition Science treatment of complexity. The P vs NP gap in RS reduces to one question: Can a Turing-equivalent model simulate the global J-cost gradient that R̂ uses to resolve SAT in O(n) recognition steps?

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)