SATInstance
plain-language theorem explainer
SATInstance supplies the input structure for a Boolean satisfiability problem, recording only the counts of variables and clauses together with positivity witnesses. Researchers tracing the Recognition Science route to a P versus NP separation cite it as the starting type that feeds JCostLandscape and the subsequent resolution-time and separation structures. The declaration is a plain structure definition that imposes no further computation or encoding.
Claim. A SAT instance consists of natural numbers $n$ (variables) and $m$ (clauses) satisfying $n>0$ and $m>0$.
background
The TuringBridge module constructs a bridge from the Recognition Science result that R-hat separates satisfiable from unsatisfiable instances on a J-cost landscape to the classical Turing-machine statement P ≠ NP. The module document states that the encoding step (step 1) and non-naturality step (step 3) are already established, while the convergence rate depends on the spectral gap and the Turing simulation remains open. SATInstance supplies the minimal data type required before any J-cost contributions or resolution times can be attached.
proof idea
Structure definition that directly introduces the four fields n_vars, n_clauses, n_pos and m_pos with no lemmas or tactics applied.
why it matters
SATInstance is the root type used by JCostLandscape, ResolutionTime, SeparationClaim and TuringBridgeCert. It therefore occupies the first position in the module's four-step strategy for converting the R-hat zero-defect condition into a statement about polynomial versus superpolynomial Turing simulation overhead. The parent structures inherit the positivity constraints and pass them forward to the claim that global J-cost minimization on the full Z³ lattice cannot be simulated by a polynomial-time machine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.