SeparationClaim
plain-language theorem explainer
SeparationClaim packages the hypothesis that the recognition operator resolves every SAT instance via some resolution time whose simulation by a Turing machine incurs superpolynomial overhead, thereby separating P from NP. Complexity theorists bridging recognition operators on J-cost landscapes to classical Turing classes would cite the structure. It is introduced as a bare definition that collects the resolution property, the overhead proposition, and the implication without further content.
Claim. Let a SAT instance be given by positive numbers of variables and clauses. Let resolution time pair an instance with a number of octaves and a reaches-minimum property. The separation claim asserts that every SAT instance admits a resolution time, that the overhead of simulating the recognition operator by a Turing machine is superpolynomial, and that this overhead implies P ≠ NP.
background
The TuringBridge module connects the recognition science result that the recognition operator separates satisfiable from unsatisfiable instances on a J-cost landscape to the classical P versus NP question. A SAT instance records positive n_vars and n_clauses; each clause contributes a local J-cost term so that total cost vanishes exactly when the instance is satisfied. Resolution time records the number of octaves needed for the operator to reach minimum defect on that landscape.
proof idea
The declaration is a structure definition. It introduces three fields: the statement that every SAT instance is resolved by some resolution time, a proposition standing for superpolynomial overhead, and the logical implication from that proposition to P ≠ NP.
why it matters
This definition supplies the interface for the open Turing simulation step in the P versus NP bridge described in the module document. It would be invoked by a future theorem that establishes the superpolynomial overhead to conclude the separation. The argument rests on the global action of the recognition operator across the full lattice versus the local cell-by-cell action of Turing machines, as stated in the declaration comment. It leaves open the concrete convergence rate on SAT landscapes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.