Compatibility API for the concrete SAT guess-and-verify machine

Import this module for the legacy satGuessVerifyNTM machine and its exact satGuessVerifyTime bounds, including guessVerify_decidesInTime and the SAT.linearGuessVerify_* theorems. These remain statements about the original concrete machine, not about the generic finite-verifier compiler.

For new NP membership proofs, use Complexitylib.Classes.NP.Verifier instead. It exposes the language-independent verifier route without importing SAT.