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

A polynomial-time decision procedure for satisfiability yields one that finds satisfying assignments; this decision-to-search self-reducibility of SAT is classical. We give a formal verification of it at the level of multitape Turing machines, checked in the Lean proof assistant relative to the machine model, complexity classes and encoding of a public formal library; the mathematics is classical, and what is new is that every machine-level step is checked. Fix the standard bitstring encoding of CNF formulas in which variable indices are written in unary, and let LSAT be the resulting language. Let Wraw be the total function that outputs [0] on inputs outside LSAT and, on inputs z ∈ LSAT, outputs [1] followed by the lexicographically first satisfying assignment of the variables 0,…,|z|. We prove Wraw ∈ FP if and only if LSAT ∈ P. From a decider running in time O(nd) the proof builds one machine for Wraw running in time at most K(n+1)2d+3, where K depends only on the decider's time bound and number of work tapes. Consequently Wraw ∉ FP implies P ≠ NP; this premise has exactly the strength of LSAT ∉ P, and by the NP-completeness of SAT (a step not formally verified here) it is equivalent to P ≠ NP. The paper also states the reduction in the vocabulary of current and predictive observation of Six Birds Theory and its Hiddenness paper. For a family of current observables on SAT computation histories, given as a parameter and not constructed here, we state the predicate that one member of the family computes the canonical witness. The failure of that predicate implies P ≠ NP provided the family admits every search machine built from a correct decider. Closure under post-processing, finite products and composition does not by itself give this admission, and the empty family shows that the admission premise cannot be dropped. Two further parts are conditional schemas: a classification of the expressions of a chosen feature syntax for arguments from carrier features, whose exclusion conclusions rest on supplied premises, and a record of the construction in an audit register. These parts are bookkeeping with short proofs and do not bear on the machine-level theorem. No unconditional separation is claimed.