SATInstance
plain-language theorem explainer
SATInstance supplies the input type for encoding Boolean satisfiability problems into J-cost landscapes inside the Recognition Science P versus NP bridge. Researchers examining R-hat separation on global lattices would cite this structure when formalizing the faithful encoding step. It is introduced as a plain structure definition carrying only the two size parameters and their positivity invariants.
Claim. A satisfiability instance consists of positive natural numbers $n$ (variables) and $m$ (clauses).
background
The TuringBridge module develops the link between R-hat minimization of J-cost on the Z³ ledger and classical Turing-machine complexity classes. J-cost is the recognition cost obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), calibrated via LedgerFactorization on the positive reals. The module doc states that the encoding of SAT instances as J-cost landscapes is already established, while the superpolynomial simulation overhead remains open.
proof idea
Structure definition with no proof body; the four fields are introduced directly with the two positivity hypotheses n_pos and m_pos.
why it matters
SATInstance is the root type feeding JCostLandscape, ResolutionTime, SeparationClaim and TuringBridgeCert. It implements the first step of the P versus NP strategy in PvsNP_SelfContained_Final.tex: encoding a SAT instance so that total J-cost vanishes exactly when the instance is satisfiable. The construction sits inside the larger forcing chain that forces D = 3 and the eight-tick octave, and it touches the open spectral-gap question that controls convergence rate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.