This market resolves all thresholds according to the year in which a valid, unconditional proof of the following claim first becomes public:

SAT ∉ DTIME(n) on deterministic multitape Turing machines.

That is, there is no deterministic multitape Turing machine M and constant c such that M decides CNF-SAT and halts within cn steps on every input. Here n is the length in bits of the formula under any standard encoding (e.g., DIMACS-style CNF).

The proof must be broadly accepted by experts, with no unresolved substantive errors discovered after posting (I'll wait at least 3 months for a consensus). A proof that P≠NP, or any result implying the statement, also resolves the market.

If the claim is shown to be false or independent of ZFC, or no qualifying proof appears before a threshold’s date, that threshold resolves NO.