pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Complexity.SAT.CNF

show as:
view Lean formalization →

This module supplies the core definitions for Boolean satisfiability over a finite set of variables. Researchers encoding complexity reductions or backpropagation arguments inside the Recognition framework cite it as the base layer. It consists entirely of type and function definitions with no proofs or theorems.

claimVariables are indexed by the finite set $V = [n] = 0,1,2,…,n-1$. A literal is an element of $V$ or its negation. A clause is a finite set of literals. A CNF formula is a finite set of clauses. An assignment is a map $V → {0,1}$. The predicates Satisfiable and UniqueSolution are defined by the usual existential and uniqueness quantifiers over satisfying assignments.

background

The module opens the Complexity.SAT namespace by fixing variable indices to Fin n for a chosen problem size n. It introduces the standard Boolean objects: Var (synonym for Fin n), Lit (signed variable), Clause (disjunction), CNF (conjunction of clauses), Assignment (total function to Bool), and the three evaluation maps evalLit, evalClause, evalCNF. These objects are the direct substrate for every later SAT construction in the library.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed eight downstream modules that import the namespace directly: Backprop (partial assignments), BWD3SchurPinch (no-fractional-witnesses Boolean phase states), Completeness (total-assignment lifting), GeoFamily (Morton-octant XOR masks), Isolation, PC (clause-or-XOR constraints), SmallBias, and XOR. The module therefore supplies the concrete syntax in which the Recognition framework encodes its complexity claims and the “no fractional witnesses” condition.

scope and limits

used by (8)

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

declarations in this module (10)