pith. sign in
module module high

IndisputableMonolith.Complexity.RSatEncoding

show as:
view Lean formalization →

The RSatEncoding module supplies the Boolean encoding that maps 3-SAT instances to J-cost functions on the hypercube. Complexity researchers working on the RS P vs NP program cite it to define satJCost and related predicates. It consists entirely of definitions with no proofs.

claimA clause is a finite list of integers (positive index for a variable, negative for its negation). A CNF formula is a list of such clauses. An assignment maps each variable index to a Boolean. satJCost($φ$, $a$) returns the J-cost of assignment $a$ under formula $φ$.

background

This module sits in the Complexity domain and imports LedgerForcing, which shows that J-symmetry forces double-entry ledger structure, and Constants, which fixes the RS time quantum τ₀ = 1 tick. It introduces the simplified 3-SAT encoding used throughout the complexity layer: Clause as a list of at most three literal indices, CNFFormula as a list of clauses, Assignment as a map from variable indices to Booleans, and satJCost as the recognition cost of an assignment relative to the formula.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds the concrete 3-SAT encoding into PvsNPAssembly, CircuitLedger, CircuitLowerBound, JFrustration, JCostLaplacian, NonNaturalness, SpectralGap, and Core.Complexity. It supplies the J-cost landscape on the Boolean hypercube required for the three-phase P vs NP argument that links J-frustration to circuit size.

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)