SATInstance
SATInstance packages a satisfiability problem as a pair of positive natural numbers giving the count of variables and clauses. Complexity researchers formalizing the Recognition Science encoding of SAT into J-cost landscapes cite this structure when constructing the input for R-hat minimization. The declaration is a direct structure definition carrying only field declarations and positivity constraints.
claimA SAT instance consists of natural numbers $n$ (variables) and $m$ (clauses) with $n > 0$ and $m > 0$.
background
The TuringBridge module develops the link between Recognition Science's global R-hat operator on the Z^3 ledger and classical Turing-machine complexity classes. It encodes a classical SAT problem as a J-cost landscape in which each clause contributes a local term; the total J-cost reaches zero exactly when the instance is satisfiable. SATInstance supplies the two size parameters required for that encoding and enforces positivity to exclude degenerate cases. The module imports J-cost core definitions and ledger factorization results that calibrate the underlying J function used downstream.
proof idea
The declaration is a structure definition with no proof body. It simply declares the four fields n_vars, n_clauses, n_pos and m_pos together with their types and the two positivity hypotheses.
why it matters in Recognition Science
SATInstance is the root datum for the entire P-vs-NP bridge. It is used directly by JCostLandscape to attach landscape size and the zero-cost equivalence, by ResolutionTime to record octave counts, and by SeparationClaim to state the superpolynomial simulation overhead that would imply P ≠ NP. The module documentation identifies this encoding step as already established, leaving only the Turing-machine simulation overhead open. The construction sits inside the global J-cost minimization framework that operates on the full lattice rather than on polynomial-size circuits.
scope and limits
- Does not specify the concrete clauses or literals of the instance.
- Does not define or compute the associated J-cost function.
- Does not address convergence rate or spectral gap of R-hat.
- Does not contain any Turing-machine simulation or complexity bound.
formal statement (Lean)
54structure SATInstance where
55 n_vars : ℕ
56 n_clauses : ℕ
57 n_pos : 0 < n_vars
58 m_pos : 0 < n_clauses
59
60/-- A J-cost landscape encoding of a SAT instance.
61 Each clause becomes a local J-cost contribution.
62 Total J-cost = 0 iff all clauses satisfied. -/