Emergence Calculus

Papers · Preprint · v2

Saturated SAT Observables: A Formally Verified Decision-to-Search Translation and a Conditional P ≠ NP Statement

A machine checked SAT search reduction, and a conditional P ≠ NP statement that names its premise.

Ioannis Tsiokos Zenodo

In plain words

If you can quickly decide whether a logic formula has a solution, you can quickly find one: fix the variables one at a time and ask again each time. This is classical. The paper checks it at the level of Turing machines in the Lean proof assistant, using the machine model and classes of a public library. From a fast decider it builds one machine that outputs the lexicographically first solution, with an explicit time bound.

So computing that canonical witness in polynomial time is possible exactly when SAT is in P. If the witness cannot be computed that fast, SAT is not in P, so P is not NP. That premise is as strong as P ≠ NP itself, and the paper says so. The conditional statement names the premise; it does not make the separation easier.

The paper then restates this in the language of current and predictive observation from the Hiddenness paper. There the conclusion needs one more assumption: the chosen family of observables must admit every search machine built from a correct decider. Closure under composition does not give this, and the empty family shows it cannot be dropped.

What it shows

  • A Lean checked proof that the canonical SAT witness is computable in polynomial time exactly when SAT is in P.
  • An explicit time bound for the search machine built from a decider.
  • A conditional P ≠ NP statement whose premise is equivalent to P ≠ NP.
  • The extra admission hypothesis needed in observation terms, and why it cannot be dropped.

What it does not claim

It proves no lower bound and no unconditional separation. The premise is assumed, not derived, and the Hiddenness paper does not supply it. The feature syntax classification and the audit record are conditional bookkeeping, not a barrier like relativization or natural proofs.

Cite

Tsiokos, I. (2026). Saturated SAT Observables: A Formally Verified Decision-to-Search Translation and a Conditional P ≠ NP Statement. Zenodo. https://doi.org/10.5281/zenodo.23086996