SAT ∈ NP — the headline theorem

This file ties together the two halves of the SAT ∈ NP proof:

• SAT.VerifierTM.verifyPairTM_decidesInTime (in VerifierTM) — the deterministic three-tape verifier decides pairLang Witness within the quadratic budget verifyPairTMTime, so pairLang Witness ∈ P.
• NP.mem_NP_of_linear_witness (in Classes.NP.Verifier.Linear) — the generic verifier route turns pairLang Witness ∈ P and the linear witness bound into language ∈ NP.

Combining them yields the unconditional theorem SAT.language_mem_NP : language ∈ NP.

theorem Complexity.SAT.pairLang_witness_mem_P : pairLang Witness ∈ P

The paired SAT verifier language is decided in polynomial (in fact quadratic) time by verifyPairTM, hence pairLang Witness ∈ P.

theorem Complexity.SAT.language_mem_NP : language ∈ NP

SAT ∈ NP. The Boolean satisfiability language is in NP, witnessed by the generic finite-certificate compiler running over the polynomial-time deterministic pair verifier.